Average Error: 0.6 → 0.6
Time: 5.9s
Precision: 64
\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
↓
\[\mathsf{fma}\left(\frac{1}{\sqrt{2}}, \frac{\pi}{\sqrt{2}}, -\sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)\]
\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
↓
\mathsf{fma}\left(\frac{1}{\sqrt{2}}, \frac{\pi}{\sqrt{2}}, -\sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)
double f(double v) {
        double r349340 = 1.0;
        double r349341 = 5.0;
        double r349342 = v;
        double r349343 = r349342 * r349342;
        double r349344 = r349341 * r349343;
        double r349345 = r349340 - r349344;
        double r349346 = r349343 - r349340;
        double r349347 = r349345 / r349346;
        double r349348 = acos(r349347);
        return r349348;
}
↓
double f(double v) {
        double r349349 = 1.0;
        double r349350 = 2.0;
        double r349351 = sqrt(r349350);
        double r349352 = r349349 / r349351;
        double r349353 = atan2(1.0, 0.0);
        double r349354 = r349353 / r349351;
        double r349355 = 1.0;
        double r349356 = 5.0;
        double r349357 = v;
        double r349358 = r349357 * r349357;
        double r349359 = r349356 * r349358;
        double r349360 = r349355 - r349359;
        double r349361 = r349358 - r349355;
        double r349362 = r349360 / r349361;
        double r349363 = asin(r349362);
        double r349364 = -r349363;
        double r349365 = fma(r349352, r349354, r349364);
        return r349365;
}

Error

Bits error versus v

Derivation

  1. Initial program 0.6

    \[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
  2. Using strategy rm

  3. Applied acos-asin0.6

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

  5. Applied add-sqr-sqrt1.5

    \[\leadsto \frac{\pi}{\color{blue}{\sqrt{2} \cdot \sqrt{2}}} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]

  6. Applied *-un-lft-identity1.5

    \[\leadsto \frac{\color{blue}{1 \cdot \pi}}{\sqrt{2} \cdot \sqrt{2}} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]

  7. Applied times-frac0.6

    \[\leadsto \color{blue}{\frac{1}{\sqrt{2}} \cdot \frac{\pi}{\sqrt{2}}} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]

  8. Applied fma-neg0.6

    \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{1}{\sqrt{2}}, \frac{\pi}{\sqrt{2}}, -\sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)}\]

  9. Final simplification0.6

    \[\leadsto \mathsf{fma}\left(\frac{1}{\sqrt{2}}, \frac{\pi}{\sqrt{2}}, -\sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)\]

Reproduce

herbie shell --seed 2020034 +o rules:numerics
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 1"
  :precision binary64
  (acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))