Average Error: 20.1 → 17.8
Time: 32.6s
Precision: 64
\[\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}\]
↓
\[\begin{array}{l} \mathbf{if}\;\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) \le 1.9705134585429066 \cdot 10^{+143}:\\ \;\;\;\;\left(\cos y \cdot \left(\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) + \sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(2.0 \cdot \sqrt{x}\right) - \frac{a}{3.0 \cdot b}\\ \mathbf{else}:\\ \;\;\;\;\left(2.0 \cdot \sqrt{x}\right) \cdot \left(\frac{-1}{2} \cdot \left(y \cdot y\right) + 1\right) - \frac{a}{3.0 \cdot b}\\ \end{array}\]
\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}
↓
\begin{array}{l}
\mathbf{if}\;\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) \le 1.9705134585429066 \cdot 10^{+143}:\\
\;\;\;\;\left(\cos y \cdot \left(\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) + \sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(2.0 \cdot \sqrt{x}\right) - \frac{a}{3.0 \cdot b}\\

\mathbf{else}:\\
\;\;\;\;\left(2.0 \cdot \sqrt{x}\right) \cdot \left(\frac{-1}{2} \cdot \left(y \cdot y\right) + 1\right) - \frac{a}{3.0 \cdot b}\\

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r34071685 = 2.0;
        double r34071686 = x;
        double r34071687 = sqrt(r34071686);
        double r34071688 = r34071685 * r34071687;
        double r34071689 = y;
        double r34071690 = z;
        double r34071691 = t;
        double r34071692 = r34071690 * r34071691;
        double r34071693 = 3.0;
        double r34071694 = r34071692 / r34071693;
        double r34071695 = r34071689 - r34071694;
        double r34071696 = cos(r34071695);
        double r34071697 = r34071688 * r34071696;
        double r34071698 = a;
        double r34071699 = b;
        double r34071700 = r34071699 * r34071693;
        double r34071701 = r34071698 / r34071700;
        double r34071702 = r34071697 - r34071701;
        return r34071702;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r34071703 = 2.0;
        double r34071704 = x;
        double r34071705 = sqrt(r34071704);
        double r34071706 = r34071703 * r34071705;
        double r34071707 = y;
        double r34071708 = z;
        double r34071709 = t;
        double r34071710 = r34071708 * r34071709;
        double r34071711 = 3.0;
        double r34071712 = r34071710 / r34071711;
        double r34071713 = r34071707 - r34071712;
        double r34071714 = cos(r34071713);
        double r34071715 = r34071706 * r34071714;
        double r34071716 = 1.9705134585429066e+143;
        bool r34071717 = r34071715 <= r34071716;
        double r34071718 = cos(r34071707);
        double r34071719 = cos(r34071712);
        double r34071720 = cbrt(r34071719);
        double r34071721 = r34071720 * r34071720;
        double r34071722 = r34071721 * r34071720;
        double r34071723 = r34071718 * r34071722;
        double r34071724 = sin(r34071707);
        double r34071725 = sin(r34071712);
        double r34071726 = r34071724 * r34071725;
        double r34071727 = r34071723 + r34071726;
        double r34071728 = r34071727 * r34071706;
        double r34071729 = a;
        double r34071730 = b;
        double r34071731 = r34071711 * r34071730;
        double r34071732 = r34071729 / r34071731;
        double r34071733 = r34071728 - r34071732;
        double r34071734 = -0.5;
        double r34071735 = r34071707 * r34071707;
        double r34071736 = r34071734 * r34071735;
        double r34071737 = 1.0;
        double r34071738 = r34071736 + r34071737;
        double r34071739 = r34071706 * r34071738;
        double r34071740 = r34071739 - r34071732;
        double r34071741 = r34071717 ? r34071733 : r34071740;
        return r34071741;
}

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.1
Target18.4
Herbie17.8
\[\begin{array}{l} \mathbf{if}\;z \lt -1.3793337487235141 \cdot 10^{+129}:\\ \;\;\;\;\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.3333333333333333}{z}}{t}\right) - \frac{\frac{a}{3.0}}{b}\\ \mathbf{elif}\;z \lt 3.516290613555987 \cdot 10^{+106}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \cos \left(y - \frac{t}{3.0} \cdot z\right) - \frac{\frac{a}{3.0}}{b}\\ \mathbf{else}:\\ \;\;\;\;\cos \left(y - \frac{\frac{0.3333333333333333}{z}}{t}\right) \cdot \left(2.0 \cdot \sqrt{x}\right) - \frac{\frac{a}{b}}{3.0}\\ \end{array}\]

Derivation

  1. Split input into 2 regimes

  2. if (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) < 1.9705134585429066e+143

    1. Initial program 14.3

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

    3. Applied cos-diff13.8

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

    5. Applied add-cube-cbrt13.8

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

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

    1. Initial program 54.6

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

    2. Taylor expanded around 0 42.2

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

    3. Simplified42.2

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

  4. Final simplification17.8

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

Reproduce

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