Given's Rotation SVD example

Average Error: 13.6 → 13.6

Time: 14.8s

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

C

double f(double p, double x) {
        double r380069 = 0.5;
        double r380070 = 1.0;
        double r380071 = x;
        double r380072 = 4.0;
        double r380073 = p;
        double r380074 = r380072 * r380073;
        double r380075 = r380074 * r380073;
        double r380076 = r380071 * r380071;
        double r380077 = r380075 + r380076;
        double r380078 = sqrt(r380077);
        double r380079 = r380071 / r380078;
        double r380080 = r380070 + r380079;
        double r380081 = r380069 * r380080;
        double r380082 = sqrt(r380081);
        return r380082;
}

↓

double f(double p, double x) {
        double r380083 = x;
        double r380084 = -1.7221823146561012e-133;
        bool r380085 = r380083 <= r380084;
        double r380086 = 1.0;
        double r380087 = r380086 * r380086;
        double r380088 = 4.0;
        double r380089 = p;
        double r380090 = r380088 * r380089;
        double r380091 = 2.0;
        double r380092 = pow(r380083, r380091);
        double r380093 = fma(r380090, r380089, r380092);
        double r380094 = sqrt(r380093);
        double r380095 = r380083 / r380094;
        double r380096 = r380095 * r380083;
        double r380097 = r380096 / r380094;
        double r380098 = r380087 - r380097;
        double r380099 = 0.5;
        double r380100 = r380098 * r380099;
        double r380101 = sqrt(r380100);
        double r380102 = r380086 - r380095;
        double r380103 = sqrt(r380102);
        double r380104 = r380101 / r380103;
        double r380105 = 3.0;
        double r380106 = pow(r380086, r380105);
        double r380107 = cbrt(r380094);
        double r380108 = fabs(r380107);
        double r380109 = sqrt(r380094);
        double r380110 = r380108 * r380109;
        double r380111 = sqrt(r380107);
        double r380112 = r380110 * r380111;
        double r380113 = r380083 / r380112;
        double r380114 = pow(r380113, r380105);
        double r380115 = r380106 + r380114;
        double r380116 = r380113 - r380086;
        double r380117 = r380113 * r380116;
        double r380118 = fma(r380086, r380086, r380117);
        double r380119 = r380115 / r380118;
        double r380120 = pow(r380119, r380105);
        double r380121 = cbrt(r380120);
        double r380122 = r380099 * r380121;
        double r380123 = sqrt(r380122);
        double r380124 = r380085 ? r380104 : r380123;
        return r380124;
}

Error

Bits error versus p

Bits error versus x

Target

Original	13.6
Target	13.6
Herbie	13.6

\[\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.7221823146561012e-133

   1. Initial program 27.1

      \[\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.1

      \[\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. Applied associate-*r/ 27.1

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

   5. Applied sqrt-div 27.1

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

   6. Simplified 27.1

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

   7. Simplified 27.1

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

   if -1.7221823146561012e-133 < x

   1. Initial program 1.2

      \[\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-sqrt 1.2

      \[\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-prod 1.2

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

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

   6. Simplified 1.2

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

   8. Applied add-cube-cbrt 1.3

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

   9. Applied sqrt-prod 1.3

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

   10. Applied associate-*r* 1.3

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

   11. Simplified 1.3

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

   13. Applied add-cbrt-cube 1.2

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

   14. Simplified 1.2

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

   16. Applied flip3-+ 1.2

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

   17. Simplified 1.2

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

4. Final simplification 13.6

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

Reproduce

herbie shell --seed 2019208 +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))))))))