Average Error: 24.0 → 15.1
Time: 23.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}\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} = -\infty:\\ \;\;\;\;x\\ \mathbf{elif}\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le -7.547292817816051891310126890515158799825 \cdot 10^{-298} \lor \neg \left(\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le -0.0\right) \land \frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le 7.280549867219067984064896300347681010703 \cdot 10^{307}:\\ \;\;\;\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y}\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \end{array}\]
\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}
↓
\begin{array}{l}
\mathbf{if}\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} = -\infty:\\
\;\;\;\;x\\

\mathbf{elif}\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le -7.547292817816051891310126890515158799825 \cdot 10^{-298} \lor \neg \left(\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le -0.0\right) \land \frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le 7.280549867219067984064896300347681010703 \cdot 10^{307}:\\
\;\;\;\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y}\\

\mathbf{else}:\\
\;\;\;\;\frac{t}{b} - \frac{a}{b}\\

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r504044 = x;
        double r504045 = y;
        double r504046 = r504044 * r504045;
        double r504047 = z;
        double r504048 = t;
        double r504049 = a;
        double r504050 = r504048 - r504049;
        double r504051 = r504047 * r504050;
        double r504052 = r504046 + r504051;
        double r504053 = b;
        double r504054 = r504053 - r504045;
        double r504055 = r504047 * r504054;
        double r504056 = r504045 + r504055;
        double r504057 = r504052 / r504056;
        return r504057;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r504058 = z;
        double r504059 = t;
        double r504060 = a;
        double r504061 = r504059 - r504060;
        double r504062 = r504058 * r504061;
        double r504063 = x;
        double r504064 = y;
        double r504065 = r504063 * r504064;
        double r504066 = r504062 + r504065;
        double r504067 = b;
        double r504068 = r504067 - r504064;
        double r504069 = r504068 * r504058;
        double r504070 = r504069 + r504064;
        double r504071 = r504066 / r504070;
        double r504072 = -inf.0;
        bool r504073 = r504071 <= r504072;
        double r504074 = -7.547292817816052e-298;
        bool r504075 = r504071 <= r504074;
        double r504076 = -0.0;
        bool r504077 = r504071 <= r504076;
        double r504078 = !r504077;
        double r504079 = 7.280549867219068e+307;
        bool r504080 = r504071 <= r504079;
        bool r504081 = r504078 && r504080;
        bool r504082 = r504075 || r504081;
        double r504083 = r504059 / r504067;
        double r504084 = r504060 / r504067;
        double r504085 = r504083 - r504084;
        double r504086 = r504082 ? r504071 : r504085;
        double r504087 = r504073 ? r504063 : r504086;
        return r504087;
}

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

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original24.0
Target18.5
Herbie15.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 3 regimes

  2. if (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) < -inf.0

    1. Initial program 64.0

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

    3. Applied clear-num64.0

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

    4. Simplified64.0

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

    6. Applied div-inv64.0

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

    7. Simplified64.0

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

    8. Taylor expanded around 0 37.3

      \[\leadsto \color{blue}{x}\]

    if -inf.0 < (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) < -7.547292817816052e-298 or -0.0 < (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) < 7.280549867219068e+307

    1. Initial program 0.3

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

    if -7.547292817816052e-298 < (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) < -0.0 or 7.280549867219068e+307 < (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))

    1. Initial program 59.1

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

    3. Applied clear-num59.1

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

    4. Simplified59.1

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

    5. Taylor expanded around inf 37.9

      \[\leadsto \color{blue}{\frac{t}{b} - \frac{a}{b}}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification15.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} = -\infty:\\ \;\;\;\;x\\ \mathbf{elif}\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le -7.547292817816051891310126890515158799825 \cdot 10^{-298} \lor \neg \left(\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le -0.0\right) \land \frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y} \le 7.280549867219067984064896300347681010703 \cdot 10^{307}:\\ \;\;\;\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(b - y\right) \cdot z + y}\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \end{array}\]

Reproduce

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

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

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