mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-07 17:40:54 +00:00
Code Activity

Add Z3_fpa_is_numeral to the API (#8026)

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-11-16 00:21:08 +00:00 • committed by GitHub
parent 43525481f0
commit 28b31cfe91
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 30 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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);
/**
\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.