Average Error: 1.0 → 0.0
Time: 8.0s
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{1}{\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{4}{\sqrt{2 - 6 \cdot \left(v \cdot v\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{1}{\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{4}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)}}\right)\right)
double f(double v) {
        double r282321 = 4.0;
        double r282322 = 3.0;
        double r282323 = atan2(1.0, 0.0);
        double r282324 = r282322 * r282323;
        double r282325 = 1.0;
        double r282326 = v;
        double r282327 = r282326 * r282326;
        double r282328 = r282325 - r282327;
        double r282329 = r282324 * r282328;
        double r282330 = 2.0;
        double r282331 = 6.0;
        double r282332 = r282331 * r282327;
        double r282333 = r282330 - r282332;
        double r282334 = sqrt(r282333);
        double r282335 = r282329 * r282334;
        double r282336 = r282321 / r282335;
        return r282336;
}
↓
double f(double v) {
        double r282337 = 1.0;
        double r282338 = 3.0;
        double r282339 = atan2(1.0, 0.0);
        double r282340 = r282338 * r282339;
        double r282341 = 1.0;
        double r282342 = v;
        double r282343 = r282342 * r282342;
        double r282344 = r282341 - r282343;
        double r282345 = r282340 * r282344;
        double r282346 = r282337 / r282345;
        double r282347 = 4.0;
        double r282348 = 2.0;
        double r282349 = 6.0;
        double r282350 = r282349 * r282343;
        double r282351 = r282348 - r282350;
        double r282352 = sqrt(r282351);
        double r282353 = r282347 / r282352;
        double r282354 = log1p(r282353);
        double r282355 = expm1(r282354);
        double r282356 = r282346 * r282355;
        return r282356;
}

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 *-un-lft-identity1.0

    \[\leadsto \frac{\color{blue}{1 \cdot 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)}}\]

  4. Applied times-frac0.0

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

  6. Applied expm1-log1p-u0.0

    \[\leadsto \frac{1}{\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)} \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{4}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)}}\right)\right)}\]

  7. Final simplification0.0

    \[\leadsto \frac{1}{\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)} \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{4}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)}}\right)\right)\]

Reproduce

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