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

Average Error: 20.1 → 17.7

Time: 12.5s

Precision: 64

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}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.99996223690193053:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) - \sin y \cdot \left(\left(\sqrt[3]{\sin \left(-\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right)} \cdot \sqrt[3]{\sin \left(-\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right)}\right) \cdot \sqrt[3]{\sin \left(-\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\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}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r832076 = 2.0;
        double r832077 = x;
        double r832078 = sqrt(r832077);
        double r832079 = r832076 * r832078;
        double r832080 = y;
        double r832081 = z;
        double r832082 = t;
        double r832083 = r832081 * r832082;
        double r832084 = 3.0;
        double r832085 = r832083 / r832084;
        double r832086 = r832080 - r832085;
        double r832087 = cos(r832086);
        double r832088 = r832079 * r832087;
        double r832089 = a;
        double r832090 = b;
        double r832091 = r832090 * r832084;
        double r832092 = r832089 / r832091;
        double r832093 = r832088 - r832092;
        return r832093;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r832094 = y;
        double r832095 = z;
        double r832096 = t;
        double r832097 = r832095 * r832096;
        double r832098 = 3.0;
        double r832099 = r832097 / r832098;
        double r832100 = r832094 - r832099;
        double r832101 = cos(r832100);
        double r832102 = 0.9999622369019305;
        bool r832103 = r832101 <= r832102;
        double r832104 = 2.0;
        double r832105 = x;
        double r832106 = sqrt(r832105);
        double r832107 = r832104 * r832106;
        double r832108 = cos(r832094);
        double r832109 = cbrt(r832099);
        double r832110 = r832109 * r832109;
        double r832111 = r832110 * r832109;
        double r832112 = cos(r832111);
        double r832113 = r832108 * r832112;
        double r832114 = sin(r832094);
        double r832115 = -r832111;
        double r832116 = sin(r832115);
        double r832117 = cbrt(r832116);
        double r832118 = r832117 * r832117;
        double r832119 = r832118 * r832117;
        double r832120 = r832114 * r832119;
        double r832121 = r832113 - r832120;
        double r832122 = r832107 * r832121;
        double r832123 = a;
        double r832124 = b;
        double r832125 = r832124 * r832098;
        double r832126 = r832123 / r832125;
        double r832127 = r832122 - r832126;
        double r832128 = 1.0;
        double r832129 = 0.5;
        double r832130 = 2.0;
        double r832131 = pow(r832094, r832130);
        double r832132 = r832129 * r832131;
        double r832133 = r832128 - r832132;
        double r832134 = r832107 * r832133;
        double r832135 = r832134 - r832126;
        double r832136 = r832103 ? r832127 : r832135;
        return r832136;
}

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.1
Target	18.6
Herbie	17.7

\[\begin{array}{l} \mathbf{if}\;z \lt -1.379333748723514 \cdot 10^{129}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.333333333333333315}{z}}{t}\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{elif}\;z \lt 3.51629061355598715 \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.333333333333333315}{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 (cos (- y (/ (* z t) 3.0))) < 0.9999622369019305

   1. Initial program 19.7

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

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

   5. Applied sub-neg 19.7

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

   6. Applied cos-sum 19.1

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

   7. Simplified 19.1

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

   9. Applied add-cube-cbrt 19.1

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

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

   1. Initial program 21.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 15.3

      \[\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 simplification 17.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.99996223690193053:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) - \sin y \cdot \left(\left(\sqrt[3]{\sin \left(-\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right)} \cdot \sqrt[3]{\sin \left(-\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right)}\right) \cdot \sqrt[3]{\sin \left(-\left(\sqrt[3]{\frac{z \cdot t}{3}} \cdot \sqrt[3]{\frac{z \cdot t}{3}}\right) \cdot \sqrt[3]{\frac{z \cdot t}{3}}\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 2020065 
(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))))