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

Average Error: 20.2 → 17.4

Time: 32.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 = -\infty \lor \neg \left(z \cdot t \le 3.7752219740464399 \cdot 10^{301}\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(\log \left(e^{\cos \left(0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right) \cdot \cos y + \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 r504780 = 2.0;
        double r504781 = x;
        double r504782 = sqrt(r504781);
        double r504783 = r504780 * r504782;
        double r504784 = y;
        double r504785 = z;
        double r504786 = t;
        double r504787 = r504785 * r504786;
        double r504788 = 3.0;
        double r504789 = r504787 / r504788;
        double r504790 = r504784 - r504789;
        double r504791 = cos(r504790);
        double r504792 = r504783 * r504791;
        double r504793 = a;
        double r504794 = b;
        double r504795 = r504794 * r504788;
        double r504796 = r504793 / r504795;
        double r504797 = r504792 - r504796;
        return r504797;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r504798 = z;
        double r504799 = t;
        double r504800 = r504798 * r504799;
        double r504801 = -inf.0;
        bool r504802 = r504800 <= r504801;
        double r504803 = 3.77522197404644e+301;
        bool r504804 = r504800 <= r504803;
        double r504805 = !r504804;
        bool r504806 = r504802 || r504805;
        double r504807 = 2.0;
        double r504808 = x;
        double r504809 = sqrt(r504808);
        double r504810 = r504807 * r504809;
        double r504811 = 1.0;
        double r504812 = 0.5;
        double r504813 = y;
        double r504814 = 2.0;
        double r504815 = pow(r504813, r504814);
        double r504816 = r504812 * r504815;
        double r504817 = r504811 - r504816;
        double r504818 = r504810 * r504817;
        double r504819 = a;
        double r504820 = b;
        double r504821 = 3.0;
        double r504822 = r504820 * r504821;
        double r504823 = r504819 / r504822;
        double r504824 = r504818 - r504823;
        double r504825 = 0.3333333333333333;
        double r504826 = r504799 * r504798;
        double r504827 = r504825 * r504826;
        double r504828 = cos(r504827);
        double r504829 = exp(r504828);
        double r504830 = log(r504829);
        double r504831 = cos(r504813);
        double r504832 = r504830 * r504831;
        double r504833 = sin(r504813);
        double r504834 = r504800 / r504821;
        double r504835 = sin(r504834);
        double r504836 = cbrt(r504835);
        double r504837 = r504836 * r504836;
        double r504838 = r504837 * r504836;
        double r504839 = r504833 * r504838;
        double r504840 = r504832 + r504839;
        double r504841 = r504810 * r504840;
        double r504842 = r504841 - r504823;
        double r504843 = r504806 ? r504824 : r504842;
        return r504843;
}

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.2
Target	18.2
Herbie	17.4

\[\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) < -inf.0 or 3.77522197404644e+301 < (* z t)

   1. Initial program 63.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 44.5

      \[\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 -inf.0 < (* z t) < 3.77522197404644e+301

   1. Initial program 14.1

      \[\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.5

      \[\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.5

      \[\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. Taylor expanded around inf 13.6

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\color{blue}{\cos \left(0.333333333333333315 \cdot \left(t \cdot z\right)\right)} \cdot \cos y + \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.6

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos \left(0.333333333333333315 \cdot \left(t \cdot z\right)\right) \cdot \cos y + \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}\]
   8. Using strategy rm

   9. Applied add-log-exp 13.6

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\color{blue}{\log \left(e^{\cos \left(0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right)} \cdot \cos y + \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}\]
3. Recombined 2 regimes into one program.

4. Final simplification 17.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t = -\infty \lor \neg \left(z \cdot t \le 3.7752219740464399 \cdot 10^{301}\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(\log \left(e^{\cos \left(0.333333333333333315 \cdot \left(t \cdot z\right)\right)}\right) \cdot \cos y + \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 2019199 
(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.0 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))))