Simplify Redundant Constraints to true

Author: rcosta358

…anguage/opt/VCConstraintElimination.java …uage/opt/VCConstraintSimplification.javaliquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java renamed to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java renamed to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java

@@ -1,20 +1,22 @@
 package liquidjava.rj_language.opt;
 
 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;
 
 /**
- * Removes antecedent constraints that are implied by stronger constraints later in the VC chain
+ * Simplifies antecedent constraints that are implied by stronger constraints later in the VC chain
  */
-public class VCConstraintElimination implements VCSimplificationPass {
+public class VCConstraintSimplification implements VCSimplificationPass {
 
     /**
-     * Applies one constraint elimination in a VC chain
+     * Applies one constraint simplification in a VC chain
      */
     @Override
     public VCImplication apply(VCImplication implication) {
@@ -24,16 +26,19 @@ public VCImplication apply(VCImplication implication) {
     }
 
     /**
-     * Removes the first antecedent implied by a later antecedent
+     * Simplifies the first antecedent implied by a later antecedent
      */
     private VCImplication simplify(VCImplication implication) {
         if (implication == null || implication.getNext() == null)
             return null;
 
-        VCImplication implying = findImplyingAntecedent(implication);
-        if (implying != null)
-            return eliminate(implication, implying);
+        if (!isTrue(implication.getRefinement().getExpression())) { // skip trivial constraints
+            VCImplication implying = findImplyingAntecedent(implication);
+            if (implying != null)
+                return simplifyConstraint(implication);
+        }
 
+        // continue searching for simplifications in the suffix
         VCImplication next = simplify(implication.getNext());
         if (next == null)
             return null;
@@ -50,33 +55,22 @@ private VCImplication simplify(VCImplication implication) {
     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;
     }
 
     /**
-     * Eliminates one redundant constraint while preserving any binder attached to it
+     * Simplifies a redundant constraint to true
      */
-    private VCImplication eliminate(VCImplication implication, VCImplication implying) {
+    private VCImplication simplifyConstraint(VCImplication implication) {
         if (!implication.hasBinder())
             return implication.getNext().clone();
 
-        VCImplication result = copyWithRefinement(implication, implying.getRefinement().clone());
-        result.setNext(remove(implication.getNext(), implying));
-        return result;
-    }
-
-    /**
-     * Removes one node from a suffix
-     */
-    private VCImplication remove(VCImplication implication, VCImplication target) {
-        if (implication == target)
-            return implication.getNext() == null ? null : implication.getNext().clone();
-
-        VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
-        result.setNext(remove(implication.getNext(), target));
+        VCImplication result = copyWithRefinement(implication, new Predicate(new LiteralBoolean(true)));
+        result.setNext(implication.getNext().clone());
         return result;
     }
 

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

@@ -11,7 +11,7 @@ public class VCSimplification {
 
     private static final List<VCSimplificationPass> PASSES = List.of(new VCSubstitution(), new VCBinderSimplification(),
             new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification(),
-            new VCConstraintElimination());
+            new VCConstraintSimplification());
 
     /**
      * Applies all available simplification steps to a VC chain until a fixed point is reached

…age/opt/VCConstraintEliminationTest.java …/opt/VCConstraintSimplificationTest.javaliquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java renamed to liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java renamed to liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java

@@ -14,9 +14,9 @@
 import liquidjava.processor.context.Context;
 import liquidjava.utils.TestUtils;
 
-class VCConstraintEliminationTest {
+class VCConstraintSimplificationTest {
 
-    private final VCConstraintElimination constraintElimination = new VCConstraintElimination();
+    private final VCConstraintSimplification simplification = new VCConstraintSimplification();
 
     @BeforeEach
     void setUpContext() {
@@ -31,42 +31,45 @@ void resetContext() {
     }
 
     @Test
-    void removesConstraintImpliedByLaterAntecedent() {
-        assertSimplificationSteps(constraintElimination,
+    void simplifiesConstraintImpliedByLaterAntecedent() {
+        assertSimplificationSteps(simplification,
                 vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"),
-                step("x > 1", "y == x + 1", "y < 0"));
+                step("true", "x > 1", "y == x + 1", "y < 0"));
     }
 
     @Test
-    void preservesBinderOnStrongerConstraint() {
-        VCImplication simplified = constraintElimination
+    void preservesBothBindersWhenSimplifyingConstraint() {
+        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());
     }
 
     @Test
     void keepsConstraintThatIsNotImpliedByLaterAntecedent() {
-        assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 1", "x > 0", "y > 0"),
+        assertSimplificationSteps(simplification, vc("∀x:int. x > 1", "x > 0", "y > 0"),
                 step("x > 1", "x > 0", "y > 0"));
     }
 
     @Test
     void ignoresUnrelatedLaterAntecedent() {
-        assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "y > 1", "x + y > 0"),
+        assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "y > 1", "x + y > 0"),
                 step("x > 0", "y > 1", "x + y > 0"));
     }
 
     @Test
-    void doesNotUseConclusionToEliminateConstraint() {
-        assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "x > 1"), step("x > 0", "x > 1"));
+    void doesNotUseConclusionToSimplifyConstraint() {
+        assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "x > 1"), step("x > 0", "x > 1"));
     }
 
     @Test
-    void removesOnlyFirstImpliedConstraint() {
-        assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "x > 1", "x > 2", "y > 0"),
-                step("x > 1", "x > 2", "y > 0"), step("x > 2", "y > 0"));
+    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"));
     }
 }

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

@@ -174,10 +174,10 @@ void simplifyLeavesUnchangedVcAsPlainPredicates() {
     }
 
     @Test
-    void simplifyEliminatesConstraintImpliedByLaterAntecedent() {
+    void simplifyNeutralizesConstraintImpliedByLaterAntecedent() {
         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("x > 1", "x + 1 < 0"));
+                step("x > 0", "x > 1", "x + 1 < 0"), step("true", "x > 1", "x + 1 < 0"));
     }
 }