Development.Shake.Progress:decay from shake-0.15.5

Average Error: 22.8 → 18.9

Time: 5.9s

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}\;z \le -5.58639378401121532712856205181949823781 \cdot 10^{76} \lor \neg \left(z \le 1.292229734757079339613065030853168892384 \cdot 10^{133}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;{\left(\frac{x \cdot y + z \cdot \left(t - a\right)}{\left(z \cdot b + y\right) - z \cdot y}\right)}^{1}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r785022 = x;
        double r785023 = y;
        double r785024 = r785022 * r785023;
        double r785025 = z;
        double r785026 = t;
        double r785027 = a;
        double r785028 = r785026 - r785027;
        double r785029 = r785025 * r785028;
        double r785030 = r785024 + r785029;
        double r785031 = b;
        double r785032 = r785031 - r785023;
        double r785033 = r785025 * r785032;
        double r785034 = r785023 + r785033;
        double r785035 = r785030 / r785034;
        return r785035;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r785036 = z;
        double r785037 = -5.5863937840112153e+76;
        bool r785038 = r785036 <= r785037;
        double r785039 = 1.2922297347570793e+133;
        bool r785040 = r785036 <= r785039;
        double r785041 = !r785040;
        bool r785042 = r785038 || r785041;
        double r785043 = t;
        double r785044 = b;
        double r785045 = r785043 / r785044;
        double r785046 = a;
        double r785047 = r785046 / r785044;
        double r785048 = r785045 - r785047;
        double r785049 = x;
        double r785050 = y;
        double r785051 = r785049 * r785050;
        double r785052 = r785043 - r785046;
        double r785053 = r785036 * r785052;
        double r785054 = r785051 + r785053;
        double r785055 = r785036 * r785044;
        double r785056 = r785055 + r785050;
        double r785057 = r785036 * r785050;
        double r785058 = r785056 - r785057;
        double r785059 = r785054 / r785058;
        double r785060 = 1.0;
        double r785061 = pow(r785059, r785060);
        double r785062 = r785042 ? r785048 : r785061;
        return r785062;
}

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	22.8
Target	17.6
Herbie	18.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 2 regimes

2. if z < -5.5863937840112153e+76 or 1.2922297347570793e+133 < z

   1. Initial program 46.2

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

   3. Applied sub-neg 46.2

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

   4. Applied distribute-rgt-in 46.4

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

   5. Applied associate-+r+ 46.4

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

   7. Applied clear-num 46.4

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

   8. Simplified 46.4

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

   9. Taylor expanded around inf 34.0

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

   if -5.5863937840112153e+76 < z < 1.2922297347570793e+133

   1. Initial program 11.8

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

   3. Applied sub-neg 11.8

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

   4. Applied distribute-rgt-in 11.8

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

   5. Applied associate-+r+ 11.8

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

   7. Applied clear-num 11.9

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

   8. Simplified 11.9

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

   10. Applied div-inv 12.1

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

   11. Applied add-cube-cbrt 12.1

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

   12. Applied times-frac 12.0

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

   13. Simplified 12.0

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

   14. Simplified 11.9

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

   16. Applied pow1 11.9

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

   17. Applied pow1 11.9

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

   18. Applied pow-prod-down 11.9

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

   19. Simplified 11.8

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

4. Final simplification 18.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -5.58639378401121532712856205181949823781 \cdot 10^{76} \lor \neg \left(z \le 1.292229734757079339613065030853168892384 \cdot 10^{133}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;{\left(\frac{x \cdot y + z \cdot \left(t - a\right)}{\left(z \cdot b + y\right) - z \cdot y}\right)}^{1}\\ \end{array}\]

Reproduce

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