mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

#5361

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-21 14:57:54 -07:00
parent 161d38397b
commit f3737f6831
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/z3_fpa.h
View file

@ -961,7 +961,8 @@ extern "C" {
\param c logical context
\param t a floating-point numeral
\param sgn sign
\param sgn the retrieved sign
\returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for
NaN, which is an invalid argument.
@ -975,6 +976,7 @@ extern "C" {
\param c logical context
\param t a floating-point numeral
\returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
Remarks: The significand \c s is always \ccode{0.0 <= s < 2.0}; the resulting string is long
enough to represent the real significand precisely.
@ -1004,6 +1006,7 @@ extern "C" {
\param c logical context
\param t a floating-point numeral
\param biased flag to indicate whether the result is in biased representation
\returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
Remarks: This function extracts the exponent in `t`, without normalization.
NaN is an invalid argument.
@ -1019,6 +1022,7 @@ extern "C" {
\param t a floating-point numeral
\param n exponent
\param biased flag to indicate whether the result is in biased representation
\returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
Remarks: This function extracts the exponent in `t`, without normalization.
NaN is an invalid argument.