Average Error: 0.0 → 0.0
Time: 4.5s
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)\]
↓
\[\frac{\sqrt{2}}{4} \cdot \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot 1 + \sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \left(-v \cdot v\right)\right)\]
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\frac{\sqrt{2}}{4} \cdot \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot 1 + \sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \left(-v \cdot v\right)\right)
double f(double v) {
        double r307606 = 2.0;
        double r307607 = sqrt(r307606);
        double r307608 = 4.0;
        double r307609 = r307607 / r307608;
        double r307610 = 1.0;
        double r307611 = 3.0;
        double r307612 = v;
        double r307613 = r307612 * r307612;
        double r307614 = r307611 * r307613;
        double r307615 = r307610 - r307614;
        double r307616 = sqrt(r307615);
        double r307617 = r307609 * r307616;
        double r307618 = r307610 - r307613;
        double r307619 = r307617 * r307618;
        return r307619;
}
↓
double f(double v) {
        double r307620 = 2.0;
        double r307621 = sqrt(r307620);
        double r307622 = 4.0;
        double r307623 = r307621 / r307622;
        double r307624 = 1.0;
        double r307625 = 3.0;
        double r307626 = v;
        double r307627 = r307626 * r307626;
        double r307628 = r307625 * r307627;
        double r307629 = r307624 - r307628;
        double r307630 = sqrt(r307629);
        double r307631 = r307630 * r307624;
        double r307632 = -r307627;
        double r307633 = r307630 * r307632;
        double r307634 = r307631 + r307633;
        double r307635 = r307623 * r307634;
        return r307635;
}

Error

Bits error versus v

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

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 associate-*l*0.0

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

  5. Applied sub-neg0.0

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

  6. Applied distribute-lft-in0.0

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

  7. Final simplification0.0

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

Reproduce

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