\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}\left(\left(z + x\right) \cdot \frac{z - x}{y} - y\right) \cdot -0.5(FPCore (x y z) :precision binary64 (/ (- (+ (* x x) (* y y)) (* z z)) (* y 2.0)))
(FPCore (x y z) :precision binary64 (* (- (* (+ z x) (/ (- z x) y)) y) -0.5))
double code(double x, double y, double z) {
return (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
}
double code(double x, double y, double z) {
return (((z + x) * ((z - x) / y)) - y) * -0.5;
}




Bits error versus x




Bits error versus y




Bits error versus z
Results
| Original | 28.5 |
|---|---|
| Target | 0.2 |
| Herbie | 0.2 |
Initial program 28.5
Simplified12.8
rmApplied *-un-lft-identity_binary6412.8
Applied difference-of-squares_binary6412.8
Applied times-frac_binary640.2
Simplified0.2
Final simplification0.2
herbie shell --seed 2020220
(FPCore (x y z)
:name "Diagrams.TwoD.Apollonian:initialConfig from diagrams-contrib-1.3.0.5, A"
:precision binary64
:herbie-target
(- (* y 0.5) (* (* (/ 0.5 y) (+ z x)) (- z x)))
(/ (- (+ (* x x) (* y y)) (* z z)) (* y 2.0)))