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

Average Error: 20.3 → 18.2

Time: 32.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}\;\cos \left(y - \frac{t \cdot z}{3.0}\right) \le 0.9986672325437655:\\ \;\;\;\;\left(\left(\log \left(e^{\cos \left(\left(t \cdot z\right) \cdot 0.3333333333333333\right)}\right) \cdot \cos y\right) \cdot \left(\sqrt{x} \cdot 2.0\right) + \left(\sin \left(\left(t \cdot z\right) \cdot 0.3333333333333333\right) \cdot \sin y\right) \cdot \left(\sqrt{x} \cdot 2.0\right)\right) - \frac{a}{b \cdot 3.0}\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \left(1 - \frac{1}{2} \cdot \left(y \cdot y\right)\right) - \frac{a}{b \cdot 3.0}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r32213538 = 2.0;
        double r32213539 = x;
        double r32213540 = sqrt(r32213539);
        double r32213541 = r32213538 * r32213540;
        double r32213542 = y;
        double r32213543 = z;
        double r32213544 = t;
        double r32213545 = r32213543 * r32213544;
        double r32213546 = 3.0;
        double r32213547 = r32213545 / r32213546;
        double r32213548 = r32213542 - r32213547;
        double r32213549 = cos(r32213548);
        double r32213550 = r32213541 * r32213549;
        double r32213551 = a;
        double r32213552 = b;
        double r32213553 = r32213552 * r32213546;
        double r32213554 = r32213551 / r32213553;
        double r32213555 = r32213550 - r32213554;
        return r32213555;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r32213556 = y;
        double r32213557 = t;
        double r32213558 = z;
        double r32213559 = r32213557 * r32213558;
        double r32213560 = 3.0;
        double r32213561 = r32213559 / r32213560;
        double r32213562 = r32213556 - r32213561;
        double r32213563 = cos(r32213562);
        double r32213564 = 0.9986672325437655;
        bool r32213565 = r32213563 <= r32213564;
        double r32213566 = 0.3333333333333333;
        double r32213567 = r32213559 * r32213566;
        double r32213568 = cos(r32213567);
        double r32213569 = exp(r32213568);
        double r32213570 = log(r32213569);
        double r32213571 = cos(r32213556);
        double r32213572 = r32213570 * r32213571;
        double r32213573 = x;
        double r32213574 = sqrt(r32213573);
        double r32213575 = 2.0;
        double r32213576 = r32213574 * r32213575;
        double r32213577 = r32213572 * r32213576;
        double r32213578 = sin(r32213567);
        double r32213579 = sin(r32213556);
        double r32213580 = r32213578 * r32213579;
        double r32213581 = r32213580 * r32213576;
        double r32213582 = r32213577 + r32213581;
        double r32213583 = a;
        double r32213584 = b;
        double r32213585 = r32213584 * r32213560;
        double r32213586 = r32213583 / r32213585;
        double r32213587 = r32213582 - r32213586;
        double r32213588 = 1.0;
        double r32213589 = 0.5;
        double r32213590 = r32213556 * r32213556;
        double r32213591 = r32213589 * r32213590;
        double r32213592 = r32213588 - r32213591;
        double r32213593 = r32213576 * r32213592;
        double r32213594 = r32213593 - r32213586;
        double r32213595 = r32213565 ? r32213587 : r32213594;
        return r32213595;
}

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.3
Target	18.6
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 (cos (- y (/ (* z t) 3.0))) < 0.9986672325437655

   1. Initial program 20.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 cos-diff 19.4

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

   4. Applied distribute-rgt-in 19.4

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

   5. Taylor expanded around inf 19.4

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

   6. Taylor expanded around inf 19.4

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

   8. Applied add-log-exp 19.4

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

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

   1. Initial program 20.6

      \[\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. Taylor expanded around 0 16.3

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

   3. Simplified 16.3

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(1 - \left(y \cdot y\right) \cdot \frac{1}{2}\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}\;\cos \left(y - \frac{t \cdot z}{3.0}\right) \le 0.9986672325437655:\\ \;\;\;\;\left(\left(\log \left(e^{\cos \left(\left(t \cdot z\right) \cdot 0.3333333333333333\right)}\right) \cdot \cos y\right) \cdot \left(\sqrt{x} \cdot 2.0\right) + \left(\sin \left(\left(t \cdot z\right) \cdot 0.3333333333333333\right) \cdot \sin y\right) \cdot \left(\sqrt{x} \cdot 2.0\right)\right) - \frac{a}{b \cdot 3.0}\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \left(1 - \frac{1}{2} \cdot \left(y \cdot y\right)\right) - \frac{a}{b \cdot 3.0}\\ \end{array}\]

Reproduce

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