Average Error: 0.0 → 0.0
Time: 54.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{1 - 3 \cdot \left(v \cdot v\right)}\right) + \log \left(\frac{\sqrt{2}}{4}\right)}\]
double f(double v) {
        double r34136425 = 2.0;
        double r34136426 = sqrt(r34136425);
        double r34136427 = 4.0;
        double r34136428 = r34136426 / r34136427;
        double r34136429 = 1.0;
        double r34136430 = 3.0;
        double r34136431 = v;
        double r34136432 = r34136431 * r34136431;
        double r34136433 = r34136430 * r34136432;
        double r34136434 = r34136429 - r34136433;
        double r34136435 = sqrt(r34136434);
        double r34136436 = r34136428 * r34136435;
        double r34136437 = r34136429 - r34136432;
        double r34136438 = r34136436 * r34136437;
        return r34136438;
}
↓
double f(double v) {
        double r34136439 = 1.0;
        double r34136440 = v;
        double r34136441 = r34136440 * r34136440;
        double r34136442 = r34136439 - r34136441;
        double r34136443 = 3.0;
        double r34136444 = r34136443 * r34136441;
        double r34136445 = r34136439 - r34136444;
        double r34136446 = sqrt(r34136445);
        double r34136447 = log(r34136446);
        double r34136448 = 2.0;
        double r34136449 = sqrt(r34136448);
        double r34136450 = 4.0;
        double r34136451 = r34136449 / r34136450;
        double r34136452 = log(r34136451);
        double r34136453 = r34136447 + r34136452;
        double r34136454 = exp(r34136453);
        double r34136455 = r34136442 * r34136454;
        return r34136455;
}


\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{1 - 3 \cdot \left(v \cdot v\right)}\right) + \log \left(\frac{\sqrt{2}}{4}\right)}

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. Final simplification0.0

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

Reproduce

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