Average Error: 13.1 → 14.1
Time: 22.6s
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)}\]
↓
\[\log \left(e^{\frac{\sqrt{\left(\left(\frac{x \cdot x}{\sqrt{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot \sqrt{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}}} \cdot \frac{x}{p \cdot \left(p \cdot 4\right) + x \cdot x}\right) \cdot 0.5 + 0.5\right) \cdot \left(0.5 \cdot 0.5\right)}}{\sqrt{\left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right) \cdot \left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right) + \left(0.5 \cdot 0.5 - 0.5 \cdot \left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right)\right)}}}\right)\]
\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}
↓
\log \left(e^{\frac{\sqrt{\left(\left(\frac{x \cdot x}{\sqrt{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot \sqrt{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}}} \cdot \frac{x}{p \cdot \left(p \cdot 4\right) + x \cdot x}\right) \cdot 0.5 + 0.5\right) \cdot \left(0.5 \cdot 0.5\right)}}{\sqrt{\left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right) \cdot \left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right) + \left(0.5 \cdot 0.5 - 0.5 \cdot \left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right)\right)}}}\right)
double f(double p, double x) {
        double r67967689 = 0.5;
        double r67967690 = 1.0;
        double r67967691 = x;
        double r67967692 = 4.0;
        double r67967693 = p;
        double r67967694 = r67967692 * r67967693;
        double r67967695 = r67967694 * r67967693;
        double r67967696 = r67967691 * r67967691;
        double r67967697 = r67967695 + r67967696;
        double r67967698 = sqrt(r67967697);
        double r67967699 = r67967691 / r67967698;
        double r67967700 = r67967690 + r67967699;
        double r67967701 = r67967689 * r67967700;
        double r67967702 = sqrt(r67967701);
        return r67967702;
}
↓
double f(double p, double x) {
        double r67967703 = x;
        double r67967704 = r67967703 * r67967703;
        double r67967705 = p;
        double r67967706 = 4.0;
        double r67967707 = r67967705 * r67967706;
        double r67967708 = r67967705 * r67967707;
        double r67967709 = r67967708 + r67967704;
        double r67967710 = sqrt(r67967709);
        double r67967711 = sqrt(r67967710);
        double r67967712 = r67967711 * r67967711;
        double r67967713 = r67967704 / r67967712;
        double r67967714 = r67967703 / r67967709;
        double r67967715 = r67967713 * r67967714;
        double r67967716 = 0.5;
        double r67967717 = r67967715 * r67967716;
        double r67967718 = r67967717 + r67967716;
        double r67967719 = r67967716 * r67967716;
        double r67967720 = r67967718 * r67967719;
        double r67967721 = sqrt(r67967720);
        double r67967722 = r67967703 / r67967710;
        double r67967723 = r67967722 * r67967716;
        double r67967724 = r67967723 * r67967723;
        double r67967725 = r67967716 * r67967723;
        double r67967726 = r67967719 - r67967725;
        double r67967727 = r67967724 + r67967726;
        double r67967728 = sqrt(r67967727);
        double r67967729 = r67967721 / r67967728;
        double r67967730 = exp(r67967729);
        double r67967731 = log(r67967730);
        return r67967731;
}

Error

Bits error versus p

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

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

Derivation

  1. Initial program 13.1

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

  2. Simplified13.1

    \[\leadsto \color{blue}{\sqrt{0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}} + 0.5}}\]
  3. Using strategy rm

  4. Applied add-log-exp13.2

    \[\leadsto \color{blue}{\log \left(e^{\sqrt{0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}} + 0.5}}\right)}\]
  5. Using strategy rm

  6. Applied flip3-+13.2

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

  7. Applied sqrt-div13.2

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

  8. Simplified13.6

    \[\leadsto \log \left(e^{\frac{\color{blue}{\sqrt{\left(0.5 \cdot \left(\frac{x \cdot x}{\sqrt{x \cdot x + p \cdot \left(p \cdot 4\right)}} \cdot \frac{x}{x \cdot x + p \cdot \left(p \cdot 4\right)}\right) + 0.5\right) \cdot \left(0.5 \cdot 0.5\right)}}}{\sqrt{\left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right) \cdot \left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right) + \left(0.5 \cdot 0.5 - \left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right) \cdot 0.5\right)}}}\right)\]
  9. Using strategy rm

  10. Applied add-sqr-sqrt13.6

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

  11. Applied sqrt-prod14.1

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

  12. Final simplification14.1

    \[\leadsto \log \left(e^{\frac{\sqrt{\left(\left(\frac{x \cdot x}{\sqrt{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot \sqrt{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}}} \cdot \frac{x}{p \cdot \left(p \cdot 4\right) + x \cdot x}\right) \cdot 0.5 + 0.5\right) \cdot \left(0.5 \cdot 0.5\right)}}{\sqrt{\left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right) \cdot \left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right) + \left(0.5 \cdot 0.5 - 0.5 \cdot \left(\frac{x}{\sqrt{p \cdot \left(p \cdot 4\right) + x \cdot x}} \cdot 0.5\right)\right)}}}\right)\]

Reproduce

herbie shell --seed 2019121 
(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))))))))