Remove Unused Binders In Simplification

Author: rcosta358

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

@@ -34,8 +34,8 @@ private VCImplication simplify(VCImplication implication) {
         if (isFalseBinder(implication))
             return collapseFalseBinder(implication);
 
-        if (isTrueBinder(implication) && !containsVar(implication.getNext(), implication.getName()))
-            return removeTrueBinder(implication);
+        if (isRemovableUnusedBinder(implication))
+            return removeBinder(implication);
 
         VCImplication next = simplify(implication.getNext());
         if (next == null)
@@ -47,12 +47,12 @@ private VCImplication simplify(VCImplication implication) {
     }
 
     /**
-     * Removes a true binder whose name is not used in the suffix
+     * Removes a binder whose name is not used in the suffix
      */
-    private VCImplication removeTrueBinder(VCImplication implication) {
+    private VCImplication removeBinder(VCImplication implication) {
         VCImplication next = implication.getNext();
 
-        // ∀x. true => P -> P
+        // ∀x. R => P -> P when x is not used in P
         if (next != null)
             return next.clone();
 
@@ -61,6 +61,16 @@ private VCImplication removeTrueBinder(VCImplication implication) {
         return new VCImplication(truePredicate);
     }
 
+    /**
+     * Checks whether a binder is unused and can be removed
+     */
+    private boolean isRemovableUnusedBinder(VCImplication implication) {
+        if (!implication.hasBinder() || containsVar(implication.getNext(), implication.getName()))
+            return false;
+
+        return implication.hasNext() || isTrueBinder(implication);
+    }
+
     /**
      * Replaces a false binder implication with true
      */

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

@@ -1,7 +1,5 @@
 package liquidjava.rj_language.opt;
 
-import java.util.Objects;
-
 import liquidjava.processor.VCImplication;
 
 /**

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

@@ -12,6 +12,16 @@ void removesTrueBinderWhenVariableIsUnusedDownstream() {
         assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "y > 0"), step("y > 0"));
     }
 
+    @Test
+    void removesNonTrueBinderWhenVariableIsUnusedDownstream() {
+        assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "y > 0"), step("y > 0"));
+    }
+
+    @Test
+    void keepsNonTrueTerminalBinderAsConclusion() {
+        assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0"), step("x > 0"));
+    }
+
     @Test
     void keepsTrueBinderWhenVariableIsUsedDownstream() {
         assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0"), step("true", "x > 0"));

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

@@ -108,14 +108,13 @@ void simplifyUsesLogicalSimplificationToEnableSubstitutionOnNextStep() {
     }
 
     @Test
-    void simplifyUsesFoldingToEnableBinderSimplificationOnNextStep() {
-        assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("false", "y > 0"), step("true"));
+    void simplifyRemovesUnusedBinderBeforeFolding() {
+        assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("y > 0"));
     }
 
     @Test
-    void simplifyUsesArithmeticAndLogicalSimplificationToEnableBinderRemoval() {
-        assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("x == x", "y > 0"), step("true", "y > 0"),
-                step("y > 0"));
+    void simplifyRemovesUnusedBinderBeforeArithmeticAndLogicalSimplification() {
+        assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("y > 0"));
     }
 
     @Test