Average Error: 0.6 → 0.6
Time: 19.5s
Precision: 64
\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
↓
\[(e^{\log_* (1 + e^{\log \left(\cos^{-1} \left(\frac{(-5 \cdot \left(v \cdot v\right) + 1)_*}{v \cdot v - 1}\right)\right)})} - 1)^*\]
\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
↓
(e^{\log_* (1 + e^{\log \left(\cos^{-1} \left(\frac{(-5 \cdot \left(v \cdot v\right) + 1)_*}{v \cdot v - 1}\right)\right)})} - 1)^*
double f(double v) {
        double r35510556 = 1.0;
        double r35510557 = 5.0;
        double r35510558 = v;
        double r35510559 = r35510558 * r35510558;
        double r35510560 = r35510557 * r35510559;
        double r35510561 = r35510556 - r35510560;
        double r35510562 = r35510559 - r35510556;
        double r35510563 = r35510561 / r35510562;
        double r35510564 = acos(r35510563);
        return r35510564;
}
↓
double f(double v) {
        double r35510565 = -5.0;
        double r35510566 = v;
        double r35510567 = r35510566 * r35510566;
        double r35510568 = 1.0;
        double r35510569 = fma(r35510565, r35510567, r35510568);
        double r35510570 = r35510567 - r35510568;
        double r35510571 = r35510569 / r35510570;
        double r35510572 = acos(r35510571);
        double r35510573 = log(r35510572);
        double r35510574 = exp(r35510573);
        double r35510575 = log1p(r35510574);
        double r35510576 = expm1(r35510575);
        return r35510576;
}

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

    \[\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 add-exp-log0.6

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

  6. Applied expm1-log1p-u0.6

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

  7. Final simplification0.6

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

Reproduce

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