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

Average Error: 19.9 → 3.1

Time: 15.3s

Precision: 64

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{b}{z \cdot c} + 9 \cdot \frac{x}{\frac{z \cdot c}{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 -4.04549077726549492755614064921751134038 \cdot 10^{-72}:\\ \;\;\;\;\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 82513253524487903641600:\\ \;\;\;\;\left(\frac{\left(x \cdot 9\right) \cdot y + b}{z} - \left(a \cdot 4\right) \cdot t\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 1.893118102310617680117230001054255080538 \cdot 10^{306}:\\ \;\;\;\;\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{b}{z \cdot c} + 9 \cdot \left(\frac{x}{z} \cdot \frac{y}{c}\right)\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 r496000 = x;
        double r496001 = 9.0;
        double r496002 = r496000 * r496001;
        double r496003 = y;
        double r496004 = r496002 * r496003;
        double r496005 = z;
        double r496006 = 4.0;
        double r496007 = r496005 * r496006;
        double r496008 = t;
        double r496009 = r496007 * r496008;
        double r496010 = a;
        double r496011 = r496009 * r496010;
        double r496012 = r496004 - r496011;
        double r496013 = b;
        double r496014 = r496012 + r496013;
        double r496015 = c;
        double r496016 = r496005 * r496015;
        double r496017 = r496014 / r496016;
        return r496017;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r496018 = x;
        double r496019 = 9.0;
        double r496020 = r496018 * r496019;
        double r496021 = y;
        double r496022 = r496020 * r496021;
        double r496023 = z;
        double r496024 = 4.0;
        double r496025 = r496023 * r496024;
        double r496026 = t;
        double r496027 = r496025 * r496026;
        double r496028 = a;
        double r496029 = r496027 * r496028;
        double r496030 = r496022 - r496029;
        double r496031 = b;
        double r496032 = r496030 + r496031;
        double r496033 = c;
        double r496034 = r496023 * r496033;
        double r496035 = r496032 / r496034;
        double r496036 = -inf.0;
        bool r496037 = r496035 <= r496036;
        double r496038 = r496031 / r496034;
        double r496039 = r496034 / r496021;
        double r496040 = r496018 / r496039;
        double r496041 = r496019 * r496040;
        double r496042 = r496038 + r496041;
        double r496043 = r496028 / r496033;
        double r496044 = r496026 * r496043;
        double r496045 = r496024 * r496044;
        double r496046 = r496042 - r496045;
        double r496047 = -4.045490777265495e-72;
        bool r496048 = r496035 <= r496047;
        double r496049 = 8.25132535244879e+22;
        bool r496050 = r496035 <= r496049;
        double r496051 = r496022 + r496031;
        double r496052 = r496051 / r496023;
        double r496053 = r496028 * r496024;
        double r496054 = r496053 * r496026;
        double r496055 = r496052 - r496054;
        double r496056 = 1.0;
        double r496057 = r496056 / r496033;
        double r496058 = r496055 * r496057;
        double r496059 = 1.8931181023106177e+306;
        bool r496060 = r496035 <= r496059;
        double r496061 = r496018 / r496023;
        double r496062 = r496021 / r496033;
        double r496063 = r496061 * r496062;
        double r496064 = r496019 * r496063;
        double r496065 = r496038 + r496064;
        double r496066 = r496065 - r496045;
        double r496067 = r496060 ? r496035 : r496066;
        double r496068 = r496050 ? r496058 : r496067;
        double r496069 = r496048 ? r496035 : r496068;
        double r496070 = r496037 ? r496046 : r496069;
        return r496070;
}

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	19.9
Target	13.8
Herbie	3.1

\[\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.100156740804104887233830094663413900721 \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.170887791174748819600820354912645756062 \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.876823679546137226963937101710277849382 \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.383851504245631860711731716196098366993 \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 4 regimes

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

   1. Initial program 64.0

      \[\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 25.7

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

   3. Taylor expanded around 0 31.6

      \[\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 31.6

      \[\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 26.9

      \[\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 26.9

      \[\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* 9.7

      \[\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)\]

   if -inf.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -4.045490777265495e-72 or 8.25132535244879e+22 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 1.8931181023106177e+306

   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 -4.045490777265495e-72 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 8.25132535244879e+22

   1. Initial program 14.4

      \[\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.9

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

   4. Applied div-inv 1.0

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

   if 1.8931181023106177e+306 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c))

   1. Initial program 63.6

      \[\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 27.8

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

   3. Taylor expanded around 0 30.3

      \[\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.3

      \[\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.2

      \[\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.2

      \[\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 times-frac 10.5

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

4. Final simplification 3.1

   \[\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{b}{z \cdot c} + 9 \cdot \frac{x}{\frac{z \cdot c}{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 -4.04549077726549492755614064921751134038 \cdot 10^{-72}:\\ \;\;\;\;\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 82513253524487903641600:\\ \;\;\;\;\left(\frac{\left(x \cdot 9\right) \cdot y + b}{z} - \left(a \cdot 4\right) \cdot t\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 1.893118102310617680117230001054255080538 \cdot 10^{306}:\\ \;\;\;\;\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{b}{z \cdot c} + 9 \cdot \left(\frac{x}{z} \cdot \frac{y}{c}\right)\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019208 
(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.1001567408041049e-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.17088779117474882e-53) (/ (+ (- (* (* x 9) y) (* (* z 4) (* t a))) b) (* z c)) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 2.8768236795461372e130) (- (+ (* (* 9 (/ y c)) (/ x z)) (/ b (* c z))) (* 4 (/ (* a t) c))) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 1.3838515042456319e158) (/ (+ (- (* (* 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)))