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

Average Error: 20.8 → 18.3

Time: 23.9s

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}\;z \cdot t \le -2.418581585015837595406771209894118464699 \cdot 10^{292} \lor \neg \left(z \cdot t \le 6.778510233185830423934873284353389767199 \cdot 10^{301}\right):\\ \;\;\;\;\log \left({\left(e^{2 \cdot \sqrt{x}}\right)}^{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right) + \cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right)}\right) - \frac{\frac{a}{b}}{3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\left(\log \left(\sqrt{e^{\cos \left(\frac{z \cdot t}{3}\right)}}\right) + \log \left(\sqrt{e^{\cos \left(\frac{z \cdot t}{3}\right)}}\right)\right) \cdot \cos y + \sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) - \frac{\frac{a}{b}}{3}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r500106 = 2.0;
        double r500107 = x;
        double r500108 = sqrt(r500107);
        double r500109 = r500106 * r500108;
        double r500110 = y;
        double r500111 = z;
        double r500112 = t;
        double r500113 = r500111 * r500112;
        double r500114 = 3.0;
        double r500115 = r500113 / r500114;
        double r500116 = r500110 - r500115;
        double r500117 = cos(r500116);
        double r500118 = r500109 * r500117;
        double r500119 = a;
        double r500120 = b;
        double r500121 = r500120 * r500114;
        double r500122 = r500119 / r500121;
        double r500123 = r500118 - r500122;
        return r500123;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r500124 = z;
        double r500125 = t;
        double r500126 = r500124 * r500125;
        double r500127 = -2.4185815850158376e+292;
        bool r500128 = r500126 <= r500127;
        double r500129 = 6.77851023318583e+301;
        bool r500130 = r500126 <= r500129;
        double r500131 = !r500130;
        bool r500132 = r500128 || r500131;
        double r500133 = 2.0;
        double r500134 = x;
        double r500135 = sqrt(r500134);
        double r500136 = r500133 * r500135;
        double r500137 = exp(r500136);
        double r500138 = y;
        double r500139 = sin(r500138);
        double r500140 = 3.0;
        double r500141 = r500126 / r500140;
        double r500142 = sin(r500141);
        double r500143 = r500139 * r500142;
        double r500144 = cos(r500141);
        double r500145 = cos(r500138);
        double r500146 = r500144 * r500145;
        double r500147 = r500143 + r500146;
        double r500148 = pow(r500137, r500147);
        double r500149 = log(r500148);
        double r500150 = a;
        double r500151 = b;
        double r500152 = r500150 / r500151;
        double r500153 = r500152 / r500140;
        double r500154 = r500149 - r500153;
        double r500155 = exp(r500144);
        double r500156 = sqrt(r500155);
        double r500157 = log(r500156);
        double r500158 = r500157 + r500157;
        double r500159 = r500158 * r500145;
        double r500160 = r500159 + r500143;
        double r500161 = r500136 * r500160;
        double r500162 = r500161 - r500153;
        double r500163 = r500132 ? r500154 : r500162;
        return r500163;
}

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.8
Target	18.7
Herbie	18.3

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

2. if (* z t) < -2.4185815850158376e+292 or 6.77851023318583e+301 < (* z t)

   1. Initial program 61.8

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

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

   4. Simplified 61.8

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

   6. Applied associate-/r* 61.8

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

   8. Applied add-log-exp 61.8

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

   10. Applied add-log-exp 62.6

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

   11. Simplified 47.1

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

   if -2.4185815850158376e+292 < (* z t) < 6.77851023318583e+301

   1. Initial program 14.2

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

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

   4. Simplified 13.6

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

   6. Applied associate-/r* 13.6

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

   8. Applied add-log-exp 13.6

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

   10. Applied add-sqr-sqrt 13.6

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

   11. Applied log-prod 13.6

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

4. Final simplification 18.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t \le -2.418581585015837595406771209894118464699 \cdot 10^{292} \lor \neg \left(z \cdot t \le 6.778510233185830423934873284353389767199 \cdot 10^{301}\right):\\ \;\;\;\;\log \left({\left(e^{2 \cdot \sqrt{x}}\right)}^{\left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right) + \cos \left(\frac{z \cdot t}{3}\right) \cdot \cos y\right)}\right) - \frac{\frac{a}{b}}{3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\left(\log \left(\sqrt{e^{\cos \left(\frac{z \cdot t}{3}\right)}}\right) + \log \left(\sqrt{e^{\cos \left(\frac{z \cdot t}{3}\right)}}\right)\right) \cdot \cos y + \sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right) - \frac{\frac{a}{b}}{3}\\ \end{array}\]

Reproduce

herbie shell --seed 2019305 
(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.379333748723514e129) (- (* (* 2 (sqrt x)) (cos (- (/ 1 y) (/ (/ 0.333333333333333315 z) t)))) (/ (/ a 3) b)) (if (< z 3.51629061355598715e106) (- (* (* (sqrt x) 2) (cos (- y (* (/ t 3) z)))) (/ (/ a 3) b)) (- (* (cos (- y (/ (/ 0.333333333333333315 z) t))) (* 2 (sqrt x))) (/ (/ a b) 3))))

  (- (* (* 2 (sqrt x)) (cos (- y (/ (* z t) 3)))) (/ a (* b 3))))