Average Error: 0.5 → 0.5
Time: 54.0s
Precision: 64
\[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(x1 + \left(\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(\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(\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1, \frac{1}{1 + x1 \cdot x1}, -3\right) + \left(6 \cdot \left(-x1 \cdot x1\right) + \left(x1 \cdot x1\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1} \cdot 4\right)\right)\right) \cdot \left(1 + x1 \cdot x1\right)\right) + x1 \cdot \left(x1 \cdot x1\right)\right)\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\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(\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(x1 + \left(\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(\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(\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1, \frac{1}{1 + x1 \cdot x1}, -3\right) + \left(6 \cdot \left(-x1 \cdot x1\right) + \left(x1 \cdot x1\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1} \cdot 4\right)\right)\right) \cdot \left(1 + x1 \cdot x1\right)\right) + x1 \cdot \left(x1 \cdot x1\right)\right)\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right)
double f(double x1, double x2) {
        double r2857837 = x1;
        double r2857838 = 2.0;
        double r2857839 = r2857838 * r2857837;
        double r2857840 = 3.0;
        double r2857841 = r2857840 * r2857837;
        double r2857842 = r2857841 * r2857837;
        double r2857843 = x2;
        double r2857844 = r2857838 * r2857843;
        double r2857845 = r2857842 + r2857844;
        double r2857846 = r2857845 - r2857837;
        double r2857847 = r2857837 * r2857837;
        double r2857848 = 1.0;
        double r2857849 = r2857847 + r2857848;
        double r2857850 = r2857846 / r2857849;
        double r2857851 = r2857839 * r2857850;
        double r2857852 = r2857850 - r2857840;
        double r2857853 = r2857851 * r2857852;
        double r2857854 = 4.0;
        double r2857855 = r2857854 * r2857850;
        double r2857856 = 6.0;
        double r2857857 = r2857855 - r2857856;
        double r2857858 = r2857847 * r2857857;
        double r2857859 = r2857853 + r2857858;
        double r2857860 = r2857859 * r2857849;
        double r2857861 = r2857842 * r2857850;
        double r2857862 = r2857860 + r2857861;
        double r2857863 = r2857847 * r2857837;
        double r2857864 = r2857862 + r2857863;
        double r2857865 = r2857864 + r2857837;
        double r2857866 = r2857842 - r2857844;
        double r2857867 = r2857866 - r2857837;
        double r2857868 = r2857867 / r2857849;
        double r2857869 = r2857840 * r2857868;
        double r2857870 = r2857865 + r2857869;
        double r2857871 = r2857837 + r2857870;
        return r2857871;
}
↓
double f(double x1, double x2) {
        double r2857872 = x1;
        double r2857873 = 3.0;
        double r2857874 = r2857873 * r2857872;
        double r2857875 = r2857874 * r2857872;
        double r2857876 = x2;
        double r2857877 = 2.0;
        double r2857878 = r2857876 * r2857877;
        double r2857879 = r2857875 + r2857878;
        double r2857880 = r2857879 - r2857872;
        double r2857881 = 1.0;
        double r2857882 = r2857872 * r2857872;
        double r2857883 = r2857881 + r2857882;
        double r2857884 = r2857880 / r2857883;
        double r2857885 = r2857875 * r2857884;
        double r2857886 = r2857872 * r2857877;
        double r2857887 = r2857886 * r2857884;
        double r2857888 = 1.0;
        double r2857889 = r2857888 / r2857883;
        double r2857890 = -r2857873;
        double r2857891 = fma(r2857880, r2857889, r2857890);
        double r2857892 = r2857887 * r2857891;
        double r2857893 = 6.0;
        double r2857894 = -r2857882;
        double r2857895 = r2857893 * r2857894;
        double r2857896 = 4.0;
        double r2857897 = r2857884 * r2857896;
        double r2857898 = r2857882 * r2857897;
        double r2857899 = r2857895 + r2857898;
        double r2857900 = r2857892 + r2857899;
        double r2857901 = r2857900 * r2857883;
        double r2857902 = r2857885 + r2857901;
        double r2857903 = r2857872 * r2857882;
        double r2857904 = r2857902 + r2857903;
        double r2857905 = r2857872 + r2857904;
        double r2857906 = r2857875 - r2857878;
        double r2857907 = r2857906 - r2857872;
        double r2857908 = r2857907 / r2857883;
        double r2857909 = r2857873 * r2857908;
        double r2857910 = r2857905 + r2857909;
        double r2857911 = r2857872 + r2857910;
        return r2857911;
}

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 sub-neg0.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} - 3\right) + \left(x1 \cdot x1\right) \cdot \color{blue}{\left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} + \left(-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)\]

  4. Applied distribute-rgt-in0.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} - 3\right) + \color{blue}{\left(\left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(x1 \cdot x1\right) + \left(-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)\]
  5. Using strategy rm

  6. Applied div-inv0.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}{\left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1\right) \cdot \frac{1}{x1 \cdot x1 + 1}} - 3\right) + \left(\left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(x1 \cdot x1\right) + \left(-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)\]

  7. Applied fma-neg0.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(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1, \frac{1}{x1 \cdot x1 + 1}, -3\right)} + \left(\left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(x1 \cdot x1\right) + \left(-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)\]

  8. Final simplification0.5

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

Reproduce

herbie shell --seed 2019171 +o rules:numerics
(FPCore (x1 x2)
  :name "Rosa's FloatVsDoubleBenchmark"
  (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2.0 x1) (/ (- (+ (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0))) (- (/ (- (+ (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0)) 3.0)) (* (* x1 x1) (- (* 4.0 (/ (- (+ (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0))) 6.0))) (+ (* x1 x1) 1.0)) (* (* (* 3.0 x1) x1) (/ (- (+ (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0)))) (* (* x1 x1) x1)) x1) (* 3.0 (/ (- (- (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0))))))