Examples.Basics.BasicTests:f3 from sbv-4.4

Average Error: 0.0 → 0.0

Time: 1.8s

Precision: binary64

Cost: 7104

Math

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

↓

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

FPCore

(FPCore (x y) :precision binary64 (* (+ x y) (+ x y)))

↓

(FPCore (x y) :precision binary64 (fma (- x) (- x) (* y (+ y (* x 2.0)))))

C

double code(double x, double y) {
	return (x + y) * (x + y);
}

↓

double code(double x, double y) {
	return fma(-x, -x, (y * (y + (x * 2.0))));
}

Julia

function code(x, y)
	return Float64(Float64(x + y) * Float64(x + y))
end

↓

function code(x, y)
	return fma(Float64(-x), Float64(-x), Float64(y * Float64(y + Float64(x * 2.0))))
end

Wolfram

code[x_, y_] := N[(N[(x + y), $MachinePrecision] * N[(x + y), $MachinePrecision]), $MachinePrecision]

↓

code[x_, y_] := N[((-x) * (-x) + N[(y * N[(y + N[(x * 2.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Target

Original	0.0
Target	0.0
Herbie	0.0

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

Derivation

1. Initial program 0.0

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

2. Taylor expanded in x around -inf 0.3

   \[\leadsto \color{blue}{2 \cdot \left(y \cdot x\right) + \left({y}^{2} + {\left(\frac{-1}{x}\right)}^{-2}\right)} \]

3. Simplified 0.0

   \[\leadsto \color{blue}{\mathsf{fma}\left(-x, -x, y \cdot \left(y + 2 \cdot x\right)\right)} \]
   Proof
   (fma.f64 (neg.f64 x) (neg.f64 x) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 x)) (neg.f64 x) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 1 -1)) x) (neg.f64 x) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 -1 x))) (neg.f64 x) (*.f64 y (+.f64 y (*.f64 2 x)))): 14 points increase in error, 0 points decrease in error
   (fma.f64 (Rewrite<= unpow-1_binary64 (pow.f64 (/.f64 -1 x) -1)) (neg.f64 x) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (Rewrite<= metadata-eval (/.f64 -2 2))) (neg.f64 x) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 x)) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (*.f64 (Rewrite<= metadata-eval (/.f64 1 -1)) x) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 -1 x))) (*.f64 y (+.f64 y (*.f64 2 x)))): 14 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (Rewrite<= unpow-1_binary64 (pow.f64 (/.f64 -1 x) -1)) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (pow.f64 (/.f64 -1 x) (Rewrite<= metadata-eval (/.f64 -2 2))) (*.f64 y (+.f64 y (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 y y) (*.f64 (*.f64 2 x) y)))): 1 points increase in error, 1 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 y 2)) (*.f64 (*.f64 2 x) y))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (+.f64 (pow.f64 y 2) (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 x y))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (+.f64 (pow.f64 y 2) (*.f64 2 (Rewrite<= *-commutative_binary64 (*.f64 y x))))): 0 points increase in error, 0 points decrease in error
   (fma.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 2 (*.f64 y x)) (pow.f64 y 2)))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (pow.f64 (/.f64 -1 x) (/.f64 -2 2)) (pow.f64 (/.f64 -1 x) (/.f64 -2 2))) (+.f64 (*.f64 2 (*.f64 y x)) (pow.f64 y 2)))): 2 points increase in error, 0 points decrease in error
   (+.f64 (Rewrite<= sqr-pow_binary64 (pow.f64 (/.f64 -1 x) -2)) (+.f64 (*.f64 2 (*.f64 y x)) (pow.f64 y 2))): 48 points increase in error, 11 points decrease in error
   (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 2 (*.f64 y x)) (pow.f64 y 2)) (pow.f64 (/.f64 -1 x) -2))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 2 (*.f64 y x)) (+.f64 (pow.f64 y 2) (pow.f64 (/.f64 -1 x) -2)))): 1 points increase in error, 1 points decrease in error

4. Final simplification 0.0

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

Alternatives

Alternative 1
Error	21.1
Cost	844

\[\begin{array}{l} \mathbf{if}\;y \leq 1.15 \cdot 10^{-156}:\\ \;\;\;\;x \cdot x\\ \mathbf{elif}\;y \leq 2.9 \cdot 10^{-122}:\\ \;\;\;\;y \cdot y\\ \mathbf{elif}\;y \leq 1.45 \cdot 10^{-81}:\\ \;\;\;\;x \cdot x\\ \mathbf{else}:\\ \;\;\;\;y \cdot \left(y + x \cdot 2\right)\\ \end{array} \]

Alternative 2
Error	0.0
Cost	448

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

Alternative 3
Error	21.6
Cost	324

\[\begin{array}{l} \mathbf{if}\;y \leq 1.15 \cdot 10^{-156}:\\ \;\;\;\;x \cdot x\\ \mathbf{else}:\\ \;\;\;\;y \cdot y\\ \end{array} \]

Alternative 4
Error	28.0
Cost	192

\[x \cdot x \]

Reproduce

herbie shell --seed 2022325 
(FPCore (x y)
  :name "Examples.Basics.BasicTests:f3 from sbv-4.4"
  :precision binary64

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

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