Average Error: 20.4 → 18.3
Time: 16.9s
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 5.342832136901402435844543544724189771452 \cdot 10^{132}:\\ \;\;\;\;\left(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)\right) + \left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sqrt[3]{{\left(\sqrt[3]{{\left(\sin \left(\frac{z \cdot t}{3}\right)\right)}^{3}}\right)}^{3}}\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 5.342832136901402435844543544724189771452 \cdot 10^{132}:\\
\;\;\;\;\left(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)\right) + \left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sqrt[3]{{\left(\sqrt[3]{{\left(\sin \left(\frac{z \cdot t}{3}\right)\right)}^{3}}\right)}^{3}}\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 r579185 = 2.0;
        double r579186 = x;
        double r579187 = sqrt(r579186);
        double r579188 = r579185 * r579187;
        double r579189 = y;
        double r579190 = z;
        double r579191 = t;
        double r579192 = r579190 * r579191;
        double r579193 = 3.0;
        double r579194 = r579192 / r579193;
        double r579195 = r579189 - r579194;
        double r579196 = cos(r579195);
        double r579197 = r579188 * r579196;
        double r579198 = a;
        double r579199 = b;
        double r579200 = r579199 * r579193;
        double r579201 = r579198 / r579200;
        double r579202 = r579197 - r579201;
        return r579202;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r579203 = 2.0;
        double r579204 = x;
        double r579205 = sqrt(r579204);
        double r579206 = r579203 * r579205;
        double r579207 = y;
        double r579208 = z;
        double r579209 = t;
        double r579210 = r579208 * r579209;
        double r579211 = 3.0;
        double r579212 = r579210 / r579211;
        double r579213 = r579207 - r579212;
        double r579214 = cos(r579213);
        double r579215 = r579206 * r579214;
        double r579216 = 5.3428321369014024e+132;
        bool r579217 = r579215 <= r579216;
        double r579218 = cos(r579207);
        double r579219 = 0.3333333333333333;
        double r579220 = r579209 * r579208;
        double r579221 = r579219 * r579220;
        double r579222 = cos(r579221);
        double r579223 = r579218 * r579222;
        double r579224 = r579206 * r579223;
        double r579225 = sin(r579207);
        double r579226 = sin(r579212);
        double r579227 = 3.0;
        double r579228 = pow(r579226, r579227);
        double r579229 = cbrt(r579228);
        double r579230 = pow(r579229, r579227);
        double r579231 = cbrt(r579230);
        double r579232 = r579225 * r579231;
        double r579233 = r579206 * r579232;
        double r579234 = r579224 + r579233;
        double r579235 = a;
        double r579236 = b;
        double r579237 = r579236 * r579211;
        double r579238 = r579235 / r579237;
        double r579239 = r579234 - r579238;
        double r579240 = 1.0;
        double r579241 = 0.5;
        double r579242 = 2.0;
        double r579243 = pow(r579207, r579242);
        double r579244 = r579241 * r579243;
        double r579245 = r579240 - r579244;
        double r579246 = r579206 * r579245;
        double r579247 = r579246 - r579238;
        double r579248 = r579217 ? r579239 : r579247;
        return r579248;
}

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.4
Target18.6
Herbie18.3
\[\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 (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) < 5.3428321369014024e+132

    1. Initial program 14.4

      \[\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 cos-diff13.9

      \[\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}\]

    4. Applied distribute-lft-in13.9

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

    5. Taylor expanded around inf 13.9

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

    7. Applied add-cbrt-cube13.9

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

    8. Simplified13.9

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

    10. Applied add-cbrt-cube13.9

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

    11. Simplified13.9

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

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

    1. Initial program 51.9

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

      \[\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.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) \le 5.342832136901402435844543544724189771452 \cdot 10^{132}:\\ \;\;\;\;\left(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)\right) + \left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sqrt[3]{{\left(\sqrt[3]{{\left(\sin \left(\frac{z \cdot t}{3}\right)\right)}^{3}}\right)}^{3}}\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 1978988140 
(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.379333748723514e129) (- (* (* 2 (sqrt x)) (cos (- (/ 1 y) (/ (/ 0.333333333333333315 z) t)))) (/ (/ a 3) b)) (if (< z 3.51629061355598715e106) (- (* (* (sqrt x) 2) (cos (- y (* (/ t 3) z)))) (/ (/ a 3) b)) (- (* (cos (- y (/ (/ 0.333333333333333315 z) t))) (* 2 (sqrt x))) (/ (/ a b) 3))))

  (- (* (* 2 (sqrt x)) (cos (- y (/ (* z t) 3)))) (/ a (* b 3))))