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

Average Error: 21.1 → 18.4

Time: 15.6s

Precision: 64

Math

\[\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3}\]

↓

\[\begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.9999999999999932276395497865451034158468:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\sqrt[3]{{\left(\log \left(e^{\cos \left(\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)}\right) \cdot \cos \left(1 \cdot y\right) - \sin \left(1 \cdot y\right) \cdot \sin \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)\right)}^{3}} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r714295 = 2.0;
        double r714296 = x;
        double r714297 = sqrt(r714296);
        double r714298 = r714295 * r714297;
        double r714299 = y;
        double r714300 = z;
        double r714301 = t;
        double r714302 = r714300 * r714301;
        double r714303 = 3.0;
        double r714304 = r714302 / r714303;
        double r714305 = r714299 - r714304;
        double r714306 = cos(r714305);
        double r714307 = r714298 * r714306;
        double r714308 = a;
        double r714309 = b;
        double r714310 = r714309 * r714303;
        double r714311 = r714308 / r714310;
        double r714312 = r714307 - r714311;
        return r714312;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r714313 = y;
        double r714314 = z;
        double r714315 = t;
        double r714316 = r714314 * r714315;
        double r714317 = 3.0;
        double r714318 = r714316 / r714317;
        double r714319 = r714313 - r714318;
        double r714320 = cos(r714319);
        double r714321 = 0.9999999999999932;
        bool r714322 = r714320 <= r714321;
        double r714323 = 2.0;
        double r714324 = x;
        double r714325 = sqrt(r714324);
        double r714326 = r714323 * r714325;
        double r714327 = r714315 * r714314;
        double r714328 = sqrt(r714317);
        double r714329 = 2.0;
        double r714330 = pow(r714328, r714329);
        double r714331 = r714327 / r714330;
        double r714332 = cos(r714331);
        double r714333 = exp(r714332);
        double r714334 = log(r714333);
        double r714335 = 1.0;
        double r714336 = r714335 * r714313;
        double r714337 = cos(r714336);
        double r714338 = r714334 * r714337;
        double r714339 = sin(r714336);
        double r714340 = -r714331;
        double r714341 = sin(r714340);
        double r714342 = r714339 * r714341;
        double r714343 = r714338 - r714342;
        double r714344 = 3.0;
        double r714345 = pow(r714343, r714344);
        double r714346 = cbrt(r714345);
        double r714347 = r714315 / r714328;
        double r714348 = -r714347;
        double r714349 = r714314 / r714328;
        double r714350 = r714347 * r714349;
        double r714351 = fma(r714348, r714349, r714350);
        double r714352 = cos(r714351);
        double r714353 = r714346 * r714352;
        double r714354 = -r714350;
        double r714355 = fma(r714335, r714313, r714354);
        double r714356 = sin(r714355);
        double r714357 = sin(r714351);
        double r714358 = r714356 * r714357;
        double r714359 = r714353 - r714358;
        double r714360 = r714326 * r714359;
        double r714361 = a;
        double r714362 = b;
        double r714363 = r714362 * r714317;
        double r714364 = r714361 / r714363;
        double r714365 = r714360 - r714364;
        double r714366 = 0.5;
        double r714367 = pow(r714313, r714329);
        double r714368 = r714366 * r714367;
        double r714369 = r714335 - r714368;
        double r714370 = r714326 * r714369;
        double r714371 = r714370 - r714364;
        double r714372 = r714322 ? r714365 : r714371;
        return r714372;
}

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

Target

Original	21.1
Target	19.1
Herbie	18.4

\[\begin{array}{l} \mathbf{if}\;z \lt -1.379333748723514136852843173740882251575 \cdot 10^{129}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.3333333333333333148296162562473909929395}{z}}{t}\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{elif}\;z \lt 3.516290613555987147199887107423758623887 \cdot 10^{106}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2\right) \cdot \cos \left(y - \frac{t}{3} \cdot z\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{else}:\\ \;\;\;\;\cos \left(y - \frac{\frac{0.3333333333333333148296162562473909929395}{z}}{t}\right) \cdot \left(2 \cdot \sqrt{x}\right) - \frac{\frac{a}{b}}{3}\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if (cos (- y (/ (* z t) 3.0))) < 0.9999999999999932

   1. Initial program 20.3

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

   3. Applied add-sqr-sqrt 20.5

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{\color{blue}{\sqrt{3} \cdot \sqrt{3}}}\right) - \frac{a}{b \cdot 3}\]

   4. Applied times-frac 20.4

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \color{blue}{\frac{z}{\sqrt{3}} \cdot \frac{t}{\sqrt{3}}}\right) - \frac{a}{b \cdot 3}\]

   5. Applied add-sqr-sqrt 45.3

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \cos \left(\color{blue}{\sqrt{y} \cdot \sqrt{y}} - \frac{z}{\sqrt{3}} \cdot \frac{t}{\sqrt{3}}\right) - \frac{a}{b \cdot 3}\]

   6. Applied prod-diff 45.3

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \cos \color{blue}{\left(\mathsf{fma}\left(\sqrt{y}, \sqrt{y}, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right) + \mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)} - \frac{a}{b \cdot 3}\]

   7. Applied cos-sum 45.2

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(\cos \left(\mathsf{fma}\left(\sqrt{y}, \sqrt{y}, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(\sqrt{y}, \sqrt{y}, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right)} - \frac{a}{b \cdot 3}\]

   8. Simplified 42.0

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\color{blue}{\cos \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)} - \sin \left(\mathsf{fma}\left(\sqrt{y}, \sqrt{y}, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\]

   9. Simplified 20.3

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \color{blue}{\sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)}\right) - \frac{a}{b \cdot 3}\]
   10. Using strategy rm

   11. Applied add-cbrt-cube 20.4

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\color{blue}{\sqrt[3]{\left(\cos \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \cos \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) \cdot \cos \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)}} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\]

   12. Simplified 20.4

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\sqrt[3]{\color{blue}{{\left(\cos \left(\mathsf{fma}\left(1, y, -\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)\right)\right)}^{3}}} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\]
   13. Using strategy rm

   14. Applied fma-udef 20.4

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\sqrt[3]{{\left(\cos \color{blue}{\left(1 \cdot y + \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)\right)}\right)}^{3}} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\]

   15. Applied cos-sum 19.8

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\sqrt[3]{{\color{blue}{\left(\cos \left(1 \cdot y\right) \cdot \cos \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right) - \sin \left(1 \cdot y\right) \cdot \sin \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)\right)}}^{3}} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\]

   16. Simplified 19.8

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\sqrt[3]{{\left(\color{blue}{\cos \left(\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right) \cdot \cos \left(1 \cdot y\right)} - \sin \left(1 \cdot y\right) \cdot \sin \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)\right)}^{3}} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\]
   17. Using strategy rm

   18. Applied add-log-exp 19.8

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\sqrt[3]{{\left(\color{blue}{\log \left(e^{\cos \left(\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)}\right)} \cdot \cos \left(1 \cdot y\right) - \sin \left(1 \cdot y\right) \cdot \sin \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)\right)}^{3}} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\]

   if 0.9999999999999932 < (cos (- y (/ (* z t) 3.0)))

   1. Initial program 22.5

      \[\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3}\]

   2. Taylor expanded around 0 15.8

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

4. Final simplification 18.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.9999999999999932276395497865451034158468:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\sqrt[3]{{\left(\log \left(e^{\cos \left(\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)}\right) \cdot \cos \left(1 \cdot y\right) - \sin \left(1 \cdot y\right) \cdot \sin \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right)\right)}^{3}} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{\sqrt{3}}, \frac{z}{\sqrt{3}}, \frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right)\right)\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

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

  :herbie-target
  (if (< z -1.379333748723514e+129) (- (* (* 2 (sqrt x)) (cos (- (/ 1 y) (/ (/ 0.3333333333333333 z) t)))) (/ (/ a 3) b)) (if (< z 3.516290613555987e+106) (- (* (* (sqrt x) 2) (cos (- y (* (/ t 3) z)))) (/ (/ a 3) b)) (- (* (cos (- y (/ (/ 0.3333333333333333 z) t))) (* 2 (sqrt x))) (/ (/ a b) 3))))

  (- (* (* 2 (sqrt x)) (cos (- y (/ (* z t) 3)))) (/ a (* b 3))))