Average Error: 1.0 → 0.0
Time: 5.6s
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{1}{3 \cdot \pi}}{1 - v \cdot v} \cdot \frac{4}{\sqrt{2 - 6 \cdot \left(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{1}{3 \cdot \pi}}{1 - v \cdot v} \cdot \frac{4}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)}}
double f(double v) {
        double r215152 = 4.0;
        double r215153 = 3.0;
        double r215154 = atan2(1.0, 0.0);
        double r215155 = r215153 * r215154;
        double r215156 = 1.0;
        double r215157 = v;
        double r215158 = r215157 * r215157;
        double r215159 = r215156 - r215158;
        double r215160 = r215155 * r215159;
        double r215161 = 2.0;
        double r215162 = 6.0;
        double r215163 = r215162 * r215158;
        double r215164 = r215161 - r215163;
        double r215165 = sqrt(r215164);
        double r215166 = r215160 * r215165;
        double r215167 = r215152 / r215166;
        return r215167;
}
↓
double f(double v) {
        double r215168 = 1.0;
        double r215169 = 3.0;
        double r215170 = atan2(1.0, 0.0);
        double r215171 = r215169 * r215170;
        double r215172 = r215168 / r215171;
        double r215173 = 1.0;
        double r215174 = v;
        double r215175 = r215174 * r215174;
        double r215176 = r215173 - r215175;
        double r215177 = r215172 / r215176;
        double r215178 = 4.0;
        double r215179 = 2.0;
        double r215180 = 6.0;
        double r215181 = r215180 * r215175;
        double r215182 = r215179 - r215181;
        double r215183 = sqrt(r215182);
        double r215184 = r215178 / r215183;
        double r215185 = r215177 * r215184;
        return r215185;
}

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 log-prod0.0

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

  13. Applied exp-sum1.0

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

  14. Applied *-un-lft-identity1.0

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

  15. Applied times-frac1.0

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

  16. Simplified0.0

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

  17. Simplified0.0

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

  18. Final simplification0.0

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

Reproduce

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