\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\begin{array}{l}
\mathbf{if}\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)} \leq -\infty \lor \neg \left(\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)} \leq 4.5123883747080296 \cdot 10^{-39}\right):\\
\;\;\;\;\frac{1}{\frac{{\left(e^{a}\right)}^{\varepsilon} - 1}{\frac{{\left(e^{a + b}\right)}^{\varepsilon} - 1}{b + \left(\log 1 + \varepsilon \cdot \left(0.5 \cdot {\left(\log 1\right)}^{2}\right)\right)}}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)}\\
\end{array}(FPCore (a b eps) :precision binary64 (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))))
(FPCore (a b eps)
:precision binary64
(if (or (<=
(/
(* eps (- (exp (* eps (+ a b))) 1.0))
(* (- (exp (* eps a)) 1.0) (- (exp (* eps b)) 1.0)))
(- INFINITY))
(not
(<=
(/
(* eps (- (exp (* eps (+ a b))) 1.0))
(* (- (exp (* eps a)) 1.0) (- (exp (* eps b)) 1.0)))
4.5123883747080296e-39)))
(/
1.0
(/
(- (pow (exp a) eps) 1.0)
(/
(- (pow (exp (+ a b)) eps) 1.0)
(+ b (+ (log 1.0) (* eps (* 0.5 (pow (log 1.0) 2.0))))))))
(/
(* eps (- (exp (* eps (+ a b))) 1.0))
(* (- (exp (* eps a)) 1.0) (- (exp (* eps b)) 1.0)))))double code(double a, double b, double eps) {
return (((double) (eps * ((double) (((double) exp(((double) (((double) (a + b)) * eps)))) - 1.0)))) / ((double) (((double) (((double) exp(((double) (a * eps)))) - 1.0)) * ((double) (((double) exp(((double) (b * eps)))) - 1.0)))));
}
double code(double a, double b, double eps) {
double tmp;
if ((((((double) (eps * ((double) (((double) exp(((double) (eps * ((double) (a + b)))))) - 1.0)))) / ((double) (((double) (((double) exp(((double) (eps * a)))) - 1.0)) * ((double) (((double) exp(((double) (eps * b)))) - 1.0))))) <= ((double) -(((double) INFINITY)))) || !((((double) (eps * ((double) (((double) exp(((double) (eps * ((double) (a + b)))))) - 1.0)))) / ((double) (((double) (((double) exp(((double) (eps * a)))) - 1.0)) * ((double) (((double) exp(((double) (eps * b)))) - 1.0))))) <= 4.5123883747080296e-39))) {
tmp = (1.0 / (((double) (((double) pow(((double) exp(a)), eps)) - 1.0)) / (((double) (((double) pow(((double) exp(((double) (a + b)))), eps)) - 1.0)) / ((double) (b + ((double) (((double) log(1.0)) + ((double) (eps * ((double) (0.5 * ((double) pow(((double) log(1.0)), 2.0)))))))))))));
} else {
tmp = (((double) (eps * ((double) (((double) exp(((double) (eps * ((double) (a + b)))))) - 1.0)))) / ((double) (((double) (((double) exp(((double) (eps * a)))) - 1.0)) * ((double) (((double) exp(((double) (eps * b)))) - 1.0)))));
}
return tmp;
}




Bits error versus a




Bits error versus b




Bits error versus eps
Results
| Original | 60.5 |
|---|---|
| Target | 14.6 |
| Herbie | 47.5 |
if (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))) < -inf.0 or 4.51238837470802961e-39 < (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))) Initial program Error: 63.7 bits
SimplifiedError: 63.4 bits
Taylor expanded around 0 Error: 55.3 bits
SimplifiedError: 55.3 bits
rmApplied associate-*r/Error: 55.0 bits
rmApplied clear-numError: 55.0 bits
SimplifiedError: 50.0 bits
if -inf.0 < (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))) < 4.51238837470802961e-39Initial program Error: 3.4 bits
Final simplificationError: 47.5 bits
herbie shell --seed 2020203
(FPCore (a b eps)
:name "expq3 (problem 3.4.2)"
:precision binary64
:pre (and (< -1.0 eps) (< eps 1.0))
:herbie-target
(/ (+ a b) (* a b))
(/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))))