Average Error: 0.0 → 0.0
Time: 2.4s
Precision: binary64
\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right) \]
↓
\[\begin{array}{l} t_0 := \sqrt{\mathsf{fma}\left(3, v \cdot v, 1\right)}\\ \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - \mathsf{fma}\left(t_0, t_0, -1\right)}\right) \cdot \left(1 - v \cdot v\right) \end{array} \]
(FPCore (v)
 :precision binary64
 (* (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (* 3.0 (* v v))))) (- 1.0 (* v v))))
↓
(FPCore (v)
 :precision binary64
 (let* ((t_0 (sqrt (fma 3.0 (* v v) 1.0))))
   (*
    (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (fma t_0 t_0 -1.0))))
    (- 1.0 (* v v)))))
double code(double v) {
	return ((sqrt(2.0) / 4.0) * sqrt((1.0 - (3.0 * (v * v))))) * (1.0 - (v * v));
}
↓
double code(double v) {
	double t_0 = sqrt(fma(3.0, (v * v), 1.0));
	return ((sqrt(2.0) / 4.0) * sqrt((1.0 - fma(t_0, t_0, -1.0)))) * (1.0 - (v * v));
}

function code(v)
	return Float64(Float64(Float64(sqrt(2.0) / 4.0) * sqrt(Float64(1.0 - Float64(3.0 * Float64(v * v))))) * Float64(1.0 - Float64(v * v)))
end
↓
function code(v)
	t_0 = sqrt(fma(3.0, Float64(v * v), 1.0))
	return Float64(Float64(Float64(sqrt(2.0) / 4.0) * sqrt(Float64(1.0 - fma(t_0, t_0, -1.0)))) * Float64(1.0 - Float64(v * v)))
end

code[v_] := N[(N[(N[(N[Sqrt[2.0], $MachinePrecision] / 4.0), $MachinePrecision] * N[Sqrt[N[(1.0 - N[(3.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
↓
code[v_] := Block[{t$95$0 = N[Sqrt[N[(3.0 * N[(v * v), $MachinePrecision] + 1.0), $MachinePrecision]], $MachinePrecision]}, N[(N[(N[(N[Sqrt[2.0], $MachinePrecision] / 4.0), $MachinePrecision] * N[Sqrt[N[(1.0 - N[(t$95$0 * t$95$0 + -1.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\begin{array}{l}
t_0 := \sqrt{\mathsf{fma}\left(3, v \cdot v, 1\right)}\\
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - \mathsf{fma}\left(t_0, t_0, -1\right)}\right) \cdot \left(1 - v \cdot v\right)
\end{array}

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. Applied egg-rr0.0

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

  3. Final simplification0.0

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

Reproduce

herbie shell --seed 2022166 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  :precision binary64
  (* (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (* 3.0 (* v v))))) (- 1.0 (* v v))))