mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity

Note that Z3_get_numeral_small is essentially redundant (#7599)

Browse source 
* Check that Z3_get_numeral_small is given non-null out params

Analogous to other Z3_get_numeral_* functions with out params.

* Note that Z3_get_numeral_small is essentially redundant

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 17:02:32 +00:00 committed by GitHub
parent 63ad2837e2
commit 8d81a2dcaf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_numeral.cpp
View file

@ -318,6 +318,10 @@ extern "C" {
LOG_Z3_get_numeral_small(c, a, num, den); LOG_Z3_get_numeral_small(c, a, num, den);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_EXPR(a, false); CHECK_IS_EXPR(a, false);
if (!num || !den) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return false;
}
rational r; rational r;
bool ok = Z3_get_numeral_rational(c, a, r); bool ok = Z3_get_numeral_rational(c, a, r);
if (ok) { if (ok) {

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)))