Average Error: 0.5 → 0.5
Time: 1.3m
Precision: 64
\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
↓
\[e^{\log \left(\cos^{-1} \left(\left(1 + v \cdot v\right) \cdot \frac{(-5 \cdot \left(v \cdot v\right) + 1)_*}{\left(v \cdot v\right) \cdot \left(v \cdot v\right) - 1}\right)\right)}\]
double f(double v) {
        double r33322678 = 1.0;
        double r33322679 = 5.0;
        double r33322680 = v;
        double r33322681 = r33322680 * r33322680;
        double r33322682 = r33322679 * r33322681;
        double r33322683 = r33322678 - r33322682;
        double r33322684 = r33322681 - r33322678;
        double r33322685 = r33322683 / r33322684;
        double r33322686 = acos(r33322685);
        return r33322686;
}
↓
double f(double v) {
        double r33322687 = 1.0;
        double r33322688 = v;
        double r33322689 = r33322688 * r33322688;
        double r33322690 = r33322687 + r33322689;
        double r33322691 = -5.0;
        double r33322692 = fma(r33322691, r33322689, r33322687);
        double r33322693 = r33322689 * r33322689;
        double r33322694 = r33322693 - r33322687;
        double r33322695 = r33322692 / r33322694;
        double r33322696 = r33322690 * r33322695;
        double r33322697 = acos(r33322696);
        double r33322698 = log(r33322697);
        double r33322699 = exp(r33322698);
        return r33322699;
}


\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
↓
e^{\log \left(\cos^{-1} \left(\left(1 + v \cdot v\right) \cdot \frac{(-5 \cdot \left(v \cdot v\right) + 1)_*}{\left(v \cdot v\right) \cdot \left(v \cdot v\right) - 1}\right)\right)}

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{(-5 \cdot \left(v \cdot v\right) + 1)_*}{v \cdot v - 1}\right)}\]
  3. Using strategy rm

  4. Applied flip--0.5

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

  5. Applied associate-/r/0.5

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

  7. Applied add-exp-log0.5

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

  8. Final simplification0.5

    \[\leadsto e^{\log \left(\cos^{-1} \left(\left(1 + v \cdot v\right) \cdot \frac{(-5 \cdot \left(v \cdot v\right) + 1)_*}{\left(v \cdot v\right) \cdot \left(v \cdot v\right) - 1}\right)\right)}\]

Reproduce

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