Average Error: 7.5 → 5.2
Time: 14.6s
Precision: 64
\[\frac{x \cdot y - z \cdot t}{a}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot t \le -3.0783448370061419 \cdot 10^{47} \lor \neg \left(x \cdot y - z \cdot t \le 7.49674299200361345 \cdot 10^{288}\right):\\ \;\;\;\;y \cdot \frac{x}{a} - \frac{t \cdot z}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{a}}{\frac{1}{x \cdot y - z \cdot t}}\\ \end{array}\]
\frac{x \cdot y - z \cdot t}{a}
↓
\begin{array}{l}
\mathbf{if}\;x \cdot y - z \cdot t \le -3.0783448370061419 \cdot 10^{47} \lor \neg \left(x \cdot y - z \cdot t \le 7.49674299200361345 \cdot 10^{288}\right):\\
\;\;\;\;y \cdot \frac{x}{a} - \frac{t \cdot z}{a}\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{1}{a}}{\frac{1}{x \cdot y - z \cdot t}}\\

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r898222 = x;
        double r898223 = y;
        double r898224 = r898222 * r898223;
        double r898225 = z;
        double r898226 = t;
        double r898227 = r898225 * r898226;
        double r898228 = r898224 - r898227;
        double r898229 = a;
        double r898230 = r898228 / r898229;
        return r898230;
}
↓
double f(double x, double y, double z, double t, double a) {
        double r898231 = x;
        double r898232 = y;
        double r898233 = r898231 * r898232;
        double r898234 = z;
        double r898235 = t;
        double r898236 = r898234 * r898235;
        double r898237 = r898233 - r898236;
        double r898238 = -3.078344837006142e+47;
        bool r898239 = r898237 <= r898238;
        double r898240 = 7.496742992003613e+288;
        bool r898241 = r898237 <= r898240;
        double r898242 = !r898241;
        bool r898243 = r898239 || r898242;
        double r898244 = a;
        double r898245 = r898231 / r898244;
        double r898246 = r898232 * r898245;
        double r898247 = r898235 * r898234;
        double r898248 = r898247 / r898244;
        double r898249 = r898246 - r898248;
        double r898250 = 1.0;
        double r898251 = r898250 / r898244;
        double r898252 = r898250 / r898237;
        double r898253 = r898251 / r898252;
        double r898254 = r898243 ? r898249 : r898253;
        return r898254;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original7.5
Target6.1
Herbie5.2
\[\begin{array}{l} \mathbf{if}\;z \lt -2.46868496869954822 \cdot 10^{170}:\\ \;\;\;\;\frac{y}{a} \cdot x - \frac{t}{a} \cdot z\\ \mathbf{elif}\;z \lt 6.30983112197837121 \cdot 10^{-71}:\\ \;\;\;\;\frac{x \cdot y - z \cdot t}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{a} \cdot x - \frac{t}{a} \cdot z\\ \end{array}\]

Derivation

  1. Split input into 2 regimes

  2. if (- (* x y) (* z t)) < -3.078344837006142e+47 or 7.496742992003613e+288 < (- (* x y) (* z t))

    1. Initial program 20.8

      \[\frac{x \cdot y - z \cdot t}{a}\]
    2. Using strategy rm

    3. Applied div-sub20.8

      \[\leadsto \color{blue}{\frac{x \cdot y}{a} - \frac{z \cdot t}{a}}\]

    4. Simplified13.3

      \[\leadsto \color{blue}{y \cdot \frac{x}{a}} - \frac{z \cdot t}{a}\]

    5. Simplified13.3

      \[\leadsto y \cdot \frac{x}{a} - \color{blue}{\frac{t \cdot z}{a}}\]

    if -3.078344837006142e+47 < (- (* x y) (* z t)) < 7.496742992003613e+288

    1. Initial program 0.9

      \[\frac{x \cdot y - z \cdot t}{a}\]
    2. Using strategy rm

    3. Applied clear-num1.2

      \[\leadsto \color{blue}{\frac{1}{\frac{a}{x \cdot y - z \cdot t}}}\]
    4. Using strategy rm

    5. Applied div-inv1.4

      \[\leadsto \frac{1}{\color{blue}{a \cdot \frac{1}{x \cdot y - z \cdot t}}}\]

    6. Applied associate-/r*1.1

      \[\leadsto \color{blue}{\frac{\frac{1}{a}}{\frac{1}{x \cdot y - z \cdot t}}}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification5.2

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot t \le -3.0783448370061419 \cdot 10^{47} \lor \neg \left(x \cdot y - z \cdot t \le 7.49674299200361345 \cdot 10^{288}\right):\\ \;\;\;\;y \cdot \frac{x}{a} - \frac{t \cdot z}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{a}}{\frac{1}{x \cdot y - z \cdot t}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020046 +o rules:numerics
(FPCore (x y z t a)
  :name "Data.Colour.Matrix:inverse from colour-2.3.3, B"
  :precision binary64

  :herbie-target
  (if (< z -2.468684968699548e+170) (- (* (/ y a) x) (* (/ t a) z)) (if (< z 6.309831121978371e-71) (/ (- (* x y) (* z t)) a) (- (* (/ y a) x) (* (/ t a) z))))

  (/ (- (* x y) (* z t)) a))