Average Error: 1.0 → 0.0
Time: 8.1s
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 r330227 = 4.0;
        double r330228 = 3.0;
        double r330229 = atan2(1.0, 0.0);
        double r330230 = r330228 * r330229;
        double r330231 = 1.0;
        double r330232 = v;
        double r330233 = r330232 * r330232;
        double r330234 = r330231 - r330233;
        double r330235 = r330230 * r330234;
        double r330236 = 2.0;
        double r330237 = 6.0;
        double r330238 = r330237 * r330233;
        double r330239 = r330236 - r330238;
        double r330240 = sqrt(r330239);
        double r330241 = r330235 * r330240;
        double r330242 = r330227 / r330241;
        return r330242;
}
↓
double f(double v) {
        double r330243 = 1.0;
        double r330244 = 3.0;
        double r330245 = atan2(1.0, 0.0);
        double r330246 = r330244 * r330245;
        double r330247 = 1.0;
        double r330248 = v;
        double r330249 = r330248 * r330248;
        double r330250 = r330247 - r330249;
        double r330251 = r330246 * r330250;
        double r330252 = r330243 / r330251;
        double r330253 = 4.0;
        double r330254 = 2.0;
        double r330255 = 6.0;
        double r330256 = r330255 * r330249;
        double r330257 = r330254 - r330256;
        double r330258 = sqrt(r330257);
        double r330259 = r330253 / r330258;
        double r330260 = log1p(r330259);
        double r330261 = expm1(r330260);
        double r330262 = r330252 * r330261;
        return r330262;
}

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)))))))