HolSmt: add some support for tuples and for the reals' min, max and abs #1187
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
Hopefully this is a temporary stop-gap measure until a more general mechanism is implemented to identify an appropriate definition that can be sent to the SMT solvers, rather than special-casing each and every definition. That said, this is still useful, especially so that we can enable some of the already-existing self-tests for the SMT-LIB translation as well, to detect future regressions whenever improvements are made. The enabled self-tests all include Z3 with proof reconstruction now.
Again, this is a temporary stop-gap measure until we can translate function definitions to SMT-LIB format, so that SMT solvers can reason about them. As it is, due to the above limitation this won't be able to solve some goals (witness the two disabled tests) but it does allow solving the simpler ones. Of the tests that were enabled, all work with Z3 proof reconstruction.
|
Fantastic; thanks! |
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 just a couple of minor improvements to allow some more HolSmt self-tests to be enabled and ensure that we don't regress on future improvements. In total, 21 more tests were enabled for cvc5 and Z3, including Z3 with proof reconstruction (although no proof reconstruction improvements were made).
It basically rewrites goals containing some terms not available in SMT-LIB into something SMT provers can understand, by simplifying using existing theorems. However, I think that in the future, a better solution would be for HolSmt to try to find the most appropriate theorems (based on the terms it finds in the assumptions and goal) and translate those theorems to SMT-LIB, so that SMT solvers can reason about them. This would allow solving more goals.
This will be especially important for function definitions, which currently are simply converted into uninterpreted symbols (thus functions are completely opaque to SMT solvers, leading to the impossibility of solving most goals containing them).
I think this concludes my low-hanging fruit improvements for HolSmt, for now. I think there's more that could be done (e.g. fix integer div and mod) but I think that could be done better if/when the work mentioned above is done first.
For now I'd like to focus on trying to add support for proof reconstruction for the most recent version of Z3, which I expect to be a hard and lengthy endeavor, so I don't expect to send PRs any time soon...
Thanks!