\[\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}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.9999735515317531575618659189785830676556:\\ \;\;\;\;\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) - \frac{1}{b} \cdot \frac{a}{3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left(\frac{-1}{2}, {y}^{2}, 1\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}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.9999735515317531575618659189785830676556:\\
\;\;\;\;\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) - \frac{1}{b} \cdot \frac{a}{3}\\

\mathbf{else}:\\
\;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left(\frac{-1}{2}, {y}^{2}, 1\right) - \frac{a}{b \cdot 3}\\

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r486449 = 2.0;
        double r486450 = x;
        double r486451 = sqrt(r486450);
        double r486452 = r486449 * r486451;
        double r486453 = y;
        double r486454 = z;
        double r486455 = t;
        double r486456 = r486454 * r486455;
        double r486457 = 3.0;
        double r486458 = r486456 / r486457;
        double r486459 = r486453 - r486458;
        double r486460 = cos(r486459);
        double r486461 = r486452 * r486460;
        double r486462 = a;
        double r486463 = b;
        double r486464 = r486463 * r486457;
        double r486465 = r486462 / r486464;
        double r486466 = r486461 - r486465;
        return r486466;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r486467 = y;
        double r486468 = z;
        double r486469 = t;
        double r486470 = r486468 * r486469;
        double r486471 = 3.0;
        double r486472 = r486470 / r486471;
        double r486473 = r486467 - r486472;
        double r486474 = cos(r486473);
        double r486475 = 0.9999735515317532;
        bool r486476 = r486474 <= r486475;
        double r486477 = 2.0;
        double r486478 = x;
        double r486479 = sqrt(r486478);
        double r486480 = r486477 * r486479;
        double r486481 = cos(r486467);
        double r486482 = cos(r486472);
        double r486483 = r486481 * r486482;
        double r486484 = sin(r486467);
        double r486485 = sin(r486472);
        double r486486 = r486484 * r486485;
        double r486487 = r486483 + r486486;
        double r486488 = r486480 * r486487;
        double r486489 = 1.0;
        double r486490 = b;
        double r486491 = r486489 / r486490;
        double r486492 = a;
        double r486493 = r486492 / r486471;
        double r486494 = r486491 * r486493;
        double r486495 = r486488 - r486494;
        double r486496 = -0.5;
        double r486497 = 2.0;
        double r486498 = pow(r486467, r486497);
        double r486499 = fma(r486496, r486498, r486489);
        double r486500 = r486480 * r486499;
        double r486501 = r486490 * r486471;
        double r486502 = r486492 / r486501;
        double r486503 = r486500 - r486502;
        double r486504 = r486476 ? r486495 : r486503;
        return r486504;
}

Original	20.8
Target	18.7
Herbie	18.0

Derivation

Split input into 2 regimes
if (cos (- y (/ (* z t) 3.0))) < 0.9999735515317532
1. Initial program 19.9
  \[\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-diff19.1
  \[\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 *-un-lft-identity19.1
  \[\leadsto \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) - \frac{\color{blue}{1 \cdot a}}{b \cdot 3}\]
6. Applied times-frac19.1
  \[\leadsto \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) - \color{blue}{\frac{1}{b} \cdot \frac{a}{3}}\]
if 0.9999735515317532 < (cos (- y (/ (* z t) 3.0)))
1. Initial program 22.3
  \[\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 16.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. Simplified16.3
  \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{2}, {y}^{2}, 1\right)} - \frac{a}{b \cdot 3}\]
Recombined 2 regimes into one program.
Final simplification18.0
\[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.9999735515317531575618659189785830676556:\\ \;\;\;\;\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) - \frac{1}{b} \cdot \frac{a}{3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left(\frac{-1}{2}, {y}^{2}, 1\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

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

Error

Target

Derivation

`if (cos (- y (/ (* z t) 3.0))) < 0.9999735515317532`

`if 0.9999735515317532 < (cos (- y (/ (* z t) 3.0)))`

Reproduce