Given's Rotation SVD example

Average Error: 13.5 → 14.5

Time: 21.0s

Precision: 64

\[10^{-150} \lt \left|x\right| \lt 10^{+150}\]

Math

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

↓

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

C

double f(double p, double x) {
        double r10745449 = 0.5;
        double r10745450 = 1.0;
        double r10745451 = x;
        double r10745452 = 4.0;
        double r10745453 = p;
        double r10745454 = r10745452 * r10745453;
        double r10745455 = r10745454 * r10745453;
        double r10745456 = r10745451 * r10745451;
        double r10745457 = r10745455 + r10745456;
        double r10745458 = sqrt(r10745457);
        double r10745459 = r10745451 / r10745458;
        double r10745460 = r10745450 + r10745459;
        double r10745461 = r10745449 * r10745460;
        double r10745462 = sqrt(r10745461);
        return r10745462;
}

↓

double f(double p, double x) {
        double r10745463 = 0.5;
        double r10745464 = r10745463 * r10745463;
        double r10745465 = r10745464 * r10745463;
        double r10745466 = x;
        double r10745467 = r10745466 * r10745463;
        double r10745468 = p;
        double r10745469 = 4.0;
        double r10745470 = r10745468 * r10745469;
        double r10745471 = r10745470 * r10745468;
        double r10745472 = r10745466 * r10745466;
        double r10745473 = r10745471 + r10745472;
        double r10745474 = r10745467 / r10745473;
        double r10745475 = r10745467 * r10745467;
        double r10745476 = sqrt(r10745473);
        double r10745477 = sqrt(r10745476);
        double r10745478 = r10745477 * r10745477;
        double r10745479 = r10745475 / r10745478;
        double r10745480 = r10745474 * r10745479;
        double r10745481 = r10745465 + r10745480;
        double r10745482 = r10745463 / r10745476;
        double r10745483 = r10745466 * r10745482;
        double r10745484 = r10745483 - r10745463;
        double r10745485 = r10745483 * r10745484;
        double r10745486 = r10745464 + r10745485;
        double r10745487 = r10745481 / r10745486;
        double r10745488 = sqrt(r10745487);
        double r10745489 = exp(r10745488);
        double r10745490 = log(r10745489);
        return r10745490;
}

Error

Bits error versus p

Bits error versus x

Target

Original	13.5
Target	13.5
Herbie	14.5

\[\sqrt{\frac{1}{2} + \frac{\mathsf{copysign}\left(\frac{1}{2}, x\right)}{\mathsf{hypot}\left(1, \frac{2 \cdot p}{x}\right)}}\]

Derivation

1. Initial program 13.5

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

2. Simplified 13.5

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

4. Applied add-log-exp 13.5

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

6. Applied add-cbrt-cube 14.3

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

8. Applied flip3-+ 14.3

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

9. Applied flip3-+ 14.3

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

10. Applied flip3-+ 14.3

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

11. Applied frac-times 14.3

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

12. Applied frac-times 14.3

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

13. Applied cbrt-div 13.5

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

14. Simplified 14.0

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

15. Simplified 14.0

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

17. Applied add-sqr-sqrt 14.5

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

18. Final simplification 14.5

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

Reproduce

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