Note that Z3_get_numeral_small is essentially redundant #7599
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Analogous to other Z3_get_numeral_* functions with out params.
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.
arbipher
pushed a commit
to arbipher/z3
that referenced
this pull request
Apr 17, 2025
* 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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.
Also:
Check that Z3_get_numeral_small is given non-null out params
Analogous to other Z3_get_numeral_* functions with out params.