\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\frac{\frac{1}{\sqrt{2 - \left(v \cdot v\right) \cdot 6}}}{\left(1 - v \cdot v\right) \cdot \left(t \cdot \pi\right)} - \frac{5}{\sqrt{2 - \left(v \cdot v\right) \cdot 6}} \cdot \frac{v \cdot v}{\left(1 - v \cdot v\right) \cdot \left(t \cdot \pi\right)}(FPCore (v t) :precision binary64 (/ (- 1.0 (* 5.0 (* v v))) (* (* (* PI t) (sqrt (* 2.0 (- 1.0 (* 3.0 (* v v)))))) (- 1.0 (* v v)))))
(FPCore (v t) :precision binary64 (- (/ (/ 1.0 (sqrt (- 2.0 (* (* v v) 6.0)))) (* (- 1.0 (* v v)) (* t PI))) (* (/ 5.0 (sqrt (- 2.0 (* (* v v) 6.0)))) (/ (* v v) (* (- 1.0 (* v v)) (* t PI))))))
double code(double v, double t) {
return (1.0 - (5.0 * (v * v))) / (((((double) M_PI) * t) * sqrt(2.0 * (1.0 - (3.0 * (v * v))))) * (1.0 - (v * v)));
}
double code(double v, double t) {
return ((1.0 / sqrt(2.0 - ((v * v) * 6.0))) / ((1.0 - (v * v)) * (t * ((double) M_PI)))) - ((5.0 / sqrt(2.0 - ((v * v) * 6.0))) * ((v * v) / ((1.0 - (v * v)) * (t * ((double) M_PI)))));
}



Bits error versus v



Bits error versus t
Results
Initial program 0.4
Simplified0.4
rmApplied div-sub_binary64_17880.4
Simplified0.4
Simplified0.4
Final simplification0.4
herbie shell --seed 2021050
(FPCore (v t)
:name "Falkner and Boettcher, Equation (20:1,3)"
:precision binary64
(/ (- 1.0 (* 5.0 (* v v))) (* (* (* PI t) (sqrt (* 2.0 (- 1.0 (* 3.0 (* v v)))))) (- 1.0 (* v v)))))