\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}
\begin{array}{l}
t_0 := p \cdot \left(4 \cdot p\right)\\
\mathbf{if}\;\frac{x}{\sqrt{t_0 + x \cdot x}} \leq -0.9999850286817621:\\
\;\;\;\;\sqrt{\mathsf{fma}\left({\left(\frac{p}{x}\right)}^{4}, -3, \mathsf{fma}\left(\frac{p}{x}, \frac{p}{x}, \frac{10}{{\left(\frac{x}{p}\right)}^{6}}\right)\right)}\\
\mathbf{else}:\\
\;\;\;\;\sqrt{{e}^{\log \left(\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\mathsf{fma}\left(x, x, t_0\right)}}, 0.5\right)\right)}}\\
\end{array}
(FPCore (p x) :precision binary64 (sqrt (* 0.5 (+ 1.0 (/ x (sqrt (+ (* (* 4.0 p) p) (* x x))))))))
(FPCore (p x)
:precision binary64
(let* ((t_0 (* p (* 4.0 p))))
(if (<= (/ x (sqrt (+ t_0 (* x x)))) -0.9999850286817621)
(sqrt
(fma
(pow (/ p x) 4.0)
-3.0
(fma (/ p x) (/ p x) (/ 10.0 (pow (/ x p) 6.0)))))
(sqrt (pow E (log (fma 0.5 (/ x (sqrt (fma x x t_0))) 0.5)))))))double code(double p, double x) {
return sqrt(0.5 * (1.0 + (x / sqrt(((4.0 * p) * p) + (x * x)))));
}
double code(double p, double x) {
double t_0 = p * (4.0 * p);
double tmp;
if ((x / sqrt(t_0 + (x * x))) <= -0.9999850286817621) {
tmp = sqrt(fma(pow((p / x), 4.0), -3.0, fma((p / x), (p / x), (10.0 / pow((x / p), 6.0)))));
} else {
tmp = sqrt(pow(((double) M_E), log(fma(0.5, (x / sqrt(fma(x, x, t_0))), 0.5))));
}
return tmp;
}




Bits error versus p




Bits error versus x
| Original | 12.7 |
|---|---|
| Target | 12.7 |
| Herbie | 5.7 |
if (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 4 p) p) (*.f64 x x)))) < -0.999985028681762089Initial program 53.1
Simplified53.1
Applied add-exp-log_binary6453.1
Taylor expanded in x around -inf 38.8
Simplified23.5
if -0.999985028681762089 < (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 4 p) p) (*.f64 x x)))) Initial program 0.0
Simplified0.0
Applied add-exp-log_binary640.0
Applied pow1_binary640.0
Applied log-pow_binary640.0
Applied exp-prod_binary640.0
Simplified0.0
Final simplification5.7
herbie shell --seed 2021329
(FPCore (p x)
:name "Given's Rotation SVD example"
:precision binary64
:pre (and (< 1e-150 (fabs x)) (< (fabs x) 1e+150))
:herbie-target
(sqrt (+ 0.5 (/ (copysign 0.5 x) (hypot 1.0 (/ (* 2.0 p) x)))))
(sqrt (* 0.5 (+ 1.0 (/ x (sqrt (+ (* (* 4.0 p) p) (* x x))))))))