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

Average Error: 20.8 → 3.3

Time: 10.2s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} = -\infty:\\ \;\;\;\;\left(\frac{1}{z} \cdot \frac{b}{c} + 9 \cdot \frac{x}{c \cdot \frac{z}{y}}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -3.86575567753969965 \cdot 10^{-184}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -0.0:\\ \;\;\;\;\left(\frac{b + \left(x \cdot 9\right) \cdot y}{z} - a \cdot \left(4 \cdot t\right)\right) \cdot \frac{1}{c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le 2.5630952637815053 \cdot 10^{303}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{1}{z} \cdot \frac{b}{c} + 9 \cdot \frac{x}{c \cdot \frac{z}{y}}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r1035087 = x;
        double r1035088 = 9.0;
        double r1035089 = r1035087 * r1035088;
        double r1035090 = y;
        double r1035091 = r1035089 * r1035090;
        double r1035092 = z;
        double r1035093 = 4.0;
        double r1035094 = r1035092 * r1035093;
        double r1035095 = t;
        double r1035096 = r1035094 * r1035095;
        double r1035097 = a;
        double r1035098 = r1035096 * r1035097;
        double r1035099 = r1035091 - r1035098;
        double r1035100 = b;
        double r1035101 = r1035099 + r1035100;
        double r1035102 = c;
        double r1035103 = r1035092 * r1035102;
        double r1035104 = r1035101 / r1035103;
        return r1035104;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r1035105 = x;
        double r1035106 = 9.0;
        double r1035107 = r1035105 * r1035106;
        double r1035108 = y;
        double r1035109 = r1035107 * r1035108;
        double r1035110 = z;
        double r1035111 = 4.0;
        double r1035112 = r1035110 * r1035111;
        double r1035113 = t;
        double r1035114 = r1035112 * r1035113;
        double r1035115 = a;
        double r1035116 = r1035114 * r1035115;
        double r1035117 = r1035109 - r1035116;
        double r1035118 = b;
        double r1035119 = r1035117 + r1035118;
        double r1035120 = c;
        double r1035121 = r1035110 * r1035120;
        double r1035122 = r1035119 / r1035121;
        double r1035123 = -inf.0;
        bool r1035124 = r1035122 <= r1035123;
        double r1035125 = 1.0;
        double r1035126 = r1035125 / r1035110;
        double r1035127 = r1035118 / r1035120;
        double r1035128 = r1035126 * r1035127;
        double r1035129 = r1035110 / r1035108;
        double r1035130 = r1035120 * r1035129;
        double r1035131 = r1035105 / r1035130;
        double r1035132 = r1035106 * r1035131;
        double r1035133 = r1035128 + r1035132;
        double r1035134 = r1035115 / r1035120;
        double r1035135 = r1035113 * r1035134;
        double r1035136 = r1035111 * r1035135;
        double r1035137 = r1035133 - r1035136;
        double r1035138 = -3.8657556775396997e-184;
        bool r1035139 = r1035122 <= r1035138;
        double r1035140 = -0.0;
        bool r1035141 = r1035122 <= r1035140;
        double r1035142 = r1035118 + r1035109;
        double r1035143 = r1035142 / r1035110;
        double r1035144 = r1035111 * r1035113;
        double r1035145 = r1035115 * r1035144;
        double r1035146 = r1035143 - r1035145;
        double r1035147 = r1035125 / r1035120;
        double r1035148 = r1035146 * r1035147;
        double r1035149 = 2.5630952637815053e+303;
        bool r1035150 = r1035122 <= r1035149;
        double r1035151 = r1035150 ? r1035122 : r1035137;
        double r1035152 = r1035141 ? r1035148 : r1035151;
        double r1035153 = r1035139 ? r1035122 : r1035152;
        double r1035154 = r1035124 ? r1035137 : r1035153;
        return r1035154;
}

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

Bits error versus c

Target

Original	20.8
Target	14.9
Herbie	3.3

\[\begin{array}{l} \mathbf{if}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt -1.10015674080410512 \cdot 10^{-171}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(z \cdot 4\right) \cdot \left(t \cdot a\right)\right) + b}{z \cdot c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt -0.0:\\ \;\;\;\;\frac{\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z}}{c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt 1.17088779117474882 \cdot 10^{-53}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(z \cdot 4\right) \cdot \left(t \cdot a\right)\right) + b}{z \cdot c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt 2.8768236795461372 \cdot 10^{130}:\\ \;\;\;\;\left(\left(9 \cdot \frac{y}{c}\right) \cdot \frac{x}{z} + \frac{b}{c \cdot z}\right) - 4 \cdot \frac{a \cdot t}{c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt 1.3838515042456319 \cdot 10^{158}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(z \cdot 4\right) \cdot \left(t \cdot a\right)\right) + b}{z \cdot c}\\ \mathbf{else}:\\ \;\;\;\;\left(9 \cdot \left(\frac{y}{c \cdot z} \cdot x\right) + \frac{b}{c \cdot z}\right) - 4 \cdot \frac{a \cdot t}{c}\\ \end{array}\]

Derivation

1. Split input into 3 regimes

2. if (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -inf.0 or 2.5630952637815053e+303 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c))

   1. Initial program 63.1

      \[\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\]

   2. Simplified 26.8

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

   3. Taylor expanded around 0 30.7

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

   5. Applied *-un-lft-identity 30.7

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

   6. Applied times-frac 25.6

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

   7. Simplified 25.6

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

   9. Applied associate-/l* 14.3

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

   10. Simplified 11.1

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

   12. Applied *-un-lft-identity 11.1

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

   13. Applied times-frac 10.6

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

   if -inf.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -3.8657556775396997e-184 or -0.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 2.5630952637815053e+303

   1. Initial program 0.7

      \[\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\]

   if -3.8657556775396997e-184 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -0.0

   1. Initial program 33.9

      \[\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\]

   2. Simplified 0.6

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

   4. Applied div-inv 0.6

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

4. Final simplification 3.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} = -\infty:\\ \;\;\;\;\left(\frac{1}{z} \cdot \frac{b}{c} + 9 \cdot \frac{x}{c \cdot \frac{z}{y}}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -3.86575567753969965 \cdot 10^{-184}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -0.0:\\ \;\;\;\;\left(\frac{b + \left(x \cdot 9\right) \cdot y}{z} - a \cdot \left(4 \cdot t\right)\right) \cdot \frac{1}{c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le 2.5630952637815053 \cdot 10^{303}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{1}{z} \cdot \frac{b}{c} + 9 \cdot \frac{x}{c \cdot \frac{z}{y}}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020047 
(FPCore (x y z t a b c)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, J"
  :precision binary64

  :herbie-target
  (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) -1.1001567408041051e-171) (/ (+ (- (* (* x 9) y) (* (* z 4) (* t a))) b) (* z c)) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) -0.0) (/ (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) z) c) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 1.1708877911747488e-53) (/ (+ (- (* (* x 9) y) (* (* z 4) (* t a))) b) (* z c)) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 2.876823679546137e+130) (- (+ (* (* 9 (/ y c)) (/ x z)) (/ b (* c z))) (* 4 (/ (* a t) c))) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 1.3838515042456319e+158) (/ (+ (- (* (* x 9) y) (* (* z 4) (* t a))) b) (* z c)) (- (+ (* 9 (* (/ y (* c z)) x)) (/ b (* c z))) (* 4 (/ (* a t) c))))))))

  (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)))