Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.7

Time: 19.5s

Precision: 64

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

Math

\[x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

↓

\[x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\mathsf{fma}\left(\frac{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}{\frac{\sqrt{\mathsf{fma}\left(x1, x1, 1\right)}}{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}}, \frac{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}{\sqrt{\mathsf{fma}\left(x1, x1, 1\right)}}, -3\right) + \left(\left(-3\right) + 3\right)\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

C

double f(double x1, double x2) {
        double r68590 = x1;
        double r68591 = 2.0;
        double r68592 = r68591 * r68590;
        double r68593 = 3.0;
        double r68594 = r68593 * r68590;
        double r68595 = r68594 * r68590;
        double r68596 = x2;
        double r68597 = r68591 * r68596;
        double r68598 = r68595 + r68597;
        double r68599 = r68598 - r68590;
        double r68600 = r68590 * r68590;
        double r68601 = 1.0;
        double r68602 = r68600 + r68601;
        double r68603 = r68599 / r68602;
        double r68604 = r68592 * r68603;
        double r68605 = r68603 - r68593;
        double r68606 = r68604 * r68605;
        double r68607 = 4.0;
        double r68608 = r68607 * r68603;
        double r68609 = 6.0;
        double r68610 = r68608 - r68609;
        double r68611 = r68600 * r68610;
        double r68612 = r68606 + r68611;
        double r68613 = r68612 * r68602;
        double r68614 = r68595 * r68603;
        double r68615 = r68613 + r68614;
        double r68616 = r68600 * r68590;
        double r68617 = r68615 + r68616;
        double r68618 = r68617 + r68590;
        double r68619 = r68595 - r68597;
        double r68620 = r68619 - r68590;
        double r68621 = r68620 / r68602;
        double r68622 = r68593 * r68621;
        double r68623 = r68618 + r68622;
        double r68624 = r68590 + r68623;
        return r68624;
}

↓

double f(double x1, double x2) {
        double r68625 = x1;
        double r68626 = 2.0;
        double r68627 = r68626 * r68625;
        double r68628 = 3.0;
        double r68629 = r68628 * r68625;
        double r68630 = r68629 * r68625;
        double r68631 = x2;
        double r68632 = r68626 * r68631;
        double r68633 = r68630 + r68632;
        double r68634 = r68633 - r68625;
        double r68635 = r68625 * r68625;
        double r68636 = 1.0;
        double r68637 = r68635 + r68636;
        double r68638 = r68634 / r68637;
        double r68639 = r68627 * r68638;
        double r68640 = fma(r68629, r68625, r68632);
        double r68641 = r68640 - r68625;
        double r68642 = cbrt(r68641);
        double r68643 = fma(r68625, r68625, r68636);
        double r68644 = sqrt(r68643);
        double r68645 = r68644 / r68642;
        double r68646 = r68642 / r68645;
        double r68647 = r68642 / r68644;
        double r68648 = -r68628;
        double r68649 = fma(r68646, r68647, r68648);
        double r68650 = r68648 + r68628;
        double r68651 = r68649 + r68650;
        double r68652 = r68639 * r68651;
        double r68653 = 4.0;
        double r68654 = r68653 * r68638;
        double r68655 = 6.0;
        double r68656 = r68654 - r68655;
        double r68657 = r68635 * r68656;
        double r68658 = r68652 + r68657;
        double r68659 = r68658 * r68637;
        double r68660 = r68630 * r68638;
        double r68661 = r68659 + r68660;
        double r68662 = r68635 * r68625;
        double r68663 = r68661 + r68662;
        double r68664 = r68663 + r68625;
        double r68665 = r68630 - r68632;
        double r68666 = r68665 - r68625;
        double r68667 = r68666 / r68637;
        double r68668 = r68628 * r68667;
        double r68669 = r68664 + r68668;
        double r68670 = r68625 + r68669;
        return r68670;
}

Error

Bits error versus x1

Bits error versus x2

Derivation

1. Initial program 0.5

   \[x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]
2. Using strategy rm

3. Applied add-sqr-sqrt 0.5

   \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - \color{blue}{\sqrt{3} \cdot \sqrt{3}}\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

4. Applied add-sqr-sqrt 0.5

   \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\color{blue}{\sqrt{x1 \cdot x1 + 1} \cdot \sqrt{x1 \cdot x1 + 1}}} - \sqrt{3} \cdot \sqrt{3}\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

5. Applied add-cube-cbrt 0.7

   \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\color{blue}{\left(\sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1} \cdot \sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}\right) \cdot \sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}}}{\sqrt{x1 \cdot x1 + 1} \cdot \sqrt{x1 \cdot x1 + 1}} - \sqrt{3} \cdot \sqrt{3}\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

6. Applied times-frac 0.7

   \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\color{blue}{\frac{\sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1} \cdot \sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}}{\sqrt{x1 \cdot x1 + 1}} \cdot \frac{\sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}}{\sqrt{x1 \cdot x1 + 1}}} - \sqrt{3} \cdot \sqrt{3}\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

7. Applied prod-diff 0.7

   \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \color{blue}{\left(\mathsf{fma}\left(\frac{\sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1} \cdot \sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}}{\sqrt{x1 \cdot x1 + 1}}, \frac{\sqrt[3]{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}}{\sqrt{x1 \cdot x1 + 1}}, -\sqrt{3} \cdot \sqrt{3}\right) + \mathsf{fma}\left(-\sqrt{3}, \sqrt{3}, \sqrt{3} \cdot \sqrt{3}\right)\right)} + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

8. Simplified 0.7

   \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\color{blue}{\mathsf{fma}\left(\frac{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}{\frac{\sqrt{\mathsf{fma}\left(x1, x1, 1\right)}}{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}}, \frac{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}{\sqrt{\mathsf{fma}\left(x1, x1, 1\right)}}, -3\right)} + \mathsf{fma}\left(-\sqrt{3}, \sqrt{3}, \sqrt{3} \cdot \sqrt{3}\right)\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

9. Simplified 0.7

   \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\mathsf{fma}\left(\frac{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}{\frac{\sqrt{\mathsf{fma}\left(x1, x1, 1\right)}}{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}}, \frac{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}{\sqrt{\mathsf{fma}\left(x1, x1, 1\right)}}, -3\right) + \color{blue}{\left(\left(-3\right) + 3\right)}\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

10. Final simplification 0.7

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\mathsf{fma}\left(\frac{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}{\frac{\sqrt{\mathsf{fma}\left(x1, x1, 1\right)}}{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}}, \frac{\sqrt[3]{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}}{\sqrt{\mathsf{fma}\left(x1, x1, 1\right)}}, -3\right) + \left(\left(-3\right) + 3\right)\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

Reproduce

herbie shell --seed 2020047 +o rules:numerics
(FPCore (x1 x2)
  :name "Rosa's FloatVsDoubleBenchmark"
  :precision binary64
  (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))))