Add Tests

Author: rcosta358

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

@@ -43,13 +43,35 @@ void leavesDivisionAndModuloByZeroUnchanged() {
         assertUnchanged("4 % 0 == 0");
     }
 
+    @Test
+    void leavesRealDivisionAndModuloByZeroUnchanged() {
+        assertUnchanged("4.0 / 0.0 == 0.0");
+        assertUnchanged("4.0 % 0.0 == 0.0");
+    }
+
     @Test
     void foldsBooleanBinaryExpressions() {
         assertFolded("true && false", "false");
         assertFolded("false --> true", "true");
         assertFolded("true != false", "true");
     }
 
+    @Test
+    void foldsBooleanSubexpressionsInsideLargerExpression() {
+        assertFolded("true && false || ok", "false || ok");
+    }
+
+    @Test
+    void foldsNestedConstantsInsideLargerExpression() {
+        assertFolded("x > 1 + 2", "x > 3");
+        assertFolded("x + 1 + 2 > 4", "x + 3 > 4");
+    }
+
+    @Test
+    void foldsPartialComparisonsWithoutDroppingSymbolicTerms() {
+        assertFolded("1 + 2 < x + 4", "3 < x + 4");
+    }
+
     @Test
     void foldsUnaryExpressions() {
         assertFolded("!true", "false");
@@ -63,6 +85,11 @@ void foldsIteExpressions() {
         assertFolded("cond ? b : b", "b");
     }
 
+    @Test
+    void foldsIteBranchesBeforeComparingThem() {
+        assertFolded("cond ? 1 + 2 : 3", "3");
+    }
+
     @Test
     void foldsAdjacentIntegerConstants() {
         assertFolded("x + 1 - 2", "x - 1");
@@ -89,6 +116,19 @@ void foldsResolvedEnumLiterals() {
         assertSimplifiedVC(result, simplified("true", "Config.LIMIT == 3"));
     }
 
+    @Test
+    void foldsResolvedEnumLiteralsInsideLargerExpression() {
+        Enum limit = new Enum("Config", "LIMIT");
+        limit.setResolvedLiteral(new LiteralInt(3));
+        BinaryExpression arithmetic = new BinaryExpression(limit, "+", new LiteralInt(2));
+        VCImplication implication = new VCImplication(
+                new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5))));
+
+        VCImplication result = VCFolding.apply(implication);
+
+        assertSimplifiedVC(result, simplified("true", "Config.LIMIT + 2 == 5"));
+    }
+
     @Test
     void preservesOriginFromExistingSimplifiedImplication() {
         VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == 1", "x + 1 + 2 > 0"));

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

@@ -30,6 +30,15 @@ void simplifyOnceAppliesSubstitutionBeforeFolding() {
         assertSimplifiedVC(result, simplified("1 + 2 > 2", "∀x:int. x > 2"));
     }
 
+    @Test
+    void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() {
+        VCImplication implication = vc("∀x:int. x == 1 + 2", "x == 3");
+
+        VCImplication result = VCSimplification.simplifyOnce(implication);
+
+        assertSimplifiedVC(result, simplified("1 + 2 == 3", "∀x:int. x == 3"));
+    }
+
     @Test
     void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() {
         VCImplication implication = vc("1 + 2 > 2");
@@ -57,6 +66,24 @@ void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() {
         assertSimplifiedVC(result, simplified("true", "∀y:int. y > x"));
     }
 
+    @Test
+    void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() {
+        VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3");
+
+        VCImplication result = VCSimplification.simplifyToFixedPoint(implication);
+
+        assertSimplifiedVC(result, simplified("true", "∀z:int. z == 3"));
+    }
+
+    @Test
+    void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() {
+        VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2");
+
+        VCImplication result = VCSimplification.simplifyToFixedPoint(implication);
+
+        assertSimplifiedVC(result, simplified("true", "∀y:int. y - 1 == 2"));
+    }
+
     @Test
     void simplifyLeavesUnchangedVcAsPlainPredicates() {
         VCImplication implication = vc("x > 0", "y > x");