\tan \left(x + \varepsilon\right) - \tan x
\frac{\tan x + \tan \varepsilon}{1 - \log \left({\left(e^{\tan x}\right)}^{\tan \varepsilon}\right)} - \tan x(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))
(FPCore (x eps) :precision binary64 (- (/ (+ (tan x) (tan eps)) (- 1.0 (log (pow (exp (tan x)) (tan eps))))) (tan x)))
double code(double x, double eps) {
return tan(x + eps) - tan(x);
}
double code(double x, double eps) {
return ((tan(x) + tan(eps)) / (1.0 - log(pow(exp(tan(x)), tan(eps))))) - tan(x);
}




Bits error versus x




Bits error versus eps
Results
| Original | 36.7 |
|---|---|
| Target | 14.9 |
| Herbie | 21.7 |
Initial program 36.7
rmApplied tan-sum_binary6421.7
rmApplied add-log-exp_binary6421.7
Simplified21.7
Final simplification21.7
herbie shell --seed 2020268
(FPCore (x eps)
:name "2tan (problem 3.3.2)"
:precision binary64
:herbie-target
(/ (sin eps) (* (cos x) (cos (+ x eps))))
(- (tan (+ x eps)) (tan x)))