Average Error: 0.0 → 0.0
Time: 23.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)\]
↓
\[\frac{1}{\frac{\frac{4}{\sqrt{2}}}{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}} - \frac{v \cdot v}{\frac{\frac{4}{\sqrt{2}}}{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\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{1}{\frac{\frac{4}{\sqrt{2}}}{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}} - \frac{v \cdot v}{\frac{\frac{4}{\sqrt{2}}}{\sqrt{\mathsf{fma}\left(v \cdot v, -3, 1\right)}}}
double f(double v) {
        double r3667869 = 2.0;
        double r3667870 = sqrt(r3667869);
        double r3667871 = 4.0;
        double r3667872 = r3667870 / r3667871;
        double r3667873 = 1.0;
        double r3667874 = 3.0;
        double r3667875 = v;
        double r3667876 = r3667875 * r3667875;
        double r3667877 = r3667874 * r3667876;
        double r3667878 = r3667873 - r3667877;
        double r3667879 = sqrt(r3667878);
        double r3667880 = r3667872 * r3667879;
        double r3667881 = r3667873 - r3667876;
        double r3667882 = r3667880 * r3667881;
        return r3667882;
}
↓
double f(double v) {
        double r3667883 = 1.0;
        double r3667884 = 4.0;
        double r3667885 = 2.0;
        double r3667886 = sqrt(r3667885);
        double r3667887 = r3667884 / r3667886;
        double r3667888 = v;
        double r3667889 = r3667888 * r3667888;
        double r3667890 = -3.0;
        double r3667891 = fma(r3667889, r3667890, r3667883);
        double r3667892 = sqrt(r3667891);
        double r3667893 = r3667887 / r3667892;
        double r3667894 = r3667883 / r3667893;
        double r3667895 = r3667889 / r3667893;
        double r3667896 = r3667894 - r3667895;
        return r3667896;
}

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

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

  4. Applied div-sub0.0

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

  5. Final simplification0.0

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

Reproduce

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