\[\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.9999972455529012593800075592298526316881:\\ \;\;\;\;\left(\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right) + \log \left(e^{\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}\\ \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.9999972455529012593800075592298526316881:\\
\;\;\;\;\left(\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right) + \log \left(e^{\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}\\

\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 r447594 = 2.0;
        double r447595 = x;
        double r447596 = sqrt(r447595);
        double r447597 = r447594 * r447596;
        double r447598 = y;
        double r447599 = z;
        double r447600 = t;
        double r447601 = r447599 * r447600;
        double r447602 = 3.0;
        double r447603 = r447601 / r447602;
        double r447604 = r447598 - r447603;
        double r447605 = cos(r447604);
        double r447606 = r447597 * r447605;
        double r447607 = a;
        double r447608 = b;
        double r447609 = r447608 * r447602;
        double r447610 = r447607 / r447609;
        double r447611 = r447606 - r447610;
        return r447611;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r447612 = y;
        double r447613 = z;
        double r447614 = t;
        double r447615 = r447613 * r447614;
        double r447616 = 3.0;
        double r447617 = r447615 / r447616;
        double r447618 = r447612 - r447617;
        double r447619 = cos(r447618);
        double r447620 = 0.9999972455529013;
        bool r447621 = r447619 <= r447620;
        double r447622 = cos(r447612);
        double r447623 = cos(r447617);
        double r447624 = r447622 * r447623;
        double r447625 = 2.0;
        double r447626 = x;
        double r447627 = sqrt(r447626);
        double r447628 = r447625 * r447627;
        double r447629 = r447624 * r447628;
        double r447630 = sin(r447612);
        double r447631 = sin(r447617);
        double r447632 = r447630 * r447631;
        double r447633 = exp(r447632);
        double r447634 = log(r447633);
        double r447635 = r447634 * r447628;
        double r447636 = r447629 + r447635;
        double r447637 = a;
        double r447638 = b;
        double r447639 = r447638 * r447616;
        double r447640 = r447637 / r447639;
        double r447641 = r447636 - r447640;
        double r447642 = -0.5;
        double r447643 = 2.0;
        double r447644 = pow(r447612, r447643);
        double r447645 = 1.0;
        double r447646 = fma(r447642, r447644, r447645);
        double r447647 = r447628 * r447646;
        double r447648 = r447647 - r447640;
        double r447649 = r447621 ? r447641 : r447648;
        return r447649;
}

Original	20.5
Target	18.8
Herbie	18.0

Derivation

Split input into 2 regimes
if (cos (- y (/ (* z t) 3.0))) < 0.9999972455529013
1. Initial program 20.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-diff19.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. Applied distribute-lft-in19.5
  \[\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. Simplified19.5
  \[\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. Simplified19.5
  \[\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 add-log-exp19.5
  \[\leadsto \left(\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right) + \color{blue}{\log \left(e^{\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}\]
if 0.9999972455529013 < (cos (- y (/ (* z t) 3.0)))
1. Initial program 21.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 15.4
  \[\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.4
  \[\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.9999972455529012593800075592298526316881:\\ \;\;\;\;\left(\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(2 \cdot \sqrt{x}\right) + \log \left(e^{\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}\\ \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 2019323 +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))))

Error

Target

Derivation

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

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

Reproduce