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

↓

\[\begin{array}{l} \mathbf{if}\;x + \frac{\left(y - x\right) \cdot z}{t} = -\infty \lor \neg \left(x + \frac{\left(y - x\right) \cdot z}{t} \le 9.7386606994553072 \cdot 10^{291}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{z}{t}, y, x - \frac{1}{\frac{\frac{t}{z}}{x}}\right)\\ \mathbf{else}:\\ \;\;\;\;x + \frac{\left(y - x\right) \cdot z}{t}\\ \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 \lor \neg \left(x + \frac{\left(y - x\right) \cdot z}{t} \le 9.7386606994553072 \cdot 10^{291}\right):\\
\;\;\;\;\mathsf{fma}\left(\frac{z}{t}, y, x - \frac{1}{\frac{\frac{t}{z}}{x}}\right)\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r449648 = x;
        double r449649 = y;
        double r449650 = r449649 - r449648;
        double r449651 = z;
        double r449652 = r449650 * r449651;
        double r449653 = t;
        double r449654 = r449652 / r449653;
        double r449655 = r449648 + r449654;
        return r449655;
}

↓

double f(double x, double y, double z, double t) {
        double r449656 = x;
        double r449657 = y;
        double r449658 = r449657 - r449656;
        double r449659 = z;
        double r449660 = r449658 * r449659;
        double r449661 = t;
        double r449662 = r449660 / r449661;
        double r449663 = r449656 + r449662;
        double r449664 = -inf.0;
        bool r449665 = r449663 <= r449664;
        double r449666 = 9.738660699455307e+291;
        bool r449667 = r449663 <= r449666;
        double r449668 = !r449667;
        bool r449669 = r449665 || r449668;
        double r449670 = r449659 / r449661;
        double r449671 = 1.0;
        double r449672 = r449661 / r449659;
        double r449673 = r449672 / r449656;
        double r449674 = r449671 / r449673;
        double r449675 = r449656 - r449674;
        double r449676 = fma(r449670, r449657, r449675);
        double r449677 = r449669 ? r449676 : r449663;
        return r449677;
}

Original	6.7
Target	2.0
Herbie	0.8

Derivation

Split input into 2 regimes
if (+ x (/ (* (- y x) z) t)) < -inf.0 or 9.738660699455307e+291 < (+ x (/ (* (- y x) z) t))
1. Initial program 54.8
  \[x + \frac{\left(y - x\right) \cdot z}{t}\]
2. Simplified3.4
  \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y - x}{t}, z, x\right)}\]
3. Using strategy rm
4. Applied div-sub3.4
  \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{t} - \frac{x}{t}}, z, x\right)\]
5. Taylor expanded around inf 54.8
  \[\leadsto \color{blue}{\left(\frac{z \cdot y}{t} + x\right) - \frac{x \cdot z}{t}}\]
6. Simplified33.1
  \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{z}{t}, y, x - \frac{x \cdot z}{t}\right)}\]
7. Using strategy rm
8. Applied associate-/l*0.7
  \[\leadsto \mathsf{fma}\left(\frac{z}{t}, y, x - \color{blue}{\frac{x}{\frac{t}{z}}}\right)\]
9. Using strategy rm
10. Applied clear-num0.8
  \[\leadsto \mathsf{fma}\left(\frac{z}{t}, y, x - \color{blue}{\frac{1}{\frac{\frac{t}{z}}{x}}}\right)\]
if -inf.0 < (+ x (/ (* (- y x) z) t)) < 9.738660699455307e+291
1. Initial program 0.8
  \[x + \frac{\left(y - x\right) \cdot z}{t}\]
Recombined 2 regimes into one program.
Final simplification0.8
\[\leadsto \begin{array}{l} \mathbf{if}\;x + \frac{\left(y - x\right) \cdot z}{t} = -\infty \lor \neg \left(x + \frac{\left(y - x\right) \cdot z}{t} \le 9.7386606994553072 \cdot 10^{291}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{z}{t}, y, x - \frac{1}{\frac{\frac{t}{z}}{x}}\right)\\ \mathbf{else}:\\ \;\;\;\;x + \frac{\left(y - x\right) \cdot z}{t}\\ \end{array}\]

Reproduce

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

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

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

Error

Target

Derivation

`if (+ x (/ (* (- y x) z) t)) < -inf.0 or 9.738660699455307e+291 < (+ x (/ (* (- y x) z) t))`

`if -inf.0 < (+ x (/ (* (- y x) z) t)) < 9.738660699455307e+291`

Reproduce