mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-23 14:11:28 +00:00
Code Activity

Add Z3_fpa_is_numeral to the API

Browse source 
This is analogous to Z3_fpa_is_numeral_nan, Z3_fpa_is_numeral_inf, etc. and
can be needed to check that inputs are valid before calling those functions.

Signed-off-by: Josh Berdine <josh@berdine.net>
This commit is contained in:
Josh Berdine 2025-04-10 10:38:44 +01:00
parent 11fb5c7dc4
commit 08f2d87c56
2 changed files with 30 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/api_fpa.cpp
View file

@ -1224,6 +1224,20 @@ extern "C" {
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);
} }
bool Z3_API Z3_fpa_is_numeral(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t)) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return false;
}
return fu.is_numeral(to_expr(t));
Z3_CATCH_RETURN(false);
}
bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) { bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
Z3_TRY; Z3_TRY;
LOG_Z3_fpa_is_numeral_nan(c, t); LOG_Z3_fpa_is_numeral_nan(c, t);

16
src/api/z3_fpa.h
View file

@ -1089,6 +1089,22 @@ extern "C" {
*/ */
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s); unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
/**
\brief Checks whether a given ast is a floating-point numeral.
\param c logical context
\param t an ast
\sa Z3_fpa_is_numeral_nan
\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', BOOL, (_in(CONTEXT), _in(AST)))
*/
bool Z3_API Z3_fpa_is_numeral(Z3_context c, Z3_ast t);
/** /**
\brief Checks whether a given floating-point numeral is a NaN. \brief Checks whether a given floating-point numeral is a NaN.