Average Error: 21.0 → 18.5
Time: 36.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}\;\cos \left(y - \frac{t \cdot z}{3}\right) \le 0.9997514971944132522452264311141334474087:\\ \;\;\;\;\left(\cos y \cdot \cos \left(\frac{\frac{t \cdot z}{\sqrt{3}}}{\sqrt{3}}\right) + \sin y \cdot \sin \left(\left(\sqrt[3]{\frac{\frac{t \cdot z}{\sqrt{3}}}{\sqrt{3}}} \cdot \frac{\sqrt[3]{\frac{t \cdot z}{\sqrt{3}}}}{\sqrt[3]{\sqrt{3}}}\right) \cdot \sqrt[3]{\frac{\frac{t \cdot z}{\sqrt{3}}}{\sqrt{3}}}\right)\right) \cdot \left(\sqrt{x} \cdot 2\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(1 - \frac{1}{2} \cdot \left(y \cdot y\right)\right) \cdot \left(\sqrt{x} \cdot 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}\;\cos \left(y - \frac{t \cdot z}{3}\right) \le 0.9997514971944132522452264311141334474087:\\
\;\;\;\;\left(\cos y \cdot \cos \left(\frac{\frac{t \cdot z}{\sqrt{3}}}{\sqrt{3}}\right) + \sin y \cdot \sin \left(\left(\sqrt[3]{\frac{\frac{t \cdot z}{\sqrt{3}}}{\sqrt{3}}} \cdot \frac{\sqrt[3]{\frac{t \cdot z}{\sqrt{3}}}}{\sqrt[3]{\sqrt{3}}}\right) \cdot \sqrt[3]{\frac{\frac{t \cdot z}{\sqrt{3}}}{\sqrt{3}}}\right)\right) \cdot \left(\sqrt{x} \cdot 2\right) - \frac{a}{b \cdot 3}\\

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

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r37352850 = 2.0;
        double r37352851 = x;
        double r37352852 = sqrt(r37352851);
        double r37352853 = r37352850 * r37352852;
        double r37352854 = y;
        double r37352855 = z;
        double r37352856 = t;
        double r37352857 = r37352855 * r37352856;
        double r37352858 = 3.0;
        double r37352859 = r37352857 / r37352858;
        double r37352860 = r37352854 - r37352859;
        double r37352861 = cos(r37352860);
        double r37352862 = r37352853 * r37352861;
        double r37352863 = a;
        double r37352864 = b;
        double r37352865 = r37352864 * r37352858;
        double r37352866 = r37352863 / r37352865;
        double r37352867 = r37352862 - r37352866;
        return r37352867;
}

double f(double x, double y, double z, double t, double a, double b) {
        double r37352868 = y;
        double r37352869 = t;
        double r37352870 = z;
        double r37352871 = r37352869 * r37352870;
        double r37352872 = 3.0;
        double r37352873 = r37352871 / r37352872;
        double r37352874 = r37352868 - r37352873;
        double r37352875 = cos(r37352874);
        double r37352876 = 0.9997514971944133;
        bool r37352877 = r37352875 <= r37352876;
        double r37352878 = cos(r37352868);
        double r37352879 = sqrt(r37352872);
        double r37352880 = r37352871 / r37352879;
        double r37352881 = r37352880 / r37352879;
        double r37352882 = cos(r37352881);
        double r37352883 = r37352878 * r37352882;
        double r37352884 = sin(r37352868);
        double r37352885 = cbrt(r37352881);
        double r37352886 = cbrt(r37352880);
        double r37352887 = cbrt(r37352879);
        double r37352888 = r37352886 / r37352887;
        double r37352889 = r37352885 * r37352888;
        double r37352890 = r37352889 * r37352885;
        double r37352891 = sin(r37352890);
        double r37352892 = r37352884 * r37352891;
        double r37352893 = r37352883 + r37352892;
        double r37352894 = x;
        double r37352895 = sqrt(r37352894);
        double r37352896 = 2.0;
        double r37352897 = r37352895 * r37352896;
        double r37352898 = r37352893 * r37352897;
        double r37352899 = a;
        double r37352900 = b;
        double r37352901 = r37352900 * r37352872;
        double r37352902 = r37352899 / r37352901;
        double r37352903 = r37352898 - r37352902;
        double r37352904 = 1.0;
        double r37352905 = 0.5;
        double r37352906 = r37352868 * r37352868;
        double r37352907 = r37352905 * r37352906;
        double r37352908 = r37352904 - r37352907;
        double r37352909 = r37352908 * r37352897;
        double r37352910 = r37352909 - r37352902;
        double r37352911 = r37352877 ? r37352903 : r37352910;
        return r37352911;
}

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

Original21.0
Target19.1
Herbie18.5
\[\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 (cos (- y (/ (* z t) 3.0))) < 0.9997514971944133

    1. Initial program 20.3

      \[\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-sqrt20.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 associate-/r*20.3

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

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

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

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

    if 0.9997514971944133 < (cos (- y (/ (* z t) 3.0)))

    1. Initial program 22.1

      \[\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 16.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}\]
    3. Simplified16.6

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

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

Reproduce

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