Average Error: 1.0 → 0.0
Time: 5.9s
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 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \cdot e^{\log \left(1 + v \cdot v\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 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \cdot e^{\log \left(1 + v \cdot v\right)}
double f(double v) {
        double r304259 = 4.0;
        double r304260 = 3.0;
        double r304261 = atan2(1.0, 0.0);
        double r304262 = r304260 * r304261;
        double r304263 = 1.0;
        double r304264 = v;
        double r304265 = r304264 * r304264;
        double r304266 = r304263 - r304265;
        double r304267 = r304262 * r304266;
        double r304268 = 2.0;
        double r304269 = 6.0;
        double r304270 = r304269 * r304265;
        double r304271 = r304268 - r304270;
        double r304272 = sqrt(r304271);
        double r304273 = r304267 * r304272;
        double r304274 = r304259 / r304273;
        return r304274;
}
↓
double f(double v) {
        double r304275 = 4.0;
        double r304276 = 3.0;
        double r304277 = atan2(1.0, 0.0);
        double r304278 = r304276 * r304277;
        double r304279 = 1.0;
        double r304280 = r304279 * r304279;
        double r304281 = v;
        double r304282 = r304281 * r304281;
        double r304283 = r304282 * r304282;
        double r304284 = r304280 - r304283;
        double r304285 = r304278 * r304284;
        double r304286 = r304275 / r304285;
        double r304287 = 2.0;
        double r304288 = 6.0;
        double r304289 = r304288 * r304282;
        double r304290 = r304287 - r304289;
        double r304291 = sqrt(r304290);
        double r304292 = r304286 / r304291;
        double r304293 = r304279 + r304282;
        double r304294 = log(r304293);
        double r304295 = exp(r304294);
        double r304296 = r304292 * r304295;
        return r304296;
}

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 flip--0.0

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

  13. Applied associate-*r/0.0

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

  14. Applied associate-*l/0.0

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

  15. Applied log-div0.0

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

  16. Applied exp-diff0.0

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

  17. Applied associate-/r/0.0

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

  18. Simplified0.0

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

  19. Final simplification0.0

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

Reproduce

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