Support SMT-LIB v2.7 bit-vector operators in psmt2 #249
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
The new bit-vector operators from v2.7 are not available in SMT-LIB 2.6 scripts, which makes sense since Dolmen is intended to be able to check adherence to the specification. On the other hand, there is no standard specification for the psmt2 format, and while it implements polymorphism differently from SMT-LIB 2.7, there is no reason for psmt2 operators to be restricted to those available in version 2.6 of the standard. Allow the new bit-vector operators from version 2.7 of the standard when parsing files with psmt2 syntax.
|
That's very reasonable indeed, I'll do that before the upcoming release. cc @bobot who might also be interested |
Gbury
approved these changes
Sep 9, 2025
|
By the way, I'm wondering if having this distinction (SMT-LIB 2.6 vs SMT-LIB 2.7) for the supported operators is actually useful. The bit-vector operators are not (as far as I can tell) mentioned in the actual standard, and only the version 2.7 with the extra operators seem to be available on the smt-lib.org website, e.g. https://smt-lib.org/theories-FixedSizeBitVectors.shtml |
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 new bit-vector operators from v2.7 are not available in SMT-LIB 2.6 scripts, which makes sense since Dolmen is intended to be able to check adherence to the specification.
On the other hand, there is no standard specification for the psmt2 format, and while it implements polymorphism differently from SMT-LIB 2.7, there is no reason for psmt2 operators to be restricted to those available in version 2.6 of the standard.
Allow the new bit-vector operators from version 2.7 of the standard when parsing files with psmt2 syntax.