Average Error: 23.9 → 10.9
Time: 24.3s
Precision: 64
\[x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t}\]
↓
\[\begin{array}{l} \mathbf{if}\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(\frac{y - x}{a - t}, z - t, x\right)\\ \mathbf{elif}\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} \le 4.039572590771429307206375395827518258788 \cdot 10^{256}:\\ \;\;\;\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\left(y - x\right) \cdot \frac{1}{a - t}, z - t, x\right)\\ \end{array}\]
x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t}
↓
\begin{array}{l}
\mathbf{if}\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} = -\infty:\\
\;\;\;\;\mathsf{fma}\left(\frac{y - x}{a - t}, z - t, x\right)\\

\mathbf{elif}\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} \le 4.039572590771429307206375395827518258788 \cdot 10^{256}:\\
\;\;\;\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t}\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\left(y - x\right) \cdot \frac{1}{a - t}, z - t, x\right)\\

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r406588 = x;
        double r406589 = y;
        double r406590 = r406589 - r406588;
        double r406591 = z;
        double r406592 = t;
        double r406593 = r406591 - r406592;
        double r406594 = r406590 * r406593;
        double r406595 = a;
        double r406596 = r406595 - r406592;
        double r406597 = r406594 / r406596;
        double r406598 = r406588 + r406597;
        return r406598;
}
↓
double f(double x, double y, double z, double t, double a) {
        double r406599 = x;
        double r406600 = y;
        double r406601 = r406600 - r406599;
        double r406602 = z;
        double r406603 = t;
        double r406604 = r406602 - r406603;
        double r406605 = r406601 * r406604;
        double r406606 = a;
        double r406607 = r406606 - r406603;
        double r406608 = r406605 / r406607;
        double r406609 = r406599 + r406608;
        double r406610 = -inf.0;
        bool r406611 = r406609 <= r406610;
        double r406612 = r406601 / r406607;
        double r406613 = fma(r406612, r406604, r406599);
        double r406614 = 4.039572590771429e+256;
        bool r406615 = r406609 <= r406614;
        double r406616 = 1.0;
        double r406617 = r406616 / r406607;
        double r406618 = r406601 * r406617;
        double r406619 = fma(r406618, r406604, r406599);
        double r406620 = r406615 ? r406609 : r406619;
        double r406621 = r406611 ? r406613 : r406620;
        return r406621;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original23.9
Target8.9
Herbie10.9
\[\begin{array}{l} \mathbf{if}\;a \lt -1.615306284544257464183904494091872805513 \cdot 10^{-142}:\\ \;\;\;\;x + \frac{y - x}{1} \cdot \frac{z - t}{a - t}\\ \mathbf{elif}\;a \lt 3.774403170083174201868024161554637965035 \cdot 10^{-182}:\\ \;\;\;\;y - \frac{z}{t} \cdot \left(y - x\right)\\ \mathbf{else}:\\ \;\;\;\;x + \frac{y - x}{1} \cdot \frac{z - t}{a - t}\\ \end{array}\]

Derivation

  1. Split input into 3 regimes

  2. if (+ x (/ (* (- y x) (- z t)) (- a t))) < -inf.0

    1. Initial program 64.0

      \[x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t}\]

    2. Simplified16.0

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y - x}{a - t}, z - t, x\right)}\]
    3. Using strategy rm

    4. Applied div-inv16.1

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left(y - x\right) \cdot \frac{1}{a - t}}, z - t, x\right)\]
    5. Using strategy rm

    6. Applied un-div-inv16.0

      \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y - x}{a - t}}, z - t, x\right)\]

    if -inf.0 < (+ x (/ (* (- y x) (- z t)) (- a t))) < 4.039572590771429e+256

    1. Initial program 8.3

      \[x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t}\]

    if 4.039572590771429e+256 < (+ x (/ (* (- y x) (- z t)) (- a t)))

    1. Initial program 54.3

      \[x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t}\]

    2. Simplified16.9

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y - x}{a - t}, z - t, x\right)}\]
    3. Using strategy rm

    4. Applied div-inv16.9

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left(y - x\right) \cdot \frac{1}{a - t}}, z - t, x\right)\]
  3. Recombined 3 regimes into one program.

  4. Final simplification10.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(\frac{y - x}{a - t}, z - t, x\right)\\ \mathbf{elif}\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} \le 4.039572590771429307206375395827518258788 \cdot 10^{256}:\\ \;\;\;\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\left(y - x\right) \cdot \frac{1}{a - t}, z - t, x\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019305 +o rules:numerics
(FPCore (x y z t a)
  :name "Graphics.Rendering.Chart.Axis.Types:linMap from Chart-1.5.3"
  :precision binary64

  :herbie-target
  (if (< a -1.6153062845442575e-142) (+ x (* (/ (- y x) 1) (/ (- z t) (- a t)))) (if (< a 3.7744031700831742e-182) (- y (* (/ z t) (- y x))) (+ x (* (/ (- y x) 1) (/ (- z t) (- a t))))))

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