Average Error: 0.0 → 0.0
Time: 10.5s
Precision: 64
\[\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]
↓
\[\mathsf{fma}\left(y, \mathsf{fma}\left(2, x, y\right), x \cdot x\right)\]
\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y
↓
\mathsf{fma}\left(y, \mathsf{fma}\left(2, x, y\right), x \cdot x\right)
double f(double x, double y) {
        double r16318700 = x;
        double r16318701 = r16318700 * r16318700;
        double r16318702 = 2.0;
        double r16318703 = r16318700 * r16318702;
        double r16318704 = y;
        double r16318705 = r16318703 * r16318704;
        double r16318706 = r16318701 + r16318705;
        double r16318707 = r16318704 * r16318704;
        double r16318708 = r16318706 + r16318707;
        return r16318708;
}
↓
double f(double x, double y) {
        double r16318709 = y;
        double r16318710 = 2.0;
        double r16318711 = x;
        double r16318712 = fma(r16318710, r16318711, r16318709);
        double r16318713 = r16318711 * r16318711;
        double r16318714 = fma(r16318709, r16318712, r16318713);
        return r16318714;
}

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. Simplified0.0

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

  3. Final simplification0.0

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

Reproduce

herbie shell --seed 2019192 +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)))