Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, K

Average Error: 20.4 → 18.1

Time: 33.9s

Precision: 64

Math

\[\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.999846322247022:\\ \;\;\;\;\frac{\left(\left(\sin y \cdot \sin \left(\frac{t \cdot z}{3.0}\right)\right) \cdot \left(\left(\sin y \cdot \sin \left(\frac{t \cdot z}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{t \cdot z}{3.0}\right)\right)\right) + \left(\cos y \cdot \cos \left(\left(t \cdot 0.3333333333333333\right) \cdot z\right)\right) \cdot \left(\left(\cos y \cdot \cos \left(\left(t \cdot 0.3333333333333333\right) \cdot z\right)\right) \cdot \left(\cos y \cdot \cos \left(\left(t \cdot 0.3333333333333333\right) \cdot z\right)\right)\right)\right) \cdot \left(\sqrt{x} \cdot 2.0\right)}{\left(\left(\sin y \cdot \sin \left(\frac{t \cdot z}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{t \cdot z}{3.0}\right)\right) - \left(\cos y \cdot \cos \left(\left(t \cdot z\right) \cdot 0.3333333333333333\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{t \cdot z}{3.0}\right)\right)\right) + \left(\cos y \cdot \cos \left(\left(t \cdot z\right) \cdot 0.3333333333333333\right)\right) \cdot \left(\cos y \cdot \cos \left(\left(t \cdot z\right) \cdot 0.3333333333333333\right)\right)} - \frac{a}{b \cdot 3.0}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{-1}{2} \cdot \left(y \cdot y\right) + 1\right) \cdot \left(\sqrt{x} \cdot 2.0\right) - \frac{a}{b \cdot 3.0}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r38446253 = 2.0;
        double r38446254 = x;
        double r38446255 = sqrt(r38446254);
        double r38446256 = r38446253 * r38446255;
        double r38446257 = y;
        double r38446258 = z;
        double r38446259 = t;
        double r38446260 = r38446258 * r38446259;
        double r38446261 = 3.0;
        double r38446262 = r38446260 / r38446261;
        double r38446263 = r38446257 - r38446262;
        double r38446264 = cos(r38446263);
        double r38446265 = r38446256 * r38446264;
        double r38446266 = a;
        double r38446267 = b;
        double r38446268 = r38446267 * r38446261;
        double r38446269 = r38446266 / r38446268;
        double r38446270 = r38446265 - r38446269;
        return r38446270;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r38446271 = y;
        double r38446272 = t;
        double r38446273 = z;
        double r38446274 = r38446272 * r38446273;
        double r38446275 = 3.0;
        double r38446276 = r38446274 / r38446275;
        double r38446277 = r38446271 - r38446276;
        double r38446278 = cos(r38446277);
        double r38446279 = 0.999846322247022;
        bool r38446280 = r38446278 <= r38446279;
        double r38446281 = sin(r38446271);
        double r38446282 = sin(r38446276);
        double r38446283 = r38446281 * r38446282;
        double r38446284 = r38446283 * r38446283;
        double r38446285 = r38446283 * r38446284;
        double r38446286 = cos(r38446271);
        double r38446287 = 0.3333333333333333;
        double r38446288 = r38446272 * r38446287;
        double r38446289 = r38446288 * r38446273;
        double r38446290 = cos(r38446289);
        double r38446291 = r38446286 * r38446290;
        double r38446292 = r38446291 * r38446291;
        double r38446293 = r38446291 * r38446292;
        double r38446294 = r38446285 + r38446293;
        double r38446295 = x;
        double r38446296 = sqrt(r38446295);
        double r38446297 = 2.0;
        double r38446298 = r38446296 * r38446297;
        double r38446299 = r38446294 * r38446298;
        double r38446300 = r38446274 * r38446287;
        double r38446301 = cos(r38446300);
        double r38446302 = r38446286 * r38446301;
        double r38446303 = r38446302 * r38446283;
        double r38446304 = r38446284 - r38446303;
        double r38446305 = r38446302 * r38446302;
        double r38446306 = r38446304 + r38446305;
        double r38446307 = r38446299 / r38446306;
        double r38446308 = a;
        double r38446309 = b;
        double r38446310 = r38446309 * r38446275;
        double r38446311 = r38446308 / r38446310;
        double r38446312 = r38446307 - r38446311;
        double r38446313 = -0.5;
        double r38446314 = r38446271 * r38446271;
        double r38446315 = r38446313 * r38446314;
        double r38446316 = 1.0;
        double r38446317 = r38446315 + r38446316;
        double r38446318 = r38446317 * r38446298;
        double r38446319 = r38446318 - r38446311;
        double r38446320 = r38446280 ? r38446312 : r38446319;
        return r38446320;
}

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

Original	20.4
Target	18.7
Herbie	18.1

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

   1. Initial program 19.9

      \[\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 cos-diff 19.2

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

   4. Taylor expanded around inf 19.2

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \color{blue}{\cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)} + \sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) - \frac{a}{b \cdot 3.0}\]
   5. Using strategy rm

   6. Applied flip3-+ 19.2

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \color{blue}{\frac{{\left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right)}^{3} + {\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)}^{3}}{\left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) \cdot \left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) + \left(\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) - \left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)\right)}} - \frac{a}{b \cdot 3.0}\]

   7. Applied associate-*r/ 19.2

      \[\leadsto \color{blue}{\frac{\left(2.0 \cdot \sqrt{x}\right) \cdot \left({\left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right)}^{3} + {\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)}^{3}\right)}{\left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) \cdot \left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) + \left(\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) - \left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)\right)}} - \frac{a}{b \cdot 3.0}\]

   8. Simplified 19.3

      \[\leadsto \frac{\color{blue}{\left(2.0 \cdot \sqrt{x}\right) \cdot \left(\left(\left(\cos \left(\left(0.3333333333333333 \cdot t\right) \cdot z\right) \cdot \cos y\right) \cdot \left(\cos \left(\left(0.3333333333333333 \cdot t\right) \cdot z\right) \cdot \cos y\right)\right) \cdot \left(\cos y \cdot \cos \left(\left(0.3333333333333333 \cdot t\right) \cdot z\right)\right) + \left(\sin \left(\frac{z \cdot t}{3.0}\right) \cdot \sin y\right) \cdot \left(\left(\sin \left(\frac{z \cdot t}{3.0}\right) \cdot \sin y\right) \cdot \left(\sin \left(\frac{z \cdot t}{3.0}\right) \cdot \sin y\right)\right)\right)}}{\left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) \cdot \left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) + \left(\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) - \left(\cos y \cdot \cos \left(0.3333333333333333 \cdot \left(t \cdot z\right)\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)\right)} - \frac{a}{b \cdot 3.0}\]

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

   1. Initial program 21.3

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

      \[\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. Simplified 16.2

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

4. Final simplification 18.1

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

Reproduce

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