Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.0 → 19.2

Time: 15.7s

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

C

double f(double x, double y, double z, double t, double a, double b) {
        double r575102 = x;
        double r575103 = y;
        double r575104 = r575102 * r575103;
        double r575105 = z;
        double r575106 = t;
        double r575107 = a;
        double r575108 = r575106 - r575107;
        double r575109 = r575105 * r575108;
        double r575110 = r575104 + r575109;
        double r575111 = b;
        double r575112 = r575111 - r575103;
        double r575113 = r575105 * r575112;
        double r575114 = r575103 + r575113;
        double r575115 = r575110 / r575114;
        return r575115;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r575116 = x;
        double r575117 = y;
        double r575118 = r575116 * r575117;
        double r575119 = z;
        double r575120 = t;
        double r575121 = a;
        double r575122 = r575120 - r575121;
        double r575123 = r575119 * r575122;
        double r575124 = r575118 + r575123;
        double r575125 = b;
        double r575126 = r575125 - r575117;
        double r575127 = r575119 * r575126;
        double r575128 = r575117 + r575127;
        double r575129 = r575124 / r575128;
        double r575130 = -inf.0;
        bool r575131 = r575129 <= r575130;
        double r575132 = 2.9230484745490878e+262;
        bool r575133 = r575129 <= r575132;
        double r575134 = r575133 ? r575129 : r575116;
        double r575135 = r575131 ? r575116 : r575134;
        return r575135;
}

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	19.2

\[\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 (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) < -inf.0 or 2.9230484745490878e+262 < (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))

   1. Initial program 61.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 61.2

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

   4. Applied distribute-rgt-in 61.2

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

   5. Applied associate-+r+ 61.2

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

   6. Simplified 61.2

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

   7. Taylor expanded around 0 48.9

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

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

   1. Initial program 6.3

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

      \[\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 *-un-lft-identity 6.4

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

   6. Applied *-un-lft-identity 6.4

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

   7. Applied times-frac 6.4

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

   8. Applied add-cube-cbrt 6.4

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

   9. Applied times-frac 6.4

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

   10. Simplified 6.4

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

   11. Simplified 6.3

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

4. Final simplification 19.2

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

Reproduce

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