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

Average Error: 0.4 → 0.1

Time: 1.0m

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

C

double f(double v, double t) {
        double r7768507 = 1.0;
        double r7768508 = 5.0;
        double r7768509 = v;
        double r7768510 = r7768509 * r7768509;
        double r7768511 = r7768508 * r7768510;
        double r7768512 = r7768507 - r7768511;
        double r7768513 = atan2(1.0, 0.0);
        double r7768514 = t;
        double r7768515 = r7768513 * r7768514;
        double r7768516 = 2.0;
        double r7768517 = 3.0;
        double r7768518 = r7768517 * r7768510;
        double r7768519 = r7768507 - r7768518;
        double r7768520 = r7768516 * r7768519;
        double r7768521 = sqrt(r7768520);
        double r7768522 = r7768515 * r7768521;
        double r7768523 = r7768507 - r7768510;
        double r7768524 = r7768522 * r7768523;
        double r7768525 = r7768512 / r7768524;
        return r7768525;
}

↓

double f(double v, double t) {
        double r7768526 = 1.0;
        double r7768527 = v;
        double r7768528 = r7768527 * r7768527;
        double r7768529 = r7768526 * r7768528;
        double r7768530 = r7768528 * r7768528;
        double r7768531 = r7768529 + r7768530;
        double r7768532 = r7768526 * r7768526;
        double r7768533 = r7768531 + r7768532;
        double r7768534 = 3.0;
        double r7768535 = r7768528 * r7768534;
        double r7768536 = r7768526 * r7768535;
        double r7768537 = r7768535 * r7768535;
        double r7768538 = r7768536 + r7768537;
        double r7768539 = r7768532 + r7768538;
        double r7768540 = sqrt(r7768539);
        double r7768541 = r7768533 * r7768540;
        double r7768542 = 5.0;
        double r7768543 = r7768528 * r7768542;
        double r7768544 = r7768526 - r7768543;
        double r7768545 = 1.0;
        double r7768546 = 2.0;
        double r7768547 = r7768532 * r7768526;
        double r7768548 = r7768535 * r7768537;
        double r7768549 = r7768547 - r7768548;
        double r7768550 = r7768546 * r7768549;
        double r7768551 = sqrt(r7768550);
        double r7768552 = r7768545 / r7768551;
        double r7768553 = atan2(1.0, 0.0);
        double r7768554 = r7768552 / r7768553;
        double r7768555 = r7768544 * r7768554;
        double r7768556 = t;
        double r7768557 = r7768555 / r7768556;
        double r7768558 = r7768528 * r7768527;
        double r7768559 = r7768558 * r7768558;
        double r7768560 = r7768547 - r7768559;
        double r7768561 = r7768557 / r7768560;
        double r7768562 = r7768541 * r7768561;
        return r7768562;
}

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 flip3-- 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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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.4

   \[\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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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.4

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

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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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.4

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

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

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

15. Applied *-un-lft-identity 0.1

    \[\leadsto \frac{\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\sqrt{\left(1 \cdot \left(1 \cdot 1\right) - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)\right) \cdot 2}}}{\color{blue}{1 \cdot \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 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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. Applied div-inv 0.1

    \[\leadsto \frac{\frac{\frac{\color{blue}{\left(1 - 5 \cdot \left(v \cdot v\right)\right) \cdot \frac{1}{\sqrt{\left(1 \cdot \left(1 \cdot 1\right) - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)\right) \cdot 2}}}}{1 \cdot \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 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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. Applied times-frac 0.1

    \[\leadsto \frac{\frac{\color{blue}{\frac{1 - 5 \cdot \left(v \cdot v\right)}{1} \cdot \frac{\frac{1}{\sqrt{\left(1 \cdot \left(1 \cdot 1\right) - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)\right) \cdot 2}}}{\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 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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. Simplified 0.1

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

19. Final simplification 0.1

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

Reproduce

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