Average Error: 13.5 → 13.5
Time: 19.9s
Precision: 64
\[10^{-150} \lt \left|x\right| \lt 10^{+150}\]
\[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]
\[\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\mathsf{fma}\left(p \cdot 4, p, x \cdot x\right)}}, 0.5\right)}\]
\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}
\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\mathsf{fma}\left(p \cdot 4, p, x \cdot x\right)}}, 0.5\right)}
double f(double p, double x) {
        double r6356827 = 0.5;
        double r6356828 = 1.0;
        double r6356829 = x;
        double r6356830 = 4.0;
        double r6356831 = p;
        double r6356832 = r6356830 * r6356831;
        double r6356833 = r6356832 * r6356831;
        double r6356834 = r6356829 * r6356829;
        double r6356835 = r6356833 + r6356834;
        double r6356836 = sqrt(r6356835);
        double r6356837 = r6356829 / r6356836;
        double r6356838 = r6356828 + r6356837;
        double r6356839 = r6356827 * r6356838;
        double r6356840 = sqrt(r6356839);
        return r6356840;
}

double f(double p, double x) {
        double r6356841 = 0.5;
        double r6356842 = x;
        double r6356843 = p;
        double r6356844 = 4.0;
        double r6356845 = r6356843 * r6356844;
        double r6356846 = r6356842 * r6356842;
        double r6356847 = fma(r6356845, r6356843, r6356846);
        double r6356848 = sqrt(r6356847);
        double r6356849 = r6356842 / r6356848;
        double r6356850 = fma(r6356841, r6356849, r6356841);
        double r6356851 = sqrt(r6356850);
        return r6356851;
}

Error

Bits error versus p

Bits error versus x

Target

Original13.5
Target13.5
Herbie13.5
\[\sqrt{\frac{1}{2} + \frac{\mathsf{copysign}\left(\frac{1}{2}, x\right)}{\mathsf{hypot}\left(1, \frac{2 \cdot p}{x}\right)}}\]

Derivation

  1. Initial program 13.5

    \[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]
  2. Simplified13.5

    \[\leadsto \color{blue}{\sqrt{\mathsf{fma}\left(\frac{x}{\sqrt{\mathsf{fma}\left(p, 4 \cdot p, x \cdot x\right)}}, 0.5, 0.5\right)}}\]
  3. Using strategy rm
  4. Applied div-inv13.7

    \[\leadsto \sqrt{\mathsf{fma}\left(\color{blue}{x \cdot \frac{1}{\sqrt{\mathsf{fma}\left(p, 4 \cdot p, x \cdot x\right)}}}, 0.5, 0.5\right)}\]
  5. Using strategy rm
  6. Applied add-log-exp13.8

    \[\leadsto \color{blue}{\log \left(e^{\sqrt{\mathsf{fma}\left(x \cdot \frac{1}{\sqrt{\mathsf{fma}\left(p, 4 \cdot p, x \cdot x\right)}}, 0.5, 0.5\right)}}\right)}\]
  7. Simplified13.5

    \[\leadsto \log \color{blue}{\left(e^{\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}}, 0.5\right)}}\right)}\]
  8. Using strategy rm
  9. Applied add-sqr-sqrt13.5

    \[\leadsto \log \left(e^{\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\color{blue}{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)} \cdot \sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}}}}, 0.5\right)}}\right)\]
  10. Applied sqrt-prod14.4

    \[\leadsto \log \left(e^{\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\color{blue}{\sqrt{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}} \cdot \sqrt{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}}}}, 0.5\right)}}\right)\]
  11. Using strategy rm
  12. Applied *-un-lft-identity14.4

    \[\leadsto \log \color{blue}{\left(1 \cdot e^{\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}} \cdot \sqrt{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}}}, 0.5\right)}}\right)}\]
  13. Applied log-prod14.4

    \[\leadsto \color{blue}{\log 1 + \log \left(e^{\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}} \cdot \sqrt{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}}}, 0.5\right)}}\right)}\]
  14. Simplified14.4

    \[\leadsto \color{blue}{0} + \log \left(e^{\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}} \cdot \sqrt{\sqrt{\mathsf{fma}\left(p, p \cdot 4, x \cdot x\right)}}}, 0.5\right)}}\right)\]
  15. Simplified13.5

    \[\leadsto 0 + \color{blue}{\sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\mathsf{fma}\left(p \cdot 4, p, x \cdot x\right)}}, 0.5\right)}}\]
  16. Final simplification13.5

    \[\leadsto \sqrt{\mathsf{fma}\left(0.5, \frac{x}{\sqrt{\mathsf{fma}\left(p \cdot 4, p, x \cdot x\right)}}, 0.5\right)}\]

Reproduce

herbie shell --seed 2019138 +o rules:numerics
(FPCore (p x)
  :name "Given's Rotation SVD example"
  :pre (< 1e-150 (fabs x) 1e+150)

  :herbie-target
  (sqrt (+ 1/2 (/ (copysign 1/2 x) (hypot 1 (/ (* 2 p) x)))))

  (sqrt (* 0.5 (+ 1 (/ x (sqrt (+ (* (* 4 p) p) (* x x))))))))