Average Error: 0.0 → 0.0
Time: 17.9s
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{1 \cdot 1 - {v}^{4}} \cdot \left(\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right)}{4 \cdot \sqrt{\mathsf{fma}\left(v, v, 1\right)}} \cdot \sqrt{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)
↓
\frac{\sqrt{1 \cdot 1 - {v}^{4}} \cdot \left(\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right)}{4 \cdot \sqrt{\mathsf{fma}\left(v, v, 1\right)}} \cdot \sqrt{1 - v \cdot v}
double f(double v) {
        double r169015 = 2.0;
        double r169016 = sqrt(r169015);
        double r169017 = 4.0;
        double r169018 = r169016 / r169017;
        double r169019 = 1.0;
        double r169020 = 3.0;
        double r169021 = v;
        double r169022 = r169021 * r169021;
        double r169023 = r169020 * r169022;
        double r169024 = r169019 - r169023;
        double r169025 = sqrt(r169024);
        double r169026 = r169018 * r169025;
        double r169027 = r169019 - r169022;
        double r169028 = r169026 * r169027;
        return r169028;
}
↓
double f(double v) {
        double r169029 = 1.0;
        double r169030 = r169029 * r169029;
        double r169031 = v;
        double r169032 = 4.0;
        double r169033 = pow(r169031, r169032);
        double r169034 = r169030 - r169033;
        double r169035 = sqrt(r169034);
        double r169036 = 2.0;
        double r169037 = sqrt(r169036);
        double r169038 = 3.0;
        double r169039 = r169031 * r169031;
        double r169040 = r169038 * r169039;
        double r169041 = r169029 - r169040;
        double r169042 = sqrt(r169041);
        double r169043 = r169037 * r169042;
        double r169044 = r169035 * r169043;
        double r169045 = 4.0;
        double r169046 = fma(r169031, r169031, r169029);
        double r169047 = sqrt(r169046);
        double r169048 = r169045 * r169047;
        double r169049 = r169044 / r169048;
        double r169050 = r169029 - r169039;
        double r169051 = sqrt(r169050);
        double r169052 = r169049 * r169051;
        return r169052;
}

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-sqr-sqrt0.0

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

  4. Applied associate-*r*0.0

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

  6. Applied flip--0.0

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

  7. Applied sqrt-div0.0

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

  8. Applied associate-*l/0.0

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

  9. Applied frac-times0.0

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

  10. Simplified0.0

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

  11. Simplified0.0

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

  12. Final simplification0.0

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

Reproduce

herbie shell --seed 2019325 +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))))