Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.9 → 17.0

Time: 7.5s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \le -1.750227877786161153105515302720964265793 \cdot 10^{294}:\\ \;\;\;\;x\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \le 2.017726237827154017354999902088434431181 \cdot 10^{279}:\\ \;\;\;\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r866586 = x;
        double r866587 = y;
        double r866588 = r866586 * r866587;
        double r866589 = z;
        double r866590 = t;
        double r866591 = a;
        double r866592 = r866590 - r866591;
        double r866593 = r866589 * r866592;
        double r866594 = r866588 + r866593;
        double r866595 = b;
        double r866596 = r866595 - r866587;
        double r866597 = r866589 * r866596;
        double r866598 = r866587 + r866597;
        double r866599 = r866594 / r866598;
        return r866599;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r866600 = x;
        double r866601 = y;
        double r866602 = r866600 * r866601;
        double r866603 = z;
        double r866604 = t;
        double r866605 = a;
        double r866606 = r866604 - r866605;
        double r866607 = r866603 * r866606;
        double r866608 = r866602 + r866607;
        double r866609 = b;
        double r866610 = r866609 - r866601;
        double r866611 = r866603 * r866610;
        double r866612 = r866601 + r866611;
        double r866613 = r866608 / r866612;
        double r866614 = -1.7502278777861612e+294;
        bool r866615 = r866613 <= r866614;
        double r866616 = 2.017726237827154e+279;
        bool r866617 = r866613 <= r866616;
        double r866618 = r866604 / r866609;
        double r866619 = r866605 / r866609;
        double r866620 = r866618 - r866619;
        double r866621 = r866617 ? r866613 : r866620;
        double r866622 = r866615 ? r866600 : r866621;
        return r866622;
}

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

Original	23.9
Target	18.6
Herbie	17.0

\[\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)))) < -1.7502278777861612e+294

   1. Initial program 60.8

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

   3. Applied clear-num 60.8

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

   5. Applied div-inv 60.8

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

   6. Applied associate-/r* 60.8

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

   7. Simplified 60.8

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

   8. Taylor expanded around 0 38.2

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

   if -1.7502278777861612e+294 < (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) < 2.017726237827154e+279

   1. Initial program 6.1

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

   if 2.017726237827154e+279 < (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))

   1. Initial program 62.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-num 62.0

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

   5. Applied div-inv 62.0

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

   6. Applied associate-/r* 62.0

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

   7. Simplified 62.0

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

   8. Taylor expanded around inf 41.0

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

4. Final simplification 17.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \le -1.750227877786161153105515302720964265793 \cdot 10^{294}:\\ \;\;\;\;x\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \le 2.017726237827154017354999902088434431181 \cdot 10^{279}:\\ \;\;\;\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \end{array}\]

Reproduce

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