-
Notifications
You must be signed in to change notification settings - Fork 1.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Implement proposed smtlib2 bitvector overflow predicates #6715
Merged
NikolajBjorner
merged 11 commits into
Z3Prover:master
from
aehyvari:antti/smtlib2-bv-of-predicates
May 9, 2023
Merged
Implement proposed smtlib2 bitvector overflow predicates #6715
NikolajBjorner
merged 11 commits into
Z3Prover:master
from
aehyvari:antti/smtlib2-bv-of-predicates
May 9, 2023
Commits on May 8, 2023
-
Logical names for function declarations in c++
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.
Configuration menu - View commit details
-
Copy full SHA for 00e3086 - Browse repository at this point
Copy the full SHA 00e3086View commit details
Commits on May 9, 2023
-
Implement smtlib overflow preds for multiplication
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.
Configuration menu - View commit details
-
Copy full SHA for e38aab3 - Browse repository at this point
Copy the full SHA e38aab3View commit details -
Configuration menu - View commit details
-
Copy full SHA for 8ef16e1 - Browse repository at this point
Copy the full SHA 8ef16e1View commit details -
Configuration menu - View commit details
-
Copy full SHA for a59ffef - Browse repository at this point
Copy the full SHA a59ffefView commit details -
Configuration menu - View commit details
-
Copy full SHA for 8ed97de - Browse repository at this point
Copy the full SHA 8ed97deView commit details -
Configuration menu - View commit details
-
Copy full SHA for e44d62e - Browse repository at this point
Copy the full SHA e44d62eView commit details -
Configuration menu - View commit details
-
Copy full SHA for b006441 - Browse repository at this point
Copy the full SHA b006441View commit details -
Configuration menu - View commit details
-
Copy full SHA for fc28aa6 - Browse repository at this point
Copy the full SHA fc28aa6View commit details -
Configuration menu - View commit details
-
Copy full SHA for 99b4322 - Browse repository at this point
Copy the full SHA 99b4322View commit details -
Configuration menu - View commit details
-
Copy full SHA for c305c5b - Browse repository at this point
Copy the full SHA c305c5bView commit details -
Configuration menu - View commit details
-
Copy full SHA for 6f70788 - Browse repository at this point
Copy the full SHA 6f70788View commit details
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.