Average Error: 0.0 → 0.0
Time: 24.7s
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{\left(\sqrt{1 - \left(\left(v \cdot \left(3 \cdot v\right)\right) \cdot \left(v \cdot \left(3 \cdot v\right)\right)\right) \cdot \left(v \cdot \left(3 \cdot v\right)\right)} \cdot \sqrt{2}\right) \cdot \left(1 - \left(v \cdot v\right) \cdot \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)\right)}{4 \cdot \left(\left(1 + \mathsf{fma}\left(v \cdot v, v \cdot v, v \cdot v\right)\right) \cdot \sqrt{\mathsf{fma}\left(v \cdot \left(3 \cdot v\right), v \cdot \left(3 \cdot v\right), v \cdot \left(3 \cdot v\right)\right) + 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{\left(\sqrt{1 - \left(\left(v \cdot \left(3 \cdot v\right)\right) \cdot \left(v \cdot \left(3 \cdot v\right)\right)\right) \cdot \left(v \cdot \left(3 \cdot v\right)\right)} \cdot \sqrt{2}\right) \cdot \left(1 - \left(v \cdot v\right) \cdot \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)\right)}{4 \cdot \left(\left(1 + \mathsf{fma}\left(v \cdot v, v \cdot v, v \cdot v\right)\right) \cdot \sqrt{\mathsf{fma}\left(v \cdot \left(3 \cdot v\right), v \cdot \left(3 \cdot v\right), v \cdot \left(3 \cdot v\right)\right) + 1}\right)}
double f(double v) {
        double r3708936 = 2.0;
        double r3708937 = sqrt(r3708936);
        double r3708938 = 4.0;
        double r3708939 = r3708937 / r3708938;
        double r3708940 = 1.0;
        double r3708941 = 3.0;
        double r3708942 = v;
        double r3708943 = r3708942 * r3708942;
        double r3708944 = r3708941 * r3708943;
        double r3708945 = r3708940 - r3708944;
        double r3708946 = sqrt(r3708945);
        double r3708947 = r3708939 * r3708946;
        double r3708948 = r3708940 - r3708943;
        double r3708949 = r3708947 * r3708948;
        return r3708949;
}
↓
double f(double v) {
        double r3708950 = 1.0;
        double r3708951 = v;
        double r3708952 = 3.0;
        double r3708953 = r3708952 * r3708951;
        double r3708954 = r3708951 * r3708953;
        double r3708955 = r3708954 * r3708954;
        double r3708956 = r3708955 * r3708954;
        double r3708957 = r3708950 - r3708956;
        double r3708958 = sqrt(r3708957);
        double r3708959 = 2.0;
        double r3708960 = sqrt(r3708959);
        double r3708961 = r3708958 * r3708960;
        double r3708962 = r3708951 * r3708951;
        double r3708963 = r3708962 * r3708962;
        double r3708964 = r3708962 * r3708963;
        double r3708965 = r3708950 - r3708964;
        double r3708966 = r3708961 * r3708965;
        double r3708967 = 4.0;
        double r3708968 = fma(r3708962, r3708962, r3708962);
        double r3708969 = r3708950 + r3708968;
        double r3708970 = fma(r3708954, r3708954, r3708954);
        double r3708971 = r3708970 + r3708950;
        double r3708972 = sqrt(r3708971);
        double r3708973 = r3708969 * r3708972;
        double r3708974 = r3708967 * r3708973;
        double r3708975 = r3708966 / r3708974;
        return r3708975;
}

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 flip3--0.0

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

  4. Applied flip3--0.0

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

  5. Applied sqrt-div0.0

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

  6. Applied frac-times0.0

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

  7. Applied frac-times0.0

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

  8. Simplified0.0

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

  9. Simplified0.0

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

  10. Final simplification0.0

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

Reproduce

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