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

Average Error: 21.5 → 18.6

Time: 23.0s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\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}\;z \cdot t = -\infty:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left(\frac{-1}{2}, {y}^{2}, 1\right) - \frac{a}{b \cdot 3}\\ \mathbf{elif}\;z \cdot t \le 1.198305287737106264207051230853461279422 \cdot 10^{307}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{\frac{z}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot t}{\sqrt[3]{3}}\right) - \left(\left(\sqrt[3]{\sin \left(\frac{z}{\frac{3}{t}}\right)} \cdot \sqrt[3]{\sin \left(\frac{z}{\frac{3}{t}}\right)}\right) \cdot \sqrt[3]{\sin \left(\frac{z}{\frac{3}{t}}\right)}\right) \cdot \left(-\sin y\right)\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\log \left({\left(e^{2 \cdot \sqrt{x}}\right)}^{\left(\cos \left(y - \frac{z}{3} \cdot t\right)\right)}\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r864814 = 2.0;
        double r864815 = x;
        double r864816 = sqrt(r864815);
        double r864817 = r864814 * r864816;
        double r864818 = y;
        double r864819 = z;
        double r864820 = t;
        double r864821 = r864819 * r864820;
        double r864822 = 3.0;
        double r864823 = r864821 / r864822;
        double r864824 = r864818 - r864823;
        double r864825 = cos(r864824);
        double r864826 = r864817 * r864825;
        double r864827 = a;
        double r864828 = b;
        double r864829 = r864828 * r864822;
        double r864830 = r864827 / r864829;
        double r864831 = r864826 - r864830;
        return r864831;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r864832 = z;
        double r864833 = t;
        double r864834 = r864832 * r864833;
        double r864835 = -inf.0;
        bool r864836 = r864834 <= r864835;
        double r864837 = 2.0;
        double r864838 = x;
        double r864839 = sqrt(r864838);
        double r864840 = r864837 * r864839;
        double r864841 = -0.5;
        double r864842 = y;
        double r864843 = 2.0;
        double r864844 = pow(r864842, r864843);
        double r864845 = 1.0;
        double r864846 = fma(r864841, r864844, r864845);
        double r864847 = r864840 * r864846;
        double r864848 = a;
        double r864849 = b;
        double r864850 = 3.0;
        double r864851 = r864849 * r864850;
        double r864852 = r864848 / r864851;
        double r864853 = r864847 - r864852;
        double r864854 = 1.1983052877371063e+307;
        bool r864855 = r864834 <= r864854;
        double r864856 = cos(r864842);
        double r864857 = cbrt(r864850);
        double r864858 = pow(r864857, r864843);
        double r864859 = r864832 / r864858;
        double r864860 = r864859 * r864833;
        double r864861 = r864860 / r864857;
        double r864862 = cos(r864861);
        double r864863 = r864856 * r864862;
        double r864864 = r864850 / r864833;
        double r864865 = r864832 / r864864;
        double r864866 = sin(r864865);
        double r864867 = cbrt(r864866);
        double r864868 = r864867 * r864867;
        double r864869 = r864868 * r864867;
        double r864870 = sin(r864842);
        double r864871 = -r864870;
        double r864872 = r864869 * r864871;
        double r864873 = r864863 - r864872;
        double r864874 = r864840 * r864873;
        double r864875 = r864874 - r864852;
        double r864876 = exp(r864840);
        double r864877 = r864832 / r864850;
        double r864878 = r864877 * r864833;
        double r864879 = r864842 - r864878;
        double r864880 = cos(r864879);
        double r864881 = pow(r864876, r864880);
        double r864882 = log(r864881);
        double r864883 = r864882 - r864852;
        double r864884 = r864855 ? r864875 : r864883;
        double r864885 = r864836 ? r864853 : r864884;
        return r864885;
}

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	21.5
Target	19.4
Herbie	18.6

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

2. if (* z t) < -inf.0

   1. Initial program 64.0

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

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{2}, {y}^{2}, 1\right)} - \frac{a}{b \cdot 3}\]

   if -inf.0 < (* z t) < 1.1983052877371063e+307

   1. Initial program 14.9

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

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

   4. Applied associate-/r* 14.8

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

   5. Simplified 14.8

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

   7. Applied add-cube-cbrt 14.9

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

   8. Applied associate-*r* 14.9

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

   9. Simplified 14.9

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

   11. Applied sub-neg 14.9

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

   12. Applied cos-sum 14.5

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

   13. Simplified 14.4

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

   14. Simplified 14.3

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

   16. Applied add-cube-cbrt 14.3

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

   17. Simplified 14.4

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

   18. Simplified 14.4

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

   if 1.1983052877371063e+307 < (* z t)

   1. Initial program 64.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 add-cube-cbrt 64.0

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

   4. Applied associate-/r* 64.0

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

   5. Simplified 64.0

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

   7. Applied add-log-exp 64.0

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

   8. Simplified 47.3

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

4. Final simplification 18.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t = -\infty:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \mathsf{fma}\left(\frac{-1}{2}, {y}^{2}, 1\right) - \frac{a}{b \cdot 3}\\ \mathbf{elif}\;z \cdot t \le 1.198305287737106264207051230853461279422 \cdot 10^{307}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{\frac{z}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot t}{\sqrt[3]{3}}\right) - \left(\left(\sqrt[3]{\sin \left(\frac{z}{\frac{3}{t}}\right)} \cdot \sqrt[3]{\sin \left(\frac{z}{\frac{3}{t}}\right)}\right) \cdot \sqrt[3]{\sin \left(\frac{z}{\frac{3}{t}}\right)}\right) \cdot \left(-\sin y\right)\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\log \left({\left(e^{2 \cdot \sqrt{x}}\right)}^{\left(\cos \left(y - \frac{z}{3} \cdot t\right)\right)}\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

herbie shell --seed 2019351 +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))))