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

Average Error: 20.7 → 18.3

Time: 26.0s

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.999999999603707223627679923083633184433:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z}{\sqrt[3]{3} \cdot \sqrt[3]{3}} \cdot \frac{t}{\sqrt[3]{3}}\right) - \frac{a}{b} \cdot \frac{1}{3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - a \cdot \frac{\frac{1}{b}}{3}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r443381 = 2.0;
        double r443382 = x;
        double r443383 = sqrt(r443382);
        double r443384 = r443381 * r443383;
        double r443385 = y;
        double r443386 = z;
        double r443387 = t;
        double r443388 = r443386 * r443387;
        double r443389 = 3.0;
        double r443390 = r443388 / r443389;
        double r443391 = r443385 - r443390;
        double r443392 = cos(r443391);
        double r443393 = r443384 * r443392;
        double r443394 = a;
        double r443395 = b;
        double r443396 = r443395 * r443389;
        double r443397 = r443394 / r443396;
        double r443398 = r443393 - r443397;
        return r443398;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r443399 = y;
        double r443400 = z;
        double r443401 = t;
        double r443402 = r443400 * r443401;
        double r443403 = 3.0;
        double r443404 = r443402 / r443403;
        double r443405 = r443399 - r443404;
        double r443406 = cos(r443405);
        double r443407 = 0.9999999996037072;
        bool r443408 = r443406 <= r443407;
        double r443409 = 2.0;
        double r443410 = x;
        double r443411 = sqrt(r443410);
        double r443412 = r443409 * r443411;
        double r443413 = cbrt(r443403);
        double r443414 = r443413 * r443413;
        double r443415 = r443400 / r443414;
        double r443416 = r443401 / r443413;
        double r443417 = r443415 * r443416;
        double r443418 = r443399 - r443417;
        double r443419 = cos(r443418);
        double r443420 = r443412 * r443419;
        double r443421 = a;
        double r443422 = b;
        double r443423 = r443421 / r443422;
        double r443424 = 1.0;
        double r443425 = r443424 / r443403;
        double r443426 = r443423 * r443425;
        double r443427 = r443420 - r443426;
        double r443428 = 0.5;
        double r443429 = 2.0;
        double r443430 = pow(r443399, r443429);
        double r443431 = r443428 * r443430;
        double r443432 = r443424 - r443431;
        double r443433 = r443412 * r443432;
        double r443434 = r443424 / r443422;
        double r443435 = r443434 / r443403;
        double r443436 = r443421 * r443435;
        double r443437 = r443433 - r443436;
        double r443438 = r443408 ? r443427 : r443437;
        return r443438;
}

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	20.7
Target	18.6
Herbie	18.3

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

   1. Initial program 19.9

      \[\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-cube-cbrt 19.9

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

   4. Applied times-frac 19.8

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

   6. Applied associate-/r* 19.9

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

   8. Applied div-inv 19.9

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

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

   1. Initial program 22.1

      \[\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-cube-cbrt 22.1

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

   4. Applied times-frac 22.1

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

   6. Applied associate-/r* 22.1

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

   8. Applied *-un-lft-identity 22.1

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

   9. Applied div-inv 22.1

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

   10. Applied times-frac 22.1

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

   11. Simplified 22.1

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

   12. Taylor expanded around 0 15.6

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

4. Final simplification 18.3

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

Reproduce

herbie shell --seed 2019322 
(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))))