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

Average Error: 19.9 → 17.2

Time: 16.5s

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.99999999999984523:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\left(\cos \left(1 \cdot y\right) \cdot \cos \left(\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right) - \sin \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right) \cdot \sin \left(1 \cdot y\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 \cdot z}{{\left(\sqrt{3}\right)}^{2}}\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 r778451 = 2.0;
        double r778452 = x;
        double r778453 = sqrt(r778452);
        double r778454 = r778451 * r778453;
        double r778455 = y;
        double r778456 = z;
        double r778457 = t;
        double r778458 = r778456 * r778457;
        double r778459 = 3.0;
        double r778460 = r778458 / r778459;
        double r778461 = r778455 - r778460;
        double r778462 = cos(r778461);
        double r778463 = r778454 * r778462;
        double r778464 = a;
        double r778465 = b;
        double r778466 = r778465 * r778459;
        double r778467 = r778464 / r778466;
        double r778468 = r778463 - r778467;
        return r778468;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r778469 = y;
        double r778470 = z;
        double r778471 = t;
        double r778472 = r778470 * r778471;
        double r778473 = 3.0;
        double r778474 = r778472 / r778473;
        double r778475 = r778469 - r778474;
        double r778476 = cos(r778475);
        double r778477 = 0.9999999999998452;
        bool r778478 = r778476 <= r778477;
        double r778479 = 2.0;
        double r778480 = x;
        double r778481 = sqrt(r778480);
        double r778482 = r778479 * r778481;
        double r778483 = 1.0;
        double r778484 = r778483 * r778469;
        double r778485 = cos(r778484);
        double r778486 = r778471 * r778470;
        double r778487 = sqrt(r778473);
        double r778488 = 2.0;
        double r778489 = pow(r778487, r778488);
        double r778490 = r778486 / r778489;
        double r778491 = cos(r778490);
        double r778492 = r778485 * r778491;
        double r778493 = -r778490;
        double r778494 = sin(r778493);
        double r778495 = sin(r778484);
        double r778496 = r778494 * r778495;
        double r778497 = r778492 - r778496;
        double r778498 = r778471 / r778487;
        double r778499 = -r778498;
        double r778500 = r778470 / r778487;
        double r778501 = r778498 * r778500;
        double r778502 = fma(r778499, r778500, r778501);
        double r778503 = cos(r778502);
        double r778504 = r778497 * r778503;
        double r778505 = fma(r778483, r778469, r778493);
        double r778506 = sin(r778505);
        double r778507 = sin(r778502);
        double r778508 = r778506 * r778507;
        double r778509 = r778504 - r778508;
        double r778510 = r778482 * r778509;
        double r778511 = a;
        double r778512 = b;
        double r778513 = r778512 * r778473;
        double r778514 = r778511 / r778513;
        double r778515 = r778510 - r778514;
        double r778516 = 0.5;
        double r778517 = pow(r778469, r778488);
        double r778518 = r778516 * r778517;
        double r778519 = r778483 - r778518;
        double r778520 = r778482 * r778519;
        double r778521 = r778520 - r778514;
        double r778522 = r778478 ? r778515 : r778521;
        return r778522;
}

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	19.9
Target	18.1
Herbie	17.2

\[\begin{array}{l} \mathbf{if}\;z \lt -1.379333748723514 \cdot 10^{129}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.333333333333333315}{z}}{t}\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{elif}\;z \lt 3.51629061355598715 \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.333333333333333315}{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.9999999999998452

   1. Initial program 19.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-sqr-sqrt 19.1

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

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

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

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

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

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

      \[\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. Taylor expanded around inf 19.1

       \[\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 \cdot z}{{\left(\sqrt{3}\right)}^{2}}\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}\]
   11. Using strategy rm

   12. Applied fma-udef 19.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos \color{blue}{\left(1 \cdot y + \left(-\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 \cdot z}{{\left(\sqrt{3}\right)}^{2}}\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. Applied cos-sum 18.5

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\color{blue}{\left(\cos \left(1 \cdot y\right) \cdot \cos \left(-\frac{t}{\sqrt{3}} \cdot \frac{z}{\sqrt{3}}\right) - \sin \left(1 \cdot y\right) \cdot \sin \left(-\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 \cdot z}{{\left(\sqrt{3}\right)}^{2}}\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}\]

   14. Simplified 18.5

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\left(\color{blue}{\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}{\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 \cdot z}{{\left(\sqrt{3}\right)}^{2}}\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. Simplified 18.5

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\left(\cos \left(1 \cdot y\right) \cdot \cos \left(\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right) - \color{blue}{\sin \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right) \cdot \sin \left(1 \cdot y\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 \cdot z}{{\left(\sqrt{3}\right)}^{2}}\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.9999999999998452 < (cos (- y (/ (* z t) 3.0)))

   1. Initial program 21.3

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

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

   \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.99999999999984523:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\left(\cos \left(1 \cdot y\right) \cdot \cos \left(\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right) - \sin \left(-\frac{t \cdot z}{{\left(\sqrt{3}\right)}^{2}}\right) \cdot \sin \left(1 \cdot y\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 \cdot z}{{\left(\sqrt{3}\right)}^{2}}\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 2020083 +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))))