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

Average Error: 20.4 → 17.9

Time: 10.7s

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 -4.4548286609804394 \cdot 10^{283} \lor \neg \left(z \cdot t \le 3.41570283314918143 \cdot 10^{303}\right):\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \left(\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3}\right)} \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3}\right)}\right) + \sin y \cdot \left(\left(\sqrt[3]{\sin \left(\frac{z \cdot t}{3}\right)} \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3}\right)}\right) \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3}\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 r866277 = 2.0;
        double r866278 = x;
        double r866279 = sqrt(r866278);
        double r866280 = r866277 * r866279;
        double r866281 = y;
        double r866282 = z;
        double r866283 = t;
        double r866284 = r866282 * r866283;
        double r866285 = 3.0;
        double r866286 = r866284 / r866285;
        double r866287 = r866281 - r866286;
        double r866288 = cos(r866287);
        double r866289 = r866280 * r866288;
        double r866290 = a;
        double r866291 = b;
        double r866292 = r866291 * r866285;
        double r866293 = r866290 / r866292;
        double r866294 = r866289 - r866293;
        return r866294;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r866295 = z;
        double r866296 = t;
        double r866297 = r866295 * r866296;
        double r866298 = -4.454828660980439e+283;
        bool r866299 = r866297 <= r866298;
        double r866300 = 3.4157028331491814e+303;
        bool r866301 = r866297 <= r866300;
        double r866302 = !r866301;
        bool r866303 = r866299 || r866302;
        double r866304 = 2.0;
        double r866305 = x;
        double r866306 = sqrt(r866305);
        double r866307 = r866304 * r866306;
        double r866308 = 1.0;
        double r866309 = 0.5;
        double r866310 = y;
        double r866311 = 2.0;
        double r866312 = pow(r866310, r866311);
        double r866313 = r866309 * r866312;
        double r866314 = r866308 - r866313;
        double r866315 = r866307 * r866314;
        double r866316 = a;
        double r866317 = b;
        double r866318 = 3.0;
        double r866319 = r866317 * r866318;
        double r866320 = r866316 / r866319;
        double r866321 = r866315 - r866320;
        double r866322 = cos(r866310);
        double r866323 = r866297 / r866318;
        double r866324 = cos(r866323);
        double r866325 = cbrt(r866324);
        double r866326 = r866325 * r866325;
        double r866327 = r866326 * r866325;
        double r866328 = r866322 * r866327;
        double r866329 = sin(r866310);
        double r866330 = sin(r866323);
        double r866331 = cbrt(r866330);
        double r866332 = r866331 * r866331;
        double r866333 = r866332 * r866331;
        double r866334 = r866329 * r866333;
        double r866335 = r866328 + r866334;
        double r866336 = r866307 * r866335;
        double r866337 = r866336 - r866320;
        double r866338 = r866303 ? r866321 : r866337;
        return r866338;
}

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.4
Herbie	17.9

\[\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 (* z t) < -4.454828660980439e+283 or 3.4157028331491814e+303 < (* z t)

   1. Initial program 61.3

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

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

   if -4.454828660980439e+283 < (* z t) < 3.4157028331491814e+303

   1. Initial program 13.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 cos-diff 13.3

      \[\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. Using strategy rm

   5. Applied add-cube-cbrt 13.3

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

   7. Applied add-cube-cbrt 13.3

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

4. Final simplification 17.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t \le -4.4548286609804394 \cdot 10^{283} \lor \neg \left(z \cdot t \le 3.41570283314918143 \cdot 10^{303}\right):\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \left(\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3}\right)} \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3}\right)}\right) + \sin y \cdot \left(\left(\sqrt[3]{\sin \left(\frac{z \cdot t}{3}\right)} \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3}\right)}\right) \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3}\right)}\right)\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

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