Average Error: 23.3 → 19.1
Time: 27.4s
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 -1.38322835723796380516786120602979593777 \cdot 10^{135} \lor \neg \left(z \le 5.115612150638236515910171343054123777678 \cdot 10^{154}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x, y, z \cdot t + z \cdot \left(-a\right)\right) \cdot \frac{1}{\mathsf{fma}\left(z, b - y, 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 -1.38322835723796380516786120602979593777 \cdot 10^{135} \lor \neg \left(z \le 5.115612150638236515910171343054123777678 \cdot 10^{154}\right):\\
\;\;\;\;\frac{t}{b} - \frac{a}{b}\\

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

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r513636 = x;
        double r513637 = y;
        double r513638 = r513636 * r513637;
        double r513639 = z;
        double r513640 = t;
        double r513641 = a;
        double r513642 = r513640 - r513641;
        double r513643 = r513639 * r513642;
        double r513644 = r513638 + r513643;
        double r513645 = b;
        double r513646 = r513645 - r513637;
        double r513647 = r513639 * r513646;
        double r513648 = r513637 + r513647;
        double r513649 = r513644 / r513648;
        return r513649;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r513650 = z;
        double r513651 = -1.3832283572379638e+135;
        bool r513652 = r513650 <= r513651;
        double r513653 = 5.1156121506382365e+154;
        bool r513654 = r513650 <= r513653;
        double r513655 = !r513654;
        bool r513656 = r513652 || r513655;
        double r513657 = t;
        double r513658 = b;
        double r513659 = r513657 / r513658;
        double r513660 = a;
        double r513661 = r513660 / r513658;
        double r513662 = r513659 - r513661;
        double r513663 = x;
        double r513664 = y;
        double r513665 = r513650 * r513657;
        double r513666 = -r513660;
        double r513667 = r513650 * r513666;
        double r513668 = r513665 + r513667;
        double r513669 = fma(r513663, r513664, r513668);
        double r513670 = 1.0;
        double r513671 = r513658 - r513664;
        double r513672 = fma(r513650, r513671, r513664);
        double r513673 = r513670 / r513672;
        double r513674 = r513669 * r513673;
        double r513675 = r513656 ? r513662 : r513674;
        return r513675;
}

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

Original23.3
Target18.1
Herbie19.1
\[\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 < -1.3832283572379638e+135 or 5.1156121506382365e+154 < z

    1. Initial program 49.3

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

    2. Simplified49.3

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

    4. Applied clear-num49.3

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

    5. Taylor expanded around inf 33.1

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

    if -1.3832283572379638e+135 < z < 5.1156121506382365e+154

    1. Initial program 14.0

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

    2. Simplified14.0

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

    4. Applied div-inv14.1

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

    6. Applied sub-neg14.1

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

    7. Applied distribute-lft-in14.1

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

  4. Final simplification19.1

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

Reproduce

herbie shell --seed 2019303 +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)))))