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

Average Error: 3.7 → 1.5

Time: 3.1s

Precision: 64

Math

\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]

↓

\[\begin{array}{l} \mathbf{if}\;z \cdot 3 \le 2.390178981002547728134938616903530718403 \cdot 10^{-148}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot 3} \cdot \frac{1}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r711986 = x;
        double r711987 = y;
        double r711988 = z;
        double r711989 = 3.0;
        double r711990 = r711988 * r711989;
        double r711991 = r711987 / r711990;
        double r711992 = r711986 - r711991;
        double r711993 = t;
        double r711994 = r711990 * r711987;
        double r711995 = r711993 / r711994;
        double r711996 = r711992 + r711995;
        return r711996;
}

↓

double f(double x, double y, double z, double t) {
        double r711997 = z;
        double r711998 = 3.0;
        double r711999 = r711997 * r711998;
        double r712000 = 2.3901789810025477e-148;
        bool r712001 = r711999 <= r712000;
        double r712002 = x;
        double r712003 = y;
        double r712004 = r712003 / r711999;
        double r712005 = r712002 - r712004;
        double r712006 = t;
        double r712007 = r712006 / r711999;
        double r712008 = 1.0;
        double r712009 = r712008 / r712003;
        double r712010 = r712007 * r712009;
        double r712011 = r712005 + r712010;
        double r712012 = r712008 / r711997;
        double r712013 = r712003 / r711998;
        double r712014 = r712012 * r712013;
        double r712015 = r712002 - r712014;
        double r712016 = r711999 * r712003;
        double r712017 = r712006 / r712016;
        double r712018 = r712015 + r712017;
        double r712019 = r712001 ? r712011 : r712018;
        return r712019;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	3.7
Target	1.6
Herbie	1.5

\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]

Derivation

1. Split input into 2 regimes

2. if (* z 3.0) < 2.3901789810025477e-148

   1. Initial program 5.7

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

   3. Applied associate-/r* 1.7

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

   5. Applied div-inv 1.7

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

   if 2.3901789810025477e-148 < (* z 3.0)

   1. Initial program 1.3

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

   3. Applied *-un-lft-identity 1.3

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

   4. Applied times-frac 1.3

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

4. Final simplification 1.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot 3 \le 2.390178981002547728134938616903530718403 \cdot 10^{-148}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot 3} \cdot \frac{1}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \end{array}\]

Reproduce

herbie shell --seed 2019356 
(FPCore (x y z t)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, H"
  :precision binary64

  :herbie-target
  (+ (- x (/ y (* z 3))) (/ (/ t (* z 3)) y))

  (+ (- x (/ y (* z 3))) (/ t (* (* z 3) y))))