Update Tests

Author: rcosta358

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

@@ -28,14 +28,17 @@ void applyReturnsNullForNullImplication() {
 
     @Test
     void foldsIntegerArithmeticAndComparisons() {
-        assertSimplificationSteps(vc("1 + 2 == 3"), VCFolding::apply, "1 + 2 == 3", "3 == 3", "true");
+        assertSimplificationSteps(VCFolding::apply, vc("1 + 2 == 3"), simplified("3 == 3", "1 + 2 == 3"),
+                simplified("true", "1 + 2 == 3"));
         assertFolded("4 > 7", "false");
     }
 
     @Test
     void foldsRealAndMixedNumericExpressions() {
-        assertSimplificationSteps(vc("1.5 + 2.0 == 3.5"), VCFolding::apply, "1.5 + 2.0 == 3.5", "3.5 == 3.5", "true");
-        assertSimplificationSteps(vc("2 + 0.5 > 2"), VCFolding::apply, "2 + 0.5 > 2", "2.5 > 2", "true");
+        assertSimplificationSteps(VCFolding::apply, vc("1.5 + 2.0 == 3.5"),
+                simplified("3.5 == 3.5", "1.5 + 2.0 == 3.5"), simplified("true", "1.5 + 2.0 == 3.5"));
+        assertSimplificationSteps(VCFolding::apply, vc("2 + 0.5 > 2"), simplified("2.5 > 2", "2 + 0.5 > 2"),
+                simplified("true", "2 + 0.5 > 2"));
     }
 
     @Test
@@ -76,7 +79,8 @@ void foldsPartialComparisonsWithoutDroppingSymbolicTerms() {
     @Test
     void foldsUnaryExpressions() {
         assertFolded("!true", "false");
-        assertSimplificationSteps(vc("-3 < 0"), VCFolding::apply, "-3 < 0", "-3 < 0", "true");
+        assertSimplificationSteps(VCFolding::apply, vc("-3 < 0"), simplified("-3 < 0", "-3 < 0"),
+                simplified("true", "-3 < 0"));
     }
 
     @Test
@@ -88,7 +92,8 @@ void foldsIteExpressions() {
 
     @Test
     void foldsIteBranchesBeforeComparingThem() {
-        assertSimplificationSteps(vc("cond ? 1 + 2 : 3"), VCFolding::apply, "cond ? 1 + 2 : 3", "cond ? 3 : 3", "3");
+        assertSimplificationSteps(VCFolding::apply, vc("cond ? 1 + 2 : 3"),
+                simplified("cond ? 3 : 3", "cond ? 1 + 2 : 3"), simplified("3", "cond ? 1 + 2 : 3"));
     }
 
     @Test
@@ -112,7 +117,7 @@ void foldsResolvedEnumLiterals() {
         VCImplication implication = new VCImplication(
                 new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3))));
 
-        assertSimplificationSteps(implication, VCFolding::apply, simplified("3 == 3", "Config.LIMIT == 3"),
+        assertSimplificationSteps(VCFolding::apply, implication, simplified("3 == 3", "Config.LIMIT == 3"),
                 simplified("true", "Config.LIMIT == 3"));
     }
 
@@ -124,15 +129,15 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() {
         VCImplication implication = new VCImplication(
                 new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5))));
 
-        assertSimplificationSteps(implication, VCFolding::apply, simplified("3 + 2 == 5", "Config.LIMIT + 2 == 5"),
+        assertSimplificationSteps(VCFolding::apply, implication, simplified("3 + 2 == 5", "Config.LIMIT + 2 == 5"),
                 simplified("5 == 5", "Config.LIMIT + 2 == 5"), simplified("true", "Config.LIMIT + 2 == 5"));
     }
 
     @Test
     void preservesOriginFromExistingSimplifiedImplication() {
         VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == 1", "x + 1 + 2 > 0"));
 
-        assertSimplificationSteps(substituted, VCFolding::apply, simplified("2 + 2 > 0", "∀x:int. x + 1 + 2 > 0"),
+        assertSimplificationSteps(VCFolding::apply, substituted, simplified("2 + 2 > 0", "∀x:int. x + 1 + 2 > 0"),
                 simplified("4 > 0", "∀x:int. x + 1 + 2 > 0"), simplified("true", "∀x:int. x + 1 + 2 > 0"));
     }
 

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

@@ -26,15 +26,15 @@ void simplifyOnceReturnsNullForNullImplication() {
     void simplifyOnceAppliesSubstitutionBeforeFolding() {
         VCImplication implication = vc("∀x:int. x == 1 + 2", "x > 2");
 
-        assertSimplificationSteps(implication, VCSimplification::simplifyOnce, simplified("1 + 2 > 2", "∀x:int. x > 2"),
+        assertSimplificationSteps(VCSimplification::simplifyOnce, implication, simplified("1 + 2 > 2", "∀x:int. x > 2"),
                 simplified("3 > 2", "∀x:int. x > 2"), simplified("true", "∀x:int. x > 2"));
     }
 
     @Test
     void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() {
         VCImplication implication = vc("∀x:int. x == 1 + 2", "x == 3");
 
-        assertSimplificationSteps(implication, VCSimplification::simplifyOnce,
+        assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
                 simplified("1 + 2 == 3", "∀x:int. x == 3"), simplified("3 == 3", "∀x:int. x == 3"),
                 simplified("true", "∀x:int. x == 3"));
     }
@@ -43,7 +43,7 @@ void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() {
     void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() {
         VCImplication implication = vc("1 + 2 > 2");
 
-        assertSimplificationSteps(implication, VCSimplification::simplifyOnce, simplified("3 > 2", "1 + 2 > 2"),
+        assertSimplificationSteps(VCSimplification::simplifyOnce, implication, simplified("3 > 2", "1 + 2 > 2"),
                 simplified("true", "1 + 2 > 2"));
     }
 

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

@@ -21,7 +21,7 @@ void substitutesBinderEqualityIntoWholeChain() {
         VCImplication result = VCSubstitution.apply(implication);
 
         assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
-        assertSimplificationSteps(result, VCSimplification::simplifyOnce, simplified("true", "∀x:int. x > 0"));
+        assertSimplificationSteps(VCSimplification::simplifyOnce, result, simplified("true", "∀x:int. x > 0"));
     }
 
     @Test
@@ -31,7 +31,7 @@ void substitutesReverseBinderEquality() {
         VCImplication result = VCSubstitution.apply(implication);
 
         assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
-        assertSimplificationSteps(result, VCSimplification::simplifyOnce, simplified("true", "∀x:int. x > 0"));
+        assertSimplificationSteps(VCSimplification::simplifyOnce, result, simplified("true", "∀x:int. x > 0"));
     }
 
     @Test
@@ -59,7 +59,7 @@ void substitutesEveryOccurrenceInPredicate() {
         VCImplication result = VCSubstitution.apply(implication);
 
         assertSimplifiedVC(result, simplified("2 + 2 > 0", "∀x:int. x + x > 0"));
-        assertSimplificationSteps(result, VCSimplification::simplifyOnce, simplified("4 > 0", "∀x:int. x + x > 0"),
+        assertSimplificationSteps(VCSimplification::simplifyOnce, result, simplified("4 > 0", "∀x:int. x + x > 0"),
                 simplified("true", "∀x:int. x + x > 0"));
     }
 
@@ -114,7 +114,7 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() {
 
         assertSimplifiedVC(result, simplified("y == 3 + 1", "∀x:int. y == x + 1"),
                 simplified("y > 3", "∀x:int. y > x"));
-        assertSimplificationSteps(result, VCSimplification::simplifyOnce, simplified("3 + 1 > 3", "∀y:int. y > x"),
+        assertSimplificationSteps(VCSimplification::simplifyOnce, result, simplified("3 + 1 > 3", "∀y:int. y > x"),
                 simplified("4 > 3", "∀y:int. y > x"), simplified("true", "∀y:int. y > x"));
     }
 

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

@@ -94,8 +94,8 @@ public static void assertVC(VCImplication implication, String... expected) {
         assertNull(current, "Expected VC chain to end after " + expected.length + " implications");
     }
 
-    public static VCImplication assertSimplificationSteps(VCImplication implication,
-            UnaryOperator<VCImplication> simplifier, ExpectedSimplifiedVCImplication... expectedSteps) {
+    public static VCImplication assertSimplificationSteps(UnaryOperator<VCImplication> simplifier,
+            VCImplication implication, ExpectedSimplifiedVCImplication... expectedSteps) {
         VCImplication current = implication;
         for (int i = 0; i < expectedSteps.length; i++) {
             current = simplifier.apply(current);
@@ -104,13 +104,6 @@ public static VCImplication assertSimplificationSteps(VCImplication implication,
         return current;
     }
 
-    public static VCImplication assertSimplificationSteps(VCImplication implication,
-            UnaryOperator<VCImplication> simplifier, String origin, String... simplifiedSteps) {
-        ExpectedSimplifiedVCImplication[] expectedSteps = java.util.Arrays.stream(simplifiedSteps)
-                .map(step -> simplified(step, origin)).toArray(ExpectedSimplifiedVCImplication[]::new);
-        return assertSimplificationSteps(implication, simplifier, expectedSteps);
-    }
-
     public static SimplifiedVCImplication simplifiedImplication(VCImplication implication, int index) {
         return assertInstanceOf(SimplifiedVCImplication.class, implication,
                 "Expected implication " + index + " to be a SimplifiedVCImplication");