\sqrt{x + 1} - \sqrt{x}
\begin{array}{l}
t_0 := \sqrt{1 + x} + \sqrt{x}\\
{\left(t_0 \cdot t_0\right)}^{-0.5}
\end{array}
(FPCore (x) :precision binary64 (- (sqrt (+ x 1.0)) (sqrt x)))
(FPCore (x) :precision binary64 (let* ((t_0 (+ (sqrt (+ 1.0 x)) (sqrt x)))) (pow (* t_0 t_0) -0.5)))
double code(double x) {
return sqrt(x + 1.0) - sqrt(x);
}
double code(double x) {
double t_0 = sqrt(1.0 + x) + sqrt(x);
return pow((t_0 * t_0), -0.5);
}




Bits error versus x
Results
| Original | 30.1 |
|---|---|
| Target | 0.2 |
| Herbie | 0.2 |
Initial program 30.1
Applied flip--_binary6429.9
Simplified0.2
Simplified0.2
Applied add-sqr-sqrt_binary640.3
Applied inv-pow_binary640.3
Applied sqrt-pow1_binary640.3
Applied inv-pow_binary640.3
Applied sqrt-pow1_binary640.3
Applied pow-prod-down_binary640.2
Final simplification0.2
herbie shell --seed 1991292424
(FPCore (x)
:name "2sqrt (example 3.1)"
:precision binary64
:herbie-target
(/ 1.0 (+ (sqrt (+ x 1.0)) (sqrt x)))
(- (sqrt (+ x 1.0)) (sqrt x)))