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

Average Error: 8.0 → 1.7

Time: 4.9s

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 \le -5.81880234558190669 \cdot 10^{134} \lor \neg \left(x \cdot y - \left(z \cdot 9\right) \cdot t \le 1.95624520253703639 \cdot 10^{220}\right):\\ \;\;\;\;\left(x \cdot 0.5\right) \cdot \frac{y}{a} - \left(t \cdot 4.5\right) \cdot \frac{z}{a}\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot y - \left(z \cdot 9\right) \cdot t\right) \cdot \frac{1}{a \cdot 2}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a) {
        double r840534 = x;
        double r840535 = y;
        double r840536 = r840534 * r840535;
        double r840537 = z;
        double r840538 = 9.0;
        double r840539 = r840537 * r840538;
        double r840540 = t;
        double r840541 = r840539 * r840540;
        double r840542 = r840536 - r840541;
        double r840543 = a;
        double r840544 = 2.0;
        double r840545 = r840543 * r840544;
        double r840546 = r840542 / r840545;
        return r840546;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r840547 = x;
        double r840548 = y;
        double r840549 = r840547 * r840548;
        double r840550 = z;
        double r840551 = 9.0;
        double r840552 = r840550 * r840551;
        double r840553 = t;
        double r840554 = r840552 * r840553;
        double r840555 = r840549 - r840554;
        double r840556 = -5.818802345581907e+134;
        bool r840557 = r840555 <= r840556;
        double r840558 = 1.9562452025370364e+220;
        bool r840559 = r840555 <= r840558;
        double r840560 = !r840559;
        bool r840561 = r840557 || r840560;
        double r840562 = 0.5;
        double r840563 = r840547 * r840562;
        double r840564 = a;
        double r840565 = r840548 / r840564;
        double r840566 = r840563 * r840565;
        double r840567 = 4.5;
        double r840568 = r840553 * r840567;
        double r840569 = r840550 / r840564;
        double r840570 = r840568 * r840569;
        double r840571 = r840566 - r840570;
        double r840572 = 1.0;
        double r840573 = 2.0;
        double r840574 = r840564 * r840573;
        double r840575 = r840572 / r840574;
        double r840576 = r840555 * r840575;
        double r840577 = r840561 ? r840571 : r840576;
        return r840577;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original	8.0
Target	5.6
Herbie	1.7

\[\begin{array}{l} \mathbf{if}\;a \lt -2.090464557976709 \cdot 10^{86}:\\ \;\;\;\;0.5 \cdot \frac{y \cdot x}{a} - 4.5 \cdot \frac{t}{\frac{a}{z}}\\ \mathbf{elif}\;a \lt 2.14403070783397609 \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)) < -5.818802345581907e+134 or 1.9562452025370364e+220 < (- (* x y) (* (* z 9.0) t))

   1. Initial program 24.6

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

   2. Taylor expanded around 0 24.2

      \[\leadsto \color{blue}{0.5 \cdot \frac{x \cdot y}{a} - 4.5 \cdot \frac{t \cdot z}{a}}\]
   3. Using strategy rm

   4. Applied *-un-lft-identity 24.2

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

   5. Applied times-frac 14.1

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

   6. Applied associate-*r* 14.2

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

   7. Simplified 14.2

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

   9. Applied *-un-lft-identity 14.2

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

   10. Applied times-frac 2.9

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

   11. Applied associate-*r* 2.8

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

   12. Simplified 2.8

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

   if -5.818802345581907e+134 < (- (* x y) (* (* z 9.0) t)) < 1.9562452025370364e+220

   1. Initial program 1.1

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

   3. Applied div-inv 1.2

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

4. Final simplification 1.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y - \left(z \cdot 9\right) \cdot t \le -5.81880234558190669 \cdot 10^{134} \lor \neg \left(x \cdot y - \left(z \cdot 9\right) \cdot t \le 1.95624520253703639 \cdot 10^{220}\right):\\ \;\;\;\;\left(x \cdot 0.5\right) \cdot \frac{y}{a} - \left(t \cdot 4.5\right) \cdot \frac{z}{a}\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot y - \left(z \cdot 9\right) \cdot t\right) \cdot \frac{1}{a \cdot 2}\\ \end{array}\]

Reproduce

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

  :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 t))) (* a 2)) (- (* (/ y a) (* x 0.5)) (* (/ t a) (* z 4.5)))))

  (/ (- (* x y) (* (* z 9) t)) (* a 2)))