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

Average Error: 21.0 → 19.3

Time: 27.1s

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}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3} \le 3.794174100982634508380029350357139440003 \cdot 10^{186}:\\ \;\;\;\;\left(2 \cdot \left(\sqrt{x} \cdot \left(\log \left(e^{\cos \left(z \cdot \left(t \cdot 0.3333333333333333148296162562473909929395\right)\right)}\right) \cdot \cos y\right)\right) + \left(\sqrt[3]{\sin y \cdot \left(\left(\sin \left(z \cdot \frac{t}{3}\right) \cdot 2\right) \cdot \sqrt{x}\right)} \cdot \sqrt[3]{\sin y \cdot \left(\left(\sin \left(z \cdot \frac{t}{3}\right) \cdot 2\right) \cdot \sqrt{x}\right)}\right) \cdot \sqrt[3]{\sin y \cdot \left(\left(\sin \left(z \cdot \frac{t}{3}\right) \cdot 2\right) \cdot \sqrt{x}\right)}\right) - \frac{\frac{a}{b}}{3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - y \cdot \left(y \cdot \frac{1}{2}\right)\right) - \frac{\frac{a}{b}}{3}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r498590 = 2.0;
        double r498591 = x;
        double r498592 = sqrt(r498591);
        double r498593 = r498590 * r498592;
        double r498594 = y;
        double r498595 = z;
        double r498596 = t;
        double r498597 = r498595 * r498596;
        double r498598 = 3.0;
        double r498599 = r498597 / r498598;
        double r498600 = r498594 - r498599;
        double r498601 = cos(r498600);
        double r498602 = r498593 * r498601;
        double r498603 = a;
        double r498604 = b;
        double r498605 = r498604 * r498598;
        double r498606 = r498603 / r498605;
        double r498607 = r498602 - r498606;
        return r498607;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r498608 = 2.0;
        double r498609 = x;
        double r498610 = sqrt(r498609);
        double r498611 = r498608 * r498610;
        double r498612 = y;
        double r498613 = z;
        double r498614 = t;
        double r498615 = r498613 * r498614;
        double r498616 = 3.0;
        double r498617 = r498615 / r498616;
        double r498618 = r498612 - r498617;
        double r498619 = cos(r498618);
        double r498620 = r498611 * r498619;
        double r498621 = a;
        double r498622 = b;
        double r498623 = r498622 * r498616;
        double r498624 = r498621 / r498623;
        double r498625 = r498620 - r498624;
        double r498626 = 3.7941741009826345e+186;
        bool r498627 = r498625 <= r498626;
        double r498628 = 0.3333333333333333;
        double r498629 = r498614 * r498628;
        double r498630 = r498613 * r498629;
        double r498631 = cos(r498630);
        double r498632 = exp(r498631);
        double r498633 = log(r498632);
        double r498634 = cos(r498612);
        double r498635 = r498633 * r498634;
        double r498636 = r498610 * r498635;
        double r498637 = r498608 * r498636;
        double r498638 = sin(r498612);
        double r498639 = r498614 / r498616;
        double r498640 = r498613 * r498639;
        double r498641 = sin(r498640);
        double r498642 = r498641 * r498608;
        double r498643 = r498642 * r498610;
        double r498644 = r498638 * r498643;
        double r498645 = cbrt(r498644);
        double r498646 = r498645 * r498645;
        double r498647 = r498646 * r498645;
        double r498648 = r498637 + r498647;
        double r498649 = r498621 / r498622;
        double r498650 = r498649 / r498616;
        double r498651 = r498648 - r498650;
        double r498652 = 1.0;
        double r498653 = 0.5;
        double r498654 = r498612 * r498653;
        double r498655 = r498612 * r498654;
        double r498656 = r498652 - r498655;
        double r498657 = r498611 * r498656;
        double r498658 = r498657 - r498650;
        double r498659 = r498627 ? r498651 : r498658;
        return r498659;
}

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.0
Target	18.9
Herbie	19.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 (- (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) (/ a (* b 3.0))) < 3.7941741009826345e+186

   1. Initial program 15.8

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

   2. Simplified 15.8

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

   4. Applied cos-diff 15.3

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

   5. Applied distribute-lft-in 15.3

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

   6. Simplified 15.3

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

   7. Simplified 15.3

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

   8. Taylor expanded around inf 15.3

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

   9. Simplified 15.2

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

   11. Applied add-log-exp 15.2

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

   12. Simplified 15.2

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

   14. Applied add-cube-cbrt 15.2

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

   15. Simplified 15.2

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

   16. Simplified 15.2

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

   if 3.7941741009826345e+186 < (- (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) (/ a (* b 3.0)))

   1. Initial program 45.4

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

   2. Simplified 45.4

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

   3. Taylor expanded around 0 38.0

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

   4. Simplified 38.0

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

4. Final simplification 19.3

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

Reproduce

herbie shell --seed 2019179 
(FPCore (x y z t a b)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, K"

  :herbie-target
  (if (< z -1.3793337487235141e+129) (- (* (* 2.0 (sqrt x)) (cos (- (/ 1.0 y) (/ (/ 0.3333333333333333 z) t)))) (/ (/ a 3.0) b)) (if (< z 3.516290613555987e+106) (- (* (* (sqrt x) 2.0) (cos (- y (* (/ t 3.0) z)))) (/ (/ a 3.0) b)) (- (* (cos (- y (/ (/ 0.3333333333333333 z) t))) (* 2.0 (sqrt x))) (/ (/ a b) 3.0))))

  (- (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) (/ a (* b 3.0))))