Average Error: 0.0 → 0.0
Time: 15.6s
Precision: 64
\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)\]
↓
\[\left(1 - v \cdot v\right) \cdot e^{\log \left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*}\right) + \log \left(\frac{\sqrt{2}}{4}\right)}\]
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\left(1 - v \cdot v\right) \cdot e^{\log \left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*}\right) + \log \left(\frac{\sqrt{2}}{4}\right)}
double f(double v) {
        double r23096380 = 2.0;
        double r23096381 = sqrt(r23096380);
        double r23096382 = 4.0;
        double r23096383 = r23096381 / r23096382;
        double r23096384 = 1.0;
        double r23096385 = 3.0;
        double r23096386 = v;
        double r23096387 = r23096386 * r23096386;
        double r23096388 = r23096385 * r23096387;
        double r23096389 = r23096384 - r23096388;
        double r23096390 = sqrt(r23096389);
        double r23096391 = r23096383 * r23096390;
        double r23096392 = r23096384 - r23096387;
        double r23096393 = r23096391 * r23096392;
        return r23096393;
}
↓
double f(double v) {
        double r23096394 = 1.0;
        double r23096395 = v;
        double r23096396 = r23096395 * r23096395;
        double r23096397 = r23096394 - r23096396;
        double r23096398 = -3.0;
        double r23096399 = fma(r23096398, r23096396, r23096394);
        double r23096400 = sqrt(r23096399);
        double r23096401 = log(r23096400);
        double r23096402 = 2.0;
        double r23096403 = sqrt(r23096402);
        double r23096404 = 4.0;
        double r23096405 = r23096403 / r23096404;
        double r23096406 = log(r23096405);
        double r23096407 = r23096401 + r23096406;
        double r23096408 = exp(r23096407);
        double r23096409 = r23096397 * r23096408;
        return r23096409;
}

Error

Bits error versus v

Derivation

  1. Initial program 0.0

    \[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)\]
  2. Using strategy rm

  3. Applied add-exp-log0.0

    \[\leadsto \left(\frac{\sqrt{2}}{4} \cdot \color{blue}{e^{\log \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right)}}\right) \cdot \left(1 - v \cdot v\right)\]

  4. Applied add-exp-log0.0

    \[\leadsto \left(\color{blue}{e^{\log \left(\frac{\sqrt{2}}{4}\right)}} \cdot e^{\log \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right)}\right) \cdot \left(1 - v \cdot v\right)\]

  5. Applied prod-exp0.0

    \[\leadsto \color{blue}{e^{\log \left(\frac{\sqrt{2}}{4}\right) + \log \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right)}} \cdot \left(1 - v \cdot v\right)\]

  6. Simplified0.0

    \[\leadsto e^{\color{blue}{\log \left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*}\right) + \log \left(\frac{\sqrt{2}}{4}\right)}} \cdot \left(1 - v \cdot v\right)\]

  7. Final simplification0.0

    \[\leadsto \left(1 - v \cdot v\right) \cdot e^{\log \left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*}\right) + \log \left(\frac{\sqrt{2}}{4}\right)}\]

Reproduce

herbie shell --seed 2019119 +o rules:numerics
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))