Average Error: 24.8 → 8.9
Time: 4.9s
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} \le -1.41749725609029325 \cdot 10^{-260} \lor \neg \left(x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} \le 0.0\right):\\ \;\;\;\;\mathsf{fma}\left(y - x, \frac{z - t}{a - t}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{t}, z, y - \frac{z \cdot y}{t}\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} \le -1.41749725609029325 \cdot 10^{-260} \lor \neg \left(x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} \le 0.0\right):\\
\;\;\;\;\mathsf{fma}\left(y - x, \frac{z - t}{a - t}, x\right)\\

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

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r722484 = x;
        double r722485 = y;
        double r722486 = r722485 - r722484;
        double r722487 = z;
        double r722488 = t;
        double r722489 = r722487 - r722488;
        double r722490 = r722486 * r722489;
        double r722491 = a;
        double r722492 = r722491 - r722488;
        double r722493 = r722490 / r722492;
        double r722494 = r722484 + r722493;
        return r722494;
}

double f(double x, double y, double z, double t, double a) {
        double r722495 = x;
        double r722496 = y;
        double r722497 = r722496 - r722495;
        double r722498 = z;
        double r722499 = t;
        double r722500 = r722498 - r722499;
        double r722501 = r722497 * r722500;
        double r722502 = a;
        double r722503 = r722502 - r722499;
        double r722504 = r722501 / r722503;
        double r722505 = r722495 + r722504;
        double r722506 = -1.4174972560902932e-260;
        bool r722507 = r722505 <= r722506;
        double r722508 = 0.0;
        bool r722509 = r722505 <= r722508;
        double r722510 = !r722509;
        bool r722511 = r722507 || r722510;
        double r722512 = r722500 / r722503;
        double r722513 = fma(r722497, r722512, r722495);
        double r722514 = r722495 / r722499;
        double r722515 = r722498 * r722496;
        double r722516 = r722515 / r722499;
        double r722517 = r722496 - r722516;
        double r722518 = fma(r722514, r722498, r722517);
        double r722519 = r722511 ? r722513 : r722518;
        return r722519;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original24.8
Target9.2
Herbie8.9
\[\begin{array}{l} \mathbf{if}\;a \lt -1.6153062845442575 \cdot 10^{-142}:\\ \;\;\;\;x + \frac{y - x}{1} \cdot \frac{z - t}{a - t}\\ \mathbf{elif}\;a \lt 3.7744031700831742 \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 2 regimes
  2. if (+ x (/ (* (- y x) (- z t)) (- a t))) < -1.4174972560902932e-260 or 0.0 < (+ x (/ (* (- y x) (- z t)) (- a t)))

    1. Initial program 21.8

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

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

      \[\leadsto \color{blue}{\frac{y - x}{a - t} \cdot \left(z - t\right) + x}\]
    5. Using strategy rm
    6. Applied div-inv11.0

      \[\leadsto \color{blue}{\left(\left(y - x\right) \cdot \frac{1}{a - t}\right)} \cdot \left(z - t\right) + x\]
    7. Applied associate-*l*7.6

      \[\leadsto \color{blue}{\left(y - x\right) \cdot \left(\frac{1}{a - t} \cdot \left(z - t\right)\right)} + x\]
    8. Simplified7.5

      \[\leadsto \left(y - x\right) \cdot \color{blue}{\frac{z - t}{a - t}} + x\]
    9. Using strategy rm
    10. Applied fma-def7.5

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

    if -1.4174972560902932e-260 < (+ x (/ (* (- y x) (- z t)) (- a t))) < 0.0

    1. Initial program 57.3

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

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

      \[\leadsto \color{blue}{\frac{y - x}{a - t} \cdot \left(z - t\right) + x}\]
    5. Using strategy rm
    6. Applied div-inv58.2

      \[\leadsto \color{blue}{\left(\left(y - x\right) \cdot \frac{1}{a - t}\right)} \cdot \left(z - t\right) + x\]
    7. Applied associate-*l*57.3

      \[\leadsto \color{blue}{\left(y - x\right) \cdot \left(\frac{1}{a - t} \cdot \left(z - t\right)\right)} + x\]
    8. Simplified57.4

      \[\leadsto \left(y - x\right) \cdot \color{blue}{\frac{z - t}{a - t}} + x\]
    9. Taylor expanded around inf 21.8

      \[\leadsto \color{blue}{\left(y + \frac{x \cdot z}{t}\right) - \frac{z \cdot y}{t}}\]
    10. Simplified24.6

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} \le -1.41749725609029325 \cdot 10^{-260} \lor \neg \left(x + \frac{\left(y - x\right) \cdot \left(z - t\right)}{a - t} \le 0.0\right):\\ \;\;\;\;\mathsf{fma}\left(y - x, \frac{z - t}{a - t}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{t}, z, y - \frac{z \cdot y}{t}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020083 +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.774403170083174e-182) (- y (* (/ z t) (- y x))) (+ x (* (/ (- y x) 1) (/ (- z t) (- a t))))))

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