Average Error: 20.5 → 18.2
Time: 14.1s
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 2.13358673845001374 \cdot 10^{302}\right):\\ \;\;\;\;\log \left({\left(e^{2 \cdot \sqrt{x}}\right)}^{\left(\mathsf{fma}\left(\cos y, \cos \left(\frac{z \cdot t}{3}\right), \sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right)\right)}\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(0.333333333333333315 \cdot \left(t \cdot z\right)\right) + \sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) - \frac{1}{b} \cdot \frac{a}{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 2.13358673845001374 \cdot 10^{302}\right):\\
\;\;\;\;\log \left({\left(e^{2 \cdot \sqrt{x}}\right)}^{\left(\mathsf{fma}\left(\cos y, \cos \left(\frac{z \cdot t}{3}\right), \sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right)\right)}\right) - \frac{a}{b \cdot 3}\\

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

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r730382 = 2.0;
        double r730383 = x;
        double r730384 = sqrt(r730383);
        double r730385 = r730382 * r730384;
        double r730386 = y;
        double r730387 = z;
        double r730388 = t;
        double r730389 = r730387 * r730388;
        double r730390 = 3.0;
        double r730391 = r730389 / r730390;
        double r730392 = r730386 - r730391;
        double r730393 = cos(r730392);
        double r730394 = r730385 * r730393;
        double r730395 = a;
        double r730396 = b;
        double r730397 = r730396 * r730390;
        double r730398 = r730395 / r730397;
        double r730399 = r730394 - r730398;
        return r730399;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r730400 = z;
        double r730401 = t;
        double r730402 = r730400 * r730401;
        double r730403 = -inf.0;
        bool r730404 = r730402 <= r730403;
        double r730405 = 2.1335867384500137e+302;
        bool r730406 = r730402 <= r730405;
        double r730407 = !r730406;
        bool r730408 = r730404 || r730407;
        double r730409 = 2.0;
        double r730410 = x;
        double r730411 = sqrt(r730410);
        double r730412 = r730409 * r730411;
        double r730413 = exp(r730412);
        double r730414 = y;
        double r730415 = cos(r730414);
        double r730416 = 3.0;
        double r730417 = r730402 / r730416;
        double r730418 = cos(r730417);
        double r730419 = sin(r730414);
        double r730420 = sin(r730417);
        double r730421 = r730419 * r730420;
        double r730422 = fma(r730415, r730418, r730421);
        double r730423 = pow(r730413, r730422);
        double r730424 = log(r730423);
        double r730425 = a;
        double r730426 = b;
        double r730427 = r730426 * r730416;
        double r730428 = r730425 / r730427;
        double r730429 = r730424 - r730428;
        double r730430 = 0.3333333333333333;
        double r730431 = r730401 * r730400;
        double r730432 = r730430 * r730431;
        double r730433 = cos(r730432);
        double r730434 = r730415 * r730433;
        double r730435 = r730434 + r730421;
        double r730436 = r730412 * r730435;
        double r730437 = 1.0;
        double r730438 = r730437 / r730426;
        double r730439 = r730425 / r730416;
        double r730440 = r730438 * r730439;
        double r730441 = r730436 - r730440;
        double r730442 = r730408 ? r730429 : r730441;
        return r730442;
}

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.5
Herbie18.2
\[\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 (* z t) < -inf.0 or 2.1335867384500137e+302 < (* z t)

    1. Initial program 63.5

      \[\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-diff63.5

      \[\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. Using strategy rm

    5. Applied add-log-exp63.6

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

    6. Simplified48.1

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

    if -inf.0 < (* z t) < 2.1335867384500137e+302

    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.7

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

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

    6. Applied *-un-lft-identity13.7

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

    7. Applied times-frac13.8

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

  4. Final simplification18.2

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

Reproduce

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