\[\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 r471796 = 2.0;
        double r471797 = x;
        double r471798 = sqrt(r471797);
        double r471799 = r471796 * r471798;
        double r471800 = y;
        double r471801 = z;
        double r471802 = t;
        double r471803 = r471801 * r471802;
        double r471804 = 3.0;
        double r471805 = r471803 / r471804;
        double r471806 = r471800 - r471805;
        double r471807 = cos(r471806);
        double r471808 = r471799 * r471807;
        double r471809 = a;
        double r471810 = b;
        double r471811 = r471810 * r471804;
        double r471812 = r471809 / r471811;
        double r471813 = r471808 - r471812;
        return r471813;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r471814 = y;
        double r471815 = z;
        double r471816 = t;
        double r471817 = r471815 * r471816;
        double r471818 = 3.0;
        double r471819 = r471817 / r471818;
        double r471820 = r471814 - r471819;
        double r471821 = cos(r471820);
        double r471822 = 0.9999972455529013;
        bool r471823 = r471821 <= r471822;
        double r471824 = cos(r471814);
        double r471825 = cos(r471819);
        double r471826 = r471824 * r471825;
        double r471827 = 2.0;
        double r471828 = x;
        double r471829 = sqrt(r471828);
        double r471830 = r471827 * r471829;
        double r471831 = r471826 * r471830;
        double r471832 = sin(r471814);
        double r471833 = sin(r471819);
        double r471834 = r471832 * r471833;
        double r471835 = exp(r471834);
        double r471836 = log(r471835);
        double r471837 = r471836 * r471830;
        double r471838 = r471831 + r471837;
        double r471839 = a;
        double r471840 = b;
        double r471841 = r471840 * r471818;
        double r471842 = r471839 / r471841;
        double r471843 = r471838 - r471842;
        double r471844 = -0.5;
        double r471845 = 2.0;
        double r471846 = pow(r471814, r471845);
        double r471847 = 1.0;
        double r471848 = fma(r471844, r471846, r471847);
        double r471849 = r471830 * r471848;
        double r471850 = r471849 - r471842;
        double r471851 = r471823 ? r471843 : r471850;
        return r471851;
}

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