Average Error: 7.9 → 0.8
Time: 2.9s
Precision: 64
\[\frac{x \cdot y - z \cdot t}{a}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot t \le -1.69576332269079147 \cdot 10^{247} \lor \neg \left(x \cdot y - z \cdot t \le 6.3521234323903313 \cdot 10^{199}\right):\\ \;\;\;\;x \cdot \frac{y}{a} - t \cdot \frac{z}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y}{a} - \frac{t \cdot z}{a}\\ \end{array}\]
\frac{x \cdot y - z \cdot t}{a}
↓
\begin{array}{l}
\mathbf{if}\;x \cdot y - z \cdot t \le -1.69576332269079147 \cdot 10^{247} \lor \neg \left(x \cdot y - z \cdot t \le 6.3521234323903313 \cdot 10^{199}\right):\\
\;\;\;\;x \cdot \frac{y}{a} - t \cdot \frac{z}{a}\\

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

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r907374 = x;
        double r907375 = y;
        double r907376 = r907374 * r907375;
        double r907377 = z;
        double r907378 = t;
        double r907379 = r907377 * r907378;
        double r907380 = r907376 - r907379;
        double r907381 = a;
        double r907382 = r907380 / r907381;
        return r907382;
}
↓
double f(double x, double y, double z, double t, double a) {
        double r907383 = x;
        double r907384 = y;
        double r907385 = r907383 * r907384;
        double r907386 = z;
        double r907387 = t;
        double r907388 = r907386 * r907387;
        double r907389 = r907385 - r907388;
        double r907390 = -1.6957633226907915e+247;
        bool r907391 = r907389 <= r907390;
        double r907392 = 6.352123432390331e+199;
        bool r907393 = r907389 <= r907392;
        double r907394 = !r907393;
        bool r907395 = r907391 || r907394;
        double r907396 = a;
        double r907397 = r907384 / r907396;
        double r907398 = r907383 * r907397;
        double r907399 = r907386 / r907396;
        double r907400 = r907387 * r907399;
        double r907401 = r907398 - r907400;
        double r907402 = r907385 / r907396;
        double r907403 = r907387 * r907386;
        double r907404 = r907403 / r907396;
        double r907405 = r907402 - r907404;
        double r907406 = r907395 ? r907401 : r907405;
        return r907406;
}

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.9
Target5.9
Herbie0.8
\[\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)) < -1.6957633226907915e+247 or 6.352123432390331e+199 < (- (* x y) (* z t))

    1. Initial program 33.6

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

    3. Applied div-sub33.6

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

    4. Simplified33.6

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

    6. Applied *-un-lft-identity33.6

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

    7. Applied times-frac18.0

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

    8. Simplified18.0

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

    10. Applied *-un-lft-identity18.0

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

    11. Applied times-frac0.8

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

    12. Simplified0.8

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

    if -1.6957633226907915e+247 < (- (* x y) (* z t)) < 6.352123432390331e+199

    1. Initial program 0.8

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

    3. Applied div-sub0.8

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

    4. Simplified0.8

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

    6. Applied associate-/l*5.4

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

    7. Taylor expanded around 0 0.8

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

  4. Final simplification0.8

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot t \le -1.69576332269079147 \cdot 10^{247} \lor \neg \left(x \cdot y - z \cdot t \le 6.3521234323903313 \cdot 10^{199}\right):\\ \;\;\;\;x \cdot \frac{y}{a} - t \cdot \frac{z}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y}{a} - \frac{t \cdot z}{a}\\ \end{array}\]

Reproduce

herbie shell --seed 2020020 
(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))