Average Error: 0.5 → 0.5
Time: 57.7s
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)\]
↓
\[\left(\left(\left(\left(\left(\left(\frac{\left(\left(\left(3 \cdot x1\right) \cdot x1 - x1\right) + x2 \cdot 2\right) \cdot 4}{1 + x1 \cdot x1} \cdot \left(x1 \cdot x1\right) + \left(6 \cdot x1\right) \cdot \left(-x1\right)\right) + \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 \left(\frac{\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2}{1 + x1 \cdot x1} - \left(3 + \frac{x1}{1 + x1 \cdot x1}\right)\right)\right) \cdot \left(1 + x1 \cdot x1\right) + \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}\right) + x1 \cdot \left(x1 \cdot x1\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) + x1\]
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)
↓
\left(\left(\left(\left(\left(\left(\frac{\left(\left(\left(3 \cdot x1\right) \cdot x1 - x1\right) + x2 \cdot 2\right) \cdot 4}{1 + x1 \cdot x1} \cdot \left(x1 \cdot x1\right) + \left(6 \cdot x1\right) \cdot \left(-x1\right)\right) + \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 \left(\frac{\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2}{1 + x1 \cdot x1} - \left(3 + \frac{x1}{1 + x1 \cdot x1}\right)\right)\right) \cdot \left(1 + x1 \cdot x1\right) + \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}\right) + x1 \cdot \left(x1 \cdot x1\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) + x1
double f(double x1, double x2) {
        double r231927 = x1;
        double r231928 = 2.0;
        double r231929 = r231928 * r231927;
        double r231930 = 3.0;
        double r231931 = r231930 * r231927;
        double r231932 = r231931 * r231927;
        double r231933 = x2;
        double r231934 = r231928 * r231933;
        double r231935 = r231932 + r231934;
        double r231936 = r231935 - r231927;
        double r231937 = r231927 * r231927;
        double r231938 = 1.0;
        double r231939 = r231937 + r231938;
        double r231940 = r231936 / r231939;
        double r231941 = r231929 * r231940;
        double r231942 = r231940 - r231930;
        double r231943 = r231941 * r231942;
        double r231944 = 4.0;
        double r231945 = r231944 * r231940;
        double r231946 = 6.0;
        double r231947 = r231945 - r231946;
        double r231948 = r231937 * r231947;
        double r231949 = r231943 + r231948;
        double r231950 = r231949 * r231939;
        double r231951 = r231932 * r231940;
        double r231952 = r231950 + r231951;
        double r231953 = r231937 * r231927;
        double r231954 = r231952 + r231953;
        double r231955 = r231954 + r231927;
        double r231956 = r231932 - r231934;
        double r231957 = r231956 - r231927;
        double r231958 = r231957 / r231939;
        double r231959 = r231930 * r231958;
        double r231960 = r231955 + r231959;
        double r231961 = r231927 + r231960;
        return r231961;
}
↓
double f(double x1, double x2) {
        double r231962 = 3.0;
        double r231963 = x1;
        double r231964 = r231962 * r231963;
        double r231965 = r231964 * r231963;
        double r231966 = r231965 - r231963;
        double r231967 = x2;
        double r231968 = 2.0;
        double r231969 = r231967 * r231968;
        double r231970 = r231966 + r231969;
        double r231971 = 4.0;
        double r231972 = r231970 * r231971;
        double r231973 = 1.0;
        double r231974 = r231963 * r231963;
        double r231975 = r231973 + r231974;
        double r231976 = r231972 / r231975;
        double r231977 = r231976 * r231974;
        double r231978 = 6.0;
        double r231979 = r231978 * r231963;
        double r231980 = -r231963;
        double r231981 = r231979 * r231980;
        double r231982 = r231977 + r231981;
        double r231983 = r231963 * r231968;
        double r231984 = r231965 + r231969;
        double r231985 = r231984 - r231963;
        double r231986 = r231985 / r231975;
        double r231987 = r231983 * r231986;
        double r231988 = r231984 / r231975;
        double r231989 = r231963 / r231975;
        double r231990 = r231962 + r231989;
        double r231991 = r231988 - r231990;
        double r231992 = r231987 * r231991;
        double r231993 = r231982 + r231992;
        double r231994 = r231993 * r231975;
        double r231995 = r231965 * r231986;
        double r231996 = r231994 + r231995;
        double r231997 = r231963 * r231974;
        double r231998 = r231996 + r231997;
        double r231999 = r231998 + r231963;
        double r232000 = r231965 - r231969;
        double r232001 = r232000 - r231963;
        double r232002 = r232001 / r231975;
        double r232003 = r232002 * r231962;
        double r232004 = r231999 + r232003;
        double r232005 = r232004 + r231963;
        return r232005;
}

Error

Bits error versus x1

Bits error versus x2

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

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-lft-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(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}\right) + \left(x1 \cdot x1\right) \cdot \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)\]

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

  6. Simplified0.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(\left(x1 \cdot x1\right) \cdot \frac{4 \cdot \left(2 \cdot x2 + \left(\left(3 \cdot x1\right) \cdot x1 - x1\right)\right)}{1 + x1 \cdot x1} + \color{blue}{\left(\left(-6\right) \cdot x1\right) \cdot x1}\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. Using strategy rm

  8. Applied div-sub0.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(\frac{\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2}{x1 \cdot x1 + 1} - \frac{x1}{x1 \cdot x1 + 1}\right)} - 3\right) + \left(\left(x1 \cdot x1\right) \cdot \frac{4 \cdot \left(2 \cdot x2 + \left(\left(3 \cdot x1\right) \cdot x1 - x1\right)\right)}{1 + x1 \cdot x1} + \left(\left(-6\right) \cdot x1\right) \cdot x1\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. Applied associate--l-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}{\left(\frac{\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2}{x1 \cdot x1 + 1} - \left(\frac{x1}{x1 \cdot x1 + 1} + 3\right)\right)} + \left(\left(x1 \cdot x1\right) \cdot \frac{4 \cdot \left(2 \cdot x2 + \left(\left(3 \cdot x1\right) \cdot x1 - x1\right)\right)}{1 + x1 \cdot x1} + \left(\left(-6\right) \cdot x1\right) \cdot x1\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. Simplified0.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(3 \cdot x1\right) \cdot x1 + 2 \cdot x2}{x1 \cdot x1 + 1} - \color{blue}{\left(\frac{x1}{1 + x1 \cdot x1} + 3\right)}\right) + \left(\left(x1 \cdot x1\right) \cdot \frac{4 \cdot \left(2 \cdot x2 + \left(\left(3 \cdot x1\right) \cdot x1 - x1\right)\right)}{1 + x1 \cdot x1} + \left(\left(-6\right) \cdot x1\right) \cdot x1\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. Final simplification0.5

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

Reproduce

herbie shell --seed 2019194 
(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))))))