mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 19:05:51 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
6ba151599e
2 changed files with 258 additions and 2 deletions
|
|
@ -5594,14 +5594,14 @@ extern "C" {
|
|||
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Increment the reference counter of the given Z3_func_interp object.
|
||||
\brief Increment the reference counter of the given \c Z3_func_interp object.
|
||||
|
||||
def_API('Z3_func_interp_inc_ref', VOID, (_in(CONTEXT), _in(FUNC_INTERP)))
|
||||
*/
|
||||
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f);
|
||||
|
||||
/**
|
||||
\brief Decrement the reference counter of the given Z3_func_interp object.
|
||||
\brief Decrement the reference counter of the given \c Z3_func_interp object.
|
||||
|
||||
def_API('Z3_func_interp_dec_ref', VOID, (_in(CONTEXT), _in(FUNC_INTERP)))
|
||||
*/
|
||||
|
|
|
|||
256
src/api/z3_fpa.h
256
src/api/z3_fpa.h
|
|
@ -32,6 +32,12 @@ extern "C" {
|
|||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_away or Z3_mk_fpa_rna
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_even or Z3_mk_fpa_rne
|
||||
\sa Z3_mk_fpa_round_toward_negative or Z3_mk_fpa_rtn
|
||||
\sa Z3_mk_fpa_round_toward_positive or Z3_mk_fpa_rtp
|
||||
\sa Z3_mk_fpa_round_toward_zero or Z3_mk_fpa_rtz
|
||||
|
||||
def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c);
|
||||
|
|
@ -39,8 +45,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_rne.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_away
|
||||
\sa Z3_mk_fpa_round_toward_negative
|
||||
\sa Z3_mk_fpa_round_toward_positive
|
||||
\sa Z3_mk_fpa_round_toward_zero
|
||||
|
||||
def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c);
|
||||
|
|
@ -48,8 +62,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_round_nearest_ties_to_even.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_rna
|
||||
\sa Z3_mk_fpa_rtn
|
||||
\sa Z3_mk_fpa_rtp
|
||||
\sa Z3_mk_fpa_rtz
|
||||
|
||||
def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c);
|
||||
|
|
@ -57,8 +79,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_rna.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_even
|
||||
\sa Z3_mk_fpa_round_toward_negative
|
||||
\sa Z3_mk_fpa_round_toward_positive
|
||||
\sa Z3_mk_fpa_round_toward_zero
|
||||
|
||||
def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c);
|
||||
|
|
@ -66,8 +96,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_round_nearest_ties_to_away.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_rne
|
||||
\sa Z3_mk_fpa_rtn
|
||||
\sa Z3_mk_fpa_rtp
|
||||
\sa Z3_mk_fpa_rtz
|
||||
|
||||
def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c);
|
||||
|
|
@ -75,8 +113,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_rtp.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_away
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_even
|
||||
\sa Z3_mk_fpa_round_toward_negative
|
||||
\sa Z3_mk_fpa_round_toward_zero
|
||||
|
||||
def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c);
|
||||
|
|
@ -84,8 +130,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_round_toward_positive.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_rna
|
||||
\sa Z3_mk_fpa_rne
|
||||
\sa Z3_mk_fpa_rtn
|
||||
\sa Z3_mk_fpa_rtz
|
||||
|
||||
def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c);
|
||||
|
|
@ -93,8 +147,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_rtn.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_away
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_even
|
||||
\sa Z3_mk_fpa_round_toward_positive
|
||||
\sa Z3_mk_fpa_round_toward_zero
|
||||
|
||||
def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c);
|
||||
|
|
@ -102,8 +164,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_round_toward_negative.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_rna
|
||||
\sa Z3_mk_fpa_rne
|
||||
\sa Z3_mk_fpa_rtp
|
||||
\sa Z3_mk_fpa_rtz
|
||||
|
||||
def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c);
|
||||
|
|
@ -111,8 +181,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_rtz.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_away
|
||||
\sa Z3_mk_fpa_round_nearest_ties_to_even
|
||||
\sa Z3_mk_fpa_round_toward_negative
|
||||
\sa Z3_mk_fpa_round_toward_positive
|
||||
|
||||
def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c);
|
||||
|
|
@ -120,8 +198,16 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
|
||||
|
||||
This is the same as #Z3_mk_fpa_round_toward_zero.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_rounding_mode_sort
|
||||
\sa Z3_mk_fpa_rna
|
||||
\sa Z3_mk_fpa_rne
|
||||
\sa Z3_mk_fpa_rtn
|
||||
\sa Z3_mk_fpa_rtp
|
||||
|
||||
def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c);
|
||||
|
|
@ -135,6 +221,11 @@ extern "C" {
|
|||
|
||||
\remark \c ebits must be larger than 1 and \c sbits must be larger than 2.
|
||||
|
||||
\sa Z3_mk_fpa_sort_half or Z3_mk_fpa_sort_16
|
||||
\sa Z3_mk_fpa_sort_single or Z3_mk_fpa_sort_32
|
||||
\sa Z3_mk_fpa_sort_double or Z3_mk_fpa_sort_64
|
||||
\sa Z3_mk_fpa_sort_quadruple or Z3_mk_fpa_sort_128
|
||||
|
||||
def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits);
|
||||
|
|
@ -142,8 +233,15 @@ extern "C" {
|
|||
/**
|
||||
\brief Create the half-precision (16-bit) FloatingPoint sort.
|
||||
|
||||
This is the same as #Z3_mk_fpa_sort_16.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_sort
|
||||
\sa Z3_mk_fpa_sort_single
|
||||
\sa Z3_mk_fpa_sort_double
|
||||
\sa Z3_mk_fpa_sort_quadruple
|
||||
|
||||
def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c);
|
||||
|
|
@ -151,8 +249,15 @@ extern "C" {
|
|||
/**
|
||||
\brief Create the half-precision (16-bit) FloatingPoint sort.
|
||||
|
||||
This is the same as #Z3_mk_fpa_sort_half.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_sort
|
||||
\sa Z3_mk_fpa_sort_32
|
||||
\sa Z3_mk_fpa_sort_64
|
||||
\sa Z3_mk_fpa_sort_128
|
||||
|
||||
def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c);
|
||||
|
|
@ -160,8 +265,15 @@ extern "C" {
|
|||
/**
|
||||
\brief Create the single-precision (32-bit) FloatingPoint sort.
|
||||
|
||||
This is the same as #Z3_mk_fpa_sort_32.
|
||||
|
||||
\param c logical context.
|
||||
|
||||
\sa Z3_mk_fpa_sort
|
||||
\sa Z3_mk_fpa_sort_half
|
||||
\sa Z3_mk_fpa_sort_double
|
||||
\sa Z3_mk_fpa_sort_quadruple
|
||||
|
||||
def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c);
|
||||
|
|
@ -169,8 +281,15 @@ extern "C" {
|
|||
/**
|
||||
\brief Create the single-precision (32-bit) FloatingPoint sort.
|
||||
|
||||
This is the same as #Z3_mk_fpa_sort_single.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_sort
|
||||
\sa Z3_mk_fpa_sort_16
|
||||
\sa Z3_mk_fpa_sort_64
|
||||
\sa Z3_mk_fpa_sort_128
|
||||
|
||||
def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c);
|
||||
|
|
@ -178,8 +297,15 @@ extern "C" {
|
|||
/**
|
||||
\brief Create the double-precision (64-bit) FloatingPoint sort.
|
||||
|
||||
This is the same as #Z3_mk_fpa_sort_64.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_sort
|
||||
\sa Z3_mk_fpa_sort_half
|
||||
\sa Z3_mk_fpa_sort_single
|
||||
\sa Z3_mk_fpa_sort_quadruple
|
||||
|
||||
def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c);
|
||||
|
|
@ -187,8 +313,15 @@ extern "C" {
|
|||
/**
|
||||
\brief Create the double-precision (64-bit) FloatingPoint sort.
|
||||
|
||||
This is the same as #Z3_mk_fpa_sort_double.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_sort
|
||||
\sa Z3_mk_fpa_sort_16
|
||||
\sa Z3_mk_fpa_sort_32
|
||||
\sa Z3_mk_fpa_sort_128
|
||||
|
||||
def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c);
|
||||
|
|
@ -196,8 +329,15 @@ extern "C" {
|
|||
/**
|
||||
\brief Create the quadruple-precision (128-bit) FloatingPoint sort.
|
||||
|
||||
This is the same as #Z3_mk_fpa_sort_128.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_sort
|
||||
\sa Z3_mk_fpa_sort_half
|
||||
\sa Z3_mk_fpa_sort_single
|
||||
\sa Z3_mk_fpa_sort_double
|
||||
|
||||
def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c);
|
||||
|
|
@ -205,8 +345,15 @@ extern "C" {
|
|||
/**
|
||||
\brief Create the quadruple-precision (128-bit) FloatingPoint sort.
|
||||
|
||||
This is the same as #Z3_mk_fpa_sort_quadruple.
|
||||
|
||||
\param c logical context
|
||||
|
||||
\sa Z3_mk_fpa_sort
|
||||
\sa Z3_mk_fpa_sort_16
|
||||
\sa Z3_mk_fpa_sort_32
|
||||
\sa Z3_mk_fpa_sort_64
|
||||
|
||||
def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);
|
||||
|
|
@ -218,6 +365,7 @@ extern "C" {
|
|||
\param s target sort
|
||||
|
||||
\sa Z3_mk_fpa_inf
|
||||
\sa Z3_mk_fpa_is_nan
|
||||
\sa Z3_mk_fpa_zero
|
||||
|
||||
def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
|
||||
|
|
@ -233,6 +381,7 @@ extern "C" {
|
|||
|
||||
When \c negative is \c true, -oo will be generated instead of +oo.
|
||||
|
||||
\sa Z3_mk_fpa_is_infinite
|
||||
\sa Z3_mk_fpa_nan
|
||||
\sa Z3_mk_fpa_zero
|
||||
|
||||
|
|
@ -250,6 +399,7 @@ extern "C" {
|
|||
When \c negative is \c true, -zero will be generated instead of +zero.
|
||||
|
||||
\sa Z3_mk_fpa_inf
|
||||
\sa Z3_mk_fpa_is_zero
|
||||
\sa Z3_mk_fpa_nan
|
||||
|
||||
def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
|
||||
|
|
@ -397,6 +547,10 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t term of FloatingPoint sort
|
||||
|
||||
\sa Z3_mk_fpa_is_negative
|
||||
\sa Z3_mk_fpa_is_positive
|
||||
\sa Z3_mk_fpa_neg
|
||||
|
||||
def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t);
|
||||
|
|
@ -407,6 +561,10 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t term of FloatingPoint sort
|
||||
|
||||
\sa Z3_mk_fpa_abs
|
||||
\sa Z3_mk_fpa_is_negative
|
||||
\sa Z3_mk_fpa_is_positive
|
||||
|
||||
def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t);
|
||||
|
|
@ -533,6 +691,8 @@ extern "C" {
|
|||
|
||||
\c t1, \c t2 must have the same FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_max
|
||||
|
||||
def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
|
@ -546,6 +706,8 @@ extern "C" {
|
|||
|
||||
\c t1, \c t2 must have the same FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_min
|
||||
|
||||
def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
|
@ -559,6 +721,11 @@ extern "C" {
|
|||
|
||||
\c t1 and \c t2 must have the same FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_eq
|
||||
\sa Z3_mk_fpa_geq
|
||||
\sa Z3_mk_fpa_gt
|
||||
\sa Z3_mk_fpa_lt
|
||||
|
||||
def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
|
@ -572,6 +739,11 @@ extern "C" {
|
|||
|
||||
\c t1 and \c t2 must have the same FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_eq
|
||||
\sa Z3_mk_fpa_geq
|
||||
\sa Z3_mk_fpa_gt
|
||||
\sa Z3_mk_fpa_leq
|
||||
|
||||
def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
|
@ -585,6 +757,11 @@ extern "C" {
|
|||
|
||||
\c t1 and \c t2 must have the same FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_eq
|
||||
\sa Z3_mk_fpa_gt
|
||||
\sa Z3_mk_fpa_leq
|
||||
\sa Z3_mk_fpa_lt
|
||||
|
||||
def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
|
@ -598,6 +775,11 @@ extern "C" {
|
|||
|
||||
\c t1 and \c t2 must have the same FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_eq
|
||||
\sa Z3_mk_fpa_geq
|
||||
\sa Z3_mk_fpa_leq
|
||||
\sa Z3_mk_fpa_lt
|
||||
|
||||
def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
|
@ -613,6 +795,11 @@ extern "C" {
|
|||
|
||||
\c t1 and \c t2 must have the same FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_geq
|
||||
\sa Z3_mk_fpa_gt
|
||||
\sa Z3_mk_fpa_leq
|
||||
\sa Z3_mk_fpa_lt
|
||||
|
||||
def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
|
@ -625,6 +812,11 @@ extern "C" {
|
|||
|
||||
\c t must have FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_is_infinite
|
||||
\sa Z3_mk_fpa_is_nan
|
||||
\sa Z3_mk_fpa_is_subnormal
|
||||
\sa Z3_mk_fpa_is_zero
|
||||
|
||||
def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);
|
||||
|
|
@ -637,6 +829,11 @@ extern "C" {
|
|||
|
||||
\c t must have FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_is_infinite
|
||||
\sa Z3_mk_fpa_is_nan
|
||||
\sa Z3_mk_fpa_is_normal
|
||||
\sa Z3_mk_fpa_is_zero
|
||||
|
||||
def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);
|
||||
|
|
@ -649,6 +846,12 @@ extern "C" {
|
|||
|
||||
\c t must have FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_is_infinite
|
||||
\sa Z3_mk_fpa_is_nan
|
||||
\sa Z3_mk_fpa_is_normal
|
||||
\sa Z3_mk_fpa_is_subnormal
|
||||
\sa Z3_mk_fpa_zero
|
||||
|
||||
def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);
|
||||
|
|
@ -661,6 +864,12 @@ extern "C" {
|
|||
|
||||
\c t must have FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_inf
|
||||
\sa Z3_mk_fpa_is_nan
|
||||
\sa Z3_mk_fpa_is_normal
|
||||
\sa Z3_mk_fpa_is_subnormal
|
||||
\sa Z3_mk_fpa_is_zero
|
||||
|
||||
def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);
|
||||
|
|
@ -673,6 +882,12 @@ extern "C" {
|
|||
|
||||
\c t must have FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_is_infinite
|
||||
\sa Z3_mk_fpa_is_normal
|
||||
\sa Z3_mk_fpa_is_subnormal
|
||||
\sa Z3_mk_fpa_is_zero
|
||||
\sa Z3_mk_fpa_nan
|
||||
|
||||
def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);
|
||||
|
|
@ -685,6 +900,10 @@ extern "C" {
|
|||
|
||||
\c t must have FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_abs
|
||||
\sa Z3_mk_fpa_is_positive
|
||||
\sa Z3_mk_fpa_neg
|
||||
|
||||
def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);
|
||||
|
|
@ -697,6 +916,10 @@ extern "C" {
|
|||
|
||||
\c t must have FloatingPoint sort.
|
||||
|
||||
\sa Z3_mk_fpa_abs
|
||||
\sa Z3_mk_fpa_is_negative
|
||||
\sa Z3_mk_fpa_neg
|
||||
|
||||
def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t);
|
||||
|
|
@ -848,6 +1071,8 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param s FloatingPoint sort
|
||||
|
||||
\sa Z3_fpa_get_sbits
|
||||
|
||||
def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT)))
|
||||
*/
|
||||
unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s);
|
||||
|
|
@ -858,6 +1083,8 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param s FloatingPoint sort
|
||||
|
||||
\sa Z3_fpa_get_ebits
|
||||
|
||||
def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT)))
|
||||
*/
|
||||
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
|
||||
|
|
@ -868,6 +1095,11 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
\sa Z3_fpa_is_numeral_inf
|
||||
\sa Z3_fpa_is_numeral_normal
|
||||
\sa Z3_fpa_is_numeral_subnormal
|
||||
\sa Z3_fpa_is_numeral_zero
|
||||
|
||||
def_API('Z3_fpa_is_numeral_nan', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
|
||||
|
|
@ -878,6 +1110,11 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
\sa Z3_fpa_is_numeral_nan
|
||||
\sa Z3_fpa_is_numeral_normal
|
||||
\sa Z3_fpa_is_numeral_subnormal
|
||||
\sa Z3_fpa_is_numeral_zero
|
||||
|
||||
def_API('Z3_fpa_is_numeral_inf', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
|
||||
|
|
@ -888,6 +1125,11 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
\sa Z3_fpa_is_numeral_inf
|
||||
\sa Z3_fpa_is_numeral_nan
|
||||
\sa Z3_fpa_is_numeral_normal
|
||||
\sa Z3_fpa_is_numeral_subnormal
|
||||
|
||||
def_API('Z3_fpa_is_numeral_zero', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
|
||||
|
|
@ -898,6 +1140,11 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
\sa Z3_fpa_is_numeral_inf
|
||||
\sa Z3_fpa_is_numeral_nan
|
||||
\sa Z3_fpa_is_numeral_subnormal
|
||||
\sa Z3_fpa_is_numeral_zero
|
||||
|
||||
def_API('Z3_fpa_is_numeral_normal', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
|
||||
|
|
@ -908,6 +1155,11 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
\sa Z3_fpa_is_numeral_inf
|
||||
\sa Z3_fpa_is_numeral_nan
|
||||
\sa Z3_fpa_is_numeral_normal
|
||||
\sa Z3_fpa_is_numeral_zero
|
||||
|
||||
def_API('Z3_fpa_is_numeral_subnormal', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
|
||||
|
|
@ -918,6 +1170,8 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
\sa Z3_fpa_is_numeral_negative
|
||||
|
||||
def_API('Z3_fpa_is_numeral_positive', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
|
||||
|
|
@ -928,6 +1182,8 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
\sa Z3_fpa_is_numeral_positive
|
||||
|
||||
def_API('Z3_fpa_is_numeral_negative', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue