Given's Rotation SVD example

Average Error: 13.0 → 13.0

Time: 18.6s

Precision: 64

\[1.000000000000000006295358232172963997211 \cdot 10^{-150} \lt \left|x\right| \lt 9.999999999999999808355961724373745905731 \cdot 10^{149}\]

Math

\[\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 -6.891572154331307140835027016342443861372 \cdot 10^{-140}:\\ \;\;\;\;\sqrt{0.5 \cdot \frac{1 \cdot 1 - \frac{x \cdot x}{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}{1 - \frac{x}{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5 \cdot \sqrt[3]{{\left(\mathsf{fma}\left(\frac{x}{\left|\sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}\right|}, \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|}, 1\right)\right)}^{3}}}\\ \end{array}\]

C

double f(double p, double x) {
        double r147184 = 0.5;
        double r147185 = 1.0;
        double r147186 = x;
        double r147187 = 4.0;
        double r147188 = p;
        double r147189 = r147187 * r147188;
        double r147190 = r147189 * r147188;
        double r147191 = r147186 * r147186;
        double r147192 = r147190 + r147191;
        double r147193 = sqrt(r147192);
        double r147194 = r147186 / r147193;
        double r147195 = r147185 + r147194;
        double r147196 = r147184 * r147195;
        double r147197 = sqrt(r147196);
        return r147197;
}

↓

double f(double p, double x) {
        double r147198 = x;
        double r147199 = -6.891572154331307e-140;
        bool r147200 = r147198 <= r147199;
        double r147201 = 0.5;
        double r147202 = 1.0;
        double r147203 = r147202 * r147202;
        double r147204 = r147198 * r147198;
        double r147205 = 4.0;
        double r147206 = p;
        double r147207 = 2.0;
        double r147208 = pow(r147206, r147207);
        double r147209 = pow(r147198, r147207);
        double r147210 = fma(r147205, r147208, r147209);
        double r147211 = r147204 / r147210;
        double r147212 = r147203 - r147211;
        double r147213 = sqrt(r147210);
        double r147214 = r147198 / r147213;
        double r147215 = r147202 - r147214;
        double r147216 = r147212 / r147215;
        double r147217 = r147201 * r147216;
        double r147218 = sqrt(r147217);
        double r147219 = cbrt(r147213);
        double r147220 = fabs(r147219);
        double r147221 = r147198 / r147220;
        double r147222 = 1.0;
        double r147223 = cbrt(r147210);
        double r147224 = fabs(r147223);
        double r147225 = r147222 / r147224;
        double r147226 = fma(r147221, r147225, r147202);
        double r147227 = 3.0;
        double r147228 = pow(r147226, r147227);
        double r147229 = cbrt(r147228);
        double r147230 = r147201 * r147229;
        double r147231 = sqrt(r147230);
        double r147232 = r147200 ? r147218 : r147231;
        return r147232;
}

Error

Bits error versus p

Bits error versus x

Target

Original	13.0
Target	13.0
Herbie	13.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 < -6.891572154331307e-140

   1. Initial program 26.4

      \[\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-+ 26.4

      \[\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. Simplified 26.4

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

   5. Simplified 26.4

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

   if -6.891572154331307e-140 < x

   1. Initial program 0.5

      \[\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-cube-cbrt 0.6

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

   4. Applied sqrt-prod 0.6

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

   5. Applied *-un-lft-identity 0.6

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

   6. Applied times-frac 0.7

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

   7. Simplified 0.7

      \[\leadsto \sqrt{0.5 \cdot \left(1 + \color{blue}{\frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|}} \cdot \frac{x}{\sqrt{\sqrt[3]{\left(4 \cdot p\right) \cdot p + x \cdot x}}}\right)}\]

   8. Simplified 0.7

      \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|} \cdot \color{blue}{\frac{x}{\sqrt{\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}}}\right)}\]
   9. Using strategy rm

   10. Applied add-sqr-sqrt 0.7

       \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|} \cdot \frac{x}{\sqrt{\sqrt[3]{\color{blue}{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)} \cdot \sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}}}}\right)}\]

   11. Applied cbrt-prod 0.7

       \[\leadsto \sqrt{0.5 \cdot \left(1 + \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|} \cdot \frac{x}{\sqrt{\color{blue}{\sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}} \cdot \sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}}}}\right)}\]
   12. Using strategy rm

   13. Applied add-cbrt-cube 0.6

       \[\leadsto \sqrt{0.5 \cdot \color{blue}{\sqrt[3]{\left(\left(1 + \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|} \cdot \frac{x}{\sqrt{\sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}} \cdot \sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}}}\right) \cdot \left(1 + \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|} \cdot \frac{x}{\sqrt{\sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}} \cdot \sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}}}\right)\right) \cdot \left(1 + \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|} \cdot \frac{x}{\sqrt{\sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}} \cdot \sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}}}\right)}}}\]

   14. Simplified 0.6

       \[\leadsto \sqrt{0.5 \cdot \sqrt[3]{\color{blue}{{\left(\frac{\frac{x}{\left|\sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}\right|}}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|} + 1\right)}^{3}}}}\]
   15. Using strategy rm

   16. Applied div-inv 0.6

       \[\leadsto \sqrt{0.5 \cdot \sqrt[3]{{\left(\color{blue}{\frac{x}{\left|\sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}\right|} \cdot \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|}} + 1\right)}^{3}}}\]

   17. Applied fma-def 0.6

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

4. Final simplification 13.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -6.891572154331307140835027016342443861372 \cdot 10^{-140}:\\ \;\;\;\;\sqrt{0.5 \cdot \frac{1 \cdot 1 - \frac{x \cdot x}{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}{1 - \frac{x}{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.5 \cdot \sqrt[3]{{\left(\mathsf{fma}\left(\frac{x}{\left|\sqrt[3]{\sqrt{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}}\right|}, \frac{1}{\left|\sqrt[3]{\mathsf{fma}\left(4, {p}^{2}, {x}^{2}\right)}\right|}, 1\right)\right)}^{3}}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019304 +o rules:numerics
(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))))))))