Add VC Constraint Simplification

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

@@ -0,0 +1,80 @@
+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.smt.SMTEvaluator;
+import liquidjava.smt.SMTResult;
+
+/**
+ * Removes antecedent constraints that are implied by another antecedent
+ */
+public class VCConstraintSimplification implements VCSimplificationPass {
+
+    /**
+     * Applies one constraint simplification in a VC chain
+     */
+    @Override
+    public VCImplication apply(VCImplication implication) {
+        VCImplication cloned = implication.clone();
+        VCImplication simplified = simplify(cloned);
+        return simplified == null ? cloned : simplified;
+    }
+
+    /**
+     * Removes the first antecedent implied by another antecedent
+     */
+    private VCImplication simplify(VCImplication implication) {
+        for (VCImplication redundant = implication; redundant.getNext() != null; redundant = redundant.getNext()) {
+            if (isTrue(redundant.getRefinement().getExpression()) || !isRemovable(implication, redundant))
+                continue;
+
+            for (VCImplication stronger = implication; stronger.getNext() != null; stronger = stronger.getNext()) {
+                if (stronger != redundant && implies(stronger.getRefinement(), redundant.getRefinement()))
+                    return remove(implication, redundant);
+            }
+        }
+        return null;
+    }
+
+    /**
+     * Checks whether removing a node also removes every use of its binder
+     */
+    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;
+    }
+
+    /**
+     * Clones a chain while removing one node
+     */
+    private VCImplication remove(VCImplication implication, VCImplication removed) {
+        if (implication == removed)
+            return implication.getNext().clone();
+
+        VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
+        result.setNext(remove(implication.getNext(), removed));
+        return result;
+    }
+
+    /**
+     * Checks logical implication using the verifier's existing SMT context
+     */
+    private boolean implies(Predicate stronger, Predicate weaker) {
+        try {
+            SMTResult result = new SMTEvaluator().verifySubtype(stronger, weaker, Context.getInstance(), true);
+            return result.isOk();
+        } catch (Exception e) {
+            return false;
+        }
+    }
+}

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

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

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

@@ -0,0 +1,80 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.utils.VCTestUtils.assertSimplificationSteps;
+import static liquidjava.utils.VCTestUtils.step;
+import static liquidjava.utils.VCTestUtils.vc;
+
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import liquidjava.processor.context.Context;
+import liquidjava.utils.TestUtils;
+
+class VCConstraintSimplificationTest {
+
+    private final VCConstraintSimplification simplification = new VCConstraintSimplification();
+
+    @BeforeEach
+    void setUpContext() {
+        Context.getInstance().reinitializeAllContext();
+        TestUtils.addIntVariableToContext("x");
+        TestUtils.addIntVariableToContext("y");
+    }
+
+    @AfterEach
+    void resetContext() {
+        Context.getInstance().reinitializeAllContext();
+    }
+
+    @Test
+    void keepsRedundantConstraintWhenItsBinderIsRequired() {
+        assertSimplificationSteps(simplification,
+                vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"),
+                step("x > 0", "x > 1", "y == x + 1", "y < 0"));
+    }
+
+    @Test
+    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
+    void ignoresUnrelatedLaterAntecedent() {
+        assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "y > 1", "x + y > 0"),
+                step("x > 0", "y > 1", "x + y > 0"));
+    }
+
+    @Test
+    void doesNotUseConclusionToSimplifyConstraint() {
+        assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "x > 1"), step("x > 0", "x > 1"));
+    }
+
+    @Test
+    void simplifiesOnlyFirstImpliedConstraint() {
+        assertSimplificationSteps(simplification,
+                vc("∀x:int. x > 2", "∀#fresh_1:boolean. x > 1", "∀#fresh_2:boolean. x > 0", "y > 0"),
+                step("x > 2", "x > 0", "y > 0"), step("x > 2", "y > 0"));
+    }
+}

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

@@ -3,10 +3,19 @@
 import static liquidjava.utils.VCTestUtils.*;
 import static org.junit.jupiter.api.Assertions.assertNull;
 
+import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.Test;
 
+import liquidjava.processor.context.Context;
+import liquidjava.utils.TestUtils;
+
 class VCSimplificationTest {
 
+    @AfterEach
+    void resetContext() {
+        Context.getInstance().reinitializeAllContext();
+    }
+
     @Test
     void simplifyReturnsNullForNullImplication() {
         assertNull(VCSimplification.simplifyToFixedPoint(null));
@@ -163,4 +172,12 @@ void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() {
     void simplifyLeavesUnchangedVcAsPlainPredicates() {
         assertSimplificationSteps(vc("x > 0", "y > x"), step("x > 0", "y > x"));
     }
+
+    @Test
+    void simplifyEliminatesRemovableConstraintImpliedByEarlierAntecedent() {
+        TestUtils.addIntVariableToContext("x");
+        TestUtils.addIntVariableToContext("y");
+        assertSimplificationSteps(vc("∀x:int. x > 1", "∀cond:boolean. x > 0", "∀y:int. y == x + 1", "y < 0"),
+                step("x > 1", "x > 0", "x + 1 < 0"), step("x > 1", "x + 1 < 0"));
+    }
 }