
(FPCore (x)
:precision binary64
(let* ((t_0 (* (* (fabs x) (fabs x)) (fabs x)))
(t_1 (* (* t_0 (fabs x)) (fabs x))))
(fabs
(*
(/ 1.0 (sqrt (PI)))
(+
(+ (+ (* 2.0 (fabs x)) (* (/ 2.0 3.0) t_0)) (* (/ 1.0 5.0) t_1))
(* (/ 1.0 21.0) (* (* t_1 (fabs x)) (fabs x))))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := \left(\left|x\right| \cdot \left|x\right|\right) \cdot \left|x\right|\\
t_1 := \left(t\_0 \cdot \left|x\right|\right) \cdot \left|x\right|\\
\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left(\left(2 \cdot \left|x\right| + \frac{2}{3} \cdot t\_0\right) + \frac{1}{5} \cdot t\_1\right) + \frac{1}{21} \cdot \left(\left(t\_1 \cdot \left|x\right|\right) \cdot \left|x\right|\right)\right)\right|
\end{array}
\end{array}
Sampling outcomes in binary64 precision:
Herbie found 12 alternatives:
| Alternative | Accuracy | Speedup |
|---|
(FPCore (x)
:precision binary64
(let* ((t_0 (* (* (fabs x) (fabs x)) (fabs x)))
(t_1 (* (* t_0 (fabs x)) (fabs x))))
(fabs
(*
(/ 1.0 (sqrt (PI)))
(+
(+ (+ (* 2.0 (fabs x)) (* (/ 2.0 3.0) t_0)) (* (/ 1.0 5.0) t_1))
(* (/ 1.0 21.0) (* (* t_1 (fabs x)) (fabs x))))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := \left(\left|x\right| \cdot \left|x\right|\right) \cdot \left|x\right|\\
t_1 := \left(t\_0 \cdot \left|x\right|\right) \cdot \left|x\right|\\
\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left(\left(2 \cdot \left|x\right| + \frac{2}{3} \cdot t\_0\right) + \frac{1}{5} \cdot t\_1\right) + \frac{1}{21} \cdot \left(\left(t\_1 \cdot \left|x\right|\right) \cdot \left|x\right|\right)\right)\right|
\end{array}
\end{array}
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(fabs
(*
(/ 1.0 (sqrt (PI)))
(+
(+
(+ (* 2.0 (fabs x_m)) (* (* (* x_m x_m) 0.6666666666666666) x_m))
(* (/ 1.0 5.0) (* (* (* x_m x_m) (* x_m x_m)) (fabs x_m))))
(* (/ 1.0 21.0) (* (* (pow (fabs x_m) 4.0) (* x_m x_m)) (fabs x_m)))))))\begin{array}{l}
x_m = \left|x\right|
\\
\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left(\left(2 \cdot \left|x\_m\right| + \left(\left(x\_m \cdot x\_m\right) \cdot 0.6666666666666666\right) \cdot x\_m\right) + \frac{1}{5} \cdot \left(\left(\left(x\_m \cdot x\_m\right) \cdot \left(x\_m \cdot x\_m\right)\right) \cdot \left|x\_m\right|\right)\right) + \frac{1}{21} \cdot \left(\left({\left(\left|x\_m\right|\right)}^{4} \cdot \left(x\_m \cdot x\_m\right)\right) \cdot \left|x\_m\right|\right)\right)\right|
\end{array}
Initial program 99.8%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.8
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-/.f64N/A
metadata-evalN/A
*-commutativeN/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lift-*.f64N/A
lower-*.f64N/A
associate-*r*N/A
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
lift-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lower-*.f64N/A
associate-*l*N/A
sqr-abs-revN/A
lift-fabs.f64N/A
lift-fabs.f64N/A
pow2N/A
metadata-evalN/A
pow2N/A
metadata-evalN/A
metadata-evalN/A
metadata-evalN/A
pow-prod-downN/A
pow2N/A
pow2N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
Applied rewrites99.9%
lift-*.f64N/A
lift-*.f64N/A
*-commutativeN/A
lift-fabs.f64N/A
*-commutativeN/A
lift-fabs.f64N/A
associate-*r*N/A
*-commutativeN/A
lift-fabs.f64N/A
rem-sqrt-square-revN/A
pow2N/A
sqrt-pow1N/A
metadata-evalN/A
pow-plus-revN/A
metadata-evalN/A
pow2N/A
lift-*.f64N/A
lower-*.f6479.2
Applied rewrites79.2%
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(let* ((t_0 (sqrt (PI)))
(t_1 (/ 1.0 t_0))
(t_2 (fabs (* (* (* (* x_m x_m) x_m) x_m) x_m))))
(if (<=
(fabs
(*
t_1
(+
(+
(+ (* 2.0 (fabs x_m)) (* (/ 2.0 3.0) (* (* x_m x_m) (fabs x_m))))
(* (/ 1.0 5.0) t_2))
(* (/ 1.0 21.0) (* (* t_2 (fabs x_m)) (fabs x_m))))))
0.0002)
(fabs (* t_1 (* (fabs x_m) 2.0)))
(fabs (* x_m (* (* (/ 0.6666666666666666 t_0) x_m) x_m))))))\begin{array}{l}
x_m = \left|x\right|
\\
\begin{array}{l}
t_0 := \sqrt{\mathsf{PI}\left(\right)}\\
t_1 := \frac{1}{t\_0}\\
t_2 := \left|\left(\left(\left(x\_m \cdot x\_m\right) \cdot x\_m\right) \cdot x\_m\right) \cdot x\_m\right|\\
\mathbf{if}\;\left|t\_1 \cdot \left(\left(\left(2 \cdot \left|x\_m\right| + \frac{2}{3} \cdot \left(\left(x\_m \cdot x\_m\right) \cdot \left|x\_m\right|\right)\right) + \frac{1}{5} \cdot t\_2\right) + \frac{1}{21} \cdot \left(\left(t\_2 \cdot \left|x\_m\right|\right) \cdot \left|x\_m\right|\right)\right)\right| \leq 0.0002:\\
\;\;\;\;\left|t\_1 \cdot \left(\left|x\_m\right| \cdot 2\right)\right|\\
\mathbf{else}:\\
\;\;\;\;\left|x\_m \cdot \left(\left(\frac{0.6666666666666666}{t\_0} \cdot x\_m\right) \cdot x\_m\right)\right|\\
\end{array}
\end{array}
if (fabs.f64 (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 (PI.f64))) (+.f64 (+.f64 (+.f64 (*.f64 #s(literal 2 binary64) (fabs.f64 x)) (*.f64 (/.f64 #s(literal 2 binary64) #s(literal 3 binary64)) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 #s(literal 1 binary64) #s(literal 5 binary64)) (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 #s(literal 1 binary64) #s(literal 21 binary64)) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))))) < 2.0000000000000001e-4Initial program 99.9%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.9
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-/.f64N/A
metadata-evalN/A
*-commutativeN/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lift-*.f64N/A
lower-*.f64N/A
associate-*r*N/A
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
lift-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lower-*.f64N/A
associate-*l*N/A
sqr-abs-revN/A
lift-fabs.f64N/A
lift-fabs.f64N/A
pow2N/A
metadata-evalN/A
pow2N/A
metadata-evalN/A
metadata-evalN/A
metadata-evalN/A
pow-prod-downN/A
pow2N/A
pow2N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
Applied rewrites99.9%
Taylor expanded in x around 0
*-commutativeN/A
lower-*.f64N/A
lower-fabs.f6499.4
Applied rewrites99.4%
if 2.0000000000000001e-4 < (fabs.f64 (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 (PI.f64))) (+.f64 (+.f64 (+.f64 (*.f64 #s(literal 2 binary64) (fabs.f64 x)) (*.f64 (/.f64 #s(literal 2 binary64) #s(literal 3 binary64)) (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 #s(literal 1 binary64) #s(literal 5 binary64)) (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))) (*.f64 (/.f64 #s(literal 1 binary64) #s(literal 21 binary64)) (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)) (fabs.f64 x)))))) Initial program 99.8%
lift-*.f64N/A
*-commutativeN/A
lift-*.f64N/A
associate-*l*N/A
lower-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f64N/A
lower-*.f6499.8
lift-/.f64N/A
metadata-eval99.8
Applied rewrites99.8%
Taylor expanded in x around inf
associate-*r*N/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
unpow2N/A
sqr-abs-revN/A
cube-multN/A
lower-pow.f64N/A
lower-fabs.f64N/A
rem-square-sqrtN/A
lower-sqrt.f64N/A
rem-square-sqrtN/A
lower-/.f64N/A
lower-PI.f6466.6
Applied rewrites66.6%
Applied rewrites66.6%
Applied rewrites66.6%
Final simplification89.0%
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(let* ((t_0 (sqrt (PI))))
(if (<= x_m 1.5)
(fabs (* (/ 1.0 t_0) (* (fabs x_m) 2.0)))
(/
(fabs
(*
(fma
0.047619047619047616
(pow (fabs x_m) 6.0)
(* (* x_m x_m) 0.6666666666666666))
x_m))
t_0))))\begin{array}{l}
x_m = \left|x\right|
\\
\begin{array}{l}
t_0 := \sqrt{\mathsf{PI}\left(\right)}\\
\mathbf{if}\;x\_m \leq 1.5:\\
\;\;\;\;\left|\frac{1}{t\_0} \cdot \left(\left|x\_m\right| \cdot 2\right)\right|\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\mathsf{fma}\left(0.047619047619047616, {\left(\left|x\_m\right|\right)}^{6}, \left(x\_m \cdot x\_m\right) \cdot 0.6666666666666666\right) \cdot x\_m\right|}{t\_0}\\
\end{array}
\end{array}
if x < 1.5Initial program 99.8%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.8
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-/.f64N/A
metadata-evalN/A
*-commutativeN/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lift-*.f64N/A
lower-*.f64N/A
associate-*r*N/A
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
lift-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lower-*.f64N/A
associate-*l*N/A
sqr-abs-revN/A
lift-fabs.f64N/A
lift-fabs.f64N/A
pow2N/A
metadata-evalN/A
pow2N/A
metadata-evalN/A
metadata-evalN/A
metadata-evalN/A
pow-prod-downN/A
pow2N/A
pow2N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
Applied rewrites99.9%
Taylor expanded in x around 0
*-commutativeN/A
lower-*.f64N/A
lower-fabs.f6469.7
Applied rewrites69.7%
if 1.5 < x Initial program 99.8%
Applied rewrites99.4%
Taylor expanded in x around inf
unpow2N/A
associate-*l*N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f64N/A
lower-fma.f64N/A
lower-pow.f64N/A
lower-fabs.f64N/A
lower-*.f64N/A
lower-fabs.f6435.6
Applied rewrites35.6%
Applied rewrites35.6%
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(if (<= x_m 1.85)
(fabs (* (/ 1.0 (sqrt (PI))) (* (fabs x_m) 2.0)))
(fabs
(*
(*
(* 0.047619047619047616 x_m)
(* (sqrt (/ 1.0 (PI))) (pow (fabs x_m) 5.0)))
x_m))))\begin{array}{l}
x_m = \left|x\right|
\\
\begin{array}{l}
\mathbf{if}\;x\_m \leq 1.85:\\
\;\;\;\;\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left|x\_m\right| \cdot 2\right)\right|\\
\mathbf{else}:\\
\;\;\;\;\left|\left(\left(0.047619047619047616 \cdot x\_m\right) \cdot \left(\sqrt{\frac{1}{\mathsf{PI}\left(\right)}} \cdot {\left(\left|x\_m\right|\right)}^{5}\right)\right) \cdot x\_m\right|\\
\end{array}
\end{array}
if x < 1.8500000000000001Initial program 99.8%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.8
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-/.f64N/A
metadata-evalN/A
*-commutativeN/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lift-*.f64N/A
lower-*.f64N/A
associate-*r*N/A
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
lift-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lower-*.f64N/A
associate-*l*N/A
sqr-abs-revN/A
lift-fabs.f64N/A
lift-fabs.f64N/A
pow2N/A
metadata-evalN/A
pow2N/A
metadata-evalN/A
metadata-evalN/A
metadata-evalN/A
pow-prod-downN/A
pow2N/A
pow2N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
Applied rewrites99.9%
Taylor expanded in x around 0
*-commutativeN/A
lower-*.f64N/A
lower-fabs.f6469.7
Applied rewrites69.7%
if 1.8500000000000001 < x Initial program 99.8%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.8
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
Taylor expanded in x around inf
*-commutativeN/A
*-commutativeN/A
associate-*r*N/A
associate-*l*N/A
unpow2N/A
associate-*r*N/A
lower-*.f64N/A
Applied rewrites35.2%
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(if (<= x_m 1.85)
(fabs (* (/ 1.0 (sqrt (PI))) (* (fabs x_m) 2.0)))
(fabs
(*
(* (* (* (pow (fabs x_m) 5.0) x_m) x_m) 0.047619047619047616)
(sqrt (/ 1.0 (PI)))))))\begin{array}{l}
x_m = \left|x\right|
\\
\begin{array}{l}
\mathbf{if}\;x\_m \leq 1.85:\\
\;\;\;\;\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left|x\_m\right| \cdot 2\right)\right|\\
\mathbf{else}:\\
\;\;\;\;\left|\left(\left(\left({\left(\left|x\_m\right|\right)}^{5} \cdot x\_m\right) \cdot x\_m\right) \cdot 0.047619047619047616\right) \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right|\\
\end{array}
\end{array}
if x < 1.8500000000000001Initial program 99.8%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.8
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-/.f64N/A
metadata-evalN/A
*-commutativeN/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lift-*.f64N/A
lower-*.f64N/A
associate-*r*N/A
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
lift-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lower-*.f64N/A
associate-*l*N/A
sqr-abs-revN/A
lift-fabs.f64N/A
lift-fabs.f64N/A
pow2N/A
metadata-evalN/A
pow2N/A
metadata-evalN/A
metadata-evalN/A
metadata-evalN/A
pow-prod-downN/A
pow2N/A
pow2N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
Applied rewrites99.9%
Taylor expanded in x around 0
*-commutativeN/A
lower-*.f64N/A
lower-fabs.f6469.7
Applied rewrites69.7%
if 1.8500000000000001 < x Initial program 99.8%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.8
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
Taylor expanded in x around inf
*-commutativeN/A
*-commutativeN/A
associate-*r*N/A
associate-*l*N/A
unpow2N/A
associate-*r*N/A
lower-*.f64N/A
Applied rewrites35.2%
Taylor expanded in x around 0
Applied rewrites35.2%
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(let* ((t_0 (fabs (* (* (* (* x_m x_m) x_m) x_m) x_m))))
(fabs
(*
(/ 1.0 (sqrt (PI)))
(+
(+
(+ (* 2.0 (fabs x_m)) (* (* x_m x_m) (* (fabs x_m) 0.6666666666666666)))
(* (/ 1.0 5.0) t_0))
(* (/ 1.0 21.0) (* (* t_0 (fabs x_m)) (fabs x_m))))))))\begin{array}{l}
x_m = \left|x\right|
\\
\begin{array}{l}
t_0 := \left|\left(\left(\left(x\_m \cdot x\_m\right) \cdot x\_m\right) \cdot x\_m\right) \cdot x\_m\right|\\
\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left(\left(2 \cdot \left|x\_m\right| + \left(x\_m \cdot x\_m\right) \cdot \left(\left|x\_m\right| \cdot 0.6666666666666666\right)\right) + \frac{1}{5} \cdot t\_0\right) + \frac{1}{21} \cdot \left(\left(t\_0 \cdot \left|x\_m\right|\right) \cdot \left|x\_m\right|\right)\right)\right|
\end{array}
\end{array}
Initial program 99.8%
lift-*.f64N/A
*-commutativeN/A
lift-*.f64N/A
associate-*l*N/A
lower-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f64N/A
lower-*.f6499.8
lift-/.f64N/A
metadata-eval99.8
Applied rewrites99.8%
Final simplification99.8%
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(fabs
(/
(fma
(fma 0.047619047619047616 (* x_m x_m) 0.2)
(pow (fabs x_m) 5.0)
(* 2.0 (fabs x_m)))
(sqrt (PI)))))\begin{array}{l}
x_m = \left|x\right|
\\
\left|\frac{\mathsf{fma}\left(\mathsf{fma}\left(0.047619047619047616, x\_m \cdot x\_m, 0.2\right), {\left(\left|x\_m\right|\right)}^{5}, 2 \cdot \left|x\_m\right|\right)}{\sqrt{\mathsf{PI}\left(\right)}}\right|
\end{array}
Initial program 99.8%
Applied rewrites99.4%
Taylor expanded in x around 0
+-commutativeN/A
Applied rewrites99.4%
Taylor expanded in x around 0
Applied rewrites98.9%
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(fabs
(*
(/ 1.0 (sqrt (PI)))
(+
(+
(+ (* 2.0 (fabs x_m)) (* (* x_m x_m) (* (fabs x_m) 0.6666666666666666)))
(* (/ 1.0 5.0) (fabs (* (* (* (* x_m x_m) x_m) x_m) x_m))))
(*
(/ 1.0 21.0)
(* (fabs (* (* (* (* x_m x_m) (* x_m x_m)) x_m) x_m)) (fabs x_m)))))))\begin{array}{l}
x_m = \left|x\right|
\\
\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left(\left(2 \cdot \left|x\_m\right| + \left(x\_m \cdot x\_m\right) \cdot \left(\left|x\_m\right| \cdot 0.6666666666666666\right)\right) + \frac{1}{5} \cdot \left|\left(\left(\left(x\_m \cdot x\_m\right) \cdot x\_m\right) \cdot x\_m\right) \cdot x\_m\right|\right) + \frac{1}{21} \cdot \left(\left|\left(\left(\left(x\_m \cdot x\_m\right) \cdot \left(x\_m \cdot x\_m\right)\right) \cdot x\_m\right) \cdot x\_m\right| \cdot \left|x\_m\right|\right)\right)\right|
\end{array}
Initial program 99.8%
lift-*.f64N/A
*-commutativeN/A
lift-*.f64N/A
associate-*l*N/A
lower-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f64N/A
lower-*.f6499.8
lift-/.f64N/A
metadata-eval99.8
Applied rewrites99.8%
lift-*.f64N/A
lift-*.f64N/A
lift-*.f64N/A
pow3N/A
pow-plusN/A
metadata-evalN/A
lift-fabs.f64N/A
rem-sqrt-square-revN/A
lift-*.f64N/A
sqrt-pow2N/A
metadata-evalN/A
pow2N/A
lower-*.f6499.8
Applied rewrites99.8%
Final simplification99.8%
x_m = (fabs.f64 x)
(FPCore (x_m)
:precision binary64
(let* ((t_0 (* (* x_m x_m) x_m)))
(fabs
(*
(/ 1.0 (sqrt (PI)))
(+
(+
(+ (* 2.0 (fabs x_m)) (* (* (* 0.6666666666666666 (fabs x_m)) x_m) x_m))
(* (/ 1.0 5.0) (* (* (* x_m x_m) (* x_m x_m)) (fabs x_m))))
(* (/ 1.0 21.0) (* (* t_0 t_0) (fabs x_m))))))))\begin{array}{l}
x_m = \left|x\right|
\\
\begin{array}{l}
t_0 := \left(x\_m \cdot x\_m\right) \cdot x\_m\\
\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left(\left(2 \cdot \left|x\_m\right| + \left(\left(0.6666666666666666 \cdot \left|x\_m\right|\right) \cdot x\_m\right) \cdot x\_m\right) + \frac{1}{5} \cdot \left(\left(\left(x\_m \cdot x\_m\right) \cdot \left(x\_m \cdot x\_m\right)\right) \cdot \left|x\_m\right|\right)\right) + \frac{1}{21} \cdot \left(\left(t\_0 \cdot t\_0\right) \cdot \left|x\_m\right|\right)\right)\right|
\end{array}
\end{array}
Initial program 99.8%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.8
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-/.f64N/A
metadata-evalN/A
*-commutativeN/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lift-*.f64N/A
lower-*.f64N/A
associate-*r*N/A
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
lift-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lower-*.f64N/A
associate-*l*N/A
sqr-abs-revN/A
lift-fabs.f64N/A
lift-fabs.f64N/A
pow2N/A
metadata-evalN/A
pow2N/A
metadata-evalN/A
metadata-evalN/A
metadata-evalN/A
pow-prod-downN/A
pow2N/A
pow2N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
Applied rewrites99.9%
lift-*.f64N/A
lift-pow.f64N/A
metadata-evalN/A
pow-plusN/A
pow3N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
lift-*.f64N/A
sqr-abs-revN/A
lift-fabs.f64N/A
lift-fabs.f64N/A
Applied rewrites99.8%
Final simplification99.8%
x_m = (fabs.f64 x) (FPCore (x_m) :precision binary64 (fabs (* (fma 0.2 (pow (fabs x_m) 5.0) (* 2.0 (fabs x_m))) (sqrt (/ 1.0 (PI))))))
\begin{array}{l}
x_m = \left|x\right|
\\
\left|\mathsf{fma}\left(0.2, {\left(\left|x\_m\right|\right)}^{5}, 2 \cdot \left|x\_m\right|\right) \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right|
\end{array}
Initial program 99.8%
Applied rewrites99.4%
Taylor expanded in x around 0
*-commutativeN/A
lower-*.f64N/A
lower-fma.f64N/A
lower-pow.f64N/A
lower-fabs.f64N/A
lower-*.f64N/A
lower-fabs.f64N/A
rem-square-sqrtN/A
lower-sqrt.f64N/A
rem-square-sqrtN/A
lower-/.f64N/A
lower-PI.f6493.1
Applied rewrites93.1%
x_m = (fabs.f64 x) (FPCore (x_m) :precision binary64 (fabs (/ (fma 0.2 (pow (fabs x_m) 5.0) (* 2.0 (fabs x_m))) (sqrt (PI)))))
\begin{array}{l}
x_m = \left|x\right|
\\
\left|\frac{\mathsf{fma}\left(0.2, {\left(\left|x\_m\right|\right)}^{5}, 2 \cdot \left|x\_m\right|\right)}{\sqrt{\mathsf{PI}\left(\right)}}\right|
\end{array}
Initial program 99.8%
Applied rewrites99.4%
Taylor expanded in x around 0
lower-fma.f64N/A
lower-pow.f64N/A
lower-fabs.f64N/A
lower-*.f64N/A
lower-fabs.f6492.6
Applied rewrites92.6%
x_m = (fabs.f64 x) (FPCore (x_m) :precision binary64 (fabs (* (/ 1.0 (sqrt (PI))) (* (fabs x_m) 2.0))))
\begin{array}{l}
x_m = \left|x\right|
\\
\left|\frac{1}{\sqrt{\mathsf{PI}\left(\right)}} \cdot \left(\left|x\_m\right| \cdot 2\right)\right|
\end{array}
Initial program 99.8%
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
lower-*.f6499.8
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
lift-*.f64N/A
pow2N/A
pow2N/A
pow-prod-upN/A
lower-pow.f64N/A
metadata-eval99.9
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-absN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-/.f64N/A
metadata-evalN/A
*-commutativeN/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lift-*.f64N/A
lower-*.f64N/A
associate-*r*N/A
lift-*.f64N/A
lift-*.f64N/A
associate-*l*N/A
*-commutativeN/A
lower-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
lift-*.f64N/A
*-commutativeN/A
lower-*.f6499.9
Applied rewrites99.9%
lift-*.f64N/A
lift-*.f64N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
lower-*.f64N/A
associate-*l*N/A
sqr-abs-revN/A
lift-fabs.f64N/A
lift-fabs.f64N/A
pow2N/A
metadata-evalN/A
pow2N/A
metadata-evalN/A
metadata-evalN/A
metadata-evalN/A
pow-prod-downN/A
pow2N/A
pow2N/A
lift-fabs.f64N/A
lift-fabs.f64N/A
sqr-abs-revN/A
Applied rewrites99.9%
Taylor expanded in x around 0
*-commutativeN/A
lower-*.f64N/A
lower-fabs.f6469.7
Applied rewrites69.7%
herbie shell --seed 2025011
(FPCore (x)
:name "Jmat.Real.erfi, branch x less than or equal to 0.5"
:precision binary64
:pre (<= x 0.5)
(fabs (* (/ 1.0 (sqrt (PI))) (+ (+ (+ (* 2.0 (fabs x)) (* (/ 2.0 3.0) (* (* (fabs x) (fabs x)) (fabs x)))) (* (/ 1.0 5.0) (* (* (* (* (fabs x) (fabs x)) (fabs x)) (fabs x)) (fabs x)))) (* (/ 1.0 21.0) (* (* (* (* (* (* (fabs x) (fabs x)) (fabs x)) (fabs x)) (fabs x)) (fabs x)) (fabs x)))))))