Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, I

Average Error: 7.9 → 0.7

Time: 19.3s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \cdot y - \left(z \cdot 9\right) \cdot t = -\infty:\\ \;\;\;\;\frac{x}{a} \cdot \frac{y}{2} - \frac{t}{2} \cdot \left(z \cdot \frac{9}{a}\right)\\ \mathbf{elif}\;x \cdot y - \left(z \cdot 9\right) \cdot t \le 1.511311171526004851396246562197501280677 \cdot 10^{306}:\\ \;\;\;\;\frac{x \cdot y}{a \cdot 2} - \frac{z \cdot t}{a} \cdot 4.5\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{a} \cdot \frac{y}{2} - \frac{t}{2} \cdot \left(z \cdot \frac{9}{a}\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a) {
        double r30644545 = x;
        double r30644546 = y;
        double r30644547 = r30644545 * r30644546;
        double r30644548 = z;
        double r30644549 = 9.0;
        double r30644550 = r30644548 * r30644549;
        double r30644551 = t;
        double r30644552 = r30644550 * r30644551;
        double r30644553 = r30644547 - r30644552;
        double r30644554 = a;
        double r30644555 = 2.0;
        double r30644556 = r30644554 * r30644555;
        double r30644557 = r30644553 / r30644556;
        return r30644557;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r30644558 = x;
        double r30644559 = y;
        double r30644560 = r30644558 * r30644559;
        double r30644561 = z;
        double r30644562 = 9.0;
        double r30644563 = r30644561 * r30644562;
        double r30644564 = t;
        double r30644565 = r30644563 * r30644564;
        double r30644566 = r30644560 - r30644565;
        double r30644567 = -inf.0;
        bool r30644568 = r30644566 <= r30644567;
        double r30644569 = a;
        double r30644570 = r30644558 / r30644569;
        double r30644571 = 2.0;
        double r30644572 = r30644559 / r30644571;
        double r30644573 = r30644570 * r30644572;
        double r30644574 = r30644564 / r30644571;
        double r30644575 = r30644562 / r30644569;
        double r30644576 = r30644561 * r30644575;
        double r30644577 = r30644574 * r30644576;
        double r30644578 = r30644573 - r30644577;
        double r30644579 = 1.511311171526005e+306;
        bool r30644580 = r30644566 <= r30644579;
        double r30644581 = r30644569 * r30644571;
        double r30644582 = r30644560 / r30644581;
        double r30644583 = r30644561 * r30644564;
        double r30644584 = r30644583 / r30644569;
        double r30644585 = 4.5;
        double r30644586 = r30644584 * r30644585;
        double r30644587 = r30644582 - r30644586;
        double r30644588 = r30644580 ? r30644587 : r30644578;
        double r30644589 = r30644568 ? r30644578 : r30644588;
        return r30644589;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original	7.9
Target	5.4
Herbie	0.7

\[\begin{array}{l} \mathbf{if}\;a \lt -2.090464557976709043451944897028999329376 \cdot 10^{86}:\\ \;\;\;\;0.5 \cdot \frac{y \cdot x}{a} - 4.5 \cdot \frac{t}{\frac{a}{z}}\\ \mathbf{elif}\;a \lt 2.144030707833976090627817222818061808815 \cdot 10^{99}:\\ \;\;\;\;\frac{x \cdot y - z \cdot \left(9 \cdot t\right)}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{a} \cdot \left(x \cdot 0.5\right) - \frac{t}{a} \cdot \left(z \cdot 4.5\right)\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if (- (* x y) (* (* z 9.0) t)) < -inf.0 or 1.511311171526005e+306 < (- (* x y) (* (* z 9.0) t))

   1. Initial program 63.4

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

   3. Applied div-sub 63.4

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

   5. Applied times-frac 32.5

      \[\leadsto \frac{x \cdot y}{a \cdot 2} - \color{blue}{\frac{z \cdot 9}{a} \cdot \frac{t}{2}}\]
   6. Using strategy rm

   7. Applied *-un-lft-identity 32.5

      \[\leadsto \frac{x \cdot y}{a \cdot 2} - \frac{z \cdot 9}{\color{blue}{1 \cdot a}} \cdot \frac{t}{2}\]

   8. Applied times-frac 32.3

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

   9. Simplified 32.3

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

   11. Applied times-frac 0.5

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

   if -inf.0 < (- (* x y) (* (* z 9.0) t)) < 1.511311171526005e+306

   1. Initial program 0.7

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

   3. Applied div-sub 0.7

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

   4. Taylor expanded around 0 0.7

      \[\leadsto \frac{x \cdot y}{a \cdot 2} - \color{blue}{4.5 \cdot \frac{t \cdot z}{a}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y - \left(z \cdot 9\right) \cdot t = -\infty:\\ \;\;\;\;\frac{x}{a} \cdot \frac{y}{2} - \frac{t}{2} \cdot \left(z \cdot \frac{9}{a}\right)\\ \mathbf{elif}\;x \cdot y - \left(z \cdot 9\right) \cdot t \le 1.511311171526004851396246562197501280677 \cdot 10^{306}:\\ \;\;\;\;\frac{x \cdot y}{a \cdot 2} - \frac{z \cdot t}{a} \cdot 4.5\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{a} \cdot \frac{y}{2} - \frac{t}{2} \cdot \left(z \cdot \frac{9}{a}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019169 +o rules:numerics
(FPCore (x y z t a)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, I"

  :herbie-target
  (if (< a -2.090464557976709e+86) (- (* 0.5 (/ (* y x) a)) (* 4.5 (/ t (/ a z)))) (if (< a 2.144030707833976e+99) (/ (- (* x y) (* z (* 9.0 t))) (* a 2.0)) (- (* (/ y a) (* x 0.5)) (* (/ t a) (* z 4.5)))))

  (/ (- (* x y) (* (* z 9.0) t)) (* a 2.0)))