Average Error: 0.0 → 0.0
Time: 1.2s
Precision: 64
\[\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]
↓
\[\mathsf{fma}\left(x, x, \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]
\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y
↓
\mathsf{fma}\left(x, x, \left(x \cdot 2\right) \cdot y\right) + y \cdot y
double f(double x, double y) {
        double r653575 = x;
        double r653576 = r653575 * r653575;
        double r653577 = 2.0;
        double r653578 = r653575 * r653577;
        double r653579 = y;
        double r653580 = r653578 * r653579;
        double r653581 = r653576 + r653580;
        double r653582 = r653579 * r653579;
        double r653583 = r653581 + r653582;
        return r653583;
}
↓
double f(double x, double y) {
        double r653584 = x;
        double r653585 = 2.0;
        double r653586 = r653584 * r653585;
        double r653587 = y;
        double r653588 = r653586 * r653587;
        double r653589 = fma(r653584, r653584, r653588);
        double r653590 = r653587 * r653587;
        double r653591 = r653589 + r653590;
        return r653591;
}

Error

Bits error versus x

Bits error versus y

Target

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

Derivation

  1. Initial program 0.0

    \[\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]
  2. Using strategy rm

  3. Applied fma-def0.0

    \[\leadsto \color{blue}{\mathsf{fma}\left(x, x, \left(x \cdot 2\right) \cdot y\right)} + y \cdot y\]

  4. Final simplification0.0

    \[\leadsto \mathsf{fma}\left(x, x, \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]

Reproduce

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

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

  (+ (+ (* x x) (* (* x 2) y)) (* y y)))