Average Error: 6.3 → 0.7
Time: 26.1s
Precision: 64
\[x + \frac{\left(y - x\right) \cdot z}{t}\]
\[\begin{array}{l} \mathbf{if}\;x + \frac{\left(y - x\right) \cdot z}{t} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(z, \frac{y - x}{t}, x\right)\\ \mathbf{elif}\;x + \frac{\left(y - x\right) \cdot z}{t} \le 9.290457324428158966196112221687067192256 \cdot 10^{286}:\\ \;\;\;\;x + \frac{\left(y - x\right) \cdot z}{t}\\ \mathbf{else}:\\ \;\;\;\;\left(y - x\right) \cdot \frac{z}{t} + x\\ \end{array}\]
x + \frac{\left(y - x\right) \cdot z}{t}
\begin{array}{l}
\mathbf{if}\;x + \frac{\left(y - x\right) \cdot z}{t} = -\infty:\\
\;\;\;\;\mathsf{fma}\left(z, \frac{y - x}{t}, x\right)\\

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

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

\end{array}
double f(double x, double y, double z, double t) {
        double r324011 = x;
        double r324012 = y;
        double r324013 = r324012 - r324011;
        double r324014 = z;
        double r324015 = r324013 * r324014;
        double r324016 = t;
        double r324017 = r324015 / r324016;
        double r324018 = r324011 + r324017;
        return r324018;
}

double f(double x, double y, double z, double t) {
        double r324019 = x;
        double r324020 = y;
        double r324021 = r324020 - r324019;
        double r324022 = z;
        double r324023 = r324021 * r324022;
        double r324024 = t;
        double r324025 = r324023 / r324024;
        double r324026 = r324019 + r324025;
        double r324027 = -inf.0;
        bool r324028 = r324026 <= r324027;
        double r324029 = r324021 / r324024;
        double r324030 = fma(r324022, r324029, r324019);
        double r324031 = 9.290457324428159e+286;
        bool r324032 = r324026 <= r324031;
        double r324033 = r324022 / r324024;
        double r324034 = r324021 * r324033;
        double r324035 = r324034 + r324019;
        double r324036 = r324032 ? r324026 : r324035;
        double r324037 = r324028 ? r324030 : r324036;
        return r324037;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original6.3
Target2.0
Herbie0.7
\[\begin{array}{l} \mathbf{if}\;x \lt -9.025511195533004570453352523209034680317 \cdot 10^{-135}:\\ \;\;\;\;x - \frac{z}{t} \cdot \left(x - y\right)\\ \mathbf{elif}\;x \lt 4.275032163700714748507147332551979944314 \cdot 10^{-250}:\\ \;\;\;\;x + \frac{y - x}{t} \cdot z\\ \mathbf{else}:\\ \;\;\;\;x + \frac{y - x}{\frac{t}{z}}\\ \end{array}\]

Derivation

  1. Split input into 3 regimes
  2. if (+ x (/ (* (- y x) z) t)) < -inf.0

    1. Initial program 64.0

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

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

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left(y - x\right) \cdot \frac{1}{t}}, z, x\right)\]
    5. Taylor expanded around 0 64.0

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

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

    if -inf.0 < (+ x (/ (* (- y x) z) t)) < 9.290457324428159e+286

    1. Initial program 0.7

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

    if 9.290457324428159e+286 < (+ x (/ (* (- y x) z) t))

    1. Initial program 44.5

      \[x + \frac{\left(y - x\right) \cdot z}{t}\]
    2. Simplified7.6

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

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

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

      \[\leadsto \color{blue}{\left(y - x\right) \cdot \frac{z}{t}} + x\]
  3. Recombined 3 regimes into one program.
  4. Final simplification0.7

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

Reproduce

herbie shell --seed 2019306 +o rules:numerics
(FPCore (x y z t)
  :name "Numeric.Histogram:binBounds from Chart-1.5.3"
  :precision binary64

  :herbie-target
  (if (< x -9.0255111955330046e-135) (- x (* (/ z t) (- x y))) (if (< x 4.2750321637007147e-250) (+ x (* (/ (- y x) t) z)) (+ x (/ (- y x) (/ t z)))))

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