Update Constraint Simplification

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java

@@ -1,17 +1,17 @@
 package liquidjava.rj_language.opt;
 
+import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
 
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.ast.LiteralBoolean;
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
 
 /**
- * Simplifies antecedent constraints that are implied by stronger constraints later in the VC chain
+ * Removes antecedent constraints that are implied by another antecedent
  */
 public class VCConstraintSimplification implements VCSimplificationPass {
 
@@ -26,51 +26,73 @@ public VCImplication apply(VCImplication implication) {
     }
 
     /**
-     * Simplifies the first antecedent implied by a later antecedent
+     * Removes the first antecedent implied by another antecedent
      */
     private VCImplication simplify(VCImplication implication) {
-        if (implication == null || implication.getNext() == null)
-            return null;
+        for (VCImplication redundant = implication; redundant.getNext() != null; redundant = redundant.getNext()) {
+            if (isTrue(redundant.getRefinement().getExpression()))
+                continue;
 
-        if (!isTrue(implication.getRefinement().getExpression())) { // skip trivial constraints
-            VCImplication implying = findImplyingAntecedent(implication);
-            if (implying != null)
-                return simplifyConstraint(implication);
+            for (VCImplication stronger = implication; stronger.getNext() != null; stronger = stronger.getNext()) {
+                if (stronger != redundant && canEliminate(implication, stronger, redundant)
+                        && implies(stronger.getRefinement(), redundant.getRefinement()))
+                    return eliminate(implication, stronger, redundant);
+            }
         }
+        return null;
+    }
 
-        // continue searching for simplifications in the suffix
-        VCImplication next = simplify(implication.getNext());
-        if (next == null)
-            return null;
+    /**
+     * Checks whether either node can be removed while preserving required binders
+     */
+    private boolean canEliminate(VCImplication implication, VCImplication stronger, VCImplication redundant) {
+        return isRemovable(implication, redundant) || isRelocatable(implication, stronger);
+    }
 
-        VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
-        result.setNext(next);
-        return result;
+    /**
+     * Removes the redundant node, or moves the stronger refinement onto its required binder and removes the stronger
+     * node
+     */
+    private VCImplication eliminate(VCImplication implication, VCImplication stronger, VCImplication redundant) {
+        if (isRemovable(implication, redundant))
+            return rewrite(implication, redundant, null, null);
+        return rewrite(implication, stronger, redundant, stronger.getRefinement());
     }
 
     /**
-     * Finds a later antecedent that implies the current constraint. The final node is the conclusion and is not a
-     * candidate
+     * Checks whether removing a node also removes every use of its binder
      */
-    private VCImplication findImplyingAntecedent(VCImplication implication) {
-        for (VCImplication candidate = implication.getNext(); candidate != null
-                && candidate.getNext() != null; candidate = candidate.getNext()) {
-            // ∀x. x > 0 => x > 1 -> ∀x. true => x > 1
-            if (implies(candidate.getRefinement(), implication.getRefinement()))
-                return candidate;
-        }
-        return null;
+    private boolean isRemovable(VCImplication implication, VCImplication node) {
+        if (!node.hasBinder())
+            return true;
+
+        for (VCImplication current = implication; current != null; current = current.getNext())
+            if (current != node && containsVar(current.getRefinement().getExpression(), node.getName()))
+                return false;
+        return true;
     }
 
     /**
-     * Simplifies a redundant constraint to true
+     * Checks whether a node can be removed while retaining its refinement elsewhere
      */
-    private VCImplication simplifyConstraint(VCImplication implication) {
-        if (!implication.hasBinder())
-            return implication.getNext().clone();
+    private boolean isRelocatable(VCImplication implication, VCImplication node) {
+        return isRemovable(implication, node)
+                && (!node.hasBinder() || !containsVar(node.getRefinement().getExpression(), node.getName()));
+    }
+
+    /**
+     * Clones a chain while removing one node and optionally replacing another node's refinement
+     */
+    private VCImplication rewrite(VCImplication implication, VCImplication removed, VCImplication replaced,
+            Predicate replacement) {
+        if (implication == null)
+            return null;
+        if (implication == removed)
+            return rewrite(implication.getNext(), removed, replaced, replacement);
 
-        VCImplication result = copyWithRefinement(implication, new Predicate(new LiteralBoolean(true)));
-        result.setNext(implication.getNext().clone());
+        Predicate refinement = implication == replaced ? replacement.clone() : implication.getRefinement().clone();
+        VCImplication result = copyWithRefinement(implication, refinement);
+        result.setNext(rewrite(implication.getNext(), removed, replaced, replacement));
         return result;
     }
 

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java

@@ -31,29 +31,49 @@ void resetContext() {
     }
 
     @Test
-    void simplifiesConstraintImpliedByLaterAntecedent() {
+    void keepsRequiredBinderAndRemovesLaterStrongerBinder() {
         assertSimplificationSteps(simplification,
                 vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"),
-                step("true", "x > 1", "y == x + 1", "y < 0"));
+                step("x > 1", "y == x + 1", "y < 0"));
     }
 
     @Test
-    void preservesBothBindersWhenSimplifyingConstraint() {
+    void preservesRequiredBinderWhenRemovingStrongerBinder() {
         VCImplication simplified = simplification
                 .apply(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"));
 
         assertTrue(simplified.hasBinder());
         assertEquals("x", simplified.getName());
         assertEquals("int", simplified.getType().getQualifiedName());
         assertTrue(simplified.getNext().hasBinder());
-        assertEquals("cond", simplified.getNext().getName());
-        assertEquals("boolean", simplified.getNext().getType().getQualifiedName());
+        assertEquals("y", simplified.getNext().getName());
+        assertEquals("int", simplified.getNext().getType().getQualifiedName());
     }
 
     @Test
-    void keepsConstraintThatIsNotImpliedByLaterAntecedent() {
-        assertSimplificationSteps(simplification, vc("∀x:int. x > 1", "x > 0", "y > 0"),
-                step("x > 1", "x > 0", "y > 0"));
+    void removesConstraintImpliedByEarlierAntecedent() {
+        assertSimplificationSteps(simplification, vc("∀x:int. x > 1", "∀cond:boolean. x > 0", "∀y:int. y == x + 1"),
+                step("x > 1", "y == x + 1"));
+    }
+
+    @Test
+    void removesCoverageConstraintsImpliedByStrongerLaterConstraints() {
+        assertSimplificationSteps(simplification,
+                vc("∀x:int. x >= 0", "∀#fresh_40:boolean. !(y < 40)", "∀#fresh_60:boolean. !(y < 60)",
+                        "∀#fresh_80:boolean. !(y < 80)", "x + y > 0"),
+                step("x >= 0", "!(y < 60)", "!(y < 80)", "x + y > 0"), step("x >= 0", "!(y < 80)", "x + y > 0"));
+    }
+
+    @Test
+    void keepsConstraintsWhenBothBindersAreRequired() {
+        assertSimplificationSteps(simplification, vc("∀x:int. y >= 0", "∀y:int. y > 0", "x + y > 0"),
+                step("y >= 0", "y > 0", "x + y > 0"));
+    }
+
+    @Test
+    void keepsConstraintsThatDoNotImplyEachOther() {
+        assertSimplificationSteps(simplification, vc("∀x:int. x > 1", "y > 0", "x + y > 0"),
+                step("x > 1", "y > 0", "x + y > 0"));
     }
 
     @Test
@@ -70,6 +90,6 @@ void doesNotUseConclusionToSimplifyConstraint() {
     @Test
     void simplifiesOnlyFirstImpliedConstraint() {
         assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "x > 1", "x > 2", "y > 0"),
-                step("true", "x > 1", "x > 2", "y > 0"), step("true", "x > 2", "y > 0"));
+                step("x > 1", "x > 2", "y > 0"), step("x > 2", "y > 0"));
     }
 }

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java

@@ -174,10 +174,10 @@ void simplifyLeavesUnchangedVcAsPlainPredicates() {
     }
 
     @Test
-    void simplifyNeutralizesConstraintImpliedByLaterAntecedent() {
+    void simplifyEliminatesConstraintImpliedByLaterAntecedent() {
         TestUtils.addIntVariableToContext("x");
         TestUtils.addIntVariableToContext("y");
         assertSimplificationSteps(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"),
-                step("x > 0", "x > 1", "x + 1 < 0"), step("true", "x > 1", "x + 1 < 0"));
+                step("x > 0", "x > 1", "x + 1 < 0"), step("x > 1", "x + 1 < 0"));
     }
 }