\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\cos th \cdot \frac{\sqrt{a1 \cdot a1 + a2 \cdot a2}}{\frac{\sqrt{2}}{\sqrt{a1 \cdot a1 + a2 \cdot a2}}}(FPCore (a1 a2 th) :precision binary64 (+ (* (/ (cos th) (sqrt 2.0)) (* a1 a1)) (* (/ (cos th) (sqrt 2.0)) (* a2 a2))))
(FPCore (a1 a2 th) :precision binary64 (* (cos th) (/ (sqrt (+ (* a1 a1) (* a2 a2))) (/ (sqrt 2.0) (sqrt (+ (* a1 a1) (* a2 a2)))))))
double code(double a1, double a2, double th) {
return ((cos(th) / sqrt(2.0)) * (a1 * a1)) + ((cos(th) / sqrt(2.0)) * (a2 * a2));
}
double code(double a1, double a2, double th) {
return cos(th) * (sqrt((a1 * a1) + (a2 * a2)) / (sqrt(2.0) / sqrt((a1 * a1) + (a2 * a2))));
}



Bits error versus a1



Bits error versus a2



Bits error versus th
Results
Initial program 0.5
Simplified0.5
rmApplied add-sqr-sqrt_binary640.5
Applied associate-/l*_binary640.5
Final simplification0.5
herbie shell --seed 2020232
(FPCore (a1 a2 th)
:name "Migdal et al, Equation (64)"
:precision binary64
(+ (* (/ (cos th) (sqrt 2.0)) (* a1 a1)) (* (/ (cos th) (sqrt 2.0)) (* a2 a2))))