Average Error: 0.1 → 0.2
Time: 13.8s
Precision: 64
\[0 \le x1 \le 2 \land 0 \le x2 \le 3 \land -2 \cdot \left(\left(x1 \cdot x1\right) \cdot \left(x1 \cdot x1\right)\right) + 2 \ge x2\]
\[\left(-12 \cdot x1 - 7 \cdot x2\right) + x2 \cdot x2\]
\[\frac{\left(x2 \cdot x2 + -49\right) \cdot x2}{7 + x2} - 12 \cdot x1\]
\left(-12 \cdot x1 - 7 \cdot x2\right) + x2 \cdot x2
\frac{\left(x2 \cdot x2 + -49\right) \cdot x2}{7 + x2} - 12 \cdot x1
double f(double x1, double x2) {
        double r40095880 = -12.0;
        double r40095881 = x1;
        double r40095882 = r40095880 * r40095881;
        double r40095883 = 7.0;
        double r40095884 = x2;
        double r40095885 = r40095883 * r40095884;
        double r40095886 = r40095882 - r40095885;
        double r40095887 = r40095884 * r40095884;
        double r40095888 = r40095886 + r40095887;
        return r40095888;
}

double f(double x1, double x2) {
        double r40095889 = x2;
        double r40095890 = r40095889 * r40095889;
        double r40095891 = -49.0;
        double r40095892 = r40095890 + r40095891;
        double r40095893 = r40095892 * r40095889;
        double r40095894 = 7.0;
        double r40095895 = r40095894 + r40095889;
        double r40095896 = r40095893 / r40095895;
        double r40095897 = 12.0;
        double r40095898 = x1;
        double r40095899 = r40095897 * r40095898;
        double r40095900 = r40095896 - r40095899;
        return r40095900;
}

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.1

    \[\left(-12 \cdot x1 - 7 \cdot x2\right) + x2 \cdot x2\]
  2. Simplified0.1

    \[\leadsto \color{blue}{\left(x2 - 7\right) \cdot x2 - x1 \cdot 12}\]
  3. Using strategy rm
  4. Applied flip--0.1

    \[\leadsto \color{blue}{\frac{x2 \cdot x2 - 7 \cdot 7}{x2 + 7}} \cdot x2 - x1 \cdot 12\]
  5. Applied associate-*l/0.2

    \[\leadsto \color{blue}{\frac{\left(x2 \cdot x2 - 7 \cdot 7\right) \cdot x2}{x2 + 7}} - x1 \cdot 12\]
  6. Simplified0.2

    \[\leadsto \frac{\color{blue}{x2 \cdot \left(x2 \cdot x2 + -49\right)}}{x2 + 7} - x1 \cdot 12\]
  7. Final simplification0.2

    \[\leadsto \frac{\left(x2 \cdot x2 + -49\right) \cdot x2}{7 + x2} - 12 \cdot x1\]

Reproduce

herbie shell --seed 1 
(FPCore (x1 x2)
  :name "floudas3"
  :pre (and (<= 0 x1 2) (<= 0 x2 3) (>= (+ (* -2 (* (* x1 x1) (* x1 x1))) 2) x2))
  (+ (- (* -12 x1) (* 7 x2)) (* x2 x2)))