Average Error: 1.0 → 0.0
Time: 29.4s
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{\frac{1}{\pi}}{1 - v}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \cdot \frac{\frac{4}{3}}{1 + v}\]
\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{\frac{1}{\pi}}{1 - v}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \cdot \frac{\frac{4}{3}}{1 + v}
double f(double v) {
        double r3097741 = 4.0;
        double r3097742 = 3.0;
        double r3097743 = atan2(1.0, 0.0);
        double r3097744 = r3097742 * r3097743;
        double r3097745 = 1.0;
        double r3097746 = v;
        double r3097747 = r3097746 * r3097746;
        double r3097748 = r3097745 - r3097747;
        double r3097749 = r3097744 * r3097748;
        double r3097750 = 2.0;
        double r3097751 = 6.0;
        double r3097752 = r3097751 * r3097747;
        double r3097753 = r3097750 - r3097752;
        double r3097754 = sqrt(r3097753);
        double r3097755 = r3097749 * r3097754;
        double r3097756 = r3097741 / r3097755;
        return r3097756;
}
↓
double f(double v) {
        double r3097757 = 1.0;
        double r3097758 = atan2(1.0, 0.0);
        double r3097759 = r3097757 / r3097758;
        double r3097760 = v;
        double r3097761 = r3097757 - r3097760;
        double r3097762 = r3097759 / r3097761;
        double r3097763 = -6.0;
        double r3097764 = r3097760 * r3097760;
        double r3097765 = 2.0;
        double r3097766 = fma(r3097763, r3097764, r3097765);
        double r3097767 = sqrt(r3097766);
        double r3097768 = r3097762 / r3097767;
        double r3097769 = 1.3333333333333333;
        double r3097770 = r3097757 + r3097760;
        double r3097771 = r3097769 / r3097770;
        double r3097772 = r3097768 * r3097771;
        return r3097772;
}

Error

Bits error versus v

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. Simplified0.0

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

  4. Applied *-un-lft-identity0.0

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

  5. Applied *-un-lft-identity0.0

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

  6. Applied difference-of-squares0.0

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

  7. Applied div-inv0.0

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

  8. Applied times-frac0.0

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

  9. Applied times-frac0.0

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

  10. Simplified0.0

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

  11. Final simplification0.0

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

Reproduce

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