Average Error: 13.3 → 13.8
Time: 32.2s
Precision: 64
\[10^{-150} \lt \left|x\right| \lt 10^{+150}\]
\[\sqrt{0.5 \cdot \left(1.0 + \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}}\right)}\]
↓
\[\sqrt{\frac{\left(\frac{x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} \cdot x\right) \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} + \left(1.0 \cdot 1.0\right) \cdot 1.0}{\frac{x \cdot x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} - 1.0 \cdot \left(\frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} - 1.0\right)} \cdot 0.5}\]
\sqrt{0.5 \cdot \left(1.0 + \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}}\right)}
↓
\sqrt{\frac{\left(\frac{x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} \cdot x\right) \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} + \left(1.0 \cdot 1.0\right) \cdot 1.0}{\frac{x \cdot x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} - 1.0 \cdot \left(\frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} - 1.0\right)} \cdot 0.5}
double f(double p, double x) {
        double r6648879 = 0.5;
        double r6648880 = 1.0;
        double r6648881 = x;
        double r6648882 = 4.0;
        double r6648883 = p;
        double r6648884 = r6648882 * r6648883;
        double r6648885 = r6648884 * r6648883;
        double r6648886 = r6648881 * r6648881;
        double r6648887 = r6648885 + r6648886;
        double r6648888 = sqrt(r6648887);
        double r6648889 = r6648881 / r6648888;
        double r6648890 = r6648880 + r6648889;
        double r6648891 = r6648879 * r6648890;
        double r6648892 = sqrt(r6648891);
        return r6648892;
}
↓
double f(double p, double x) {
        double r6648893 = x;
        double r6648894 = 4.0;
        double r6648895 = p;
        double r6648896 = r6648894 * r6648895;
        double r6648897 = r6648896 * r6648895;
        double r6648898 = r6648893 * r6648893;
        double r6648899 = r6648897 + r6648898;
        double r6648900 = r6648893 / r6648899;
        double r6648901 = r6648900 * r6648893;
        double r6648902 = sqrt(r6648899);
        double r6648903 = r6648893 / r6648902;
        double r6648904 = r6648901 * r6648903;
        double r6648905 = 1.0;
        double r6648906 = r6648905 * r6648905;
        double r6648907 = r6648906 * r6648905;
        double r6648908 = r6648904 + r6648907;
        double r6648909 = r6648898 / r6648899;
        double r6648910 = r6648903 - r6648905;
        double r6648911 = r6648905 * r6648910;
        double r6648912 = r6648909 - r6648911;
        double r6648913 = r6648908 / r6648912;
        double r6648914 = 0.5;
        double r6648915 = r6648913 * r6648914;
        double r6648916 = sqrt(r6648915);
        return r6648916;
}

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.3
Target13.3
Herbie13.8
\[\sqrt{0.5 + \frac{\mathsf{copysign}\left(0.5, x\right)}{\mathsf{hypot}\left(1.0, \frac{2.0 \cdot p}{x}\right)}}\]

Derivation

  1. Initial program 13.3

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

  3. Applied flip3-+13.3

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

  4. Simplified13.3

    \[\leadsto \sqrt{0.5 \cdot \frac{\color{blue}{1.0 \cdot \left(1.0 \cdot 1.0\right) + \frac{x \cdot x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}}}}{1.0 \cdot 1.0 + \left(\frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} - 1.0 \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}}\right)}}\]

  5. Simplified13.3

    \[\leadsto \sqrt{0.5 \cdot \frac{1.0 \cdot \left(1.0 \cdot 1.0\right) + \frac{x \cdot x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}}}{\color{blue}{\frac{x \cdot x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} - 1.0 \cdot \left(\frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} - 1.0\right)}}}\]
  6. Using strategy rm

  7. Applied associate-/l*13.5

    \[\leadsto \sqrt{0.5 \cdot \frac{1.0 \cdot \left(1.0 \cdot 1.0\right) + \color{blue}{\frac{x}{\frac{\left(4.0 \cdot p\right) \cdot p + x \cdot x}{x}}} \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}}}{\frac{x \cdot x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} - 1.0 \cdot \left(\frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} - 1.0\right)}}\]
  8. Using strategy rm

  9. Applied associate-/r/13.8

    \[\leadsto \sqrt{0.5 \cdot \frac{1.0 \cdot \left(1.0 \cdot 1.0\right) + \color{blue}{\left(\frac{x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} \cdot x\right)} \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}}}{\frac{x \cdot x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} - 1.0 \cdot \left(\frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} - 1.0\right)}}\]

  10. Final simplification13.8

    \[\leadsto \sqrt{\frac{\left(\frac{x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} \cdot x\right) \cdot \frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} + \left(1.0 \cdot 1.0\right) \cdot 1.0}{\frac{x \cdot x}{\left(4.0 \cdot p\right) \cdot p + x \cdot x} - 1.0 \cdot \left(\frac{x}{\sqrt{\left(4.0 \cdot p\right) \cdot p + x \cdot x}} - 1.0\right)} \cdot 0.5}\]

Reproduce

herbie shell --seed 2019165 
(FPCore (p x)
  :name "Given's Rotation SVD example"
  :pre (< 1e-150 (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))))))))