Average Error: 13.0 → 13.0
Time: 16.7s
Precision: 64
\[1.000000000000000006295358232172963997211 \cdot 10^{-150} \lt \left|x\right| \lt 9.999999999999999808355961724373745905731 \cdot 10^{149}\]
\[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \le -1.08656835205634492253514124544623283701 \cdot 10^{-115}:\\ \;\;\;\;\sqrt{0.5 \cdot \frac{1 \cdot 1 - \frac{x \cdot x}{4 \cdot {p}^{2} + {x}^{2}}}{1 - \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}} \cdot \frac{x}{\sqrt{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}}\right)}\\ \end{array}\]
\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}
↓
\begin{array}{l}
\mathbf{if}\;x \le -1.08656835205634492253514124544623283701 \cdot 10^{-115}:\\
\;\;\;\;\sqrt{0.5 \cdot \frac{1 \cdot 1 - \frac{x \cdot x}{4 \cdot {p}^{2} + {x}^{2}}}{1 - \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}}}\\

\mathbf{else}:\\
\;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}} \cdot \frac{x}{\sqrt{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}}\right)}\\

\end{array}
double f(double p, double x) {
        double r133574 = 0.5;
        double r133575 = 1.0;
        double r133576 = x;
        double r133577 = 4.0;
        double r133578 = p;
        double r133579 = r133577 * r133578;
        double r133580 = r133579 * r133578;
        double r133581 = r133576 * r133576;
        double r133582 = r133580 + r133581;
        double r133583 = sqrt(r133582);
        double r133584 = r133576 / r133583;
        double r133585 = r133575 + r133584;
        double r133586 = r133574 * r133585;
        double r133587 = sqrt(r133586);
        return r133587;
}
↓
double f(double p, double x) {
        double r133588 = x;
        double r133589 = -1.086568352056345e-115;
        bool r133590 = r133588 <= r133589;
        double r133591 = 0.5;
        double r133592 = 1.0;
        double r133593 = r133592 * r133592;
        double r133594 = r133588 * r133588;
        double r133595 = 4.0;
        double r133596 = p;
        double r133597 = 2.0;
        double r133598 = pow(r133596, r133597);
        double r133599 = r133595 * r133598;
        double r133600 = pow(r133588, r133597);
        double r133601 = r133599 + r133600;
        double r133602 = r133594 / r133601;
        double r133603 = r133593 - r133602;
        double r133604 = r133595 * r133596;
        double r133605 = r133604 * r133596;
        double r133606 = r133605 + r133594;
        double r133607 = sqrt(r133606);
        double r133608 = r133588 / r133607;
        double r133609 = r133592 - r133608;
        double r133610 = r133603 / r133609;
        double r133611 = r133591 * r133610;
        double r133612 = sqrt(r133611);
        double r133613 = 1.0;
        double r133614 = sqrt(r133607);
        double r133615 = r133613 / r133614;
        double r133616 = r133588 / r133614;
        double r133617 = r133615 * r133616;
        double r133618 = r133592 + r133617;
        double r133619 = r133591 * r133618;
        double r133620 = sqrt(r133619);
        double r133621 = r133590 ? r133612 : r133620;
        return r133621;
}

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

Derivation

  1. Split input into 2 regimes

  2. if x < -1.086568352056345e-115

    1. Initial program 27.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 flip-+27.3

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

    4. Simplified27.3

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

    if -1.086568352056345e-115 < x

    1. Initial program 1.7

      \[\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 add-sqr-sqrt1.7

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

    4. Applied sqrt-prod1.7

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

    5. Applied *-un-lft-identity1.7

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

    6. Applied times-frac1.7

      \[\leadsto \sqrt{0.5 \cdot \left(1 + \color{blue}{\frac{1}{\sqrt{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}} \cdot \frac{x}{\sqrt{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}}}\right)}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification13.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.08656835205634492253514124544623283701 \cdot 10^{-115}:\\ \;\;\;\;\sqrt{0.5 \cdot \frac{1 \cdot 1 - \frac{x \cdot x}{4 \cdot {p}^{2} + {x}^{2}}}{1 - \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5 \cdot \left(1 + \frac{1}{\sqrt{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}} \cdot \frac{x}{\sqrt{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}}\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019304 
(FPCore (p x)
  :name "Given's Rotation SVD example"
  :precision binary64
  :pre (< 1.00000000000000001e-150 (fabs x) 9.99999999999999981e149)

  :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))))))))