\left(-x \cdot \frac{1}{\tan B}\right) + \frac{F}{\sin B} \cdot {\left(\left(F \cdot F + 2\right) + 2 \cdot x\right)}^{\left(-\frac{1}{2}\right)}F \cdot \frac{{\left(\left(F \cdot F + 2\right) + 2 \cdot x\right)}^{-0.5}}{\sin B} - \frac{x}{\tan B}(FPCore (F B x) :precision binary64 (+ (- (* x (/ 1.0 (tan B)))) (* (/ F (sin B)) (pow (+ (+ (* F F) 2.0) (* 2.0 x)) (- (/ 1.0 2.0))))))
(FPCore (F B x) :precision binary64 (- (* F (/ (pow (+ (+ (* F F) 2.0) (* 2.0 x)) -0.5) (sin B))) (/ x (tan B))))
double code(double F, double B, double x) {
return -(x * (1.0 / tan(B))) + ((F / sin(B)) * pow((((F * F) + 2.0) + (2.0 * x)), -(1.0 / 2.0)));
}
double code(double F, double B, double x) {
return (F * (pow((((F * F) + 2.0) + (2.0 * x)), -0.5) / sin(B))) - (x / tan(B));
}



Bits error versus F



Bits error versus B



Bits error versus x
Results
Initial program 13.5
Simplified13.5
rmApplied div-inv_binary6413.5
Applied associate-*l*_binary6410.6
Simplified10.6
Final simplification10.6
herbie shell --seed 2020277
(FPCore (F B x)
:name "VandenBroeck and Keller, Equation (23)"
:precision binary64
(+ (- (* x (/ 1.0 (tan B)))) (* (/ F (sin B)) (pow (+ (+ (* F F) 2.0) (* 2.0 x)) (- (/ 1.0 2.0))))))