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

Average Error: 20.5 → 17.5

Time: 16.5s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

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 -1.4153686713047554694536085848185002123 \cdot 10^{302} \lor \neg \left(z \cdot t \le 8.738587929750899877247276628793759210701 \cdot 10^{305}\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(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) + \left(\sqrt[3]{\left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right)} \cdot \sqrt[3]{\left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right)}\right) \cdot \sqrt[3]{\left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right)}\right) - \frac{\frac{a}{3}}{b}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r775658 = 2.0;
        double r775659 = x;
        double r775660 = sqrt(r775659);
        double r775661 = r775658 * r775660;
        double r775662 = y;
        double r775663 = z;
        double r775664 = t;
        double r775665 = r775663 * r775664;
        double r775666 = 3.0;
        double r775667 = r775665 / r775666;
        double r775668 = r775662 - r775667;
        double r775669 = cos(r775668);
        double r775670 = r775661 * r775669;
        double r775671 = a;
        double r775672 = b;
        double r775673 = r775672 * r775666;
        double r775674 = r775671 / r775673;
        double r775675 = r775670 - r775674;
        return r775675;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r775676 = z;
        double r775677 = t;
        double r775678 = r775676 * r775677;
        double r775679 = -1.4153686713047555e+302;
        bool r775680 = r775678 <= r775679;
        double r775681 = 8.7385879297509e+305;
        bool r775682 = r775678 <= r775681;
        double r775683 = !r775682;
        bool r775684 = r775680 || r775683;
        double r775685 = 2.0;
        double r775686 = x;
        double r775687 = sqrt(r775686);
        double r775688 = r775685 * r775687;
        double r775689 = 1.0;
        double r775690 = 0.5;
        double r775691 = y;
        double r775692 = 2.0;
        double r775693 = pow(r775691, r775692);
        double r775694 = r775690 * r775693;
        double r775695 = r775689 - r775694;
        double r775696 = r775688 * r775695;
        double r775697 = a;
        double r775698 = b;
        double r775699 = 3.0;
        double r775700 = r775698 * r775699;
        double r775701 = r775697 / r775700;
        double r775702 = r775696 - r775701;
        double r775703 = cos(r775691);
        double r775704 = r775678 / r775699;
        double r775705 = cos(r775704);
        double r775706 = r775703 * r775705;
        double r775707 = r775688 * r775706;
        double r775708 = sin(r775691);
        double r775709 = sin(r775704);
        double r775710 = r775708 * r775709;
        double r775711 = r775688 * r775710;
        double r775712 = cbrt(r775711);
        double r775713 = r775712 * r775712;
        double r775714 = r775713 * r775712;
        double r775715 = r775707 + r775714;
        double r775716 = r775697 / r775699;
        double r775717 = r775716 / r775698;
        double r775718 = r775715 - r775717;
        double r775719 = r775684 ? r775702 : r775718;
        return r775719;
}

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.5
Target	18.2
Herbie	17.5

\[\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) < -1.4153686713047555e+302 or 8.7385879297509e+305 < (* z t)

   1. Initial program 63.4

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

      \[\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 -1.4153686713047555e+302 < (* z t) < 8.7385879297509e+305

   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.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. Applied distribute-lft-in 13.6

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

   6. Applied *-un-lft-identity 13.6

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

   7. Applied times-frac 13.7

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

   9. Applied *-un-lft-identity 13.7

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

   10. Applied *-un-lft-identity 13.7

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

   11. Applied times-frac 13.7

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

   12. Applied associate-*l* 13.7

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

   13. Simplified 13.6

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

   15. Applied add-cube-cbrt 13.6

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

4. Final simplification 17.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t \le -1.4153686713047554694536085848185002123 \cdot 10^{302} \lor \neg \left(z \cdot t \le 8.738587929750899877247276628793759210701 \cdot 10^{305}\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(\left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) + \left(\sqrt[3]{\left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right)} \cdot \sqrt[3]{\left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right)}\right) \cdot \sqrt[3]{\left(2 \cdot \sqrt{x}\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3}\right)\right)}\right) - \frac{\frac{a}{3}}{b}\\ \end{array}\]

Reproduce

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