Add More Tests

Author: rcosta358

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

@@ -33,6 +33,12 @@ void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() {
                 step("true"));
     }
 
+    @Test
+    void simplifyCombinesSubstitutionWithArithmeticAndLogicalSimplification() {
+        assertSimplificationSteps(vc("∀x:int. x == y + 0", "x > 0 && true"), step("y + 0 > 0 && true"),
+                step("y > 0 && true"), step("y > 0"));
+    }
+
     @Test
     void simplifyOnceAppliesBinderSimplificationBeforeFolding() {
         assertSimplificationSteps(vc("∀x:int. true", "1 + 2 > 0"), step("1 + 2 > 0"), step("3 > 0"));
@@ -43,14 +49,25 @@ void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() {
         assertSimplificationSteps(vc("∀x:int. true", "y && true"), step("y && true"), step("y"));
     }
 
+    @Test
+    void simplifyOnceAppliesBinderSimplificationBeforeArithmeticSimplification() {
+        assertSimplificationSteps(vc("∀x:int. true", "y + 0 > 0"), step("y + 0 > 0"), step("y > 0"));
+    }
+
     @Test
     void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() {
         assertSimplificationSteps(vc("1 + 2 > 2"), step("3 > 2"), step("true"));
     }
 
     @Test
     void simplifyOnceAppliesFoldingBeforeArithmeticSimplification() {
-        assertSimplificationSteps(vc("1 + 2 + x + 0 > 0"), step("3 + x + 0 > 0"));
+        assertSimplificationSteps(vc("1 + 2 + x + 0 > 0"), step("3 + x + 0 > 0"), step("3 + x > 0"));
+    }
+
+    @Test
+    void simplifyCombinesFoldingArithmeticAndLogicalSimplification() {
+        assertSimplificationSteps(vc("1 + 2 + x + 0 == 3 + x"), step("3 + x + 0 == 3 + x"), step("3 + x == 3 + x"),
+                step("true"));
     }
 
     @Test
@@ -63,11 +80,45 @@ void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() {
         assertSimplificationSteps(vc("x + 0 == x"), step("x == x"), step("true"));
     }
 
+    @Test
+    void simplifyOnceAppliesArithmeticBeforeFoldingOnNextStep() {
+        assertSimplificationSteps(vc("x - x == 0"), step("0 == 0"), step("true"));
+    }
+
     @Test
     void simplifyOnceAppliesLogicalWhenNoEarlierSimplificationIsAvailable() {
         assertSimplificationSteps(vc("x && true"), step("x"));
     }
 
+    @Test
+    void simplifyUsesFoldingToEnableSubstitutionOnNextStep() {
+        assertSimplificationSteps(vc("∀x:int. (x) == 3", "x > 0"), step("x == 3", "x > 0"), step("3 > 0"),
+                step("true"));
+    }
+
+    @Test
+    void simplifyUsesArithmeticToEnableSubstitutionOnNextStep() {
+        assertSimplificationSteps(vc("∀x:int. x + 0 == 3", "x > 0"), step("x == 3", "x > 0"), step("3 > 0"),
+                step("true"));
+    }
+
+    @Test
+    void simplifyUsesLogicalSimplificationToEnableSubstitutionOnNextStep() {
+        assertSimplificationSteps(vc("∀x:int. true && x == 3", "x > 0"), step("x == 3", "x > 0"), step("3 > 0"),
+                step("true"));
+    }
+
+    @Test
+    void simplifyUsesFoldingToEnableBinderSimplificationOnNextStep() {
+        assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("false", "y > 0"), step("true"));
+    }
+
+    @Test
+    void simplifyUsesArithmeticAndLogicalSimplificationToEnableBinderRemoval() {
+        assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("x == x", "y > 0"), step("true", "y > 0"),
+                step("y > 0"));
+    }
+
     @Test
     void simplifyAppliesLogicalStepsUntilFixedPoint() {
         assertSimplificationSteps(vc("x && true && true"), step("x && true"), step("x"));

liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java

@@ -68,6 +68,7 @@ private static void assertSimplificationResult(VCSimplificationResult previous,
     private static void assertSimplifiedVC(VCImplication implication, String... expected) {
         VCImplication current = implication;
         for (int i = 0; i < expected.length; i++) {
+            assertNotNull(current, "Expected implication " + i + " with refinement " + expected[i]);
             assertEquals(Predicate.class, current.getRefinement().getClass(),
                     "Expected simplified refinement at implication " + i + " to be a plain Predicate");
             assertEquals(expected[i], formatRefinement(current),