x + \left(\tan \left(y + z\right) - \tan a\right)
x + \left(\tan \left(y + z\right) - \tan a\right)
(FPCore (x y z a) :precision binary64 (+ x (- (tan (+ y z)) (tan a))))
(FPCore (x y z a) :precision binary64 (+ x (- (tan (+ y z)) (tan a))))
double code(double x, double y, double z, double a) {
return x + (tan(y + z) - tan(a));
}
double code(double x, double y, double z, double a) {
return x + (tan(y + z) - tan(a));
}



Bits error versus x



Bits error versus y



Bits error versus z



Bits error versus a
Results
Initial program 13.4
herbie shell --seed 2021027
(FPCore (x y z a)
:name "tan-example"
:precision binary64
:pre (and (or (== x 0.0) (<= 0.5884142 x 505.5909)) (or (<= -1.796658e+308 y -9.425585e-310) (<= 1.284938e-309 y 1.7512240000000001e+308)) (or (<= -1.7767070000000002e+308 z -8.599796e-310) (<= 3.293145e-311 z 1.725154e+308)) (or (<= -1.796658e+308 a -9.425585e-310) (<= 1.284938e-309 a 1.7512240000000001e+308)))
(+ x (- (tan (+ y z)) (tan a))))