Average Error: 20.5 → 17.9
Time: 26.3s
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}\;y - \frac{z \cdot t}{3} = -\infty \lor \neg \left(y - \frac{z \cdot t}{3} \le 3.516666701465602032849647204560993340237 \cdot 10^{304}\right):\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos \left(\frac{t}{\frac{3}{z}}\right) \cdot \cos y - \sin \left(-\frac{t \cdot z}{3}\right) \cdot \sin y\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}\;y - \frac{z \cdot t}{3} = -\infty \lor \neg \left(y - \frac{z \cdot t}{3} \le 3.516666701465602032849647204560993340237 \cdot 10^{304}\right):\\
\;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\

\mathbf{else}:\\
\;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos \left(\frac{t}{\frac{3}{z}}\right) \cdot \cos y - \sin \left(-\frac{t \cdot z}{3}\right) \cdot \sin y\right) - \frac{a}{b \cdot 3}\\

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r465762 = 2.0;
        double r465763 = x;
        double r465764 = sqrt(r465763);
        double r465765 = r465762 * r465764;
        double r465766 = y;
        double r465767 = z;
        double r465768 = t;
        double r465769 = r465767 * r465768;
        double r465770 = 3.0;
        double r465771 = r465769 / r465770;
        double r465772 = r465766 - r465771;
        double r465773 = cos(r465772);
        double r465774 = r465765 * r465773;
        double r465775 = a;
        double r465776 = b;
        double r465777 = r465776 * r465770;
        double r465778 = r465775 / r465777;
        double r465779 = r465774 - r465778;
        return r465779;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r465780 = y;
        double r465781 = z;
        double r465782 = t;
        double r465783 = r465781 * r465782;
        double r465784 = 3.0;
        double r465785 = r465783 / r465784;
        double r465786 = r465780 - r465785;
        double r465787 = -inf.0;
        bool r465788 = r465786 <= r465787;
        double r465789 = 3.516666701465602e+304;
        bool r465790 = r465786 <= r465789;
        double r465791 = !r465790;
        bool r465792 = r465788 || r465791;
        double r465793 = 2.0;
        double r465794 = x;
        double r465795 = sqrt(r465794);
        double r465796 = r465793 * r465795;
        double r465797 = 1.0;
        double r465798 = 0.5;
        double r465799 = 2.0;
        double r465800 = pow(r465780, r465799);
        double r465801 = r465798 * r465800;
        double r465802 = r465797 - r465801;
        double r465803 = r465796 * r465802;
        double r465804 = a;
        double r465805 = b;
        double r465806 = r465805 * r465784;
        double r465807 = r465804 / r465806;
        double r465808 = r465803 - r465807;
        double r465809 = r465784 / r465781;
        double r465810 = r465782 / r465809;
        double r465811 = cos(r465810);
        double r465812 = cos(r465780);
        double r465813 = r465811 * r465812;
        double r465814 = r465782 * r465781;
        double r465815 = r465814 / r465784;
        double r465816 = -r465815;
        double r465817 = sin(r465816);
        double r465818 = sin(r465780);
        double r465819 = r465817 * r465818;
        double r465820 = r465813 - r465819;
        double r465821 = r465796 * r465820;
        double r465822 = r465821 - r465807;
        double r465823 = r465792 ? r465808 : r465822;
        return r465823;
}

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.5
Target18.6
Herbie17.9
\[\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 (- y (/ (* z t) 3.0)) < -inf.0 or 3.516666701465602e+304 < (- y (/ (* z t) 3.0))

    1. Initial program 62.6

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

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

    if -inf.0 < (- y (/ (* z t) 3.0)) < 3.516666701465602e+304

    1. Initial program 14.2

      \[\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-sqrt14.2

      \[\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-frac14.2

      \[\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. Using strategy rm

    6. Applied sub-neg14.2

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

    7. Applied cos-sum13.8

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

    8. Simplified13.7

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

    9. Simplified13.8

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

  4. Final simplification17.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;y - \frac{z \cdot t}{3} = -\infty \lor \neg \left(y - \frac{z \cdot t}{3} \le 3.516666701465602032849647204560993340237 \cdot 10^{304}\right):\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos \left(\frac{t}{\frac{3}{z}}\right) \cdot \cos y - \sin \left(-\frac{t \cdot z}{3}\right) \cdot \sin y\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

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