Average Error: 20.5 → 18.1
Time: 29.5s
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}\;z \cdot t = -\infty \lor \neg \left(z \cdot t \le 3.982214551187210407512533577328782205679 \cdot 10^{305}\right):\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left({y}^{2}, \frac{-1}{2}, 1\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \left(\left(\frac{z}{\sqrt{3}} \cdot t\right) \cdot \left(\sqrt[3]{\frac{1}{\sqrt{3}}} \cdot \sqrt[3]{\frac{1}{\sqrt{3}}}\right)\right) \cdot \sqrt[3]{\frac{1}{\sqrt{3}}}\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}\;z \cdot t = -\infty \lor \neg \left(z \cdot t \le 3.982214551187210407512533577328782205679 \cdot 10^{305}\right):\\
\;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left({y}^{2}, \frac{-1}{2}, 1\right) - \frac{a}{b \cdot 3}\\

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

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r488378 = 2.0;
        double r488379 = x;
        double r488380 = sqrt(r488379);
        double r488381 = r488378 * r488380;
        double r488382 = y;
        double r488383 = z;
        double r488384 = t;
        double r488385 = r488383 * r488384;
        double r488386 = 3.0;
        double r488387 = r488385 / r488386;
        double r488388 = r488382 - r488387;
        double r488389 = cos(r488388);
        double r488390 = r488381 * r488389;
        double r488391 = a;
        double r488392 = b;
        double r488393 = r488392 * r488386;
        double r488394 = r488391 / r488393;
        double r488395 = r488390 - r488394;
        return r488395;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r488396 = z;
        double r488397 = t;
        double r488398 = r488396 * r488397;
        double r488399 = -inf.0;
        bool r488400 = r488398 <= r488399;
        double r488401 = 3.9822145511872104e+305;
        bool r488402 = r488398 <= r488401;
        double r488403 = !r488402;
        bool r488404 = r488400 || r488403;
        double r488405 = 2.0;
        double r488406 = x;
        double r488407 = sqrt(r488406);
        double r488408 = r488405 * r488407;
        double r488409 = y;
        double r488410 = 2.0;
        double r488411 = pow(r488409, r488410);
        double r488412 = -0.5;
        double r488413 = 1.0;
        double r488414 = fma(r488411, r488412, r488413);
        double r488415 = r488408 * r488414;
        double r488416 = a;
        double r488417 = b;
        double r488418 = 3.0;
        double r488419 = r488417 * r488418;
        double r488420 = r488416 / r488419;
        double r488421 = r488415 - r488420;
        double r488422 = sqrt(r488418);
        double r488423 = r488396 / r488422;
        double r488424 = r488423 * r488397;
        double r488425 = r488413 / r488422;
        double r488426 = cbrt(r488425);
        double r488427 = r488426 * r488426;
        double r488428 = r488424 * r488427;
        double r488429 = r488428 * r488426;
        double r488430 = r488409 - r488429;
        double r488431 = cos(r488430);
        double r488432 = r488408 * r488431;
        double r488433 = r488432 - r488420;
        double r488434 = r488404 ? r488421 : r488433;
        return r488434;
}

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

Target

Original20.5
Target18.6
Herbie18.1
\[\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 (* z t) < -inf.0 or 3.9822145511872104e+305 < (* z t)

    1. Initial program 63.7

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

      \[\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. Simplified45.2

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\mathsf{fma}\left({y}^{2}, \frac{-1}{2}, 1\right)} - \frac{a}{b \cdot 3}\]

    if -inf.0 < (* z t) < 3.9822145511872104e+305

    1. Initial program 14.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-sqrt14.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 times-frac14.3

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

    6. Applied div-inv14.3

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

    7. Applied associate-*r*14.3

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

    9. Applied add-cube-cbrt14.2

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

    10. Applied associate-*r*14.2

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

  4. Final simplification18.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t = -\infty \lor \neg \left(z \cdot t \le 3.982214551187210407512533577328782205679 \cdot 10^{305}\right):\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left({y}^{2}, \frac{-1}{2}, 1\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \left(\left(\frac{z}{\sqrt{3}} \cdot t\right) \cdot \left(\sqrt[3]{\frac{1}{\sqrt{3}}} \cdot \sqrt[3]{\frac{1}{\sqrt{3}}}\right)\right) \cdot \sqrt[3]{\frac{1}{\sqrt{3}}}\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

herbie shell --seed 2019325 +o rules:numerics
(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))))