
(FPCore (u s)
:precision binary32
(let* ((t_0 (/ 1.0 (+ 1.0 (exp (/ (PI) s))))))
(*
(- s)
(log
(-
(/ 1.0 (+ (* u (- (/ 1.0 (+ 1.0 (exp (/ (- (PI)) s)))) t_0)) t_0))
1.0)))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\\
\left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - t\_0\right) + t\_0} - 1\right)
\end{array}
\end{array}
Sampling outcomes in binary32 precision:
Herbie found 17 alternatives:
| Alternative | Accuracy | Speedup |
|---|
(FPCore (u s)
:precision binary32
(let* ((t_0 (/ 1.0 (+ 1.0 (exp (/ (PI) s))))))
(*
(- s)
(log
(-
(/ 1.0 (+ (* u (- (/ 1.0 (+ 1.0 (exp (/ (- (PI)) s)))) t_0)) t_0))
1.0)))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}\\
\left(-s\right) \cdot \log \left(\frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{-\mathsf{PI}\left(\right)}{s}}} - t\_0\right) + t\_0} - 1\right)
\end{array}
\end{array}
(FPCore (u s)
:precision binary32
(let* ((t_0 (exp (/ (PI) s)))
(t_1
(+
(+ (/ u (+ 1.0 (exp (/ (PI) (- s))))) (/ u (- -1.0 t_0)))
(/ 1.0 (+ 1.0 t_0)))))
(*
(- s)
(log (/ (+ (pow t_1 -3.0) -1.0) (+ (pow t_1 -2.0) (+ 1.0 (/ 1.0 t_1))))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := e^{\frac{\mathsf{PI}\left(\right)}{s}}\\
t_1 := \left(\frac{u}{1 + e^{\frac{\mathsf{PI}\left(\right)}{-s}}} + \frac{u}{-1 - t\_0}\right) + \frac{1}{1 + t\_0}\\
\left(-s\right) \cdot \log \left(\frac{{t\_1}^{-3} + -1}{{t\_1}^{-2} + \left(1 + \frac{1}{t\_1}\right)}\right)
\end{array}
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Applied rewrites99.0%
Applied rewrites99.0%
Final simplification99.0%
(FPCore (u s)
:precision binary32
(let* ((t_0
(+
(/ u (+ 1.0 (exp (/ (PI) (- s)))))
(/ (+ u -1.0) (- -1.0 (exp (/ (PI) s)))))))
(*
(- s)
(log (/ (+ -1.0 (pow t_0 -3.0)) (+ (/ 1.0 t_0) (+ 1.0 (pow t_0 -2.0))))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := \frac{u}{1 + e^{\frac{\mathsf{PI}\left(\right)}{-s}}} + \frac{u + -1}{-1 - e^{\frac{\mathsf{PI}\left(\right)}{s}}}\\
\left(-s\right) \cdot \log \left(\frac{-1 + {t\_0}^{-3}}{\frac{1}{t\_0} + \left(1 + {t\_0}^{-2}\right)}\right)
\end{array}
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Applied rewrites99.0%
Applied rewrites99.0%
Applied rewrites99.0%
Final simplification99.0%
(FPCore (u s)
:precision binary32
(let* ((t_0 (exp (/ (PI) s)))
(t_1
(+
(+ (/ u (+ 1.0 (exp (/ (PI) (- s))))) (/ u (- -1.0 t_0)))
(/ 1.0 (+ 1.0 t_0)))))
(* (- s) (log (/ (+ -1.0 (pow t_1 -2.0)) (- (/ 1.0 t_1) -1.0))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := e^{\frac{\mathsf{PI}\left(\right)}{s}}\\
t_1 := \left(\frac{u}{1 + e^{\frac{\mathsf{PI}\left(\right)}{-s}}} + \frac{u}{-1 - t\_0}\right) + \frac{1}{1 + t\_0}\\
\left(-s\right) \cdot \log \left(\frac{-1 + {t\_1}^{-2}}{\frac{1}{t\_1} - -1}\right)
\end{array}
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Applied rewrites99.0%
Applied rewrites99.0%
Final simplification99.0%
(FPCore (u s)
:precision binary32
(let* ((t_0 (exp (/ (PI) s))))
(if (<=
(*
(- s)
(log
(+
-1.0
(/
1.0
(+
(/ 1.0 (+ 1.0 t_0))
(*
u
(+
(/ 1.0 (+ 1.0 (exp (/ (PI) (- s)))))
(/ 1.0 (- -1.0 t_0)))))))))
-4.9999998413276127e-20)
(* s (/ -1.0 (/ s (PI))))
(/ (* s s) (* u (* (PI) 0.5))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := e^{\frac{\mathsf{PI}\left(\right)}{s}}\\
\mathbf{if}\;\left(-s\right) \cdot \log \left(-1 + \frac{1}{\frac{1}{1 + t\_0} + u \cdot \left(\frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{-s}}} + \frac{1}{-1 - t\_0}\right)}\right) \leq -4.9999998413276127 \cdot 10^{-20}:\\
\;\;\;\;s \cdot \frac{-1}{\frac{s}{\mathsf{PI}\left(\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{s \cdot s}{u \cdot \left(\mathsf{PI}\left(\right) \cdot 0.5\right)}\\
\end{array}
\end{array}
if (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) < -4.99999984e-20Initial program 98.8%
Applied rewrites98.7%
Taylor expanded in u around 0
lower-/.f32N/A
lower-PI.f3215.2
Applied rewrites15.2%
lift-PI.f32N/A
clear-numN/A
lower-/.f32N/A
lower-/.f3215.2
Applied rewrites15.2%
if -4.99999984e-20 < (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) Initial program 99.2%
Taylor expanded in u around inf
mul-1-negN/A
distribute-rgt-neg-inN/A
lower-fma.f32N/A
lower-neg.f32N/A
lower-log.f32N/A
lower-/.f32N/A
lower-*.f32N/A
sub-negN/A
lower-+.f32N/A
Applied rewrites10.6%
Taylor expanded in s around inf
lower-/.f32N/A
unpow2N/A
lower-*.f32N/A
lower-*.f32N/A
distribute-rgt-out--N/A
metadata-evalN/A
lower-*.f32N/A
lower-PI.f3213.8
Applied rewrites13.8%
Final simplification14.5%
(FPCore (u s)
:precision binary32
(let* ((t_0 (exp (/ (PI) s))))
(if (<=
(*
(- s)
(log
(+
-1.0
(/
1.0
(+
(/ 1.0 (+ 1.0 t_0))
(*
u
(+
(/ 1.0 (+ 1.0 (exp (/ (PI) (- s)))))
(/ 1.0 (- -1.0 t_0)))))))))
-4.9999998413276127e-20)
(* (PI) (* s (/ -1.0 s)))
(/ (* s s) (* u (* (PI) 0.5))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := e^{\frac{\mathsf{PI}\left(\right)}{s}}\\
\mathbf{if}\;\left(-s\right) \cdot \log \left(-1 + \frac{1}{\frac{1}{1 + t\_0} + u \cdot \left(\frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{-s}}} + \frac{1}{-1 - t\_0}\right)}\right) \leq -4.9999998413276127 \cdot 10^{-20}:\\
\;\;\;\;\mathsf{PI}\left(\right) \cdot \left(s \cdot \frac{-1}{s}\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{s \cdot s}{u \cdot \left(\mathsf{PI}\left(\right) \cdot 0.5\right)}\\
\end{array}
\end{array}
if (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) < -4.99999984e-20Initial program 98.8%
Applied rewrites98.7%
Taylor expanded in u around 0
lower-/.f32N/A
lower-PI.f3215.2
Applied rewrites15.2%
lift-neg.f32N/A
lift-PI.f32N/A
lift-/.f32N/A
*-commutativeN/A
lift-/.f32N/A
div-invN/A
associate-*l*N/A
lower-*.f32N/A
lower-*.f32N/A
lower-/.f3215.2
Applied rewrites15.2%
if -4.99999984e-20 < (*.f32 (neg.f32 s) (log.f32 (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 (*.f32 u (-.f32 (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 #s(literal 1 binary32) (+.f32 #s(literal 1 binary32) (exp.f32 (/.f32 (PI.f32) s)))))) #s(literal 1 binary32)))) Initial program 99.2%
Taylor expanded in u around inf
mul-1-negN/A
distribute-rgt-neg-inN/A
lower-fma.f32N/A
lower-neg.f32N/A
lower-log.f32N/A
lower-/.f32N/A
lower-*.f32N/A
sub-negN/A
lower-+.f32N/A
Applied rewrites10.6%
Taylor expanded in s around inf
lower-/.f32N/A
unpow2N/A
lower-*.f32N/A
lower-*.f32N/A
distribute-rgt-out--N/A
metadata-evalN/A
lower-*.f32N/A
lower-PI.f3213.8
Applied rewrites13.8%
Final simplification14.5%
(FPCore (u s)
:precision binary32
(let* ((t_0 (exp (/ (PI) s))))
(*
(- s)
(log
(+
-1.0
(/
1.0
(+
(+ (/ u (+ 1.0 (exp (/ (PI) (- s))))) (/ u (- -1.0 t_0)))
(/ 1.0 (+ 1.0 t_0)))))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := e^{\frac{\mathsf{PI}\left(\right)}{s}}\\
\left(-s\right) \cdot \log \left(-1 + \frac{1}{\left(\frac{u}{1 + e^{\frac{\mathsf{PI}\left(\right)}{-s}}} + \frac{u}{-1 - t\_0}\right) + \frac{1}{1 + t\_0}}\right)
\end{array}
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Applied rewrites99.0%
Applied rewrites99.0%
Final simplification99.0%
(FPCore (u s)
:precision binary32
(*
(- s)
(log
(+
-1.0
(/
1.0
(+
(/ u (+ 1.0 (exp (/ (PI) (- s)))))
(/ 1.0 (+ 1.0 (exp (/ (PI) s))))))))))\begin{array}{l}
\\
\left(-s\right) \cdot \log \left(-1 + \frac{1}{\frac{u}{1 + e^{\frac{\mathsf{PI}\left(\right)}{-s}}} + \frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{s}}}}\right)
\end{array}
Initial program 99.0%
Taylor expanded in s around inf
associate-+r+N/A
+-commutativeN/A
lower-+.f32N/A
lower-/.f32N/A
lower-PI.f32N/A
+-commutativeN/A
associate-*r/N/A
*-commutativeN/A
associate-/l*N/A
lower-fma.f32N/A
unpow2N/A
lower-*.f32N/A
lower-PI.f32N/A
lower-PI.f32N/A
lower-/.f32N/A
unpow2N/A
lower-*.f3295.0
Applied rewrites95.0%
Taylor expanded in s around 0
lower-/.f32N/A
lower-+.f32N/A
lower-exp.f32N/A
associate-*r/N/A
lower-/.f32N/A
mul-1-negN/A
lower-neg.f32N/A
lower-PI.f3298.7
Applied rewrites98.7%
Final simplification98.7%
(FPCore (u s)
:precision binary32
(let* ((t_0 (/ (PI) s)))
(*
(- s)
(log
(+
-1.0
(/
1.0
(+
(*
u
(+
(/ 1.0 (+ 1.0 (exp (/ (PI) (- s)))))
(/ 1.0 (- -1.0 (+ t_0 (fma (* (PI) (PI)) (/ 0.5 (* s s)) 1.0))))))
(/ 1.0 (+ 1.0 (+ 1.0 t_0))))))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := \frac{\mathsf{PI}\left(\right)}{s}\\
\left(-s\right) \cdot \log \left(-1 + \frac{1}{u \cdot \left(\frac{1}{1 + e^{\frac{\mathsf{PI}\left(\right)}{-s}}} + \frac{1}{-1 - \left(t\_0 + \mathsf{fma}\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), \frac{0.5}{s \cdot s}, 1\right)\right)}\right) + \frac{1}{1 + \left(1 + t\_0\right)}}\right)
\end{array}
\end{array}
Initial program 99.0%
Taylor expanded in s around inf
associate-+r+N/A
+-commutativeN/A
lower-+.f32N/A
lower-/.f32N/A
lower-PI.f32N/A
+-commutativeN/A
associate-*r/N/A
*-commutativeN/A
associate-/l*N/A
lower-fma.f32N/A
unpow2N/A
lower-*.f32N/A
lower-PI.f32N/A
lower-PI.f32N/A
lower-/.f32N/A
unpow2N/A
lower-*.f3295.0
Applied rewrites95.0%
Taylor expanded in s around inf
lower-+.f32N/A
lower-/.f32N/A
lower-PI.f3286.1
Applied rewrites86.1%
Final simplification86.1%
(FPCore (u s)
:precision binary32
(let* ((t_0 (/ (PI) s)))
(*
(- s)
(log
(+
-1.0
(/
1.0
(+
(/ 1.0 (+ 1.0 (exp t_0)))
(*
u
(+
(/ 1.0 (+ 1.0 1.0))
(/
1.0
(- -1.0 (+ t_0 (fma (* (PI) (PI)) (/ 0.5 (* s s)) 1.0)))))))))))))\begin{array}{l}
\\
\begin{array}{l}
t_0 := \frac{\mathsf{PI}\left(\right)}{s}\\
\left(-s\right) \cdot \log \left(-1 + \frac{1}{\frac{1}{1 + e^{t\_0}} + u \cdot \left(\frac{1}{1 + 1} + \frac{1}{-1 - \left(t\_0 + \mathsf{fma}\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), \frac{0.5}{s \cdot s}, 1\right)\right)}\right)}\right)
\end{array}
\end{array}
Initial program 99.0%
Taylor expanded in s around inf
associate-+r+N/A
+-commutativeN/A
lower-+.f32N/A
lower-/.f32N/A
lower-PI.f32N/A
+-commutativeN/A
associate-*r/N/A
*-commutativeN/A
associate-/l*N/A
lower-fma.f32N/A
unpow2N/A
lower-*.f32N/A
lower-PI.f32N/A
lower-PI.f32N/A
lower-/.f32N/A
unpow2N/A
lower-*.f3295.0
Applied rewrites95.0%
Taylor expanded in s around inf
Applied rewrites37.7%
Final simplification37.7%
(FPCore (u s)
:precision binary32
(*
(- s)
(log
(+
-1.0
(*
(/ s (* (* u u) (fma 0.25 (* (PI) (PI)) (/ (* 0.5 (* s (PI))) u))))
(fma 0.5 (fma u (PI) s) (* (PI) 0.25)))))))\begin{array}{l}
\\
\left(-s\right) \cdot \log \left(-1 + \frac{s}{\left(u \cdot u\right) \cdot \mathsf{fma}\left(0.25, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), \frac{0.5 \cdot \left(s \cdot \mathsf{PI}\left(\right)\right)}{u}\right)} \cdot \mathsf{fma}\left(0.5, \mathsf{fma}\left(u, \mathsf{PI}\left(\right), s\right), \mathsf{PI}\left(\right) \cdot 0.25\right)\right)
\end{array}
Initial program 99.0%
Taylor expanded in s around -inf
lower-+.f32N/A
associate-*r/N/A
Applied rewrites0.6%
Taylor expanded in s around 0
lower-/.f32N/A
+-commutativeN/A
distribute-lft-outN/A
lower-fma.f32N/A
lower-+.f32N/A
*-commutativeN/A
lower-*.f32N/A
lower-PI.f32N/A
*-commutativeN/A
lower-*.f32N/A
lower-PI.f32-0.0
Applied rewrites-0.0%
Applied rewrites0.0%
Taylor expanded in u around inf
lower-*.f32N/A
unpow2N/A
lower-*.f32N/A
lower-fma.f32N/A
unpow2N/A
lower-*.f32N/A
lower-PI.f32N/A
lower-PI.f32N/A
associate-*r/N/A
lower-/.f32N/A
lower-*.f32N/A
lower-*.f32N/A
lower-PI.f3218.5
Applied rewrites18.5%
Final simplification18.5%
(FPCore (u s)
:precision binary32
(*
(- s)
(log
(+
-1.0
(+
(fma -8.0 (/ (fma 0.5 (* u (* (PI) 0.5)) (* (PI) 0.25)) s) 2.0)
(* 0.25 (/ (* (PI) 12.0) s)))))))\begin{array}{l}
\\
\left(-s\right) \cdot \log \left(-1 + \left(\mathsf{fma}\left(-8, \frac{\mathsf{fma}\left(0.5, u \cdot \left(\mathsf{PI}\left(\right) \cdot 0.5\right), \mathsf{PI}\left(\right) \cdot 0.25\right)}{s}, 2\right) + 0.25 \cdot \frac{\mathsf{PI}\left(\right) \cdot 12}{s}\right)\right)
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Taylor expanded in s around inf
cancel-sign-sub-invN/A
lower-+.f32N/A
Applied rewrites20.3%
Final simplification20.3%
(FPCore (u s) :precision binary32 (* (- s) (log (+ 1.0 (fma 0.5 (/ (* (* u (PI)) -4.0) s) (/ (PI) s))))))
\begin{array}{l}
\\
\left(-s\right) \cdot \log \left(1 + \mathsf{fma}\left(0.5, \frac{\left(u \cdot \mathsf{PI}\left(\right)\right) \cdot -4}{s}, \frac{\mathsf{PI}\left(\right)}{s}\right)\right)
\end{array}
Initial program 99.0%
Taylor expanded in s around -inf
lower-+.f32N/A
associate-*r/N/A
Applied rewrites0.6%
Taylor expanded in s around 0
lower-/.f32N/A
+-commutativeN/A
distribute-lft-outN/A
lower-fma.f32N/A
lower-+.f32N/A
*-commutativeN/A
lower-*.f32N/A
lower-PI.f32N/A
*-commutativeN/A
lower-*.f32N/A
lower-PI.f32-0.0
Applied rewrites-0.0%
Applied rewrites0.0%
Taylor expanded in s around inf
lower-+.f32N/A
lower-fma.f32N/A
lower-/.f32N/A
distribute-rgt-out--N/A
metadata-evalN/A
lower-*.f32N/A
lower-*.f32N/A
lower-PI.f32N/A
lower-/.f32N/A
lower-PI.f3216.7
Applied rewrites16.8%
(FPCore (u s) :precision binary32 (let* ((t_0 (* s (PI)))) (/ (/ (* t_0 t_0) (* (- s) (PI))) s)))
\begin{array}{l}
\\
\begin{array}{l}
t_0 := s \cdot \mathsf{PI}\left(\right)\\
\frac{\frac{t\_0 \cdot t\_0}{\left(-s\right) \cdot \mathsf{PI}\left(\right)}}{s}
\end{array}
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Taylor expanded in u around 0
lower-/.f32N/A
lower-PI.f3211.3
Applied rewrites11.3%
lift-neg.f32N/A
lift-PI.f32N/A
associate-*r/N/A
lower-/.f32N/A
lift-neg.f32N/A
distribute-lft-neg-outN/A
lower-neg.f32N/A
lower-*.f3211.3
Applied rewrites11.3%
lift-PI.f32N/A
lift-*.f32N/A
neg-sub0N/A
flip--N/A
lower-/.f32N/A
metadata-evalN/A
lower--.f32N/A
lower-*.f32N/A
lower-+.f3214.3
Applied rewrites14.3%
Final simplification14.3%
(FPCore (u s) :precision binary32 (* (/ (PI) s) (* (* s s) (/ -1.0 s))))
\begin{array}{l}
\\
\frac{\mathsf{PI}\left(\right)}{s} \cdot \left(\left(s \cdot s\right) \cdot \frac{-1}{s}\right)
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Taylor expanded in u around 0
lower-/.f32N/A
lower-PI.f3211.3
Applied rewrites11.3%
Applied rewrites14.0%
Final simplification14.0%
(FPCore (u s) :precision binary32 (* (/ (PI) (- s)) (/ (* s s) s)))
\begin{array}{l}
\\
\frac{\mathsf{PI}\left(\right)}{-s} \cdot \frac{s \cdot s}{s}
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Taylor expanded in u around 0
lower-/.f32N/A
lower-PI.f3211.3
Applied rewrites11.3%
lift-neg.f3211.3
--rgt-identityN/A
flip--N/A
lift-*.f32N/A
metadata-evalN/A
--rgt-identityN/A
metadata-evalN/A
sub-negN/A
--rgt-identityN/A
lower-/.f3214.0
lift-*.f32N/A
lift-neg.f32N/A
lift-neg.f32N/A
sqr-negN/A
lift-*.f3214.0
Applied rewrites14.0%
Final simplification14.0%
(FPCore (u s) :precision binary32 (/ (* s (PI)) (- s)))
\begin{array}{l}
\\
\frac{s \cdot \mathsf{PI}\left(\right)}{-s}
\end{array}
Initial program 99.0%
Applied rewrites98.9%
Taylor expanded in u around 0
lower-/.f32N/A
lower-PI.f3211.3
Applied rewrites11.3%
lift-neg.f32N/A
lift-PI.f32N/A
associate-*r/N/A
lower-/.f32N/A
lift-neg.f32N/A
distribute-lft-neg-outN/A
lower-neg.f32N/A
lower-*.f3211.3
Applied rewrites11.3%
Final simplification11.3%
(FPCore (u s) :precision binary32 (- (PI)))
\begin{array}{l}
\\
-\mathsf{PI}\left(\right)
\end{array}
Initial program 99.0%
Taylor expanded in u around 0
mul-1-negN/A
lower-neg.f32N/A
lower-PI.f3211.3
Applied rewrites11.3%
herbie shell --seed 2024216
(FPCore (u s)
:name "Sample trimmed logistic on [-pi, pi]"
:precision binary32
:pre (and (and (<= 2.328306437e-10 u) (<= u 1.0)) (and (<= 0.0 s) (<= s 1.0651631)))
(* (- s) (log (- (/ 1.0 (+ (* u (- (/ 1.0 (+ 1.0 (exp (/ (- (PI)) s)))) (/ 1.0 (+ 1.0 (exp (/ (PI) s)))))) (/ 1.0 (+ 1.0 (exp (/ (PI) s)))))) 1.0))))