Average Error: 19.8 → 15.3
Time: 43.9s
Precision: 64
\[\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}\]
\[\begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{t \cdot z}{3.0}\right) \le 0.9999896787288287:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \left(\left(\mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{log1p}\left(\mathsf{expm1}\left(\cos \left(-z \cdot \frac{t}{3.0}\right)\right)\right)\right)\right) \cdot \cos y - \sin y \cdot \sin \left(-z \cdot \frac{t}{3.0}\right)\right) \cdot \cos \left(\mathsf{fma}\left(\frac{-t}{3.0}, z, z \cdot \frac{t}{3.0}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -z \cdot \frac{t}{3.0}\right)\right) \cdot \sin \left(\mathsf{fma}\left(\frac{-t}{3.0}, z, z \cdot \frac{t}{3.0}\right)\right)\right) - \frac{a}{b \cdot 3.0}\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \mathsf{fma}\left(y \cdot y, \frac{-1}{2}, 1\right) - \frac{a}{b \cdot 3.0}\\ \end{array}\]
\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}
\begin{array}{l}
\mathbf{if}\;\cos \left(y - \frac{t \cdot z}{3.0}\right) \le 0.9999896787288287:\\
\;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \left(\left(\mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{log1p}\left(\mathsf{expm1}\left(\cos \left(-z \cdot \frac{t}{3.0}\right)\right)\right)\right)\right) \cdot \cos y - \sin y \cdot \sin \left(-z \cdot \frac{t}{3.0}\right)\right) \cdot \cos \left(\mathsf{fma}\left(\frac{-t}{3.0}, z, z \cdot \frac{t}{3.0}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -z \cdot \frac{t}{3.0}\right)\right) \cdot \sin \left(\mathsf{fma}\left(\frac{-t}{3.0}, z, z \cdot \frac{t}{3.0}\right)\right)\right) - \frac{a}{b \cdot 3.0}\\

\mathbf{else}:\\
\;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \mathsf{fma}\left(y \cdot y, \frac{-1}{2}, 1\right) - \frac{a}{b \cdot 3.0}\\

\end{array}
double f(double x, double y, double z, double t, double a, double b) {
        double r38423064 = 2.0;
        double r38423065 = x;
        double r38423066 = sqrt(r38423065);
        double r38423067 = r38423064 * r38423066;
        double r38423068 = y;
        double r38423069 = z;
        double r38423070 = t;
        double r38423071 = r38423069 * r38423070;
        double r38423072 = 3.0;
        double r38423073 = r38423071 / r38423072;
        double r38423074 = r38423068 - r38423073;
        double r38423075 = cos(r38423074);
        double r38423076 = r38423067 * r38423075;
        double r38423077 = a;
        double r38423078 = b;
        double r38423079 = r38423078 * r38423072;
        double r38423080 = r38423077 / r38423079;
        double r38423081 = r38423076 - r38423080;
        return r38423081;
}

double f(double x, double y, double z, double t, double a, double b) {
        double r38423082 = y;
        double r38423083 = t;
        double r38423084 = z;
        double r38423085 = r38423083 * r38423084;
        double r38423086 = 3.0;
        double r38423087 = r38423085 / r38423086;
        double r38423088 = r38423082 - r38423087;
        double r38423089 = cos(r38423088);
        double r38423090 = 0.9999896787288287;
        bool r38423091 = r38423089 <= r38423090;
        double r38423092 = x;
        double r38423093 = sqrt(r38423092);
        double r38423094 = 2.0;
        double r38423095 = r38423093 * r38423094;
        double r38423096 = r38423083 / r38423086;
        double r38423097 = r38423084 * r38423096;
        double r38423098 = -r38423097;
        double r38423099 = cos(r38423098);
        double r38423100 = expm1(r38423099);
        double r38423101 = log1p(r38423100);
        double r38423102 = log1p(r38423101);
        double r38423103 = expm1(r38423102);
        double r38423104 = cos(r38423082);
        double r38423105 = r38423103 * r38423104;
        double r38423106 = sin(r38423082);
        double r38423107 = sin(r38423098);
        double r38423108 = r38423106 * r38423107;
        double r38423109 = r38423105 - r38423108;
        double r38423110 = -r38423083;
        double r38423111 = r38423110 / r38423086;
        double r38423112 = fma(r38423111, r38423084, r38423097);
        double r38423113 = cos(r38423112);
        double r38423114 = r38423109 * r38423113;
        double r38423115 = 1.0;
        double r38423116 = fma(r38423115, r38423082, r38423098);
        double r38423117 = sin(r38423116);
        double r38423118 = sin(r38423112);
        double r38423119 = r38423117 * r38423118;
        double r38423120 = r38423114 - r38423119;
        double r38423121 = r38423095 * r38423120;
        double r38423122 = a;
        double r38423123 = b;
        double r38423124 = r38423123 * r38423086;
        double r38423125 = r38423122 / r38423124;
        double r38423126 = r38423121 - r38423125;
        double r38423127 = r38423082 * r38423082;
        double r38423128 = -0.5;
        double r38423129 = fma(r38423127, r38423128, r38423115);
        double r38423130 = r38423095 * r38423129;
        double r38423131 = r38423130 - r38423125;
        double r38423132 = r38423091 ? r38423126 : r38423131;
        return r38423132;
}

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

Target

Original19.8
Target17.9
Herbie15.3
\[\begin{array}{l} \mathbf{if}\;z \lt -1.3793337487235141 \cdot 10^{+129}:\\ \;\;\;\;\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.3333333333333333}{z}}{t}\right) - \frac{\frac{a}{3.0}}{b}\\ \mathbf{elif}\;z \lt 3.516290613555987 \cdot 10^{+106}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \cos \left(y - \frac{t}{3.0} \cdot z\right) - \frac{\frac{a}{3.0}}{b}\\ \mathbf{else}:\\ \;\;\;\;\cos \left(y - \frac{\frac{0.3333333333333333}{z}}{t}\right) \cdot \left(2.0 \cdot \sqrt{x}\right) - \frac{\frac{a}{b}}{3.0}\\ \end{array}\]

Derivation

  1. Split input into 2 regimes
  2. if (cos (- y (/ (* z t) 3.0))) < 0.9999896787288287

    1. Initial program 19.2

      \[\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}\]
    2. Using strategy rm
    3. Applied *-un-lft-identity19.2

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{\color{blue}{1 \cdot 3.0}}\right) - \frac{a}{b \cdot 3.0}\]
    4. Applied times-frac19.2

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \color{blue}{\frac{z}{1} \cdot \frac{t}{3.0}}\right) - \frac{a}{b \cdot 3.0}\]
    5. Applied *-un-lft-identity19.2

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(\color{blue}{1 \cdot y} - \frac{z}{1} \cdot \frac{t}{3.0}\right) - \frac{a}{b \cdot 3.0}\]
    6. Applied prod-diff19.2

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \cos \color{blue}{\left(\mathsf{fma}\left(1, y, -\frac{t}{3.0} \cdot \frac{z}{1}\right) + \mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right)} - \frac{a}{b \cdot 3.0}\]
    7. Applied cos-sum16.4

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(\cos \left(\mathsf{fma}\left(1, y, -\frac{t}{3.0} \cdot \frac{z}{1}\right)\right) \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{3.0} \cdot \frac{z}{1}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right)\right)} - \frac{a}{b \cdot 3.0}\]
    8. Using strategy rm
    9. Applied fma-udef16.4

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \left(\cos \color{blue}{\left(1 \cdot y + \left(-\frac{t}{3.0} \cdot \frac{z}{1}\right)\right)} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{3.0} \cdot \frac{z}{1}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right)\right) - \frac{a}{b \cdot 3.0}\]
    10. Applied cos-sum15.5

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \left(\color{blue}{\left(\cos \left(1 \cdot y\right) \cdot \cos \left(-\frac{t}{3.0} \cdot \frac{z}{1}\right) - \sin \left(1 \cdot y\right) \cdot \sin \left(-\frac{t}{3.0} \cdot \frac{z}{1}\right)\right)} \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{3.0} \cdot \frac{z}{1}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right)\right) - \frac{a}{b \cdot 3.0}\]
    11. Using strategy rm
    12. Applied expm1-log1p-u15.5

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \left(\left(\cos \left(1 \cdot y\right) \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\cos \left(-\frac{t}{3.0} \cdot \frac{z}{1}\right)\right)\right)} - \sin \left(1 \cdot y\right) \cdot \sin \left(-\frac{t}{3.0} \cdot \frac{z}{1}\right)\right) \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{3.0} \cdot \frac{z}{1}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right)\right) - \frac{a}{b \cdot 3.0}\]
    13. Using strategy rm
    14. Applied log1p-expm1-u15.5

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \left(\left(\cos \left(1 \cdot y\right) \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\mathsf{log1p}\left(\mathsf{expm1}\left(\cos \left(-\frac{t}{3.0} \cdot \frac{z}{1}\right)\right)\right)}\right)\right) - \sin \left(1 \cdot y\right) \cdot \sin \left(-\frac{t}{3.0} \cdot \frac{z}{1}\right)\right) \cdot \cos \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -\frac{t}{3.0} \cdot \frac{z}{1}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{t}{3.0}, \frac{z}{1}, \frac{t}{3.0} \cdot \frac{z}{1}\right)\right)\right) - \frac{a}{b \cdot 3.0}\]

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

    1. Initial program 20.7

      \[\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}\]
    2. Taylor expanded around 0 15.0

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(1 - \frac{1}{2} \cdot {y}^{2}\right)} - \frac{a}{b \cdot 3.0}\]
    3. Simplified15.0

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \color{blue}{\mathsf{fma}\left(y \cdot y, \frac{-1}{2}, 1\right)} - \frac{a}{b \cdot 3.0}\]
  3. Recombined 2 regimes into one program.
  4. Final simplification15.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{t \cdot z}{3.0}\right) \le 0.9999896787288287:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \left(\left(\mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{log1p}\left(\mathsf{expm1}\left(\cos \left(-z \cdot \frac{t}{3.0}\right)\right)\right)\right)\right) \cdot \cos y - \sin y \cdot \sin \left(-z \cdot \frac{t}{3.0}\right)\right) \cdot \cos \left(\mathsf{fma}\left(\frac{-t}{3.0}, z, z \cdot \frac{t}{3.0}\right)\right) - \sin \left(\mathsf{fma}\left(1, y, -z \cdot \frac{t}{3.0}\right)\right) \cdot \sin \left(\mathsf{fma}\left(\frac{-t}{3.0}, z, z \cdot \frac{t}{3.0}\right)\right)\right) - \frac{a}{b \cdot 3.0}\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \mathsf{fma}\left(y \cdot y, \frac{-1}{2}, 1\right) - \frac{a}{b \cdot 3.0}\\ \end{array}\]

Reproduce

herbie shell --seed 2019168 +o rules:numerics
(FPCore (x y z t a b)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, K"

  :herbie-target
  (if (< z -1.3793337487235141e+129) (- (* (* 2.0 (sqrt x)) (cos (- (/ 1 y) (/ (/ 0.3333333333333333 z) t)))) (/ (/ a 3.0) b)) (if (< z 3.516290613555987e+106) (- (* (* (sqrt x) 2.0) (cos (- y (* (/ t 3.0) z)))) (/ (/ a 3.0) b)) (- (* (cos (- y (/ (/ 0.3333333333333333 z) t))) (* 2.0 (sqrt x))) (/ (/ a b) 3.0))))

  (- (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) (/ a (* b 3.0))))