Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.5 → 15.9

Time: 7.6s

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)} = -\infty:\\ \;\;\;\;x\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \le 5.66500938043718374 \cdot 10^{306}:\\ \;\;\;\;\frac{\mathsf{fma}\left(y, x, z \cdot \left(t - a\right)\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 r917298 = x;
        double r917299 = y;
        double r917300 = r917298 * r917299;
        double r917301 = z;
        double r917302 = t;
        double r917303 = a;
        double r917304 = r917302 - r917303;
        double r917305 = r917301 * r917304;
        double r917306 = r917300 + r917305;
        double r917307 = b;
        double r917308 = r917307 - r917299;
        double r917309 = r917301 * r917308;
        double r917310 = r917299 + r917309;
        double r917311 = r917306 / r917310;
        return r917311;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r917312 = x;
        double r917313 = y;
        double r917314 = r917312 * r917313;
        double r917315 = z;
        double r917316 = t;
        double r917317 = a;
        double r917318 = r917316 - r917317;
        double r917319 = r917315 * r917318;
        double r917320 = r917314 + r917319;
        double r917321 = b;
        double r917322 = r917321 - r917313;
        double r917323 = r917315 * r917322;
        double r917324 = r917313 + r917323;
        double r917325 = r917320 / r917324;
        double r917326 = -inf.0;
        bool r917327 = r917325 <= r917326;
        double r917328 = 5.665009380437184e+306;
        bool r917329 = r917325 <= r917328;
        double r917330 = fma(r917313, r917312, r917319);
        double r917331 = r917330 / r917324;
        double r917332 = r917316 / r917321;
        double r917333 = r917317 / r917321;
        double r917334 = r917332 - r917333;
        double r917335 = r917329 ? r917331 : r917334;
        double r917336 = r917327 ? r917312 : r917335;
        return r917336;
}

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.5
Target	18.1
Herbie	15.9

\[\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-num 64.0

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

   4. Simplified 64.0

      \[\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 0 34.1

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

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

   1. Initial program 5.8

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

   3. Applied add-cube-cbrt 6.3

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

   5. Applied *-un-lft-identity 6.3

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

   6. Applied associate-/r* 6.3

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

   7. Simplified 5.8

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

   if 5.665009380437184e+306 < (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))

   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-num 64.0

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

   4. Simplified 64.0

      \[\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 40.9

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

4. Final simplification 15.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} = -\infty:\\ \;\;\;\;x\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \le 5.66500938043718374 \cdot 10^{306}:\\ \;\;\;\;\frac{\mathsf{fma}\left(y, x, z \cdot \left(t - a\right)\right)}{y + z \cdot \left(b - y\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \end{array}\]

Reproduce

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