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

\mathbf{else}:\\
\;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left({y}^{2}, \frac{-1}{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 r510631 = 2.0;
        double r510632 = x;
        double r510633 = sqrt(r510632);
        double r510634 = r510631 * r510633;
        double r510635 = y;
        double r510636 = z;
        double r510637 = t;
        double r510638 = r510636 * r510637;
        double r510639 = 3.0;
        double r510640 = r510638 / r510639;
        double r510641 = r510635 - r510640;
        double r510642 = cos(r510641);
        double r510643 = r510634 * r510642;
        double r510644 = a;
        double r510645 = b;
        double r510646 = r510645 * r510639;
        double r510647 = r510644 / r510646;
        double r510648 = r510643 - r510647;
        return r510648;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r510649 = y;
        double r510650 = z;
        double r510651 = t;
        double r510652 = r510650 * r510651;
        double r510653 = 3.0;
        double r510654 = r510652 / r510653;
        double r510655 = r510649 - r510654;
        double r510656 = cos(r510655);
        double r510657 = 0.9999999999999865;
        bool r510658 = r510656 <= r510657;
        double r510659 = 2.0;
        double r510660 = x;
        double r510661 = sqrt(r510660);
        double r510662 = r510659 * r510661;
        double r510663 = cos(r510649);
        double r510664 = 0.3333333333333333;
        double r510665 = r510651 * r510650;
        double r510666 = r510664 * r510665;
        double r510667 = cos(r510666);
        double r510668 = r510663 * r510667;
        double r510669 = sin(r510649);
        double r510670 = -r510654;
        double r510671 = sin(r510670);
        double r510672 = r510669 * r510671;
        double r510673 = r510668 - r510672;
        double r510674 = r510662 * r510673;
        double r510675 = a;
        double r510676 = b;
        double r510677 = r510676 * r510653;
        double r510678 = r510675 / r510677;
        double r510679 = r510674 - r510678;
        double r510680 = 2.0;
        double r510681 = pow(r510649, r510680);
        double r510682 = -0.5;
        double r510683 = 1.0;
        double r510684 = fma(r510681, r510682, r510683);
        double r510685 = r510662 * r510684;
        double r510686 = r510685 - r510678;
        double r510687 = r510658 ? r510679 : r510686;
        return r510687;
}

Original	20.5
Target	18.5
Herbie	17.6

Derivation

Split input into 2 regimes
if (cos (- y (/ (* z t) 3.0))) < 0.9999999999999865
1. Initial program 19.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 sub-neg19.6
  \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \cos \color{blue}{\left(y + \left(-\frac{z \cdot t}{3}\right)\right)} - \frac{a}{b \cdot 3}\]
4. Applied cos-sum18.9
  \[\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}\]
5. Simplified18.9
  \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\color{blue}{\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}\]
6. Taylor expanded around inf 18.9
  \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \color{blue}{\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)} - \sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) - \frac{a}{b \cdot 3}\]
if 0.9999999999999865 < (cos (- y (/ (* z t) 3.0)))
1. Initial program 22.0
  \[\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 15.5
  \[\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. Simplified15.5
  \[\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}\]
Recombined 2 regimes into one program.
Final simplification17.6
\[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.9999999999999864552790995730902068316936:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right) - \sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left({y}^{2}, \frac{-1}{2}, 1\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

herbie shell --seed 2019208 +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.9999999999999865`

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

Reproduce