Average Error: 22.9 → 18.8
Time: 23.0s
Precision: 64
\[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -5.059448256191389971955295445532251364324 \cdot 10^{125} \lor \neg \left(z \le 4.516505167907681114402918924850717737343 \cdot 10^{120}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot y + z \cdot \left(t - a\right)\right) \cdot \frac{1}{\mathsf{fma}\left(b - y, z, y\right)}\\ \end{array}\]
\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}
↓
\begin{array}{l}
\mathbf{if}\;z \le -5.059448256191389971955295445532251364324 \cdot 10^{125} \lor \neg \left(z \le 4.516505167907681114402918924850717737343 \cdot 10^{120}\right):\\
\;\;\;\;\frac{t}{b} - \frac{a}{b}\\

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

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r1253799 = x;
        double r1253800 = y;
        double r1253801 = r1253799 * r1253800;
        double r1253802 = z;
        double r1253803 = t;
        double r1253804 = a;
        double r1253805 = r1253803 - r1253804;
        double r1253806 = r1253802 * r1253805;
        double r1253807 = r1253801 + r1253806;
        double r1253808 = b;
        double r1253809 = r1253808 - r1253800;
        double r1253810 = r1253802 * r1253809;
        double r1253811 = r1253800 + r1253810;
        double r1253812 = r1253807 / r1253811;
        return r1253812;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r1253813 = z;
        double r1253814 = -5.05944825619139e+125;
        bool r1253815 = r1253813 <= r1253814;
        double r1253816 = 4.516505167907681e+120;
        bool r1253817 = r1253813 <= r1253816;
        double r1253818 = !r1253817;
        bool r1253819 = r1253815 || r1253818;
        double r1253820 = t;
        double r1253821 = b;
        double r1253822 = r1253820 / r1253821;
        double r1253823 = a;
        double r1253824 = r1253823 / r1253821;
        double r1253825 = r1253822 - r1253824;
        double r1253826 = x;
        double r1253827 = y;
        double r1253828 = r1253826 * r1253827;
        double r1253829 = r1253820 - r1253823;
        double r1253830 = r1253813 * r1253829;
        double r1253831 = r1253828 + r1253830;
        double r1253832 = 1.0;
        double r1253833 = r1253821 - r1253827;
        double r1253834 = fma(r1253833, r1253813, r1253827);
        double r1253835 = r1253832 / r1253834;
        double r1253836 = r1253831 * r1253835;
        double r1253837 = r1253819 ? r1253825 : r1253836;
        return r1253837;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Target

Original22.9
Target18.0
Herbie18.8
\[\frac{z \cdot t + y \cdot x}{y + z \cdot \left(b - y\right)} - \frac{a}{\left(b - y\right) + \frac{y}{z}}\]

Derivation

  1. Split input into 2 regimes

  2. if z < -5.05944825619139e+125 or 4.516505167907681e+120 < z

    1. Initial program 47.6

      \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\]
    2. Using strategy rm

    3. Applied clear-num47.7

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

    4. Simplified47.7

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

    5. Taylor expanded around inf 33.6

      \[\leadsto \color{blue}{\frac{t}{b} - \frac{a}{b}}\]

    if -5.05944825619139e+125 < z < 4.516505167907681e+120

    1. Initial program 12.5

      \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\]
    2. Using strategy rm

    3. Applied div-inv12.6

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

    4. Simplified12.6

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

  4. Final simplification18.8

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

Reproduce

herbie shell --seed 2019306 +o rules:numerics
(FPCore (x y z t a b)
  :name "Development.Shake.Progress:decay from shake-0.15.5"
  :precision binary64

  :herbie-target
  (- (/ (+ (* z t) (* y x)) (+ y (* z (- b y)))) (/ a (+ (- b y) (/ y z))))

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