Average Error: 13.0 → 13.3
Time: 20.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)}\]
↓
\[\frac{\sqrt{\frac{\left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right) \cdot \left(\left(\frac{1}{x \cdot x + p \cdot \left(4 \cdot p\right)} \cdot \left(x \cdot x\right)\right) \cdot x\right)}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}} + 0.5 \cdot \left(0.5 \cdot 0.5\right)}}{\sqrt{0.5 \cdot 0.5 - \left(0.5 - \frac{x \cdot 0.5}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right) \cdot \frac{x \cdot 0.5}{e^{\log \left(\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}\right)}}}}\]
\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}
↓
\frac{\sqrt{\frac{\left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right) \cdot \left(\left(\frac{1}{x \cdot x + p \cdot \left(4 \cdot p\right)} \cdot \left(x \cdot x\right)\right) \cdot x\right)}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}} + 0.5 \cdot \left(0.5 \cdot 0.5\right)}}{\sqrt{0.5 \cdot 0.5 - \left(0.5 - \frac{x \cdot 0.5}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right) \cdot \frac{x \cdot 0.5}{e^{\log \left(\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}\right)}}}}
double f(double p, double x) {
        double r7615292 = 0.5;
        double r7615293 = 1.0;
        double r7615294 = x;
        double r7615295 = 4.0;
        double r7615296 = p;
        double r7615297 = r7615295 * r7615296;
        double r7615298 = r7615297 * r7615296;
        double r7615299 = r7615294 * r7615294;
        double r7615300 = r7615298 + r7615299;
        double r7615301 = sqrt(r7615300);
        double r7615302 = r7615294 / r7615301;
        double r7615303 = r7615293 + r7615302;
        double r7615304 = r7615292 * r7615303;
        double r7615305 = sqrt(r7615304);
        return r7615305;
}
↓
double f(double p, double x) {
        double r7615306 = 0.5;
        double r7615307 = r7615306 * r7615306;
        double r7615308 = r7615306 * r7615307;
        double r7615309 = 1.0;
        double r7615310 = x;
        double r7615311 = r7615310 * r7615310;
        double r7615312 = p;
        double r7615313 = 4.0;
        double r7615314 = r7615313 * r7615312;
        double r7615315 = r7615312 * r7615314;
        double r7615316 = r7615311 + r7615315;
        double r7615317 = r7615309 / r7615316;
        double r7615318 = r7615317 * r7615311;
        double r7615319 = r7615318 * r7615310;
        double r7615320 = r7615308 * r7615319;
        double r7615321 = sqrt(r7615316);
        double r7615322 = r7615320 / r7615321;
        double r7615323 = r7615322 + r7615308;
        double r7615324 = sqrt(r7615323);
        double r7615325 = r7615310 * r7615306;
        double r7615326 = r7615325 / r7615321;
        double r7615327 = r7615306 - r7615326;
        double r7615328 = log(r7615321);
        double r7615329 = exp(r7615328);
        double r7615330 = r7615325 / r7615329;
        double r7615331 = r7615327 * r7615330;
        double r7615332 = r7615307 - r7615331;
        double r7615333 = sqrt(r7615332);
        double r7615334 = r7615324 / r7615333;
        return r7615334;
}

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.0
Target13.0
Herbie13.3
\[\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.0

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

  2. Simplified13.0

    \[\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 flip3-+13.0

    \[\leadsto \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)}}}\]

  5. Applied sqrt-div13.0

    \[\leadsto \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)}}}\]

  6. Simplified13.0

    \[\leadsto \frac{\color{blue}{\sqrt{\frac{\left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right) \cdot \left(x \cdot \frac{x \cdot x}{x \cdot x + \left(p \cdot 4\right) \cdot p}\right)}{\sqrt{x \cdot x + \left(p \cdot 4\right) \cdot p}} + 0.5 \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)}}\]

  7. Simplified13.0

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

  9. Applied div-inv13.3

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

  11. Applied add-exp-log13.3

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

  12. Final simplification13.3

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

Reproduce

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