Average Error: 20.7 → 18.3
Time: 11.3s
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}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) \le 6.208773729303549596759795947686272567144 \cdot 10^{136}:\\ \;\;\;\;\left(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \mathsf{log1p}\left(\mathsf{expm1}\left(\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)\right)\right)\right) + \left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(0.3333333333333333148296162562473909929395 \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}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) \le 6.208773729303549596759795947686272567144 \cdot 10^{136}:\\
\;\;\;\;\left(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \mathsf{log1p}\left(\mathsf{expm1}\left(\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)\right)\right)\right) + \left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(0.3333333333333333148296162562473909929395 \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 r641175 = 2.0;
        double r641176 = x;
        double r641177 = sqrt(r641176);
        double r641178 = r641175 * r641177;
        double r641179 = y;
        double r641180 = z;
        double r641181 = t;
        double r641182 = r641180 * r641181;
        double r641183 = 3.0;
        double r641184 = r641182 / r641183;
        double r641185 = r641179 - r641184;
        double r641186 = cos(r641185);
        double r641187 = r641178 * r641186;
        double r641188 = a;
        double r641189 = b;
        double r641190 = r641189 * r641183;
        double r641191 = r641188 / r641190;
        double r641192 = r641187 - r641191;
        return r641192;
}

double f(double x, double y, double z, double t, double a, double b) {
        double r641193 = 2.0;
        double r641194 = x;
        double r641195 = sqrt(r641194);
        double r641196 = r641193 * r641195;
        double r641197 = y;
        double r641198 = z;
        double r641199 = t;
        double r641200 = r641198 * r641199;
        double r641201 = 3.0;
        double r641202 = r641200 / r641201;
        double r641203 = r641197 - r641202;
        double r641204 = cos(r641203);
        double r641205 = r641196 * r641204;
        double r641206 = 6.20877372930355e+136;
        bool r641207 = r641205 <= r641206;
        double r641208 = cos(r641197);
        double r641209 = 0.3333333333333333;
        double r641210 = r641199 * r641198;
        double r641211 = r641209 * r641210;
        double r641212 = cos(r641211);
        double r641213 = expm1(r641212);
        double r641214 = log1p(r641213);
        double r641215 = r641208 * r641214;
        double r641216 = r641196 * r641215;
        double r641217 = sin(r641197);
        double r641218 = sin(r641211);
        double r641219 = r641217 * r641218;
        double r641220 = r641196 * r641219;
        double r641221 = r641216 + r641220;
        double r641222 = a;
        double r641223 = b;
        double r641224 = r641223 * r641201;
        double r641225 = r641222 / r641224;
        double r641226 = r641221 - r641225;
        double r641227 = 1.0;
        double r641228 = 0.5;
        double r641229 = 2.0;
        double r641230 = pow(r641197, r641229);
        double r641231 = r641228 * r641230;
        double r641232 = r641227 - r641231;
        double r641233 = r641196 * r641232;
        double r641234 = r641233 - r641225;
        double r641235 = r641207 ? r641226 : r641234;
        return r641235;
}

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.7
Target18.5
Herbie18.3
\[\begin{array}{l} \mathbf{if}\;z \lt -1.379333748723514136852843173740882251575 \cdot 10^{129}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.3333333333333333148296162562473909929395}{z}}{t}\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{elif}\;z \lt 3.516290613555987147199887107423758623887 \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.3333333333333333148296162562473909929395}{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 (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) < 6.20877372930355e+136

    1. Initial program 14.0

      \[\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-diff13.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-in13.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. Taylor expanded around inf 13.5

      \[\leadsto \left(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \color{blue}{\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\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}\]
    6. Taylor expanded around inf 13.5

      \[\leadsto \left(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)\right) + \left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \color{blue}{\sin \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)}\right)\right) - \frac{a}{b \cdot 3}\]
    7. Using strategy rm
    8. Applied log1p-expm1-u13.5

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

    if 6.20877372930355e+136 < (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0))))

    1. Initial program 54.4

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

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) \le 6.208773729303549596759795947686272567144 \cdot 10^{136}:\\ \;\;\;\;\left(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \mathsf{log1p}\left(\mathsf{expm1}\left(\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)\right)\right)\right) + \left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(0.3333333333333333148296162562473909929395 \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 2020002 +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))))