Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.5

Time: 56.8s

Precision: 64

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(x1 \cdot \left(x1 \cdot x1\right) + \left(\left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1} + \left(1 + x1 \cdot x1\right) \cdot \left(\left(\left(x1 \cdot 2\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right) \cdot \mathsf{fma}\left(\frac{1}{\sqrt{1 + x1 \cdot x1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{\sqrt{1 + x1 \cdot x1}}, -3\right) + \left(\left(x1 \cdot x1\right) \cdot \mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}, \left(-\sqrt{6}\right) \cdot \sqrt{6}\right) + \left(x1 \cdot x1\right) \cdot 0\right)\right)\right)\right) + x1\right) + \frac{\left(\left(3 \cdot x1\right) \cdot x1 - x2 \cdot 2\right) - x1}{1 + x1 \cdot x1} \cdot 3\right)\]

C

double f(double x1, double x2) {
        double r2718816 = x1;
        double r2718817 = 2.0;
        double r2718818 = r2718817 * r2718816;
        double r2718819 = 3.0;
        double r2718820 = r2718819 * r2718816;
        double r2718821 = r2718820 * r2718816;
        double r2718822 = x2;
        double r2718823 = r2718817 * r2718822;
        double r2718824 = r2718821 + r2718823;
        double r2718825 = r2718824 - r2718816;
        double r2718826 = r2718816 * r2718816;
        double r2718827 = 1.0;
        double r2718828 = r2718826 + r2718827;
        double r2718829 = r2718825 / r2718828;
        double r2718830 = r2718818 * r2718829;
        double r2718831 = r2718829 - r2718819;
        double r2718832 = r2718830 * r2718831;
        double r2718833 = 4.0;
        double r2718834 = r2718833 * r2718829;
        double r2718835 = 6.0;
        double r2718836 = r2718834 - r2718835;
        double r2718837 = r2718826 * r2718836;
        double r2718838 = r2718832 + r2718837;
        double r2718839 = r2718838 * r2718828;
        double r2718840 = r2718821 * r2718829;
        double r2718841 = r2718839 + r2718840;
        double r2718842 = r2718826 * r2718816;
        double r2718843 = r2718841 + r2718842;
        double r2718844 = r2718843 + r2718816;
        double r2718845 = r2718821 - r2718823;
        double r2718846 = r2718845 - r2718816;
        double r2718847 = r2718846 / r2718828;
        double r2718848 = r2718819 * r2718847;
        double r2718849 = r2718844 + r2718848;
        double r2718850 = r2718816 + r2718849;
        return r2718850;
}

↓

double f(double x1, double x2) {
        double r2718851 = x1;
        double r2718852 = r2718851 * r2718851;
        double r2718853 = r2718851 * r2718852;
        double r2718854 = 3.0;
        double r2718855 = r2718854 * r2718851;
        double r2718856 = r2718855 * r2718851;
        double r2718857 = x2;
        double r2718858 = 2.0;
        double r2718859 = r2718857 * r2718858;
        double r2718860 = r2718856 + r2718859;
        double r2718861 = r2718860 - r2718851;
        double r2718862 = 1.0;
        double r2718863 = r2718862 + r2718852;
        double r2718864 = r2718861 / r2718863;
        double r2718865 = r2718856 * r2718864;
        double r2718866 = r2718851 * r2718858;
        double r2718867 = r2718866 * r2718864;
        double r2718868 = sqrt(r2718863);
        double r2718869 = r2718862 / r2718868;
        double r2718870 = r2718861 / r2718868;
        double r2718871 = -3.0;
        double r2718872 = fma(r2718869, r2718870, r2718871);
        double r2718873 = r2718867 * r2718872;
        double r2718874 = 4.0;
        double r2718875 = 6.0;
        double r2718876 = sqrt(r2718875);
        double r2718877 = -r2718876;
        double r2718878 = r2718877 * r2718876;
        double r2718879 = fma(r2718874, r2718864, r2718878);
        double r2718880 = r2718852 * r2718879;
        double r2718881 = 0.0;
        double r2718882 = r2718852 * r2718881;
        double r2718883 = r2718880 + r2718882;
        double r2718884 = r2718873 + r2718883;
        double r2718885 = r2718863 * r2718884;
        double r2718886 = r2718865 + r2718885;
        double r2718887 = r2718853 + r2718886;
        double r2718888 = r2718887 + r2718851;
        double r2718889 = r2718856 - r2718859;
        double r2718890 = r2718889 - r2718851;
        double r2718891 = r2718890 / r2718863;
        double r2718892 = r2718891 * r2718854;
        double r2718893 = r2718888 + r2718892;
        double r2718894 = r2718851 + r2718893;
        return r2718894;
}

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}{\color{blue}{\sqrt{x1 \cdot x1 + 1} \cdot \sqrt{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)\]

4. Applied *-un-lft-identity 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{\color{blue}{1 \cdot \left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1\right)}}{\sqrt{x1 \cdot x1 + 1} \cdot \sqrt{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)\]

5. Applied times-frac 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(\color{blue}{\frac{1}{\sqrt{x1 \cdot x1 + 1}} \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{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)\]

6. Applied fma-neg 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 \color{blue}{\mathsf{fma}\left(\frac{1}{\sqrt{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{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)\]

7. Simplified 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 \mathsf{fma}\left(\frac{1}{\sqrt{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{x1 \cdot x1 + 1}}, \color{blue}{-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)\]
8. Using strategy rm

9. 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 \mathsf{fma}\left(\frac{1}{\sqrt{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{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} - \color{blue}{\sqrt{6} \cdot \sqrt{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. Applied prod-diff 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 \mathsf{fma}\left(\frac{1}{\sqrt{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{x1 \cdot x1 + 1}}, -3\right) + \left(x1 \cdot x1\right) \cdot \color{blue}{\left(\mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}, -\sqrt{6} \cdot \sqrt{6}\right) + \mathsf{fma}\left(-\sqrt{6}, \sqrt{6}, \sqrt{6} \cdot \sqrt{6}\right)\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)\]

11. Applied distribute-rgt-in 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 \mathsf{fma}\left(\frac{1}{\sqrt{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{x1 \cdot x1 + 1}}, -3\right) + \color{blue}{\left(\mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}, -\sqrt{6} \cdot \sqrt{6}\right) \cdot \left(x1 \cdot x1\right) + \mathsf{fma}\left(-\sqrt{6}, \sqrt{6}, \sqrt{6} \cdot \sqrt{6}\right) \cdot \left(x1 \cdot x1\right)\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)\]

12. Simplified 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 \mathsf{fma}\left(\frac{1}{\sqrt{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{x1 \cdot x1 + 1}}, -3\right) + \left(\mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}, -\sqrt{6} \cdot \sqrt{6}\right) \cdot \left(x1 \cdot x1\right) + \color{blue}{0 \cdot \left(x1 \cdot x1\right)}\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)\]

13. Final simplification 0.5

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

Reproduce

herbie shell --seed 2019135 +o rules:numerics
(FPCore (x1 x2)
  :name "Rosa's FloatVsDoubleBenchmark"
  (+ 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))))))