Add VC Binder Simplification

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

@@ -0,0 +1,118 @@
+package liquidjava.rj_language.opt;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import liquidjava.processor.SimplifiedVCImplication;
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.LiteralBoolean;
+
+/**
+ * Simplifies VCImplication chains by removing vacuous binder implications
+ */
+public class VCBinderSimplification implements VCSimplificationPass {
+
+    /**
+     * Applies one binder simplification in a VC chain
+     */
+    @Override
+    public VCImplication apply(VCImplication implication) {
+        VCImplication cloned = implication.clone();
+        VCImplication simplified = simplify(cloned);
+        return simplified == null ? cloned : simplified;
+    }
+
+    /**
+     * Simplifies the first applicable binder in a VC chain
+     */
+    private VCImplication simplify(VCImplication implication) {
+        if (implication == null)
+            return null;
+
+        if (isFalseBinder(implication))
+            return collapseFalseBinder(implication);
+
+        if (isTrueBinder(implication) && !containsVar(implication.getNext(), implication.getName()))
+            return removeTrueBinder(implication);
+
+        VCImplication next = simplify(implication.getNext());
+        if (next == null)
+            return null;
+
+        VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
+        result.setNext(next);
+        return result;
+    }
+
+    /**
+     * Removes a true binder whose name is not used in the suffix
+     */
+    private VCImplication removeTrueBinder(VCImplication implication) {
+        VCImplication next = implication.getNext();
+
+        // ∀x. true => P -> P
+        if (next != null) {
+            VCImplication origin = new VCImplication(implication.getName(), implication.getType(),
+                    next.getOriginRefinement());
+            VCImplication result = new SimplifiedVCImplication(next, next.getRefinement().clone(), origin);
+            result.setNext(next.getNext() == null ? null : next.getNext().clone());
+            return result;
+        }
+
+        // ∀x. true -> true
+        Predicate truePredicate = new Predicate(new LiteralBoolean(true));
+        return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication);
+    }
+
+    /**
+     * Replaces a false binder implication with true
+     */
+    private VCImplication collapseFalseBinder(VCImplication implication) {
+        // ∀x. false => P -> true
+        Predicate truePredicate = new Predicate(new LiteralBoolean(true));
+        return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication);
+    }
+
+    /**
+     * Checks whether a VC node is a binder refined with true
+     */
+    private boolean isTrueBinder(VCImplication implication) {
+        return implication.hasBinder() && isTrue(implication.getRefinement().getExpression());
+    }
+
+    /**
+     * Checks whether a VC node is a binder refined with false
+     */
+    private boolean isFalseBinder(VCImplication implication) {
+        return implication.hasBinder() && isFalse(implication.getRefinement().getExpression());
+    }
+
+    /**
+     * Checks whether an expression is true
+     */
+    private boolean isTrue(Expression expression) {
+        return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
+    }
+
+    /**
+     * Checks whether an expression is false
+     */
+    private boolean isFalse(Expression expression) {
+        return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue();
+    }
+
+    /**
+     * Checks whether a VC suffix contains a variable name
+     */
+    private boolean containsVar(VCImplication implication, String name) {
+        for (VCImplication current = implication; current != null; current = current.getNext()) {
+            List<String> names = new ArrayList<>();
+            current.getRefinement().getExpression().getVariableNames(names);
+            if (names.contains(name))
+                return true;
+        }
+        return false;
+    }
+}

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

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

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

@@ -0,0 +1,69 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.utils.VCTestUtils.*;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+
+import liquidjava.processor.VCImplication;
+import org.junit.jupiter.api.Test;
+
+class VCBinderSimplificationTest {
+
+    private final VCBinderSimplification binderSimplification = new VCBinderSimplification();
+
+    @Test
+    void removesTrueBinderWhenVariableIsUnusedDownstream() {
+        VCImplication implication = vc("∀x:int. true", "y > 0");
+
+        assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("y > 0", "∀x:int. y > 0")));
+    }
+
+    @Test
+    void keepsTrueBinderWhenVariableIsUsedDownstream() {
+        VCImplication implication = vc("∀x:int. true", "x > 0");
+
+        assertSimplificationSteps(binderSimplification::apply, implication,
+                chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0")));
+    }
+
+    @Test
+    void collapsesFalseBinderSuffixToPlainTrue() {
+        VCImplication implication = vc("∀x:int. false", "x > 0", "y > 0");
+        VCImplication result = binderSimplification.apply(implication);
+
+        assertFalse(result.hasBinder());
+        assertSimplifiedVC(result, expect("true", "∀x:int. false"));
+    }
+
+    @Test
+    void simplifiesOnlyFirstApplicableBinder() {
+        VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0");
+
+        assertSimplificationSteps(binderSimplification::apply, implication,
+                chain(expect("true", "∀x:int. true"), expect("z > 0", "z > 0")));
+    }
+
+    @Test
+    void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() {
+        VCImplication implication = vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0");
+
+        assertSimplificationSteps(binderSimplification::apply, implication,
+                chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0"), expect("z > 0", "∀y:int. z > 0")));
+    }
+
+    @Test
+    void ignoresNonBinderBooleanLiterals() {
+        VCImplication implication = vc("true", "false");
+
+        assertSimplificationSteps(binderSimplification::apply, implication,
+                chain(expect("true", "true"), expect("false", "false")));
+    }
+
+    @Test
+    void trueBinderWithoutSuffixBecomesPlainTrue() {
+        VCImplication implication = vc("∀x:int. true");
+        VCImplication result = binderSimplification.apply(implication);
+
+        assertFalse(result.hasBinder());
+        assertSimplifiedVC(result, expect("true", "∀x:int. true"));
+    }
+}

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

@@ -21,7 +21,7 @@ public VCImplicationGenerator() {
 
     @Override
     public VCImplication generate(SourceOfRandomness random, GenerationStatus status) {
-        return switch (random.nextInt(0, 12)) {
+        return switch (random.nextInt(0, 14)) {
         case 0 -> vc(substitution(random, "x"), comparison(random, "x"));
         case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x"));
         case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y"));
@@ -34,6 +34,8 @@ public VCImplication generate(SourceOfRandomness random, GenerationStatus status
         case 9 -> vc(arithmeticIdentity(random));
         case 10 -> guardedArithmeticIdentity(random);
         case 11 -> vc(logicalIdentity(random));
+        case 12 -> vc(unusedTrueBinder(random));
+        case 13 -> vc(falseBinder(random));
         default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random));
         };
     }
@@ -60,6 +62,14 @@ private static String nonSubstitution(SourceOfRandomness random, String binder)
         return "∀" + binder + ":int. " + binder + " == " + binder + " " + signed(random.nextInt(1, 5));
     }
 
+    private static String[] unusedTrueBinder(SourceOfRandomness random) {
+        return new String[] { "∀x:int. true", comparison(random, "a") };
+    }
+
+    private static String[] falseBinder(SourceOfRandomness random) {
+        return new String[] { "∀x:int. false", comparison(random, "x") };
+    }
+
     private static String comparison(SourceOfRandomness random, String preferredVar) {
         String left = random.nextBoolean() ? preferredVar : arithmetic(random, preferredVar);
         String right = random.nextBoolean() ? intLiteral(random)

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

@@ -36,6 +36,31 @@ void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() {
                 chain(expect("true", "3 == 3")));
     }
 
+    @Test
+    void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() {
+        VCImplication implication = vc("∀x:int. x == 3", "∀y:int. true", "x > 0");
+
+        assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
+                chain(expect("true", "∀y:int. true"), expect("3 > 0", "∀x:int. x > 0")),
+                chain(expect("3 > 0", "∀y:int. x > 0")), chain(expect("true", "3 > 0")));
+    }
+
+    @Test
+    void simplifyOnceAppliesBinderSimplificationBeforeFolding() {
+        VCImplication implication = vc("∀x:int. true", "1 + 2 > 0");
+
+        assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
+                chain(expect("1 + 2 > 0", "∀x:int. 1 + 2 > 0")), chain(expect("3 > 0", "1 + 2 > 0")));
+    }
+
+    @Test
+    void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() {
+        VCImplication implication = vc("∀x:int. true", "y && true");
+
+        assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
+                chain(expect("y && true", "∀x:int. y && true")), chain(expect("y", "y && true")));
+    }
+
     @Test
     void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() {
         VCImplication implication = vc("1 + 2 > 2");
@@ -91,6 +116,13 @@ void simplifyKeepsApplyingStepsUntilFixedPoint() {
                 chain(expect("4 > 3", "3 + 1 > 3")), chain(expect("true", "4 > 3")));
     }
 
+    @Test
+    void simplifyToFixedPointRemovesTrueBindersOverMultipleSteps() {
+        VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0");
+
+        assertSimplifiedVC(VCSimplification.simplifyToFixedPoint(implication), expect("z > 0", "∀y:int. z > 0"));
+    }
+
     @Test
     void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() {
         VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");