| Alternative 1 | |
|---|---|
| Accuracy | 98.4% |
| Cost | 20676 |

(FPCore (x eps) :precision binary64 (- (pow (+ x eps) 5.0) (pow x 5.0)))
(FPCore (x eps)
:precision binary64
(if (<= x -1.02e-51)
(fma
(* eps 5.0)
(pow x 4.0)
(* (* x x) (+ (* (pow eps 3.0) 10.0) (* x (* eps (* eps 10.0))))))
(if (<= x 1.55e-52)
(- (pow (+ x eps) 5.0) (pow x 5.0))
(fma
(* x x)
(* (* eps eps) (* 10.0 (+ x eps)))
(* eps (* 5.0 (pow x 4.0)))))))double code(double x, double eps) {
return pow((x + eps), 5.0) - pow(x, 5.0);
}
double code(double x, double eps) {
double tmp;
if (x <= -1.02e-51) {
tmp = fma((eps * 5.0), pow(x, 4.0), ((x * x) * ((pow(eps, 3.0) * 10.0) + (x * (eps * (eps * 10.0))))));
} else if (x <= 1.55e-52) {
tmp = pow((x + eps), 5.0) - pow(x, 5.0);
} else {
tmp = fma((x * x), ((eps * eps) * (10.0 * (x + eps))), (eps * (5.0 * pow(x, 4.0))));
}
return tmp;
}
function code(x, eps) return Float64((Float64(x + eps) ^ 5.0) - (x ^ 5.0)) end
function code(x, eps) tmp = 0.0 if (x <= -1.02e-51) tmp = fma(Float64(eps * 5.0), (x ^ 4.0), Float64(Float64(x * x) * Float64(Float64((eps ^ 3.0) * 10.0) + Float64(x * Float64(eps * Float64(eps * 10.0)))))); elseif (x <= 1.55e-52) tmp = Float64((Float64(x + eps) ^ 5.0) - (x ^ 5.0)); else tmp = fma(Float64(x * x), Float64(Float64(eps * eps) * Float64(10.0 * Float64(x + eps))), Float64(eps * Float64(5.0 * (x ^ 4.0)))); end return tmp end
code[x_, eps_] := N[(N[Power[N[(x + eps), $MachinePrecision], 5.0], $MachinePrecision] - N[Power[x, 5.0], $MachinePrecision]), $MachinePrecision]
code[x_, eps_] := If[LessEqual[x, -1.02e-51], N[(N[(eps * 5.0), $MachinePrecision] * N[Power[x, 4.0], $MachinePrecision] + N[(N[(x * x), $MachinePrecision] * N[(N[(N[Power[eps, 3.0], $MachinePrecision] * 10.0), $MachinePrecision] + N[(x * N[(eps * N[(eps * 10.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[x, 1.55e-52], N[(N[Power[N[(x + eps), $MachinePrecision], 5.0], $MachinePrecision] - N[Power[x, 5.0], $MachinePrecision]), $MachinePrecision], N[(N[(x * x), $MachinePrecision] * N[(N[(eps * eps), $MachinePrecision] * N[(10.0 * N[(x + eps), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(eps * N[(5.0 * N[Power[x, 4.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
{\left(x + \varepsilon\right)}^{5} - {x}^{5}
\begin{array}{l}
\mathbf{if}\;x \leq -1.02 \cdot 10^{-51}:\\
\;\;\;\;\mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \left(x \cdot x\right) \cdot \left({\varepsilon}^{3} \cdot 10 + x \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)\right)\right)\\
\mathbf{elif}\;x \leq 1.55 \cdot 10^{-52}:\\
\;\;\;\;{\left(x + \varepsilon\right)}^{5} - {x}^{5}\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x \cdot x, \left(\varepsilon \cdot \varepsilon\right) \cdot \left(10 \cdot \left(x + \varepsilon\right)\right), \varepsilon \cdot \left(5 \cdot {x}^{4}\right)\right)\\
\end{array}
Herbie found 9 alternatives:
| Alternative | Accuracy | Speedup |
|---|
if x < -1.01999999999999998e-51Initial program 39.3%
Taylor expanded in x around inf 99.8%
Simplified99.8%
[Start]99.8% | \[ \left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)
\] |
|---|---|
fma-def [=>]99.8% | \[ \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)}
\] |
distribute-lft1-in [=>]99.8% | \[ \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)
\] |
metadata-eval [=>]99.8% | \[ \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)
\] |
*-commutative [=>]99.8% | \[ \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)
\] |
+-commutative [=>]99.8% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right)
\] |
*-commutative [=>]99.8% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right)
\] |
*-commutative [=>]99.8% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right)
\] |
unpow3 [=>]99.8% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)
\] |
unpow2 [<=]99.8% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)
\] |
associate-*l* [=>]99.8% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right)
\] |
distribute-lft-out [=>]99.8% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right)
\] |
if -1.01999999999999998e-51 < x < 1.5499999999999999e-52Initial program 99.7%
if 1.5499999999999999e-52 < x Initial program 42.6%
Taylor expanded in x around inf 95.7%
Simplified95.7%
[Start]95.7% | \[ \left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)
\] |
|---|---|
fma-def [=>]95.7% | \[ \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)}
\] |
distribute-lft1-in [=>]95.7% | \[ \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)
\] |
metadata-eval [=>]95.7% | \[ \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)
\] |
*-commutative [=>]95.7% | \[ \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)
\] |
+-commutative [=>]95.7% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right)
\] |
*-commutative [=>]95.7% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right)
\] |
*-commutative [=>]95.7% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right)
\] |
unpow3 [=>]95.7% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)
\] |
unpow2 [<=]95.7% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)
\] |
associate-*l* [=>]95.7% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right)
\] |
distribute-lft-out [=>]95.7% | \[ \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right)
\] |
Taylor expanded in eps around 0 95.6%
Simplified95.7%
[Start]95.6% | \[ 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + \left(5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)\right)
\] |
|---|---|
associate-*r* [=>]95.6% | \[ \color{blue}{\left(10 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}} + \left(5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)\right)
\] |
*-commutative [=>]95.6% | \[ \color{blue}{\left({\varepsilon}^{2} \cdot 10\right)} \cdot {x}^{3} + \left(5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)\right)
\] |
associate-*r* [<=]95.6% | \[ \color{blue}{{\varepsilon}^{2} \cdot \left(10 \cdot {x}^{3}\right)} + \left(5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)\right)
\] |
unpow2 [=>]95.6% | \[ \color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot \left(10 \cdot {x}^{3}\right) + \left(5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)\right)
\] |
associate-*r* [<=]95.6% | \[ \color{blue}{\varepsilon \cdot \left(\varepsilon \cdot \left(10 \cdot {x}^{3}\right)\right)} + \left(5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)\right)
\] |
+-commutative [=>]95.6% | \[ \varepsilon \cdot \left(\varepsilon \cdot \left(10 \cdot {x}^{3}\right)\right) + \color{blue}{\left(10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right) + 5 \cdot \left(\varepsilon \cdot {x}^{4}\right)\right)}
\] |
associate-*r* [=>]95.7% | \[ \varepsilon \cdot \left(\varepsilon \cdot \left(10 \cdot {x}^{3}\right)\right) + \left(10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right) + \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}}\right)
\] |
*-commutative [<=]95.7% | \[ \varepsilon \cdot \left(\varepsilon \cdot \left(10 \cdot {x}^{3}\right)\right) + \left(10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right) + \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4}\right)
\] |
associate-*r* [<=]95.7% | \[ \varepsilon \cdot \left(\varepsilon \cdot \left(10 \cdot {x}^{3}\right)\right) + \left(10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right) + \color{blue}{\varepsilon \cdot \left(5 \cdot {x}^{4}\right)}\right)
\] |
associate-+r+ [=>]95.7% | \[ \color{blue}{\left(\varepsilon \cdot \left(\varepsilon \cdot \left(10 \cdot {x}^{3}\right)\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)\right) + \varepsilon \cdot \left(5 \cdot {x}^{4}\right)}
\] |
Taylor expanded in eps around 0 95.7%
Simplified95.7%
[Start]95.7% | \[ \mathsf{fma}\left(x \cdot x, 10 \cdot {\varepsilon}^{3} + 10 \cdot \left({\varepsilon}^{2} \cdot x\right), \varepsilon \cdot \left(5 \cdot {x}^{4}\right)\right)
\] |
|---|---|
distribute-lft-out [=>]95.7% | \[ \mathsf{fma}\left(x \cdot x, \color{blue}{10 \cdot \left({\varepsilon}^{3} + {\varepsilon}^{2} \cdot x\right)}, \varepsilon \cdot \left(5 \cdot {x}^{4}\right)\right)
\] |
unpow3 [=>]95.7% | \[ \mathsf{fma}\left(x \cdot x, 10 \cdot \left(\color{blue}{\left(\varepsilon \cdot \varepsilon\right) \cdot \varepsilon} + {\varepsilon}^{2} \cdot x\right), \varepsilon \cdot \left(5 \cdot {x}^{4}\right)\right)
\] |
unpow2 [=>]95.7% | \[ \mathsf{fma}\left(x \cdot x, 10 \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \varepsilon + \color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot x\right), \varepsilon \cdot \left(5 \cdot {x}^{4}\right)\right)
\] |
distribute-lft-in [<=]95.7% | \[ \mathsf{fma}\left(x \cdot x, 10 \cdot \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right)\right)}, \varepsilon \cdot \left(5 \cdot {x}^{4}\right)\right)
\] |
*-commutative [=>]95.7% | \[ \mathsf{fma}\left(x \cdot x, \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right)\right) \cdot 10}, \varepsilon \cdot \left(5 \cdot {x}^{4}\right)\right)
\] |
associate-*l* [=>]95.7% | \[ \mathsf{fma}\left(x \cdot x, \color{blue}{\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(\varepsilon + x\right) \cdot 10\right)}, \varepsilon \cdot \left(5 \cdot {x}^{4}\right)\right)
\] |
Final simplification99.4%
| Alternative 1 | |
|---|---|
| Accuracy | 98.4% |
| Cost | 20676 |
| Alternative 2 | |
|---|---|
| Accuracy | 99.4% |
| Cost | 39881 |
| Alternative 3 | |
|---|---|
| Accuracy | 98.4% |
| Cost | 14217 |
| Alternative 4 | |
|---|---|
| Accuracy | 98.3% |
| Cost | 14024 |
| Alternative 5 | |
|---|---|
| Accuracy | 98.2% |
| Cost | 13897 |
| Alternative 6 | |
|---|---|
| Accuracy | 96.9% |
| Cost | 7049 |
| Alternative 7 | |
|---|---|
| Accuracy | 96.9% |
| Cost | 7048 |
| Alternative 8 | |
|---|---|
| Accuracy | 96.8% |
| Cost | 6792 |
| Alternative 9 | |
|---|---|
| Accuracy | 82.5% |
| Cost | 704 |
herbie shell --seed 2023165
(FPCore (x eps)
:name "ENA, Section 1.4, Exercise 4b, n=5"
:precision binary64
:pre (and (and (<= -1000000000.0 x) (<= x 1000000000.0)) (and (<= -1.0 eps) (<= eps 1.0)))
(- (pow (+ x eps) 5.0) (pow x 5.0)))