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(\left(\sqrt[3]{\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3} \cdot \sqrt[3]{\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3}\right) \cdot \sqrt[3]{\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)double f(double x1, double x2) {
double r41862 = x1;
double r41863 = 2.0;
double r41864 = r41863 * r41862;
double r41865 = 3.0;
double r41866 = r41865 * r41862;
double r41867 = r41866 * r41862;
double r41868 = x2;
double r41869 = r41863 * r41868;
double r41870 = r41867 + r41869;
double r41871 = r41870 - r41862;
double r41872 = r41862 * r41862;
double r41873 = 1.0;
double r41874 = r41872 + r41873;
double r41875 = r41871 / r41874;
double r41876 = r41864 * r41875;
double r41877 = r41875 - r41865;
double r41878 = r41876 * r41877;
double r41879 = 4.0;
double r41880 = r41879 * r41875;
double r41881 = 6.0;
double r41882 = r41880 - r41881;
double r41883 = r41872 * r41882;
double r41884 = r41878 + r41883;
double r41885 = r41884 * r41874;
double r41886 = r41867 * r41875;
double r41887 = r41885 + r41886;
double r41888 = r41872 * r41862;
double r41889 = r41887 + r41888;
double r41890 = r41889 + r41862;
double r41891 = r41867 - r41869;
double r41892 = r41891 - r41862;
double r41893 = r41892 / r41874;
double r41894 = r41865 * r41893;
double r41895 = r41890 + r41894;
double r41896 = r41862 + r41895;
return r41896;
}
double f(double x1, double x2) {
double r41897 = x1;
double r41898 = 2.0;
double r41899 = r41898 * r41897;
double r41900 = 3.0;
double r41901 = r41900 * r41897;
double r41902 = r41901 * r41897;
double r41903 = x2;
double r41904 = r41898 * r41903;
double r41905 = r41902 + r41904;
double r41906 = r41905 - r41897;
double r41907 = r41897 * r41897;
double r41908 = 1.0;
double r41909 = r41907 + r41908;
double r41910 = r41906 / r41909;
double r41911 = r41899 * r41910;
double r41912 = r41910 - r41900;
double r41913 = cbrt(r41912);
double r41914 = r41913 * r41913;
double r41915 = r41914 * r41913;
double r41916 = r41911 * r41915;
double r41917 = 4.0;
double r41918 = r41917 * r41910;
double r41919 = 6.0;
double r41920 = r41918 - r41919;
double r41921 = r41907 * r41920;
double r41922 = r41916 + r41921;
double r41923 = r41922 * r41909;
double r41924 = r41902 * r41910;
double r41925 = r41923 + r41924;
double r41926 = r41907 * r41897;
double r41927 = r41925 + r41926;
double r41928 = r41927 + r41897;
double r41929 = r41902 - r41904;
double r41930 = r41929 - r41897;
double r41931 = r41930 / r41909;
double r41932 = r41900 * r41931;
double r41933 = r41928 + r41932;
double r41934 = r41897 + r41933;
return r41934;
}



Bits error versus x1



Bits error versus x2
Results
Initial program 0.5
rmApplied add-cube-cbrt0.6
Final simplification0.6
herbie shell --seed 2020057
(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))))))