Falkner and Boettcher, Equation (20:1,3)

Average Error: 0.4 → 0.1

Time: 28.8s

Precision: 64

Math

\[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]

↓

\[\frac{\frac{\frac{\frac{1 - \left(v \cdot v\right) \cdot 5}{\sqrt{\left(2 \cdot \left(3 \cdot \left(v \cdot v\right) + 1\right)\right) \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}}{\pi}}{t}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\left(\left(\left(v \cdot v\right) \cdot 1 + \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right) + 1 \cdot 1\right) \cdot \sqrt{3 \cdot \left(v \cdot v\right) + 1}\right)\]

C

double f(double v, double t) {
        double r7964832 = 1.0;
        double r7964833 = 5.0;
        double r7964834 = v;
        double r7964835 = r7964834 * r7964834;
        double r7964836 = r7964833 * r7964835;
        double r7964837 = r7964832 - r7964836;
        double r7964838 = atan2(1.0, 0.0);
        double r7964839 = t;
        double r7964840 = r7964838 * r7964839;
        double r7964841 = 2.0;
        double r7964842 = 3.0;
        double r7964843 = r7964842 * r7964835;
        double r7964844 = r7964832 - r7964843;
        double r7964845 = r7964841 * r7964844;
        double r7964846 = sqrt(r7964845);
        double r7964847 = r7964840 * r7964846;
        double r7964848 = r7964832 - r7964835;
        double r7964849 = r7964847 * r7964848;
        double r7964850 = r7964837 / r7964849;
        return r7964850;
}

↓

double f(double v, double t) {
        double r7964851 = 1.0;
        double r7964852 = v;
        double r7964853 = r7964852 * r7964852;
        double r7964854 = 5.0;
        double r7964855 = r7964853 * r7964854;
        double r7964856 = r7964851 - r7964855;
        double r7964857 = 2.0;
        double r7964858 = 3.0;
        double r7964859 = r7964858 * r7964853;
        double r7964860 = r7964859 + r7964851;
        double r7964861 = r7964857 * r7964860;
        double r7964862 = r7964851 - r7964859;
        double r7964863 = r7964861 * r7964862;
        double r7964864 = sqrt(r7964863);
        double r7964865 = r7964856 / r7964864;
        double r7964866 = atan2(1.0, 0.0);
        double r7964867 = r7964865 / r7964866;
        double r7964868 = t;
        double r7964869 = r7964867 / r7964868;
        double r7964870 = r7964851 * r7964851;
        double r7964871 = r7964870 * r7964851;
        double r7964872 = r7964852 * r7964853;
        double r7964873 = r7964872 * r7964872;
        double r7964874 = r7964871 - r7964873;
        double r7964875 = r7964869 / r7964874;
        double r7964876 = r7964853 * r7964851;
        double r7964877 = r7964853 * r7964853;
        double r7964878 = r7964876 + r7964877;
        double r7964879 = r7964878 + r7964870;
        double r7964880 = sqrt(r7964860);
        double r7964881 = r7964879 * r7964880;
        double r7964882 = r7964875 * r7964881;
        return r7964882;
}

Error

Bits error versus v

Bits error versus t

Derivation

1. Initial program 0.4

   \[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]
2. Using strategy rm

3. Applied flip3-- 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \color{blue}{\frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}}\]

4. Applied flip-- 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \color{blue}{\frac{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

5. Applied associate-*r/ 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{\color{blue}{\frac{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

6. Applied sqrt-div 0.5

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \color{blue}{\frac{\sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

7. Applied associate-*r/ 0.5

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}} \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\]

8. Applied frac-times 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)}}}\]

9. Applied associate-/r/ 0.5

   \[\leadsto \color{blue}{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)}\]

10. Simplified 0.3

    \[\leadsto \color{blue}{\frac{\frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{\pi}}{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}}{1 \cdot \left(1 \cdot 1\right) - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)}} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
11. Using strategy rm

12. Applied *-un-lft-identity 0.3

    \[\leadsto \frac{\frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{\color{blue}{1 \cdot \pi}}}{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}}{1 \cdot \left(1 \cdot 1\right) - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

13. Applied *-un-lft-identity 0.3

    \[\leadsto \frac{\frac{\frac{\color{blue}{1 \cdot \left(1 - \left(5 \cdot v\right) \cdot v\right)}}{1 \cdot \pi}}{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}}{1 \cdot \left(1 \cdot 1\right) - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

14. Applied times-frac 0.3

    \[\leadsto \frac{\frac{\color{blue}{\frac{1}{1} \cdot \frac{1 - \left(5 \cdot v\right) \cdot v}{\pi}}}{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}}{1 \cdot \left(1 \cdot 1\right) - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

15. Applied times-frac 0.3

    \[\leadsto \frac{\color{blue}{\frac{\frac{1}{1}}{t} \cdot \frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{\pi}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}}}{1 \cdot \left(1 \cdot 1\right) - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

16. Simplified 0.3

    \[\leadsto \frac{\color{blue}{\frac{1}{t}} \cdot \frac{\frac{1 - \left(5 \cdot v\right) \cdot v}{\pi}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}}{1 \cdot \left(1 \cdot 1\right) - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

17. Simplified 0.3

    \[\leadsto \frac{\frac{1}{t} \cdot \color{blue}{\frac{\frac{1 - \left(v \cdot v\right) \cdot 5}{\sqrt{\left(2 \cdot \left(1 + 3 \cdot \left(v \cdot v\right)\right)\right) \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}}{\pi}}}{1 \cdot \left(1 \cdot 1\right) - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
18. Using strategy rm

19. Applied associate-*l/ 0.1

    \[\leadsto \frac{\color{blue}{\frac{1 \cdot \frac{\frac{1 - \left(v \cdot v\right) \cdot 5}{\sqrt{\left(2 \cdot \left(1 + 3 \cdot \left(v \cdot v\right)\right)\right) \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}}{\pi}}{t}}}{1 \cdot \left(1 \cdot 1\right) - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

20. Final simplification 0.1

    \[\leadsto \frac{\frac{\frac{\frac{1 - \left(v \cdot v\right) \cdot 5}{\sqrt{\left(2 \cdot \left(3 \cdot \left(v \cdot v\right) + 1\right)\right) \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}}{\pi}}{t}}{\left(1 \cdot 1\right) \cdot 1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)} \cdot \left(\left(\left(\left(v \cdot v\right) \cdot 1 + \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right) + 1 \cdot 1\right) \cdot \sqrt{3 \cdot \left(v \cdot v\right) + 1}\right)\]

Reproduce

herbie shell --seed 2019174 
(FPCore (v t)
  :name "Falkner and Boettcher, Equation (20:1,3)"
  (/ (- 1.0 (* 5.0 (* v v))) (* (* (* PI t) (sqrt (* 2.0 (- 1.0 (* 3.0 (* v v)))))) (- 1.0 (* v v)))))