Given's Rotation SVD example

Average Error: 14.0 → 14.0

Time: 31.2s

Precision: 64

\[10^{-150} \lt \left|x\right| \lt 10^{+150}\]

Math

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

↓

\[\frac{\sqrt{\mathsf{fma}\left(\frac{x}{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}} \cdot \frac{x \cdot x}{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}, 0.5, 0.5\right)}}{\sqrt{\mathsf{fma}\left(\frac{x}{{e}^{\left(\log \left(\sqrt[3]{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}} \cdot \sqrt[3]{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}}\right)\right)} \cdot {e}^{\left(\log \left(\sqrt[3]{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}}\right)\right)}}, \frac{x}{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}} - 1, 1\right)}}\]

C

double f(double p, double x) {
        double r3943667 = 0.5;
        double r3943668 = 1.0;
        double r3943669 = x;
        double r3943670 = 4.0;
        double r3943671 = p;
        double r3943672 = r3943670 * r3943671;
        double r3943673 = r3943672 * r3943671;
        double r3943674 = r3943669 * r3943669;
        double r3943675 = r3943673 + r3943674;
        double r3943676 = sqrt(r3943675);
        double r3943677 = r3943669 / r3943676;
        double r3943678 = r3943668 + r3943677;
        double r3943679 = r3943667 * r3943678;
        double r3943680 = sqrt(r3943679);
        return r3943680;
}

↓

double f(double p, double x) {
        double r3943681 = x;
        double r3943682 = 4.0;
        double r3943683 = p;
        double r3943684 = r3943683 * r3943683;
        double r3943685 = r3943681 * r3943681;
        double r3943686 = fma(r3943682, r3943684, r3943685);
        double r3943687 = sqrt(r3943686);
        double r3943688 = r3943681 / r3943687;
        double r3943689 = r3943685 / r3943686;
        double r3943690 = r3943688 * r3943689;
        double r3943691 = 0.5;
        double r3943692 = fma(r3943690, r3943691, r3943691);
        double r3943693 = sqrt(r3943692);
        double r3943694 = exp(1.0);
        double r3943695 = cbrt(r3943687);
        double r3943696 = r3943695 * r3943695;
        double r3943697 = log(r3943696);
        double r3943698 = pow(r3943694, r3943697);
        double r3943699 = log(r3943695);
        double r3943700 = pow(r3943694, r3943699);
        double r3943701 = r3943698 * r3943700;
        double r3943702 = r3943681 / r3943701;
        double r3943703 = 1.0;
        double r3943704 = r3943688 - r3943703;
        double r3943705 = fma(r3943702, r3943704, r3943703);
        double r3943706 = sqrt(r3943705);
        double r3943707 = r3943693 / r3943706;
        return r3943707;
}

Error

Bits error versus p

Bits error versus x

Target

Original	14.0
Target	14.0
Herbie	14.0

\[\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 14.0

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

3. Applied flip3-+ 14.0

   \[\leadsto \sqrt{0.5 \cdot \color{blue}{\frac{{1}^{3} + {\left(\frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}^{3}}{1 \cdot 1 + \left(\frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}} \cdot \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}} - 1 \cdot \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}}}\]

4. Applied associate-*r/ 14.0

   \[\leadsto \sqrt{\color{blue}{\frac{0.5 \cdot \left({1}^{3} + {\left(\frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}^{3}\right)}{1 \cdot 1 + \left(\frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}} \cdot \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}} - 1 \cdot \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}}}\]

5. Applied sqrt-div 14.0

   \[\leadsto \color{blue}{\frac{\sqrt{0.5 \cdot \left({1}^{3} + {\left(\frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}^{3}\right)}}{\sqrt{1 \cdot 1 + \left(\frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}} \cdot \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}} - 1 \cdot \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}}}\]

6. Simplified 14.0

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

7. Simplified 14.0

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

9. Applied add-exp-log 14.0

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

11. Applied pow1 14.0

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

12. Applied log-pow 14.0

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

13. Applied exp-prod 14.0

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

14. Simplified 14.0

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

16. Applied add-cube-cbrt 14.0

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

17. Applied log-prod 14.0

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

18. Applied unpow-prod-up 14.0

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

19. Final simplification 14.0

    \[\leadsto \frac{\sqrt{\mathsf{fma}\left(\frac{x}{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}} \cdot \frac{x \cdot x}{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}, 0.5, 0.5\right)}}{\sqrt{\mathsf{fma}\left(\frac{x}{{e}^{\left(\log \left(\sqrt[3]{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}} \cdot \sqrt[3]{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}}\right)\right)} \cdot {e}^{\left(\log \left(\sqrt[3]{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}}\right)\right)}}, \frac{x}{\sqrt{\mathsf{fma}\left(4, p \cdot p, x \cdot x\right)}} - 1, 1\right)}}\]

Reproduce

herbie shell --seed 2019154 +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))))))))