\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\begin{array}{l}
\mathbf{if}\;x \le 72400405592338880:\\
\;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{{z}^{2}}{x}, y, 7.93650079365100015 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} - \mathsf{fma}\left(\log \left(\frac{1}{x}\right), x, x\right)\right)\\
\end{array}double code(double x, double y, double z) {
return (((((x - 0.5) * log(x)) - x) + 0.91893853320467) + ((((((y + 0.0007936500793651) * z) - 0.0027777777777778) * z) + 0.083333333333333) / x));
}
double code(double x, double y, double z) {
double VAR;
if ((x <= 7.240040559233888e+16)) {
VAR = (((((x - 0.5) * log(x)) - x) + 0.91893853320467) + ((((((y + 0.0007936500793651) * z) - 0.0027777777777778) * z) + 0.083333333333333) / x));
} else {
VAR = fma((pow(z, 2.0) / x), y, ((0.0007936500793651 * (pow(z, 2.0) / x)) - fma(log((1.0 / x)), x, x)));
}
return VAR;
}




Bits error versus x




Bits error versus y




Bits error versus z
Results
| Original | 5.9 |
|---|---|
| Target | 1.2 |
| Herbie | 4.0 |
if x < 7.240040559233888e+16Initial program 0.1
if 7.240040559233888e+16 < x Initial program 10.3
Simplified10.2
Taylor expanded around inf 10.4
Simplified7.0
Final simplification4.0
herbie shell --seed 2020100 +o rules:numerics
(FPCore (x y z)
:name "Numeric.SpecFunctions:$slogFactorial from math-functions-0.1.5.2, B"
:precision binary64
:herbie-target
(+ (+ (+ (* (- x 0.5) (log x)) (- 0.91893853320467 x)) (/ 0.083333333333333 x)) (* (/ z x) (- (* z (+ y 0.0007936500793651)) 0.0027777777777778)))
(+ (+ (- (* (- x 0.5) (log x)) x) 0.91893853320467) (/ (+ (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) 0.083333333333333) x)))