Implement proposed smtlib2 bitvector overflow predicates #6715
Conversation
This file contains 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
Currently, for example, the function declaration symbol member for checking whether multiplication *does not* overflow is called `m_bv_smul_ovfl`. Since we are introducing the upcoming smtlib2 symbols that check that multpliciation *does* overflow, the not overflow check symbols are renamed to `m_bv_smul_no_ovfl` etc.
Smtlib2 is being extended to include overflow predicates for bit vectors (see https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI). This commit introduces the predicates `bvumulo` and `bvsmulo` that return `true` if the unsigned multiplication overflows or the signed multiplication underflows or overflows, respectively.
aehyvari
force-pushed
the
antti/smtlib2-bv-of-predicates
branch
from
846b0e0
to
6f70788
Compare
|
@microsoft-github-policy-service agree company="Certora" |
|
I checked this branch against cvc5's overflow regression tests in https://github.com/cvc5/cvc5/tree/main/test/regress/cli/regress0/bv/overflow and everything passes. |
|
Is there any way for API users to access these functions yet? I think they have not been added to the C or C++ APIs yet, but is there a way for a project using API calls also interact with these newly-added functions too? |
|
there are already functions accessible over the API that serve this functionality. They have different names. They have been available for a very long time. They are not new. |
mmcloughlin
added a commit
to avanhatt/wasmtime
that referenced
this pull request
Nov 1, 2023
Adds the `bvsaddo` SMT-LIB operator. This operator is due to be standardized in SMT-LIB 2.7, and is already supported in Z3. https://groups.google.com/g/smt-lib/c/J4D99wT0aKI Z3Prover/z3#6715
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Smtlib2 is being extended to include overflow predicates for bit vectors (see https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI). This PR introduces the predicates
bvumulo,bvsmulo,bvsdivo,bvnego,bvuaddo,bvsaddo,bvusubo, andbvssubo.