From 236afeb8cb0257c916b3d2b0291bb9f3807665bb Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Thu, 26 Oct 2023 00:07:03 +0700 Subject: [PATCH] docs: More intra-doc linking, bit of formatting. (#6963) --- src/api/z3_api.h | 4 +- src/api/z3_fpa.h | 256 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 258 insertions(+), 2 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9a93611b43d..894bd60dcc9 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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))) */ diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 4ab0d91775b..9c4b22153fe 100644 --- a/src/api/z3_fpa.h +++ b/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);