Average Error: 20.0 → 17.6
Time: 14.8s
Precision: 64
\[\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) \le 1.95709970069839588 \cdot 10^{140}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \frac{\sqrt[3]{z \cdot t}}{\sqrt[3]{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) - \sin y \cdot \sin \left(-0.333333333333333315 \cdot \left(t \cdot z\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}\]
\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) \le 1.95709970069839588 \cdot 10^{140}:\\
\;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \frac{\sqrt[3]{z \cdot t}}{\sqrt[3]{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) - \sin y \cdot \sin \left(-0.333333333333333315 \cdot \left(t \cdot z\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}
double f(double x, double y, double z, double t, double a, double b) {
        double r719609 = 2.0;
        double r719610 = x;
        double r719611 = sqrt(r719610);
        double r719612 = r719609 * r719611;
        double r719613 = y;
        double r719614 = z;
        double r719615 = t;
        double r719616 = r719614 * r719615;
        double r719617 = 3.0;
        double r719618 = r719616 / r719617;
        double r719619 = r719613 - r719618;
        double r719620 = cos(r719619);
        double r719621 = r719612 * r719620;
        double r719622 = a;
        double r719623 = b;
        double r719624 = r719623 * r719617;
        double r719625 = r719622 / r719624;
        double r719626 = r719621 - r719625;
        return r719626;
}

double f(double x, double y, double z, double t, double a, double b) {
        double r719627 = 2.0;
        double r719628 = x;
        double r719629 = sqrt(r719628);
        double r719630 = r719627 * r719629;
        double r719631 = y;
        double r719632 = z;
        double r719633 = t;
        double r719634 = r719632 * r719633;
        double r719635 = 3.0;
        double r719636 = r719634 / r719635;
        double r719637 = r719631 - r719636;
        double r719638 = cos(r719637);
        double r719639 = r719630 * r719638;
        double r719640 = 1.957099700698396e+140;
        bool r719641 = r719639 <= r719640;
        double r719642 = cos(r719631);
        double r719643 = cbrt(r719636);
        double r719644 = cbrt(r719634);
        double r719645 = cbrt(r719635);
        double r719646 = r719644 / r719645;
        double r719647 = r719643 * r719646;
        double r719648 = r719647 * r719643;
        double r719649 = cos(r719648);
        double r719650 = r719642 * r719649;
        double r719651 = sin(r719631);
        double r719652 = 0.3333333333333333;
        double r719653 = r719633 * r719632;
        double r719654 = r719652 * r719653;
        double r719655 = -r719654;
        double r719656 = sin(r719655);
        double r719657 = r719651 * r719656;
        double r719658 = r719650 - r719657;
        double r719659 = r719630 * r719658;
        double r719660 = a;
        double r719661 = b;
        double r719662 = r719661 * r719635;
        double r719663 = r719660 / r719662;
        double r719664 = r719659 - r719663;
        double r719665 = 1.0;
        double r719666 = 0.5;
        double r719667 = 2.0;
        double r719668 = pow(r719631, r719667);
        double r719669 = r719666 * r719668;
        double r719670 = r719665 - r719669;
        double r719671 = r719630 * r719670;
        double r719672 = r719671 - r719663;
        double r719673 = r719641 ? r719664 : r719672;
        return r719673;
}

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

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original20.0
Target18.0
Herbie17.6
\[\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 (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) < 1.957099700698396e+140

    1. Initial program 13.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 sub-neg13.9

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

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

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

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

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \color{blue}{\frac{\sqrt[3]{z \cdot t}}{\sqrt[3]{3}}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) - \sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) - \frac{a}{b \cdot 3}\]
    10. Taylor expanded around inf 13.5

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

    if 1.957099700698396e+140 < (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0))))

    1. Initial program 56.2

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

      \[\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 simplification17.6

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