Add basic support for the SMT-LIB BV and QF_BV logics #730
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
bclement-ocp
force-pushed
the
bclement/bv2
branch
2 times, most recently
from
cd4704d
to
17820c9
Compare
This is the first part in a reloaded version of OCamlPro#669. It only includes parsing and typechecking support for the bit-vector primitives: bvnot, bvand, bvor, bv2nat and nat2bv (called int2bv because it also accepts negative inputs) are treated as uninterpreted functions; the other operators defined in the SMT-LIB are defined in terms of these primitives and of the existing `concat` and `extract` operators. The support for the bit-vector functions will be improved in separate PRs focusing on the bv2nat/nat2bv interaction, so that we are at least able to solve simple arithmetic goals. In the future, we might want to consider additional strategies (e.g. bitblasting), but that is out of scope for now. Following the discussion in OCamlPro#669, including the apparent restrictions around the building of "ite" in the theory and the lack of infrastructure for actually doing simplifications there (at least for now), the definition of most functions are moved back to `Expr.ml`. The PR also includes a few helper functions to help write the definition of the bitvector operators more concisely, which should help ensuring that they are correct.
bclement-ocp
force-pushed
the
bclement/bv2
branch
from
17820c9
to
270d270
Compare
|
I had mixed up |
|
This is +3295 on QF_BV just by being able to parse some otherwise trivial benches. There are 54 errors, all of which are stack overflows while typing (similar to #669, iirc). |
hra687261
approved these changes
Jul 12, 2023
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.
This is the first part in a reloaded version of #669. It only includes parsing and typechecking support for the bit-vector primitives: bvnot, bvand, bvor, bv2nat and nat2bv (called int2bv because it also accepts negative inputs) are treated as uninterpreted functions; the other operators defined in the SMT-LIB are defined in terms of these primitives and of the existing
concatandextractoperators.The support for the bit-vector functions will be improved in separate PRs focusing on the bv2nat/nat2bv interaction, so that we are at least able to solve simple arithmetic goals. In the future, we might want to consider additional strategies (e.g. bitblasting), but that is out of scope for now.
Following the discussion in #669, including the apparent restrictions around the building of "ite" in the theory and the lack of infrastructure for actually doing simplifications there (at least for now), the definition of most functions are moved back to
Expr.ml. The PR also includes a few helper functions to help write the definition of the bitvector operators more concisely, which should help ensuring that they are correct.