\left(x + y\right) \cdot \left(x - y\right)
x \cdot x - y \cdot y
(FPCore (x y) :precision binary64 (* (+ x y) (- x y)))
(FPCore (x y) :precision binary64 (- (* x x) (* y y)))
double code(double x, double y) {
return (x + y) * (x - y);
}
double code(double x, double y) {
return (x * x) - (y * y);
}



Bits error versus x



Bits error versus y
Results
Initial program 0.0
Taylor expanded around 0 0.0
Simplified0.0
Final simplification0.0
herbie shell --seed 2021093
(FPCore (x y)
:name "Examples.Basics.BasicTests:f1 from sbv-4.4"
:precision binary64
(* (+ x y) (- x y)))