Average Error: 0.0 → 0.0
Time: 19.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)\]
↓
\[\left(\sqrt{1 - \left(v \cdot v\right) \cdot 3} \cdot \frac{\sqrt{2}}{4}\right) \cdot \left(-v \cdot v\right) + \left(\sqrt{1 - \left(v \cdot v\right) \cdot 3} \cdot \frac{\sqrt{2}}{4}\right) \cdot 1\]
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\left(\sqrt{1 - \left(v \cdot v\right) \cdot 3} \cdot \frac{\sqrt{2}}{4}\right) \cdot \left(-v \cdot v\right) + \left(\sqrt{1 - \left(v \cdot v\right) \cdot 3} \cdot \frac{\sqrt{2}}{4}\right) \cdot 1
double f(double v) {
        double r6899864 = 2.0;
        double r6899865 = sqrt(r6899864);
        double r6899866 = 4.0;
        double r6899867 = r6899865 / r6899866;
        double r6899868 = 1.0;
        double r6899869 = 3.0;
        double r6899870 = v;
        double r6899871 = r6899870 * r6899870;
        double r6899872 = r6899869 * r6899871;
        double r6899873 = r6899868 - r6899872;
        double r6899874 = sqrt(r6899873);
        double r6899875 = r6899867 * r6899874;
        double r6899876 = r6899868 - r6899871;
        double r6899877 = r6899875 * r6899876;
        return r6899877;
}
↓
double f(double v) {
        double r6899878 = 1.0;
        double r6899879 = v;
        double r6899880 = r6899879 * r6899879;
        double r6899881 = 3.0;
        double r6899882 = r6899880 * r6899881;
        double r6899883 = r6899878 - r6899882;
        double r6899884 = sqrt(r6899883);
        double r6899885 = 2.0;
        double r6899886 = sqrt(r6899885);
        double r6899887 = 4.0;
        double r6899888 = r6899886 / r6899887;
        double r6899889 = r6899884 * r6899888;
        double r6899890 = -r6899880;
        double r6899891 = r6899889 * r6899890;
        double r6899892 = r6899889 * r6899878;
        double r6899893 = r6899891 + r6899892;
        return r6899893;
}

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 sub-neg0.0

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

  4. Applied distribute-lft-in0.0

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

  5. Final simplification0.0

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

Reproduce

herbie shell --seed 2019172 +o rules:numerics
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  (* (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (* 3.0 (* v v))))) (- 1.0 (* v v))))