Average Error: 13.3 → 13.6
Time: 6.0s
Precision: 64
\[1.00000000000000001 \cdot 10^{-150} \lt \left|x\right| \lt 9.99999999999999981 \cdot 10^{149}\]
\[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]
↓
\[\log \left(\sqrt{e^{\sqrt{0.5 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(1 + x \cdot \frac{1}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)\right)}}}\right) + \log \left(\sqrt{e^{\sqrt{0.5 \cdot \left(1 + x \cdot \frac{1}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}}}\right)\]
\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}
↓
\log \left(\sqrt{e^{\sqrt{0.5 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(1 + x \cdot \frac{1}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)\right)}}}\right) + \log \left(\sqrt{e^{\sqrt{0.5 \cdot \left(1 + x \cdot \frac{1}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}}}\right)
double f(double p, double x) {
        double r254339 = 0.5;
        double r254340 = 1.0;
        double r254341 = x;
        double r254342 = 4.0;
        double r254343 = p;
        double r254344 = r254342 * r254343;
        double r254345 = r254344 * r254343;
        double r254346 = r254341 * r254341;
        double r254347 = r254345 + r254346;
        double r254348 = sqrt(r254347);
        double r254349 = r254341 / r254348;
        double r254350 = r254340 + r254349;
        double r254351 = r254339 * r254350;
        double r254352 = sqrt(r254351);
        return r254352;
}
↓
double f(double p, double x) {
        double r254353 = 0.5;
        double r254354 = 1.0;
        double r254355 = x;
        double r254356 = 1.0;
        double r254357 = 4.0;
        double r254358 = p;
        double r254359 = r254357 * r254358;
        double r254360 = r254359 * r254358;
        double r254361 = r254355 * r254355;
        double r254362 = r254360 + r254361;
        double r254363 = sqrt(r254362);
        double r254364 = r254356 / r254363;
        double r254365 = r254355 * r254364;
        double r254366 = r254354 + r254365;
        double r254367 = log1p(r254366);
        double r254368 = expm1(r254367);
        double r254369 = r254353 * r254368;
        double r254370 = sqrt(r254369);
        double r254371 = exp(r254370);
        double r254372 = sqrt(r254371);
        double r254373 = log(r254372);
        double r254374 = r254353 * r254366;
        double r254375 = sqrt(r254374);
        double r254376 = exp(r254375);
        double r254377 = sqrt(r254376);
        double r254378 = log(r254377);
        double r254379 = r254373 + r254378;
        return r254379;
}

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.6
\[\sqrt{0.5 + \frac{\mathsf{copysign}\left(0.5, x\right)}{\mathsf{hypot}\left(1, \frac{2 \cdot p}{x}\right)}}\]

Derivation

  1. Initial program 13.3

    \[\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 div-inv13.5

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

  5. Applied add-log-exp13.6

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

  7. Applied add-sqr-sqrt13.6

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

  8. Applied log-prod13.6

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

  10. Applied expm1-log1p-u13.6

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

  11. Final simplification13.6

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

Reproduce

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

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

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