Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.7

Time: 20.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 r68717 = x1;
        double r68718 = 2.0;
        double r68719 = r68718 * r68717;
        double r68720 = 3.0;
        double r68721 = r68720 * r68717;
        double r68722 = r68721 * r68717;
        double r68723 = x2;
        double r68724 = r68718 * r68723;
        double r68725 = r68722 + r68724;
        double r68726 = r68725 - r68717;
        double r68727 = r68717 * r68717;
        double r68728 = 1.0;
        double r68729 = r68727 + r68728;
        double r68730 = r68726 / r68729;
        double r68731 = r68719 * r68730;
        double r68732 = r68730 - r68720;
        double r68733 = r68731 * r68732;
        double r68734 = 4.0;
        double r68735 = r68734 * r68730;
        double r68736 = 6.0;
        double r68737 = r68735 - r68736;
        double r68738 = r68727 * r68737;
        double r68739 = r68733 + r68738;
        double r68740 = r68739 * r68729;
        double r68741 = r68722 * r68730;
        double r68742 = r68740 + r68741;
        double r68743 = r68727 * r68717;
        double r68744 = r68742 + r68743;
        double r68745 = r68744 + r68717;
        double r68746 = r68722 - r68724;
        double r68747 = r68746 - r68717;
        double r68748 = r68747 / r68729;
        double r68749 = r68720 * r68748;
        double r68750 = r68745 + r68749;
        double r68751 = r68717 + r68750;
        return r68751;
}

↓

double f(double x1, double x2) {
        double r68752 = x1;
        double r68753 = 2.0;
        double r68754 = r68753 * r68752;
        double r68755 = 3.0;
        double r68756 = r68755 * r68752;
        double r68757 = r68756 * r68752;
        double r68758 = x2;
        double r68759 = r68753 * r68758;
        double r68760 = r68757 + r68759;
        double r68761 = r68760 - r68752;
        double r68762 = r68752 * r68752;
        double r68763 = 1.0;
        double r68764 = r68762 + r68763;
        double r68765 = r68761 / r68764;
        double r68766 = r68754 * r68765;
        double r68767 = fma(r68756, r68752, r68759);
        double r68768 = r68767 - r68752;
        double r68769 = cbrt(r68768);
        double r68770 = fma(r68752, r68752, r68763);
        double r68771 = sqrt(r68770);
        double r68772 = r68771 / r68769;
        double r68773 = r68769 / r68772;
        double r68774 = r68769 / r68771;
        double r68775 = -r68755;
        double r68776 = fma(r68773, r68774, r68775);
        double r68777 = r68775 + r68755;
        double r68778 = r68776 + r68777;
        double r68779 = r68766 * r68778;
        double r68780 = 4.0;
        double r68781 = r68780 * r68765;
        double r68782 = 6.0;
        double r68783 = r68781 - r68782;
        double r68784 = r68762 * r68783;
        double r68785 = r68779 + r68784;
        double r68786 = r68785 * r68764;
        double r68787 = r68757 * r68765;
        double r68788 = r68786 + r68787;
        double r68789 = r68762 * r68752;
        double r68790 = r68788 + r68789;
        double r68791 = r68790 + r68752;
        double r68792 = r68757 - r68759;
        double r68793 = r68792 - r68752;
        double r68794 = r68793 / r68764;
        double r68795 = r68755 * r68794;
        double r68796 = r68791 + r68795;
        double r68797 = r68752 + r68796;
        return r68797;
}

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))))))