Add a new experimental term_theories operation
#1366
Merged
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
robdockins
force-pushed
the
smt-theories
branch
2 times, most recently
from
4c10fa9 to
dfb31bf
Compare
|
This PR addresses #1340. It is not yet completely accurate because of GaloisInc/what4#139. This means that terms requiring uninterpreted functions will be reported as not requiring any SMT theories. We will need to fix and update the What4 submodule to close this gap. |
|
I think it makes sense to merge this before we fix GaloisInc/what4#139 and update afterewards. |
brianhuffman
approved these changes
Jul 14, 2021
robdockins
added
the
PR: ready to merge
Evaluates a term into a proof obligation via What4 and examines what logical theories would be required to attempt a proof of the property. The names of the required theories are computed and returned to the user.
|
Failed SIKE test is some kind of caching error. I'm going to merge anyway since the 8.10.3 version passed. |
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.
Evaluates a term into a proof obligation via What4 and examines
what logical theories would be required to attempt a proof
of the property. The names of the required theories are computed
and returned to the user.