Average Error: 0.0 → 0.0
Time: 2.7m
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)\]
↓
\[\sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*} \cdot \sqrt[3]{\frac{2 \cdot \sqrt{2}}{\left(\frac{4}{1 - v \cdot v} \cdot \frac{4}{1 - v \cdot v}\right) \cdot \frac{4}{1 - v \cdot v}}}\]
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*} \cdot \sqrt[3]{\frac{2 \cdot \sqrt{2}}{\left(\frac{4}{1 - v \cdot v} \cdot \frac{4}{1 - v \cdot v}\right) \cdot \frac{4}{1 - v \cdot v}}}
double f(double v) {
        double r64559901 = 2.0;
        double r64559902 = sqrt(r64559901);
        double r64559903 = 4.0;
        double r64559904 = r64559902 / r64559903;
        double r64559905 = 1.0;
        double r64559906 = 3.0;
        double r64559907 = v;
        double r64559908 = r64559907 * r64559907;
        double r64559909 = r64559906 * r64559908;
        double r64559910 = r64559905 - r64559909;
        double r64559911 = sqrt(r64559910);
        double r64559912 = r64559904 * r64559911;
        double r64559913 = r64559905 - r64559908;
        double r64559914 = r64559912 * r64559913;
        return r64559914;
}
↓
double f(double v) {
        double r64559915 = v;
        double r64559916 = r64559915 * r64559915;
        double r64559917 = -3.0;
        double r64559918 = 1.0;
        double r64559919 = fma(r64559916, r64559917, r64559918);
        double r64559920 = sqrt(r64559919);
        double r64559921 = 2.0;
        double r64559922 = sqrt(r64559921);
        double r64559923 = r64559921 * r64559922;
        double r64559924 = 4.0;
        double r64559925 = r64559918 - r64559916;
        double r64559926 = r64559924 / r64559925;
        double r64559927 = r64559926 * r64559926;
        double r64559928 = r64559927 * r64559926;
        double r64559929 = r64559923 / r64559928;
        double r64559930 = cbrt(r64559929);
        double r64559931 = r64559920 * r64559930;
        return r64559931;
}

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{\sqrt{2}}{\frac{4}{1 - v \cdot v}} \cdot \sqrt{(\left(v \cdot v\right) \cdot -3 + 1)_*}}\]
  3. Using strategy rm

  4. Applied add-cbrt-cube0.0

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

  5. Applied add-cbrt-cube1.0

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

  6. Applied cbrt-undiv0.0

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

  7. Simplified0.0

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

  8. Final simplification0.0

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

Reproduce

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