mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

Note that Z3_get_numeral_small is essentially redundant

Browse source 
The error behavior of Z3_get_numeral_small does not follow the pattern of
the other functions. The functions that have out params and return a bool
indicating success (such as Z3_get_numeral_rational_int64) return false
rather than signaling an error when given an unsupported expression
argument (such as a rounding mode value). The functions that do not have out
params signal an error in such cases. Z3_get_numeral_small is the odd one
out in that it signals errors and returns a status bool.

This error handling is the only difference between Z3_get_numeral_small and
Z3_get_numeral_rational_int64, so this patch adds a comment to the
documentation.
This commit is contained in:
Josh Berdine 2025-03-29 12:57:14 +00:00
parent 9b5a9b2089
commit e2d3f39735
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/z3_api.h
View file

@ -5109,6 +5109,8 @@ extern "C" {
Return \c true if the numeral value fits in 64 bit numerals, \c false otherwise. Return \c true if the numeral value fits in 64 bit numerals, \c false otherwise.
Equivalent to \c Z3_get_numeral_rational_int64 except that for unsupported expression arguments \c Z3_get_numeral_small signals an error while \c Z3_get_numeral_rational_int64 returns \c false.
\pre Z3_get_ast_kind(a) == Z3_NUMERAL_AST \pre Z3_get_ast_kind(a) == Z3_NUMERAL_AST
def_API('Z3_get_numeral_small', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64))) def_API('Z3_get_numeral_small', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64)))