Average Error: 20.7 → 17.9
Time: 24.4s
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 8.139896335094742174168253426990729793648 \cdot 10^{149}:\\ \;\;\;\;\frac{\left(2 \cdot \sqrt{x}\right) \cdot \left({\left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right)}^{3} + {\left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right)}^{3}\right)}{\left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right) \cdot \left(\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right) \cdot \cos y\right) + \left(\left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right) \cdot \left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right) - \left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right) \cdot \left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right)\right)} - \frac{\frac{a}{b}}{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 8.139896335094742174168253426990729793648 \cdot 10^{149}:\\
\;\;\;\;\frac{\left(2 \cdot \sqrt{x}\right) \cdot \left({\left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right)}^{3} + {\left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right)}^{3}\right)}{\left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right) \cdot \left(\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right) \cdot \cos y\right) + \left(\left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right) \cdot \left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right) - \left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right) \cdot \left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right)\right)} - \frac{\frac{a}{b}}{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 r593281 = 2.0;
        double r593282 = x;
        double r593283 = sqrt(r593282);
        double r593284 = r593281 * r593283;
        double r593285 = y;
        double r593286 = z;
        double r593287 = t;
        double r593288 = r593286 * r593287;
        double r593289 = 3.0;
        double r593290 = r593288 / r593289;
        double r593291 = r593285 - r593290;
        double r593292 = cos(r593291);
        double r593293 = r593284 * r593292;
        double r593294 = a;
        double r593295 = b;
        double r593296 = r593295 * r593289;
        double r593297 = r593294 / r593296;
        double r593298 = r593293 - r593297;
        return r593298;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r593299 = 2.0;
        double r593300 = x;
        double r593301 = sqrt(r593300);
        double r593302 = r593299 * r593301;
        double r593303 = y;
        double r593304 = z;
        double r593305 = t;
        double r593306 = r593304 * r593305;
        double r593307 = 3.0;
        double r593308 = r593306 / r593307;
        double r593309 = r593303 - r593308;
        double r593310 = cos(r593309);
        double r593311 = r593302 * r593310;
        double r593312 = 8.139896335094742e+149;
        bool r593313 = r593311 <= r593312;
        double r593314 = cos(r593308);
        double r593315 = cos(r593303);
        double r593316 = r593314 * r593315;
        double r593317 = 3.0;
        double r593318 = pow(r593316, r593317);
        double r593319 = sin(r593308);
        double r593320 = sin(r593303);
        double r593321 = r593319 * r593320;
        double r593322 = pow(r593321, r593317);
        double r593323 = r593318 + r593322;
        double r593324 = r593302 * r593323;
        double r593325 = 0.3333333333333333;
        double r593326 = r593305 * r593304;
        double r593327 = r593325 * r593326;
        double r593328 = cos(r593327);
        double r593329 = r593328 * r593315;
        double r593330 = r593316 * r593329;
        double r593331 = r593321 * r593321;
        double r593332 = r593316 * r593321;
        double r593333 = r593331 - r593332;
        double r593334 = r593330 + r593333;
        double r593335 = r593324 / r593334;
        double r593336 = a;
        double r593337 = b;
        double r593338 = r593336 / r593337;
        double r593339 = r593338 / r593307;
        double r593340 = r593335 - r593339;
        double r593341 = 1.0;
        double r593342 = 0.5;
        double r593343 = 2.0;
        double r593344 = pow(r593303, r593343);
        double r593345 = r593342 * r593344;
        double r593346 = r593341 - r593345;
        double r593347 = r593302 * r593346;
        double r593348 = r593337 * r593307;
        double r593349 = r593336 / r593348;
        double r593350 = r593347 - r593349;
        double r593351 = r593313 ? r593340 : r593350;
        return r593351;
}

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.7
Target18.7
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 (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) < 8.139896335094742e+149

    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 cos-diff14.0

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

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

    5. Simplified14.0

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

    7. Applied associate-/r*14.1

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

    9. Applied flip3-+14.1

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

    10. Applied associate-*r/14.1

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

    11. Taylor expanded around inf 14.2

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

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

    1. Initial program 60.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 42.3

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) \le 8.139896335094742174168253426990729793648 \cdot 10^{149}:\\ \;\;\;\;\frac{\left(2 \cdot \sqrt{x}\right) \cdot \left({\left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right)}^{3} + {\left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right)}^{3}\right)}{\left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right) \cdot \left(\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right) \cdot \cos y\right) + \left(\left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right) \cdot \left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right) - \left(\cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right) \cdot \left(\sin \left(\frac{z \cdot t}{3}\right) \cdot \sin y\right)\right)} - \frac{\frac{a}{b}}{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 2019303 
(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))))