Average Error: 20.5 → 17.6
Time: 18.6s
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 \le -1.4153686713047554694536085848185002123 \cdot 10^{302} \lor \neg \left(z \cdot t \le 8.738587929750899877247276628793759210701 \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(\left(\cos y \cdot \sqrt[3]{{\left(\cos \left(\frac{z \cdot t}{3}\right)\right)}^{3}}\right) \cdot \left(2 \cdot \sqrt{x}\right) + \left(\sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)} \cdot \sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)}\right) \cdot \sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)}\right) - \frac{\frac{a}{b}}{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 \le -1.4153686713047554694536085848185002123 \cdot 10^{302} \lor \neg \left(z \cdot t \le 8.738587929750899877247276628793759210701 \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(\left(\cos y \cdot \sqrt[3]{{\left(\cos \left(\frac{z \cdot t}{3}\right)\right)}^{3}}\right) \cdot \left(2 \cdot \sqrt{x}\right) + \left(\sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)} \cdot \sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)}\right) \cdot \sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)}\right) - \frac{\frac{a}{b}}{3}\\

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r958413 = 2.0;
        double r958414 = x;
        double r958415 = sqrt(r958414);
        double r958416 = r958413 * r958415;
        double r958417 = y;
        double r958418 = z;
        double r958419 = t;
        double r958420 = r958418 * r958419;
        double r958421 = 3.0;
        double r958422 = r958420 / r958421;
        double r958423 = r958417 - r958422;
        double r958424 = cos(r958423);
        double r958425 = r958416 * r958424;
        double r958426 = a;
        double r958427 = b;
        double r958428 = r958427 * r958421;
        double r958429 = r958426 / r958428;
        double r958430 = r958425 - r958429;
        return r958430;
}

double f(double x, double y, double z, double t, double a, double b) {
        double r958431 = z;
        double r958432 = t;
        double r958433 = r958431 * r958432;
        double r958434 = -1.4153686713047555e+302;
        bool r958435 = r958433 <= r958434;
        double r958436 = 8.7385879297509e+305;
        bool r958437 = r958433 <= r958436;
        double r958438 = !r958437;
        bool r958439 = r958435 || r958438;
        double r958440 = 2.0;
        double r958441 = x;
        double r958442 = sqrt(r958441);
        double r958443 = r958440 * r958442;
        double r958444 = y;
        double r958445 = 2.0;
        double r958446 = pow(r958444, r958445);
        double r958447 = -0.5;
        double r958448 = 1.0;
        double r958449 = fma(r958446, r958447, r958448);
        double r958450 = r958443 * r958449;
        double r958451 = a;
        double r958452 = b;
        double r958453 = 3.0;
        double r958454 = r958452 * r958453;
        double r958455 = r958451 / r958454;
        double r958456 = r958450 - r958455;
        double r958457 = cos(r958444);
        double r958458 = r958433 / r958453;
        double r958459 = cos(r958458);
        double r958460 = 3.0;
        double r958461 = pow(r958459, r958460);
        double r958462 = cbrt(r958461);
        double r958463 = r958457 * r958462;
        double r958464 = r958463 * r958443;
        double r958465 = sin(r958444);
        double r958466 = sin(r958458);
        double r958467 = r958465 * r958466;
        double r958468 = r958467 * r958443;
        double r958469 = cbrt(r958468);
        double r958470 = r958469 * r958469;
        double r958471 = r958470 * r958469;
        double r958472 = r958464 + r958471;
        double r958473 = r958451 / r958452;
        double r958474 = r958473 / r958453;
        double r958475 = r958472 - r958474;
        double r958476 = r958439 ? r958456 : r958475;
        return r958476;
}

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.2
Herbie17.6
\[\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) < -1.4153686713047555e+302 or 8.7385879297509e+305 < (* z t)

    1. Initial program 63.4

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

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

      \[\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 -1.4153686713047555e+302 < (* z t) < 8.7385879297509e+305

    1. Initial program 14.1

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

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

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

      \[\leadsto \left(\color{blue}{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\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. Simplified13.6

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

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

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

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

      \[\leadsto \left(\left(\cos y \cdot \sqrt[3]{\color{blue}{{\left(\cos \left(\frac{z \cdot t}{3}\right)\right)}^{3}}}\right) \cdot \left(2 \cdot \sqrt{x}\right) + \left(\sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)} \cdot \sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)}\right) \cdot \sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)}\right) - \frac{\frac{a}{b}}{3}\]
  3. Recombined 2 regimes into one program.
  4. Final simplification17.6

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t \le -1.4153686713047554694536085848185002123 \cdot 10^{302} \lor \neg \left(z \cdot t \le 8.738587929750899877247276628793759210701 \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(\left(\cos y \cdot \sqrt[3]{{\left(\cos \left(\frac{z \cdot t}{3}\right)\right)}^{3}}\right) \cdot \left(2 \cdot \sqrt{x}\right) + \left(\sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)} \cdot \sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)}\right) \cdot \sqrt[3]{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right)}\right) - \frac{\frac{a}{b}}{3}\\ \end{array}\]

Reproduce

herbie shell --seed 2019350 +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))))