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

Average Error: 20.2 → 18.2

Time: 34.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}\;z \cdot t \le -1.458868184330442 \cdot 10^{+297}:\\ \;\;\;\;\left(\left(y \cdot \frac{-1}{2}\right) \cdot y + 1\right) \cdot \left(\sqrt{x} \cdot 2.0\right) - \frac{a}{3.0 \cdot b}\\ \mathbf{elif}\;z \cdot t \le 3.947993520431114 \cdot 10^{+303}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \cos \left(y - \left(\sqrt[3]{\frac{z \cdot t}{3.0}} \cdot \sqrt[3]{\frac{z \cdot t}{3.0}}\right) \cdot \left(\sqrt[3]{z} \cdot \left(\sqrt[3]{\frac{t}{\sqrt{3.0}}} \cdot \sqrt[3]{\frac{1}{\sqrt{3.0}}}\right)\right)\right) - \frac{a}{3.0 \cdot b}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(y \cdot \frac{-1}{2}\right) \cdot y + 1\right) \cdot \left(\sqrt{x} \cdot 2.0\right) - \frac{a}{3.0 \cdot b}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r35680284 = 2.0;
        double r35680285 = x;
        double r35680286 = sqrt(r35680285);
        double r35680287 = r35680284 * r35680286;
        double r35680288 = y;
        double r35680289 = z;
        double r35680290 = t;
        double r35680291 = r35680289 * r35680290;
        double r35680292 = 3.0;
        double r35680293 = r35680291 / r35680292;
        double r35680294 = r35680288 - r35680293;
        double r35680295 = cos(r35680294);
        double r35680296 = r35680287 * r35680295;
        double r35680297 = a;
        double r35680298 = b;
        double r35680299 = r35680298 * r35680292;
        double r35680300 = r35680297 / r35680299;
        double r35680301 = r35680296 - r35680300;
        return r35680301;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r35680302 = z;
        double r35680303 = t;
        double r35680304 = r35680302 * r35680303;
        double r35680305 = -1.458868184330442e+297;
        bool r35680306 = r35680304 <= r35680305;
        double r35680307 = y;
        double r35680308 = -0.5;
        double r35680309 = r35680307 * r35680308;
        double r35680310 = r35680309 * r35680307;
        double r35680311 = 1.0;
        double r35680312 = r35680310 + r35680311;
        double r35680313 = x;
        double r35680314 = sqrt(r35680313);
        double r35680315 = 2.0;
        double r35680316 = r35680314 * r35680315;
        double r35680317 = r35680312 * r35680316;
        double r35680318 = a;
        double r35680319 = 3.0;
        double r35680320 = b;
        double r35680321 = r35680319 * r35680320;
        double r35680322 = r35680318 / r35680321;
        double r35680323 = r35680317 - r35680322;
        double r35680324 = 3.947993520431114e+303;
        bool r35680325 = r35680304 <= r35680324;
        double r35680326 = r35680304 / r35680319;
        double r35680327 = cbrt(r35680326);
        double r35680328 = r35680327 * r35680327;
        double r35680329 = cbrt(r35680302);
        double r35680330 = sqrt(r35680319);
        double r35680331 = r35680303 / r35680330;
        double r35680332 = cbrt(r35680331);
        double r35680333 = r35680311 / r35680330;
        double r35680334 = cbrt(r35680333);
        double r35680335 = r35680332 * r35680334;
        double r35680336 = r35680329 * r35680335;
        double r35680337 = r35680328 * r35680336;
        double r35680338 = r35680307 - r35680337;
        double r35680339 = cos(r35680338);
        double r35680340 = r35680316 * r35680339;
        double r35680341 = r35680340 - r35680322;
        double r35680342 = r35680325 ? r35680341 : r35680323;
        double r35680343 = r35680306 ? r35680323 : r35680342;
        return r35680343;
}

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.2
Target	18.5
Herbie	18.2

\[\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 (* z t) < -1.458868184330442e+297 or 3.947993520431114e+303 < (* z t)

   1. Initial program 61.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. Using strategy rm

   3. Applied add-cube-cbrt 61.4

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

   5. Applied add-cbrt-cube 61.4

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

   6. Taylor expanded around 0 45.9

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

   7. Simplified 45.9

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

   if -1.458868184330442e+297 < (* z t) < 3.947993520431114e+303

   1. Initial program 14.1

      \[\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 add-cube-cbrt 14.1

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

   5. Applied *-un-lft-identity 14.1

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

   6. Applied times-frac 14.1

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

   7. Applied cbrt-prod 14.1

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

   8. Simplified 14.1

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

   10. Applied add-sqr-sqrt 14.1

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

   11. Applied *-un-lft-identity 14.1

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

   12. Applied times-frac 14.1

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

   13. Applied cbrt-prod 14.1

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

4. Final simplification 18.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t \le -1.458868184330442 \cdot 10^{+297}:\\ \;\;\;\;\left(\left(y \cdot \frac{-1}{2}\right) \cdot y + 1\right) \cdot \left(\sqrt{x} \cdot 2.0\right) - \frac{a}{3.0 \cdot b}\\ \mathbf{elif}\;z \cdot t \le 3.947993520431114 \cdot 10^{+303}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \cos \left(y - \left(\sqrt[3]{\frac{z \cdot t}{3.0}} \cdot \sqrt[3]{\frac{z \cdot t}{3.0}}\right) \cdot \left(\sqrt[3]{z} \cdot \left(\sqrt[3]{\frac{t}{\sqrt{3.0}}} \cdot \sqrt[3]{\frac{1}{\sqrt{3.0}}}\right)\right)\right) - \frac{a}{3.0 \cdot b}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(y \cdot \frac{-1}{2}\right) \cdot y + 1\right) \cdot \left(\sqrt{x} \cdot 2.0\right) - \frac{a}{3.0 \cdot b}\\ \end{array}\]

Reproduce

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