Average Error: 0.0 → 0.0
Time: 7.2s
Precision: 64
\[\left(x \cdot x + \left(x \cdot 2.0\right) \cdot y\right) + y \cdot y\]
↓
\[y \cdot y + \left(x \cdot x + \left(x \cdot 2.0\right) \cdot y\right)\]
\left(x \cdot x + \left(x \cdot 2.0\right) \cdot y\right) + y \cdot y
↓
y \cdot y + \left(x \cdot x + \left(x \cdot 2.0\right) \cdot y\right)
double f(double x, double y) {
        double r19419661 = x;
        double r19419662 = r19419661 * r19419661;
        double r19419663 = 2.0;
        double r19419664 = r19419661 * r19419663;
        double r19419665 = y;
        double r19419666 = r19419664 * r19419665;
        double r19419667 = r19419662 + r19419666;
        double r19419668 = r19419665 * r19419665;
        double r19419669 = r19419667 + r19419668;
        return r19419669;
}
↓
double f(double x, double y) {
        double r19419670 = y;
        double r19419671 = r19419670 * r19419670;
        double r19419672 = x;
        double r19419673 = r19419672 * r19419672;
        double r19419674 = 2.0;
        double r19419675 = r19419672 * r19419674;
        double r19419676 = r19419675 * r19419670;
        double r19419677 = r19419673 + r19419676;
        double r19419678 = r19419671 + r19419677;
        return r19419678;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original0.0
Target0.0
Herbie0.0
\[x \cdot x + \left(y \cdot y + \left(x \cdot y\right) \cdot 2.0\right)\]

Derivation

  1. Initial program 0.0

    \[\left(x \cdot x + \left(x \cdot 2.0\right) \cdot y\right) + y \cdot y\]

  2. Final simplification0.0

    \[\leadsto y \cdot y + \left(x \cdot x + \left(x \cdot 2.0\right) \cdot y\right)\]

Reproduce

herbie shell --seed 2019163 +o rules:numerics
(FPCore (x y)
  :name "Examples.Basics.ProofTests:f4 from sbv-4.4"

  :herbie-target
  (+ (* x x) (+ (* y y) (* (* x y) 2.0)))

  (+ (+ (* x x) (* (* x 2.0) y)) (* y y)))