Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.0 → 15.1

Time: 20.1s

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}\;y \le 4.997789746797433380054450287723707755622 \cdot 10^{-51}:\\ \;\;\;\;\frac{\sqrt[3]{y} \cdot x}{\sqrt[3]{z \cdot \left(b - y\right) + y}} \cdot \frac{\frac{\sqrt[3]{y} \cdot \sqrt[3]{y}}{\sqrt[3]{z \cdot \left(b - y\right) + y}}}{\sqrt[3]{z \cdot \left(b - y\right) + y}} - \frac{z}{z \cdot \left(b - y\right) + y} \cdot \left(a - t\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{\frac{z \cdot \left(b - y\right) + y}{x}} - \frac{a - t}{z \cdot \left(b - y\right) + y} \cdot z\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r623238 = x;
        double r623239 = y;
        double r623240 = r623238 * r623239;
        double r623241 = z;
        double r623242 = t;
        double r623243 = a;
        double r623244 = r623242 - r623243;
        double r623245 = r623241 * r623244;
        double r623246 = r623240 + r623245;
        double r623247 = b;
        double r623248 = r623247 - r623239;
        double r623249 = r623241 * r623248;
        double r623250 = r623239 + r623249;
        double r623251 = r623246 / r623250;
        return r623251;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r623252 = y;
        double r623253 = 4.9977897467974334e-51;
        bool r623254 = r623252 <= r623253;
        double r623255 = cbrt(r623252);
        double r623256 = x;
        double r623257 = r623255 * r623256;
        double r623258 = z;
        double r623259 = b;
        double r623260 = r623259 - r623252;
        double r623261 = r623258 * r623260;
        double r623262 = r623261 + r623252;
        double r623263 = cbrt(r623262);
        double r623264 = r623257 / r623263;
        double r623265 = r623255 * r623255;
        double r623266 = r623265 / r623263;
        double r623267 = r623266 / r623263;
        double r623268 = r623264 * r623267;
        double r623269 = r623258 / r623262;
        double r623270 = a;
        double r623271 = t;
        double r623272 = r623270 - r623271;
        double r623273 = r623269 * r623272;
        double r623274 = r623268 - r623273;
        double r623275 = r623262 / r623256;
        double r623276 = r623252 / r623275;
        double r623277 = r623272 / r623262;
        double r623278 = r623277 * r623258;
        double r623279 = r623276 - r623278;
        double r623280 = r623254 ? r623274 : r623279;
        return r623280;
}

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.0
Target	17.8
Herbie	15.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 y < 4.9977897467974334e-51

   1. Initial program 20.8

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

   2. Simplified 20.8

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

   4. Applied div-sub 20.8

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

   5. Simplified 20.8

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

   6. Simplified 16.3

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

   8. Applied associate-/l* 16.7

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

   9. Simplified 16.7

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

   11. Applied *-un-lft-identity 16.7

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

   12. Applied add-cube-cbrt 17.0

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

   13. Applied times-frac 17.0

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

   14. Applied add-cube-cbrt 16.9

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

   15. Applied times-frac 13.3

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

   16. Simplified 13.3

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

   17. Simplified 13.4

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

   if 4.9977897467974334e-51 < y

   1. Initial program 27.9

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

   2. Simplified 27.9

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

   4. Applied div-sub 27.9

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

   5. Simplified 27.9

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

   6. Simplified 25.5

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

   8. Applied associate-/l* 19.6

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

   9. Simplified 19.6

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

   11. Applied div-inv 19.6

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

   12. Applied associate-*l* 19.0

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

   13. Simplified 19.0

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

4. Final simplification 15.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \le 4.997789746797433380054450287723707755622 \cdot 10^{-51}:\\ \;\;\;\;\frac{\sqrt[3]{y} \cdot x}{\sqrt[3]{z \cdot \left(b - y\right) + y}} \cdot \frac{\frac{\sqrt[3]{y} \cdot \sqrt[3]{y}}{\sqrt[3]{z \cdot \left(b - y\right) + y}}}{\sqrt[3]{z \cdot \left(b - y\right) + y}} - \frac{z}{z \cdot \left(b - y\right) + y} \cdot \left(a - t\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{\frac{z \cdot \left(b - y\right) + y}{x}} - \frac{a - t}{z \cdot \left(b - y\right) + y} \cdot z\\ \end{array}\]

Reproduce

herbie shell --seed 2019194 
(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)))))