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

Average Error: 7.9 → 0.7

Time: 18.2s

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 r31576583 = x;
        double r31576584 = y;
        double r31576585 = r31576583 * r31576584;
        double r31576586 = z;
        double r31576587 = 9.0;
        double r31576588 = r31576586 * r31576587;
        double r31576589 = t;
        double r31576590 = r31576588 * r31576589;
        double r31576591 = r31576585 - r31576590;
        double r31576592 = a;
        double r31576593 = 2.0;
        double r31576594 = r31576592 * r31576593;
        double r31576595 = r31576591 / r31576594;
        return r31576595;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r31576596 = x;
        double r31576597 = y;
        double r31576598 = r31576596 * r31576597;
        double r31576599 = z;
        double r31576600 = 9.0;
        double r31576601 = r31576599 * r31576600;
        double r31576602 = t;
        double r31576603 = r31576601 * r31576602;
        double r31576604 = r31576598 - r31576603;
        double r31576605 = -inf.0;
        bool r31576606 = r31576604 <= r31576605;
        double r31576607 = a;
        double r31576608 = r31576596 / r31576607;
        double r31576609 = 2.0;
        double r31576610 = r31576597 / r31576609;
        double r31576611 = r31576608 * r31576610;
        double r31576612 = r31576602 / r31576609;
        double r31576613 = r31576600 / r31576607;
        double r31576614 = r31576599 * r31576613;
        double r31576615 = r31576612 * r31576614;
        double r31576616 = r31576611 - r31576615;
        double r31576617 = 1.511311171526005e+306;
        bool r31576618 = r31576604 <= r31576617;
        double r31576619 = r31576607 * r31576609;
        double r31576620 = r31576598 / r31576619;
        double r31576621 = r31576599 * r31576602;
        double r31576622 = r31576621 / r31576607;
        double r31576623 = 4.5;
        double r31576624 = r31576622 * r31576623;
        double r31576625 = r31576620 - r31576624;
        double r31576626 = r31576618 ? r31576625 : r31576616;
        double r31576627 = r31576606 ? r31576616 : r31576626;
        return r31576627;
}

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 
(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)))