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

Average Error: 0.4 → 0.1

Time: 26.9s

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

C

double f(double v, double t) {
        double r5864514 = 1.0;
        double r5864515 = 5.0;
        double r5864516 = v;
        double r5864517 = r5864516 * r5864516;
        double r5864518 = r5864515 * r5864517;
        double r5864519 = r5864514 - r5864518;
        double r5864520 = atan2(1.0, 0.0);
        double r5864521 = t;
        double r5864522 = r5864520 * r5864521;
        double r5864523 = 2.0;
        double r5864524 = 3.0;
        double r5864525 = r5864524 * r5864517;
        double r5864526 = r5864514 - r5864525;
        double r5864527 = r5864523 * r5864526;
        double r5864528 = sqrt(r5864527);
        double r5864529 = r5864522 * r5864528;
        double r5864530 = r5864514 - r5864517;
        double r5864531 = r5864529 * r5864530;
        double r5864532 = r5864519 / r5864531;
        return r5864532;
}

↓

double f(double v, double t) {
        double r5864533 = 1.0;
        double r5864534 = atan2(1.0, 0.0);
        double r5864535 = r5864533 / r5864534;
        double r5864536 = 2.0;
        double r5864537 = 1.0;
        double r5864538 = r5864537 * r5864537;
        double r5864539 = 3.0;
        double r5864540 = v;
        double r5864541 = r5864539 * r5864540;
        double r5864542 = r5864541 * r5864540;
        double r5864543 = r5864542 * r5864542;
        double r5864544 = r5864538 - r5864543;
        double r5864545 = r5864536 * r5864544;
        double r5864546 = sqrt(r5864545);
        double r5864547 = r5864537 * r5864538;
        double r5864548 = r5864540 * r5864540;
        double r5864549 = r5864548 * r5864540;
        double r5864550 = r5864549 * r5864549;
        double r5864551 = r5864547 - r5864550;
        double r5864552 = r5864546 * r5864551;
        double r5864553 = r5864535 / r5864552;
        double r5864554 = t;
        double r5864555 = r5864553 / r5864554;
        double r5864556 = r5864539 * r5864548;
        double r5864557 = r5864537 + r5864556;
        double r5864558 = sqrt(r5864557);
        double r5864559 = r5864537 * r5864548;
        double r5864560 = r5864548 * r5864548;
        double r5864561 = r5864559 + r5864560;
        double r5864562 = r5864538 + r5864561;
        double r5864563 = r5864558 * r5864562;
        double r5864564 = r5864555 * r5864563;
        double r5864565 = 5.0;
        double r5864566 = r5864565 * r5864548;
        double r5864567 = r5864537 - r5864566;
        double r5864568 = r5864564 * r5864567;
        return r5864568;
}

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 add-sqr-sqrt 0.4

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

4. Applied associate-/l* 0.4

   \[\leadsto \color{blue}{\frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{\frac{\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)}{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}}}\]
5. Using strategy rm

6. Applied div-inv 0.4

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

7. Applied *-un-lft-identity 0.4

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

8. Applied sqrt-prod 0.4

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

9. Applied times-frac 0.4

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

10. Simplified 0.4

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

11. Simplified 0.4

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

13. Applied associate-/r* 0.3

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

15. Applied flip3-- 0.3

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

16. Applied flip-- 0.3

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

17. Applied associate-*r/ 0.3

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

18. Applied sqrt-div 0.3

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

19. Applied frac-times 0.3

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

20. Applied associate-/r/ 0.3

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

21. Simplified 0.1

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

22. Final simplification 0.1

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

Reproduce

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