Average Error: 0.5 → 0.9
Time: 20.9s
Precision: 64
\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
↓
\[\cos^{-1} \left(\frac{\sqrt{\mathsf{fma}\left(-v, v \cdot 5, 1\right)}}{v - \sqrt{1}} \cdot \frac{\sqrt{\mathsf{fma}\left(-v, v \cdot 5, 1\right)}}{v + \sqrt{1}}\right)\]
\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
↓
\cos^{-1} \left(\frac{\sqrt{\mathsf{fma}\left(-v, v \cdot 5, 1\right)}}{v - \sqrt{1}} \cdot \frac{\sqrt{\mathsf{fma}\left(-v, v \cdot 5, 1\right)}}{v + \sqrt{1}}\right)
double f(double v) {
        double r225392 = 1.0;
        double r225393 = 5.0;
        double r225394 = v;
        double r225395 = r225394 * r225394;
        double r225396 = r225393 * r225395;
        double r225397 = r225392 - r225396;
        double r225398 = r225395 - r225392;
        double r225399 = r225397 / r225398;
        double r225400 = acos(r225399);
        return r225400;
}
↓
double f(double v) {
        double r225401 = v;
        double r225402 = -r225401;
        double r225403 = 5.0;
        double r225404 = r225401 * r225403;
        double r225405 = 1.0;
        double r225406 = fma(r225402, r225404, r225405);
        double r225407 = sqrt(r225406);
        double r225408 = sqrt(r225405);
        double r225409 = r225401 - r225408;
        double r225410 = r225407 / r225409;
        double r225411 = r225401 + r225408;
        double r225412 = r225407 / r225411;
        double r225413 = r225410 * r225412;
        double r225414 = acos(r225413);
        return r225414;
}

Error

Bits error versus v

Derivation

  1. Initial program 0.5

    \[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]

  2. Simplified0.5

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

  4. Applied add-sqr-sqrt0.5

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

  5. Applied difference-of-squares0.9

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

  6. Applied add-sqr-sqrt0.9

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

  7. Applied times-frac0.9

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

  8. Simplified0.9

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

  9. Simplified0.9

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

  10. Final simplification0.9

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

Reproduce

herbie shell --seed 2019179 +o rules:numerics
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 1"
  (acos (/ (- 1.0 (* 5.0 (* v v))) (- (* v v) 1.0))))