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

Average Error: 0.4 → 0.1

Time: 21.7s

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)}\]

↓

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

C

double f(double v, double t) {
        double r244709 = 1.0;
        double r244710 = 5.0;
        double r244711 = v;
        double r244712 = r244711 * r244711;
        double r244713 = r244710 * r244712;
        double r244714 = r244709 - r244713;
        double r244715 = atan2(1.0, 0.0);
        double r244716 = t;
        double r244717 = r244715 * r244716;
        double r244718 = 2.0;
        double r244719 = 3.0;
        double r244720 = r244719 * r244712;
        double r244721 = r244709 - r244720;
        double r244722 = r244718 * r244721;
        double r244723 = sqrt(r244722);
        double r244724 = r244717 * r244723;
        double r244725 = r244709 - r244712;
        double r244726 = r244724 * r244725;
        double r244727 = r244714 / r244726;
        return r244727;
}

↓

double f(double v, double t) {
        double r244728 = 1.0;
        double r244729 = r244728 * r244728;
        double r244730 = v;
        double r244731 = r244730 * r244730;
        double r244732 = r244731 * r244731;
        double r244733 = r244731 * r244728;
        double r244734 = r244732 + r244733;
        double r244735 = r244729 + r244734;
        double r244736 = 3.0;
        double r244737 = r244736 * r244731;
        double r244738 = r244728 + r244737;
        double r244739 = sqrt(r244738);
        double r244740 = r244735 * r244739;
        double r244741 = atan2(1.0, 0.0);
        double r244742 = r244728 / r244741;
        double r244743 = 4.0;
        double r244744 = pow(r244730, r244743);
        double r244745 = r244736 * r244736;
        double r244746 = r244744 * r244745;
        double r244747 = r244729 - r244746;
        double r244748 = 2.0;
        double r244749 = r244747 * r244748;
        double r244750 = sqrt(r244749);
        double r244751 = r244742 / r244750;
        double r244752 = t;
        double r244753 = r244751 / r244752;
        double r244754 = 2.0;
        double r244755 = pow(r244730, r244754);
        double r244756 = r244752 * r244741;
        double r244757 = r244750 * r244756;
        double r244758 = 5.0;
        double r244759 = r244757 / r244758;
        double r244760 = r244755 / r244759;
        double r244761 = r244753 - r244760;
        double r244762 = 3.0;
        double r244763 = pow(r244728, r244762);
        double r244764 = 6.0;
        double r244765 = pow(r244730, r244764);
        double r244766 = r244763 - r244765;
        double r244767 = r244761 / r244766;
        double r244768 = r244740 * r244767;
        return r244768;
}

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 - 3 \cdot \left(3 \cdot {v}^{\left(2 \cdot 2\right)}\right)\right)}}}{{1}^{3} - {v}^{\left(2 \cdot 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)\]
11. Using strategy rm

12. Applied div-sub 0.3

    \[\leadsto \frac{\frac{\color{blue}{\frac{1}{\pi} - \frac{\left(5 \cdot v\right) \cdot v}{\pi}}}{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - 3 \cdot \left(3 \cdot {v}^{\left(2 \cdot 2\right)}\right)\right)}}}{{1}^{3} - {v}^{\left(2 \cdot 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)\]

13. Applied div-sub 0.3

    \[\leadsto \frac{\color{blue}{\frac{\frac{1}{\pi}}{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - 3 \cdot \left(3 \cdot {v}^{\left(2 \cdot 2\right)}\right)\right)}} - \frac{\frac{\left(5 \cdot v\right) \cdot v}{\pi}}{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - 3 \cdot \left(3 \cdot {v}^{\left(2 \cdot 2\right)}\right)\right)}}}}{{1}^{3} - {v}^{\left(2 \cdot 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)\]

14. Simplified 0.1

    \[\leadsto \frac{\color{blue}{\frac{\frac{\frac{1}{\pi}}{\sqrt{\left(1 \cdot 1 - \left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot 2}}}{t}} - \frac{\frac{\left(5 \cdot v\right) \cdot v}{\pi}}{t \cdot \sqrt{2 \cdot \left(1 \cdot 1 - 3 \cdot \left(3 \cdot {v}^{\left(2 \cdot 2\right)}\right)\right)}}}{{1}^{3} - {v}^{\left(2 \cdot 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)\]

15. Simplified 0.1

    \[\leadsto \frac{\frac{\frac{\frac{1}{\pi}}{\sqrt{\left(1 \cdot 1 - \left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot 2}}}{t} - \color{blue}{\frac{{v}^{2}}{\frac{\left(\pi \cdot t\right) \cdot \sqrt{\left(1 \cdot 1 - \left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot 2}}{5}}}}{{1}^{3} - {v}^{\left(2 \cdot 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)\]

16. Final simplification 0.1

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

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