java-backend: support SMTLIB translation for KVar binders #1237
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
daejunpark
force-pushed
the
smtlib-forall
branch
from
09f2009
to
edb4b23
Compare
| @@ -656,6 +676,13 @@ public SMTLibTerm transform(BitVector bitVector) { | |||
|
|
|||
| @Override | |||
| public SMTLibTerm transform(UninterpretedToken uninterpretedToken) { | |||
| if (uninterpretedToken.sort() == Sort.KVARIABLE) { | |||
| if (binders.search(uninterpretedToken) != -1) { | |||
There was a problem hiding this comment.
contains() must be used here
| @@ -571,10 +587,14 @@ public SMTLibTerm transform(KItem kItem) { | |||
| if (label.startsWith("(")) { | |||
| // smtlib expression instead of operator | |||
| String expression = label; | |||
| boolean hasBinder = recordBinders(label, kList); | |||
There was a problem hiding this comment.
This whole feature is extraordinary error-prone. I'd say a warning must be added here when it is used.
There was a problem hiding this comment.
This is no longer applicable.
| @@ -243,6 +246,7 @@ public static CharSequence translateImplication( | |||
| private final LinkedHashSet<Variable> variables; | |||
| private final LinkedHashMap<Term, Variable> termAbstractionMap; | |||
| private final LinkedHashMap<UninterpretedToken, Integer> tokenEncoding; | |||
| private final Stack<Term> binders; | |||
There was a problem hiding this comment.
This variable must be renamed. Like smtlibForallOrExistsBinder ? Long names are better than confusing names.
There was a problem hiding this comment.
Now this PR becomes more general, and the name binders is appropriate.
daejunpark
changed the title
daejunpark
changed the title
|
Now this PR becomes more general, supporting SMTLIB translation for arbitrary KVar binders. Please re-review. |
denis-bogdanas
approved these changes
Apr 27, 2020
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.
Support the format[smtlib((forall|exists ((#1 <sort>)) <term>))]. See the test for an example.Support SMTLIB translation for binders of sort
KVar.