Average Error: 1.0 → 0.0
Time: 7.5s
Precision: 64
\[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}\]
↓
\[\frac{\frac{4}{\left(3 \cdot \pi\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}}{\sqrt{{2}^{3} - {\left(6 \cdot \left(v \cdot v\right)\right)}^{3}}} \cdot e^{\log \left(\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 \sqrt{2 \cdot 2 + \left(\left(6 \cdot \left(v \cdot v\right)\right) \cdot \left(6 \cdot \left(v \cdot v\right)\right) + 2 \cdot \left(6 \cdot \left(v \cdot v\right)\right)\right)}\right)}\]
\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}
↓
\frac{\frac{4}{\left(3 \cdot \pi\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}}{\sqrt{{2}^{3} - {\left(6 \cdot \left(v \cdot v\right)\right)}^{3}}} \cdot e^{\log \left(\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 \sqrt{2 \cdot 2 + \left(\left(6 \cdot \left(v \cdot v\right)\right) \cdot \left(6 \cdot \left(v \cdot v\right)\right) + 2 \cdot \left(6 \cdot \left(v \cdot v\right)\right)\right)}\right)}
double f(double v) {
        double r320526 = 4.0;
        double r320527 = 3.0;
        double r320528 = atan2(1.0, 0.0);
        double r320529 = r320527 * r320528;
        double r320530 = 1.0;
        double r320531 = v;
        double r320532 = r320531 * r320531;
        double r320533 = r320530 - r320532;
        double r320534 = r320529 * r320533;
        double r320535 = 2.0;
        double r320536 = 6.0;
        double r320537 = r320536 * r320532;
        double r320538 = r320535 - r320537;
        double r320539 = sqrt(r320538);
        double r320540 = r320534 * r320539;
        double r320541 = r320526 / r320540;
        return r320541;
}
↓
double f(double v) {
        double r320542 = 4.0;
        double r320543 = 3.0;
        double r320544 = atan2(1.0, 0.0);
        double r320545 = r320543 * r320544;
        double r320546 = 1.0;
        double r320547 = 3.0;
        double r320548 = pow(r320546, r320547);
        double r320549 = v;
        double r320550 = r320549 * r320549;
        double r320551 = pow(r320550, r320547);
        double r320552 = r320548 - r320551;
        double r320553 = r320545 * r320552;
        double r320554 = r320542 / r320553;
        double r320555 = 2.0;
        double r320556 = pow(r320555, r320547);
        double r320557 = 6.0;
        double r320558 = r320557 * r320550;
        double r320559 = pow(r320558, r320547);
        double r320560 = r320556 - r320559;
        double r320561 = sqrt(r320560);
        double r320562 = r320554 / r320561;
        double r320563 = r320546 * r320546;
        double r320564 = r320550 * r320550;
        double r320565 = r320546 * r320550;
        double r320566 = r320564 + r320565;
        double r320567 = r320563 + r320566;
        double r320568 = r320555 * r320555;
        double r320569 = r320558 * r320558;
        double r320570 = r320555 * r320558;
        double r320571 = r320569 + r320570;
        double r320572 = r320568 + r320571;
        double r320573 = sqrt(r320572);
        double r320574 = r320567 * r320573;
        double r320575 = log(r320574);
        double r320576 = exp(r320575);
        double r320577 = r320562 * r320576;
        return r320577;
}

Error

Bits error versus v

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 1.0

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

  3. Applied add-exp-log1.0

    \[\leadsto \frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \color{blue}{e^{\log \left(\sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}}}\]

  4. Applied add-exp-log1.0

    \[\leadsto \frac{4}{\left(\left(3 \cdot \pi\right) \cdot \color{blue}{e^{\log \left(1 - v \cdot v\right)}}\right) \cdot e^{\log \left(\sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}}\]

  5. Applied add-exp-log1.0

    \[\leadsto \frac{4}{\left(\left(3 \cdot \color{blue}{e^{\log \pi}}\right) \cdot e^{\log \left(1 - v \cdot v\right)}\right) \cdot e^{\log \left(\sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}}\]

  6. Applied add-exp-log1.0

    \[\leadsto \frac{4}{\left(\left(\color{blue}{e^{\log 3}} \cdot e^{\log \pi}\right) \cdot e^{\log \left(1 - v \cdot v\right)}\right) \cdot e^{\log \left(\sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}}\]

  7. Applied prod-exp1.0

    \[\leadsto \frac{4}{\left(\color{blue}{e^{\log 3 + \log \pi}} \cdot e^{\log \left(1 - v \cdot v\right)}\right) \cdot e^{\log \left(\sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}}\]

  8. Applied prod-exp1.0

    \[\leadsto \frac{4}{\color{blue}{e^{\left(\log 3 + \log \pi\right) + \log \left(1 - v \cdot v\right)}} \cdot e^{\log \left(\sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}}\]

  9. Applied prod-exp0.0

    \[\leadsto \frac{4}{\color{blue}{e^{\left(\left(\log 3 + \log \pi\right) + \log \left(1 - v \cdot v\right)\right) + \log \left(\sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}}}\]

  10. Simplified0.0

    \[\leadsto \frac{4}{e^{\color{blue}{\log \left(\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}}}\]
  11. Using strategy rm

  12. Applied flip3--0.0

    \[\leadsto \frac{4}{e^{\log \left(\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{\color{blue}{\frac{{2}^{3} - {\left(6 \cdot \left(v \cdot v\right)\right)}^{3}}{2 \cdot 2 + \left(\left(6 \cdot \left(v \cdot v\right)\right) \cdot \left(6 \cdot \left(v \cdot v\right)\right) + 2 \cdot \left(6 \cdot \left(v \cdot v\right)\right)\right)}}}\right)}}\]

  13. Applied sqrt-div0.0

    \[\leadsto \frac{4}{e^{\log \left(\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \color{blue}{\frac{\sqrt{{2}^{3} - {\left(6 \cdot \left(v \cdot v\right)\right)}^{3}}}{\sqrt{2 \cdot 2 + \left(\left(6 \cdot \left(v \cdot v\right)\right) \cdot \left(6 \cdot \left(v \cdot v\right)\right) + 2 \cdot \left(6 \cdot \left(v \cdot v\right)\right)\right)}}}\right)}}\]

  14. Applied flip3--0.0

    \[\leadsto \frac{4}{e^{\log \left(\left(\left(3 \cdot \pi\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)}}\right) \cdot \frac{\sqrt{{2}^{3} - {\left(6 \cdot \left(v \cdot v\right)\right)}^{3}}}{\sqrt{2 \cdot 2 + \left(\left(6 \cdot \left(v \cdot v\right)\right) \cdot \left(6 \cdot \left(v \cdot v\right)\right) + 2 \cdot \left(6 \cdot \left(v \cdot v\right)\right)\right)}}\right)}}\]

  15. Applied associate-*r/0.0

    \[\leadsto \frac{4}{e^{\log \left(\color{blue}{\frac{\left(3 \cdot \pi\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}} \cdot \frac{\sqrt{{2}^{3} - {\left(6 \cdot \left(v \cdot v\right)\right)}^{3}}}{\sqrt{2 \cdot 2 + \left(\left(6 \cdot \left(v \cdot v\right)\right) \cdot \left(6 \cdot \left(v \cdot v\right)\right) + 2 \cdot \left(6 \cdot \left(v \cdot v\right)\right)\right)}}\right)}}\]

  16. Applied frac-times0.0

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

  17. Applied log-div1.6

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

  18. Applied exp-diff1.0

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

  19. Applied associate-/r/1.0

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

  20. Simplified0.0

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

  21. Final simplification0.0

    \[\leadsto \frac{\frac{4}{\left(3 \cdot \pi\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}}{\sqrt{{2}^{3} - {\left(6 \cdot \left(v \cdot v\right)\right)}^{3}}} \cdot e^{\log \left(\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 \sqrt{2 \cdot 2 + \left(\left(6 \cdot \left(v \cdot v\right)\right) \cdot \left(6 \cdot \left(v \cdot v\right)\right) + 2 \cdot \left(6 \cdot \left(v \cdot v\right)\right)\right)}\right)}\]

Reproduce

herbie shell --seed 2020100 
(FPCore (v)
  :name "Falkner and Boettcher, Equation (22+)"
  :precision binary64
  (/ 4 (* (* (* 3 PI) (- 1 (* v v))) (sqrt (- 2 (* 6 (* v v)))))))