Average Error: 20.9 → 18.7
Time: 11.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}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) \le 6.3135193842745707 \cdot 10^{133}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \sin \left(-\left({\left(\sqrt[3]{\sqrt[3]{0.333333333333333315}}\right)}^{4} \cdot \left(\sqrt[3]{\sqrt[3]{0.333333333333333315}} \cdot \sqrt[3]{\sqrt[3]{0.333333333333333315}}\right)\right) \cdot \left(\sqrt[3]{0.333333333333333315} \cdot \left(t \cdot z\right)\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 6.3135193842745707 \cdot 10^{133}:\\
\;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \sin \left(-\left({\left(\sqrt[3]{\sqrt[3]{0.333333333333333315}}\right)}^{4} \cdot \left(\sqrt[3]{\sqrt[3]{0.333333333333333315}} \cdot \sqrt[3]{\sqrt[3]{0.333333333333333315}}\right)\right) \cdot \left(\sqrt[3]{0.333333333333333315} \cdot \left(t \cdot z\right)\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 r645858 = 2.0;
        double r645859 = x;
        double r645860 = sqrt(r645859);
        double r645861 = r645858 * r645860;
        double r645862 = y;
        double r645863 = z;
        double r645864 = t;
        double r645865 = r645863 * r645864;
        double r645866 = 3.0;
        double r645867 = r645865 / r645866;
        double r645868 = r645862 - r645867;
        double r645869 = cos(r645868);
        double r645870 = r645861 * r645869;
        double r645871 = a;
        double r645872 = b;
        double r645873 = r645872 * r645866;
        double r645874 = r645871 / r645873;
        double r645875 = r645870 - r645874;
        return r645875;
}

double f(double x, double y, double z, double t, double a, double b) {
        double r645876 = 2.0;
        double r645877 = x;
        double r645878 = sqrt(r645877);
        double r645879 = r645876 * r645878;
        double r645880 = y;
        double r645881 = z;
        double r645882 = t;
        double r645883 = r645881 * r645882;
        double r645884 = 3.0;
        double r645885 = r645883 / r645884;
        double r645886 = r645880 - r645885;
        double r645887 = cos(r645886);
        double r645888 = r645879 * r645887;
        double r645889 = 6.313519384274571e+133;
        bool r645890 = r645888 <= r645889;
        double r645891 = cos(r645880);
        double r645892 = cos(r645885);
        double r645893 = r645891 * r645892;
        double r645894 = sin(r645880);
        double r645895 = 0.3333333333333333;
        double r645896 = cbrt(r645895);
        double r645897 = cbrt(r645896);
        double r645898 = 4.0;
        double r645899 = pow(r645897, r645898);
        double r645900 = r645897 * r645897;
        double r645901 = r645899 * r645900;
        double r645902 = r645882 * r645881;
        double r645903 = r645896 * r645902;
        double r645904 = r645901 * r645903;
        double r645905 = -r645904;
        double r645906 = sin(r645905);
        double r645907 = r645894 * r645906;
        double r645908 = r645893 - r645907;
        double r645909 = r645879 * r645908;
        double r645910 = a;
        double r645911 = b;
        double r645912 = r645911 * r645884;
        double r645913 = r645910 / r645912;
        double r645914 = r645909 - r645913;
        double r645915 = 1.0;
        double r645916 = 0.5;
        double r645917 = 2.0;
        double r645918 = pow(r645880, r645917);
        double r645919 = r645916 * r645918;
        double r645920 = r645915 - r645919;
        double r645921 = r645879 * r645920;
        double r645922 = r645921 - r645913;
        double r645923 = r645890 ? r645914 : r645922;
        return r645923;
}

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.9
Target19.0
Herbie18.7
\[\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)))) < 6.313519384274571e+133

    1. Initial program 14.6

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

      \[\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-sum14.1

      \[\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. Simplified14.1

      \[\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. Taylor expanded around inf 14.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\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}\]
    7. Using strategy rm
    8. Applied add-cube-cbrt14.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \sin \left(-\color{blue}{\left(\left(\sqrt[3]{0.333333333333333315} \cdot \sqrt[3]{0.333333333333333315}\right) \cdot \sqrt[3]{0.333333333333333315}\right)} \cdot \left(t \cdot z\right)\right)\right) - \frac{a}{b \cdot 3}\]
    9. Applied associate-*l*14.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \sin \left(-\color{blue}{\left(\sqrt[3]{0.333333333333333315} \cdot \sqrt[3]{0.333333333333333315}\right) \cdot \left(\sqrt[3]{0.333333333333333315} \cdot \left(t \cdot z\right)\right)}\right)\right) - \frac{a}{b \cdot 3}\]
    10. Using strategy rm
    11. Applied add-cube-cbrt14.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \sin \left(-\left(\sqrt[3]{0.333333333333333315} \cdot \color{blue}{\left(\left(\sqrt[3]{\sqrt[3]{0.333333333333333315}} \cdot \sqrt[3]{\sqrt[3]{0.333333333333333315}}\right) \cdot \sqrt[3]{\sqrt[3]{0.333333333333333315}}\right)}\right) \cdot \left(\sqrt[3]{0.333333333333333315} \cdot \left(t \cdot z\right)\right)\right)\right) - \frac{a}{b \cdot 3}\]
    12. Applied add-cube-cbrt14.1

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

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

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

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

    1. Initial program 53.8

      \[\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.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. Recombined 2 regimes into one program.
  4. Final simplification18.7

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