Add VC Substitution Simplification#249
Conversation
CatarinaGamboa
left a comment
There was a problem hiding this comment.
Tests look good, some code organization changes
| } | ||
|
|
||
| public boolean hasBinder() { | ||
| return name != null && type != null; |
There was a problem hiding this comment.
so dont all have binders? i think every VCImplication had a name and type, the question might be if they appear inside the refinement, but i didnt think this would be a possibility
There was a problem hiding this comment.
Not all of them. We have this constructor VCImplication(Predicate ref) which does not set the name and type. For example in ∀x:int. x == 1 => x > 0 the first vc has a binder but the second doesnt.
|
|
||
| class VCSimplificationUtils { | ||
|
|
||
| public static Expression activeExpression(Predicate refinement) { |
There was a problem hiding this comment.
whats an activeExpression? maybe we can add a method to Predicate to get the expression clone instead of this utils
There was a problem hiding this comment.
The active expression is the current expression we are simplifying. Yes we can remove this method and simply clone the current expression.
| return refinement.getExpression().clone(); | ||
| } | ||
|
|
||
| public static Predicate originPredicate(Predicate refinement) { |
| return new VCImplication(refinement); | ||
| } | ||
|
|
||
| public static boolean sameVc(VCImplication left, VCImplication right) { |
There was a problem hiding this comment.
Equals in VCImplication?
There was a problem hiding this comment.
Yep, that's better. I'll add it.
| return refinement.clone(); | ||
| } | ||
|
|
||
| public static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) { |
There was a problem hiding this comment.
this could actually be a new constructor of VCImplication right?
| return substitute(implication.getNext(), source, value); | ||
|
|
||
| Predicate refinement = substituteRefinement(implication.getRefinement(), source, value); | ||
| VCImplication result = VCSimplificationUtils.copyWithRefinement(implication, refinement); |
There was a problem hiding this comment.
shouldnt we also set the origin here?
There was a problem hiding this comment.
The origin is already set in substituteRefinement.
| /** | ||
| * Checks whether an expression is a variable with a given name | ||
| */ | ||
| public static boolean isVar(Expression expression, String name) { |
There was a problem hiding this comment.
Yeah simply because we need it in the tests and I didn't want to repeat the same code.
| /** | ||
| * Checks whether an expression contains a variable name | ||
| */ | ||
| public static boolean containsVariable(Expression expression, String name) { |
| static final String[] BINDERS = { "x", "y", "z" }; | ||
| static final String[] FREE_VARS = { "a", "b", "c" }; | ||
| private static final String[] COMPARISON_OPS = { "==", "!=", ">=", ">", "<=", "<" }; | ||
|
|
There was a problem hiding this comment.
then you'll add other operations when you implement those substitutions?
like &&, ite, etc?
5d37099 to
92f3d12
Compare
Description
This PR adds VC simplification for binder equalities through
VCImplicationchains. When a binder refinement establishes a known value (constant or not), the simplifier rewrites later refinements with that value and removes the substitution source from the VC chain preserving its origin and substituted binders.It also adds focused unit tests and property-based tests using JUnit Quickcheck to randomly generate VCs and assert if the simplified VC is equivalent to the original.
Example
Related Issue
None.
Type of change
Checklist
mvn testpasses locally