
(FPCore (x s) :precision binary32 (/ 1.0 (+ 1.0 (exp (/ (- x) s)))))
float code(float x, float s) {
return 1.0f / (1.0f + expf((-x / s)));
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
code = 1.0e0 / (1.0e0 + exp((-x / s)))
end function
function code(x, s) return Float32(Float32(1.0) / Float32(Float32(1.0) + exp(Float32(Float32(-x) / s)))) end
function tmp = code(x, s) tmp = single(1.0) / (single(1.0) + exp((-x / s))); end
\begin{array}{l}
\\
\frac{1}{1 + e^{\frac{-x}{s}}}
\end{array}
Sampling outcomes in binary32 precision:
Herbie found 14 alternatives:
| Alternative | Accuracy | Speedup |
|---|
(FPCore (x s) :precision binary32 (/ 1.0 (+ 1.0 (exp (/ (- x) s)))))
float code(float x, float s) {
return 1.0f / (1.0f + expf((-x / s)));
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
code = 1.0e0 / (1.0e0 + exp((-x / s)))
end function
function code(x, s) return Float32(Float32(1.0) / Float32(Float32(1.0) + exp(Float32(Float32(-x) / s)))) end
function tmp = code(x, s) tmp = single(1.0) / (single(1.0) + exp((-x / s))); end
\begin{array}{l}
\\
\frac{1}{1 + e^{\frac{-x}{s}}}
\end{array}
(FPCore (x s) :precision binary32 (exp (- (log1p (exp (/ (- x) s))))))
float code(float x, float s) {
return expf(-log1pf(expf((-x / s))));
}
function code(x, s) return exp(Float32(-log1p(exp(Float32(Float32(-x) / s))))) end
\begin{array}{l}
\\
e^{-\mathsf{log1p}\left(e^{\frac{-x}{s}}\right)}
\end{array}
Initial program 99.8%
lift-/.f32N/A
inv-powN/A
pow-to-expN/A
*-commutativeN/A
log-powN/A
inv-powN/A
lift-/.f32N/A
lower-exp.f32N/A
lift-/.f32N/A
log-recN/A
lower-neg.f32N/A
lift-+.f32N/A
lower-log1p.f3299.8
Applied rewrites99.8%
(FPCore (x s) :precision binary32 (/ 1.0 (+ (pow (exp -1.0) (* (/ 1.0 s) x)) 1.0)))
float code(float x, float s) {
return 1.0f / (powf(expf(-1.0f), ((1.0f / s) * x)) + 1.0f);
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
code = 1.0e0 / ((exp((-1.0e0)) ** ((1.0e0 / s) * x)) + 1.0e0)
end function
function code(x, s) return Float32(Float32(1.0) / Float32((exp(Float32(-1.0)) ^ Float32(Float32(Float32(1.0) / s) * x)) + Float32(1.0))) end
function tmp = code(x, s) tmp = single(1.0) / ((exp(single(-1.0)) ^ ((single(1.0) / s) * x)) + single(1.0)); end
\begin{array}{l}
\\
\frac{1}{{\left(e^{-1}\right)}^{\left(\frac{1}{s} \cdot x\right)} + 1}
\end{array}
Initial program 99.8%
lift-exp.f32N/A
lift-/.f32N/A
lift-neg.f32N/A
distribute-frac-negN/A
neg-mul-1N/A
exp-prodN/A
lower-pow.f32N/A
lower-exp.f32N/A
lower-/.f3299.8
Applied rewrites99.8%
lift-/.f32N/A
div-invN/A
lift-/.f32N/A
*-commutativeN/A
lift-*.f3299.8
Applied rewrites99.8%
Final simplification99.8%
(FPCore (x s) :precision binary32 (/ 1.0 (+ (pow (exp -1.0) (/ x s)) 1.0)))
float code(float x, float s) {
return 1.0f / (powf(expf(-1.0f), (x / s)) + 1.0f);
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
code = 1.0e0 / ((exp((-1.0e0)) ** (x / s)) + 1.0e0)
end function
function code(x, s) return Float32(Float32(1.0) / Float32((exp(Float32(-1.0)) ^ Float32(x / s)) + Float32(1.0))) end
function tmp = code(x, s) tmp = single(1.0) / ((exp(single(-1.0)) ^ (x / s)) + single(1.0)); end
\begin{array}{l}
\\
\frac{1}{{\left(e^{-1}\right)}^{\left(\frac{x}{s}\right)} + 1}
\end{array}
Initial program 99.8%
lift-exp.f32N/A
lift-/.f32N/A
lift-neg.f32N/A
distribute-frac-negN/A
neg-mul-1N/A
exp-prodN/A
lower-pow.f32N/A
lower-exp.f32N/A
lower-/.f3299.8
Applied rewrites99.8%
Final simplification99.8%
(FPCore (x s) :precision binary32 (/ 1.0 (+ (/ 1.0 (exp (/ x s))) 1.0)))
float code(float x, float s) {
return 1.0f / ((1.0f / expf((x / s))) + 1.0f);
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
code = 1.0e0 / ((1.0e0 / exp((x / s))) + 1.0e0)
end function
function code(x, s) return Float32(Float32(1.0) / Float32(Float32(Float32(1.0) / exp(Float32(x / s))) + Float32(1.0))) end
function tmp = code(x, s) tmp = single(1.0) / ((single(1.0) / exp((x / s))) + single(1.0)); end
\begin{array}{l}
\\
\frac{1}{\frac{1}{e^{\frac{x}{s}}} + 1}
\end{array}
Initial program 99.8%
lift-exp.f32N/A
lift-/.f32N/A
lift-neg.f32N/A
distribute-frac-negN/A
exp-negN/A
lower-/.f32N/A
lower-exp.f32N/A
lower-/.f3299.8
Applied rewrites99.8%
Final simplification99.8%
(FPCore (x s) :precision binary32 (/ 1.0 (+ 1.0 (exp (/ (- x) s)))))
float code(float x, float s) {
return 1.0f / (1.0f + expf((-x / s)));
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
code = 1.0e0 / (1.0e0 + exp((-x / s)))
end function
function code(x, s) return Float32(Float32(1.0) / Float32(Float32(1.0) + exp(Float32(Float32(-x) / s)))) end
function tmp = code(x, s) tmp = single(1.0) / (single(1.0) + exp((-x / s))); end
\begin{array}{l}
\\
\frac{1}{1 + e^{\frac{-x}{s}}}
\end{array}
Initial program 99.8%
(FPCore (x s)
:precision binary32
(if (<= (/ (- x) s) 0.6000000238418579)
0.5
(/
1.0
(fma
(fma
(fma (/ x (* (* s s) s)) -0.16666666666666666 (/ 0.5 (* s s)))
x
(/ -1.0 s))
x
2.0))))
float code(float x, float s) {
float tmp;
if ((-x / s) <= 0.6000000238418579f) {
tmp = 0.5f;
} else {
tmp = 1.0f / fmaf(fmaf(fmaf((x / ((s * s) * s)), -0.16666666666666666f, (0.5f / (s * s))), x, (-1.0f / s)), x, 2.0f);
}
return tmp;
}
function code(x, s) tmp = Float32(0.0) if (Float32(Float32(-x) / s) <= Float32(0.6000000238418579)) tmp = Float32(0.5); else tmp = Float32(Float32(1.0) / fma(fma(fma(Float32(x / Float32(Float32(s * s) * s)), Float32(-0.16666666666666666), Float32(Float32(0.5) / Float32(s * s))), x, Float32(Float32(-1.0) / s)), x, Float32(2.0))); end return tmp end
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;\frac{-x}{s} \leq 0.6000000238418579:\\
\;\;\;\;0.5\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{x}{\left(s \cdot s\right) \cdot s}, -0.16666666666666666, \frac{0.5}{s \cdot s}\right), x, \frac{-1}{s}\right), x, 2\right)}\\
\end{array}
\end{array}
if (/.f32 (neg.f32 x) s) < 0.600000024Initial program 99.8%
Taylor expanded in s around inf
Applied rewrites51.4%
if 0.600000024 < (/.f32 (neg.f32 x) s) Initial program 99.7%
lift-/.f32N/A
div-invN/A
lift-neg.f32N/A
neg-sub0N/A
flip3--N/A
frac-timesN/A
metadata-evalN/A
sub0-negN/A
cube-negN/A
lift-neg.f32N/A
metadata-evalN/A
unpow-prod-downN/A
*-rgt-identityN/A
lift-neg.f32N/A
cube-negN/A
sub0-negN/A
metadata-evalN/A
lower-/.f32N/A
Applied rewrites62.8%
Taylor expanded in x around 0
+-commutativeN/A
*-commutativeN/A
lower-fma.f32N/A
Applied rewrites86.6%
(FPCore (x s)
:precision binary32
(if (<= (/ (- x) s) 0.6000000238418579)
0.5
(/
1.0
(fma
(fma (/ x (* s s)) (fma -0.16666666666666666 (/ x s) 0.5) (/ -1.0 s))
x
2.0))))
float code(float x, float s) {
float tmp;
if ((-x / s) <= 0.6000000238418579f) {
tmp = 0.5f;
} else {
tmp = 1.0f / fmaf(fmaf((x / (s * s)), fmaf(-0.16666666666666666f, (x / s), 0.5f), (-1.0f / s)), x, 2.0f);
}
return tmp;
}
function code(x, s) tmp = Float32(0.0) if (Float32(Float32(-x) / s) <= Float32(0.6000000238418579)) tmp = Float32(0.5); else tmp = Float32(Float32(1.0) / fma(fma(Float32(x / Float32(s * s)), fma(Float32(-0.16666666666666666), Float32(x / s), Float32(0.5)), Float32(Float32(-1.0) / s)), x, Float32(2.0))); end return tmp end
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;\frac{-x}{s} \leq 0.6000000238418579:\\
\;\;\;\;0.5\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{x}{s \cdot s}, \mathsf{fma}\left(-0.16666666666666666, \frac{x}{s}, 0.5\right), \frac{-1}{s}\right), x, 2\right)}\\
\end{array}
\end{array}
if (/.f32 (neg.f32 x) s) < 0.600000024Initial program 99.8%
Taylor expanded in s around inf
Applied rewrites51.4%
if 0.600000024 < (/.f32 (neg.f32 x) s) Initial program 99.7%
Taylor expanded in s around inf
Applied rewrites85.1%
(FPCore (x s)
:precision binary32
(if (<= (/ (- x) s) -10000.0)
0.5
(/
1.0
(+
(/ (- (* (* (fma -0.16666666666666666 (/ x s) 0.5) x) (/ x s)) x) s)
2.0))))
float code(float x, float s) {
float tmp;
if ((-x / s) <= -10000.0f) {
tmp = 0.5f;
} else {
tmp = 1.0f / (((((fmaf(-0.16666666666666666f, (x / s), 0.5f) * x) * (x / s)) - x) / s) + 2.0f);
}
return tmp;
}
function code(x, s) tmp = Float32(0.0) if (Float32(Float32(-x) / s) <= Float32(-10000.0)) tmp = Float32(0.5); else tmp = Float32(Float32(1.0) / Float32(Float32(Float32(Float32(Float32(fma(Float32(-0.16666666666666666), Float32(x / s), Float32(0.5)) * x) * Float32(x / s)) - x) / s) + Float32(2.0))); end return tmp end
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;\frac{-x}{s} \leq -10000:\\
\;\;\;\;0.5\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\frac{\left(\mathsf{fma}\left(-0.16666666666666666, \frac{x}{s}, 0.5\right) \cdot x\right) \cdot \frac{x}{s} - x}{s} + 2}\\
\end{array}
\end{array}
if (/.f32 (neg.f32 x) s) < -1e4Initial program 100.0%
Taylor expanded in s around inf
Applied rewrites28.1%
if -1e4 < (/.f32 (neg.f32 x) s) Initial program 99.6%
lift-/.f32N/A
div-invN/A
lift-neg.f32N/A
neg-sub0N/A
flip3--N/A
frac-timesN/A
metadata-evalN/A
sub0-negN/A
cube-negN/A
lift-neg.f32N/A
metadata-evalN/A
unpow-prod-downN/A
*-rgt-identityN/A
lift-neg.f32N/A
cube-negN/A
sub0-negN/A
metadata-evalN/A
lower-/.f32N/A
Applied rewrites47.2%
Taylor expanded in s around inf
Applied rewrites85.9%
Applied rewrites86.6%
Final simplification63.3%
(FPCore (x s) :precision binary32 (if (<= (/ (- x) s) 250.0) 0.5 (/ 1.0 (* (/ -0.16666666666666666 (* (* s s) s)) (* (* x x) x)))))
float code(float x, float s) {
float tmp;
if ((-x / s) <= 250.0f) {
tmp = 0.5f;
} else {
tmp = 1.0f / ((-0.16666666666666666f / ((s * s) * s)) * ((x * x) * x));
}
return tmp;
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
real(4) :: tmp
if ((-x / s) <= 250.0e0) then
tmp = 0.5e0
else
tmp = 1.0e0 / (((-0.16666666666666666e0) / ((s * s) * s)) * ((x * x) * x))
end if
code = tmp
end function
function code(x, s) tmp = Float32(0.0) if (Float32(Float32(-x) / s) <= Float32(250.0)) tmp = Float32(0.5); else tmp = Float32(Float32(1.0) / Float32(Float32(Float32(-0.16666666666666666) / Float32(Float32(s * s) * s)) * Float32(Float32(x * x) * x))); end return tmp end
function tmp_2 = code(x, s) tmp = single(0.0); if ((-x / s) <= single(250.0)) tmp = single(0.5); else tmp = single(1.0) / ((single(-0.16666666666666666) / ((s * s) * s)) * ((x * x) * x)); end tmp_2 = tmp; end
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;\frac{-x}{s} \leq 250:\\
\;\;\;\;0.5\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\frac{-0.16666666666666666}{\left(s \cdot s\right) \cdot s} \cdot \left(\left(x \cdot x\right) \cdot x\right)}\\
\end{array}
\end{array}
if (/.f32 (neg.f32 x) s) < 250Initial program 99.7%
Taylor expanded in s around inf
Applied rewrites49.3%
if 250 < (/.f32 (neg.f32 x) s) Initial program 100.0%
lift-/.f32N/A
div-invN/A
lift-neg.f32N/A
neg-sub0N/A
flip3--N/A
frac-timesN/A
metadata-evalN/A
sub0-negN/A
cube-negN/A
lift-neg.f32N/A
metadata-evalN/A
unpow-prod-downN/A
*-rgt-identityN/A
lift-neg.f32N/A
cube-negN/A
sub0-negN/A
metadata-evalN/A
lower-/.f32N/A
Applied rewrites63.0%
Taylor expanded in s around inf
Applied rewrites87.1%
Taylor expanded in s around 0
Applied rewrites92.1%
(FPCore (x s) :precision binary32 (if (<= (/ (- x) s) 10000000.0) 0.5 (/ 1.0 (* (/ (* (* x x) x) (* (* s s) s)) -0.16666666666666666))))
float code(float x, float s) {
float tmp;
if ((-x / s) <= 10000000.0f) {
tmp = 0.5f;
} else {
tmp = 1.0f / ((((x * x) * x) / ((s * s) * s)) * -0.16666666666666666f);
}
return tmp;
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
real(4) :: tmp
if ((-x / s) <= 10000000.0e0) then
tmp = 0.5e0
else
tmp = 1.0e0 / ((((x * x) * x) / ((s * s) * s)) * (-0.16666666666666666e0))
end if
code = tmp
end function
function code(x, s) tmp = Float32(0.0) if (Float32(Float32(-x) / s) <= Float32(10000000.0)) tmp = Float32(0.5); else tmp = Float32(Float32(1.0) / Float32(Float32(Float32(Float32(x * x) * x) / Float32(Float32(s * s) * s)) * Float32(-0.16666666666666666))); end return tmp end
function tmp_2 = code(x, s) tmp = single(0.0); if ((-x / s) <= single(10000000.0)) tmp = single(0.5); else tmp = single(1.0) / ((((x * x) * x) / ((s * s) * s)) * single(-0.16666666666666666)); end tmp_2 = tmp; end
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;\frac{-x}{s} \leq 10000000:\\
\;\;\;\;0.5\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\frac{\left(x \cdot x\right) \cdot x}{\left(s \cdot s\right) \cdot s} \cdot -0.16666666666666666}\\
\end{array}
\end{array}
if (/.f32 (neg.f32 x) s) < 1e7Initial program 99.7%
Taylor expanded in s around inf
Applied rewrites48.6%
if 1e7 < (/.f32 (neg.f32 x) s) Initial program 100.0%
Taylor expanded in s around -inf
mul-1-negN/A
unsub-negN/A
lower--.f32N/A
lower-/.f32N/A
Applied rewrites90.1%
Taylor expanded in s around 0
Applied rewrites94.2%
Final simplification62.5%
(FPCore (x s) :precision binary32 (if (<= (/ (- x) s) -10000.0) 0.5 (/ 1.0 (fma (/ x s) (fma (/ 0.5 s) x -1.0) 2.0))))
float code(float x, float s) {
float tmp;
if ((-x / s) <= -10000.0f) {
tmp = 0.5f;
} else {
tmp = 1.0f / fmaf((x / s), fmaf((0.5f / s), x, -1.0f), 2.0f);
}
return tmp;
}
function code(x, s) tmp = Float32(0.0) if (Float32(Float32(-x) / s) <= Float32(-10000.0)) tmp = Float32(0.5); else tmp = Float32(Float32(1.0) / fma(Float32(x / s), fma(Float32(Float32(0.5) / s), x, Float32(-1.0)), Float32(2.0))); end return tmp end
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;\frac{-x}{s} \leq -10000:\\
\;\;\;\;0.5\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\mathsf{fma}\left(\frac{x}{s}, \mathsf{fma}\left(\frac{0.5}{s}, x, -1\right), 2\right)}\\
\end{array}
\end{array}
if (/.f32 (neg.f32 x) s) < -1e4Initial program 100.0%
Taylor expanded in s around inf
Applied rewrites28.1%
if -1e4 < (/.f32 (neg.f32 x) s) Initial program 99.6%
Taylor expanded in s around inf
associate-+r+N/A
+-commutativeN/A
unpow2N/A
associate-/l*N/A
associate-*r*N/A
*-commutativeN/A
associate-*r*N/A
+-commutativeN/A
associate-+l+N/A
Applied rewrites82.0%
(FPCore (x s) :precision binary32 (if (<= (- x) 1.0000000036274937e-15) 0.5 (/ 1.0 (- 2.0 (* (* (* x x) x) (/ 0.16666666666666666 (* (* s s) s)))))))
float code(float x, float s) {
float tmp;
if (-x <= 1.0000000036274937e-15f) {
tmp = 0.5f;
} else {
tmp = 1.0f / (2.0f - (((x * x) * x) * (0.16666666666666666f / ((s * s) * s))));
}
return tmp;
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
real(4) :: tmp
if (-x <= 1.0000000036274937e-15) then
tmp = 0.5e0
else
tmp = 1.0e0 / (2.0e0 - (((x * x) * x) * (0.16666666666666666e0 / ((s * s) * s))))
end if
code = tmp
end function
function code(x, s) tmp = Float32(0.0) if (Float32(-x) <= Float32(1.0000000036274937e-15)) tmp = Float32(0.5); else tmp = Float32(Float32(1.0) / Float32(Float32(2.0) - Float32(Float32(Float32(x * x) * x) * Float32(Float32(0.16666666666666666) / Float32(Float32(s * s) * s))))); end return tmp end
function tmp_2 = code(x, s) tmp = single(0.0); if (-x <= single(1.0000000036274937e-15)) tmp = single(0.5); else tmp = single(1.0) / (single(2.0) - (((x * x) * x) * (single(0.16666666666666666) / ((s * s) * s)))); end tmp_2 = tmp; end
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;-x \leq 1.0000000036274937 \cdot 10^{-15}:\\
\;\;\;\;0.5\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{2 - \left(\left(x \cdot x\right) \cdot x\right) \cdot \frac{0.16666666666666666}{\left(s \cdot s\right) \cdot s}}\\
\end{array}
\end{array}
if (neg.f32 x) < 1e-15Initial program 99.8%
Taylor expanded in s around inf
Applied rewrites48.7%
if 1e-15 < (neg.f32 x) Initial program 99.8%
Taylor expanded in s around -inf
mul-1-negN/A
unsub-negN/A
lower--.f32N/A
lower-/.f32N/A
Applied rewrites85.3%
Taylor expanded in s around inf
Applied rewrites78.1%
Taylor expanded in s around 0
Applied rewrites89.7%
Final simplification63.0%
(FPCore (x s) :precision binary32 (if (<= (/ (- x) s) -10000.0) 0.5 (/ 1.0 (- 2.0 (/ x s)))))
float code(float x, float s) {
float tmp;
if ((-x / s) <= -10000.0f) {
tmp = 0.5f;
} else {
tmp = 1.0f / (2.0f - (x / s));
}
return tmp;
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
real(4) :: tmp
if ((-x / s) <= (-10000.0e0)) then
tmp = 0.5e0
else
tmp = 1.0e0 / (2.0e0 - (x / s))
end if
code = tmp
end function
function code(x, s) tmp = Float32(0.0) if (Float32(Float32(-x) / s) <= Float32(-10000.0)) tmp = Float32(0.5); else tmp = Float32(Float32(1.0) / Float32(Float32(2.0) - Float32(x / s))); end return tmp end
function tmp_2 = code(x, s) tmp = single(0.0); if ((-x / s) <= single(-10000.0)) tmp = single(0.5); else tmp = single(1.0) / (single(2.0) - (x / s)); end tmp_2 = tmp; end
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;\frac{-x}{s} \leq -10000:\\
\;\;\;\;0.5\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{2 - \frac{x}{s}}\\
\end{array}
\end{array}
if (/.f32 (neg.f32 x) s) < -1e4Initial program 100.0%
Taylor expanded in s around inf
Applied rewrites28.1%
if -1e4 < (/.f32 (neg.f32 x) s) Initial program 99.6%
Taylor expanded in s around inf
mul-1-negN/A
unsub-negN/A
lower--.f32N/A
lower-/.f3259.0
Applied rewrites59.0%
(FPCore (x s) :precision binary32 0.5)
float code(float x, float s) {
return 0.5f;
}
real(4) function code(x, s)
real(4), intent (in) :: x
real(4), intent (in) :: s
code = 0.5e0
end function
function code(x, s) return Float32(0.5) end
function tmp = code(x, s) tmp = single(0.5); end
\begin{array}{l}
\\
0.5
\end{array}
Initial program 99.8%
Taylor expanded in s around inf
Applied rewrites35.7%
herbie shell --seed 2024235
(FPCore (x s)
:name "Logistic function"
:precision binary32
:pre (and (<= 0.0 s) (<= s 1.0651631))
(/ 1.0 (+ 1.0 (exp (/ (- x) s)))))