Average Error: 20.8 → 18.0
Time: 31.4s
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}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.999845195289002731:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \left(\left(\sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)} \cdot \sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right) \cdot \sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right)\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\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.999845195289002731:\\
\;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \left(\left(\sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)} \cdot \sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right) \cdot \sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right)\right) - \frac{a}{b \cdot 3}\\

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

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r4215 = 2.0;
        double r4216 = x;
        double r4217 = sqrt(r4216);
        double r4218 = r4215 * r4217;
        double r4219 = y;
        double r4220 = z;
        double r4221 = t;
        double r4222 = r4220 * r4221;
        double r4223 = 3.0;
        double r4224 = r4222 / r4223;
        double r4225 = r4219 - r4224;
        double r4226 = cos(r4225);
        double r4227 = r4218 * r4226;
        double r4228 = a;
        double r4229 = b;
        double r4230 = r4229 * r4223;
        double r4231 = r4228 / r4230;
        double r4232 = r4227 - r4231;
        return r4232;
}
↓
double f(double x, double y, double z, double t, double a, double b) {
        double r4233 = y;
        double r4234 = z;
        double r4235 = t;
        double r4236 = r4234 * r4235;
        double r4237 = 3.0;
        double r4238 = r4236 / r4237;
        double r4239 = r4233 - r4238;
        double r4240 = cos(r4239);
        double r4241 = 0.9998451952890027;
        bool r4242 = r4240 <= r4241;
        double r4243 = 2.0;
        double r4244 = x;
        double r4245 = sqrt(r4244);
        double r4246 = r4243 * r4245;
        double r4247 = cos(r4233);
        double r4248 = cos(r4238);
        double r4249 = r4247 * r4248;
        double r4250 = sin(r4233);
        double r4251 = 0.3333333333333333;
        double r4252 = r4235 * r4234;
        double r4253 = r4251 * r4252;
        double r4254 = -r4253;
        double r4255 = sin(r4254);
        double r4256 = cbrt(r4255);
        double r4257 = r4256 * r4256;
        double r4258 = r4257 * r4256;
        double r4259 = r4250 * r4258;
        double r4260 = r4249 - r4259;
        double r4261 = r4246 * r4260;
        double r4262 = a;
        double r4263 = b;
        double r4264 = r4263 * r4237;
        double r4265 = r4262 / r4264;
        double r4266 = r4261 - r4265;
        double r4267 = 1.0;
        double r4268 = 0.5;
        double r4269 = 2.0;
        double r4270 = pow(r4233, r4269);
        double r4271 = r4268 * r4270;
        double r4272 = r4267 - r4271;
        double r4273 = r4246 * r4272;
        double r4274 = r4273 - r4265;
        double r4275 = r4242 ? r4266 : r4274;
        return r4275;
}

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

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original20.8
Target18.9
Herbie18.0
\[\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 (cos (- y (/ (* z t) 3.0))) < 0.9998451952890027

    1. Initial program 20.3

      \[\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-neg20.3

      \[\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-sum19.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}\]

    5. Simplified19.5

      \[\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 19.6

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

    8. Applied add-cube-cbrt19.6

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

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

    1. Initial program 21.6

      \[\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. Recombined 2 regimes into one program.

  4. Final simplification18.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.999845195289002731:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \left(\left(\sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)} \cdot \sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right) \cdot \sqrt[3]{\sin \left(-0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right)\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

herbie shell --seed 2020025 
(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))))