Code Refactoring

Author: rcosta358

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

@@ -0,0 +1,46 @@
+package liquidjava.rj_language.opt;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.SimplifiedPredicate;
+import liquidjava.rj_language.SimplifiedPredicate.Binder;
+import liquidjava.rj_language.ast.Expression;
+
+class VCSimplificationUtils {
+
+    private VCSimplificationUtils() {
+    }
+
+    static Expression activeExpression(Predicate refinement) {
+        if (refinement instanceof SimplifiedPredicate simplified)
+            return simplified.getSimplifiedPredicate().getExpression().clone();
+        return refinement.getExpression().clone();
+    }
+
+    static Predicate originPredicate(Predicate refinement) {
+        if (refinement instanceof SimplifiedPredicate simplified)
+            return simplified.getOrigin().clone();
+        return refinement.clone();
+    }
+
+    static List<Binder> binders(Predicate refinement) {
+        if (refinement instanceof SimplifiedPredicate simplified)
+            return new ArrayList<>(simplified.getBinders());
+        return new ArrayList<>();
+    }
+
+    static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) {
+        if (implication.hasBinder())
+            return new VCImplication(implication.getName(), implication.getType(), refinement);
+        return new VCImplication(refinement);
+    }
+
+    static boolean sameVc(VCImplication left, VCImplication right) {
+        if (left == null || right == null)
+            return left == right;
+        return left.toString().equals(right.toString());
+    }
+}

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

@@ -11,15 +11,7 @@ public class VCSimplifier {
      * Applies all available simplification steps to a VC chain
      */
     public static VCImplication simplify(VCImplication implication) {
-        // TODO: implement remaining simplification steps
-        return VCSubstitution.apply(implication);
-    }
-
-    /**
-     * Applies one simplification step to a VC chain
-     */
-    public static VCImplication simplifyOnce(VCImplication implication) {
-        // TODO: implement remaining simplification steps
+        // TODO: implement remaining simplification steps with fixed point iteration
         return VCSubstitution.applyOnce(implication);
     }
 }

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

@@ -23,25 +23,6 @@ public class VCSubstitution {
     private record Substitution(VCImplication source, Expression value) {
     }
 
-    /**
-     * Applies all available binder equality substitutions in a VC chain
-     */
-    public static VCImplication apply(VCImplication implication) {
-        if (implication == null)
-            return null;
-
-        VCImplication result = implication.clone();
-        Optional<VCSubstitution.Substitution> substitutionOpt = VCSubstitution.findSubstitution(result);
-
-        // keep applying substitutions until there are no more substitutions available
-        while (substitutionOpt.isPresent()) {
-            VCSubstitution.Substitution substitution = substitutionOpt.get();
-            result = VCSubstitution.substitute(result, substitution.source(), substitution.value());
-            substitutionOpt = VCSubstitution.findSubstitution(result);
-        }
-        return result;
-    }
-
     /**
      * Applies one substitution in a VC chain
      */
@@ -72,7 +53,7 @@ private static VCImplication substitute(VCImplication implication, VCImplication
             return substitute(implication.getNext(), source, value);
 
         Predicate refinement = substituteRefinement(implication.getRefinement(), source, value);
-        VCImplication result = copyWithRefinement(implication, refinement);
+        VCImplication result = VCSimplificationUtils.copyWithRefinement(implication, refinement);
         result.setNext(substitute(implication.getNext(), source, value));
         return result;
     }
@@ -85,28 +66,10 @@ private static Predicate substituteRefinement(Predicate refinement, VCImplicatio
         Binder binder = new Binder(source.getName(), source.getType());
         Expression substituted = active.substitute(new Var(binder.getName()), value.clone());
 
-        return new SimplifiedPredicate(new Predicate(substituted), originPredicate(refinement),
+        return new SimplifiedPredicate(new Predicate(substituted), VCSimplificationUtils.originPredicate(refinement),
                 bindersAfterSubstitution(refinement, active, binder));
     }
 
-    /**
-     * Copies an implication node with a replacement refinement
-     */
-    private static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) {
-        if (implication.hasBinder())
-            return new VCImplication(implication.getName(), implication.getType(), refinement);
-        return new VCImplication(refinement);
-    }
-
-    /**
-     * Returns the expression that should be shown as the original formula
-     */
-    private static Predicate originPredicate(Predicate refinement) {
-        if (refinement instanceof SimplifiedPredicate simplified)
-            return simplified.getOrigin().clone();
-        return refinement.clone();
-    }
-
     /**
      * Builds the binder metadata after one substitution
      */
@@ -176,8 +139,6 @@ public static boolean containsVariable(Expression expression, String name) {
      * Returns the expression used for matching and substitution
      */
     public static Expression activeExpression(Predicate refinement) {
-        if (refinement instanceof SimplifiedPredicate simplified)
-            return simplified.getSimplifiedPredicate().getExpression().clone();
-        return refinement.getExpression().clone();
+        return VCSimplificationUtils.activeExpression(refinement);
     }
 }

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

@@ -29,7 +29,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera
         VCImplication current = vc;
 
         for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) {
-            VCImplication simplified = VCSimplifier.simplifyOnce(current);
+            VCImplication simplified = VCSimplifier.simplify(current);
             if (sameVc(current, simplified))
                 break;
 

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

@@ -10,15 +10,15 @@
 class VCSubstitutionTest {
 
     @Test
-    void applyReturnsNullForNullImplication() {
-        assertNull(VCSubstitution.apply(null));
+    void applyOnceReturnsNullForNullImplication() {
+        assertNull(VCSubstitution.applyOnce(null));
     }
 
     @Test
     void substitutesBinderEqualityIntoWholeChain() {
         VCImplication implication = vc("∀x:int. x == 3", "x > 0");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
         assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int"));
     }
@@ -27,7 +27,7 @@ void substitutesBinderEqualityIntoWholeChain() {
     void substitutesReverseBinderEquality() {
         VCImplication implication = vc("∀x:int. 3 == x", "x > 0");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
         assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int"));
     }
@@ -36,7 +36,7 @@ void substitutesReverseBinderEquality() {
     void substitutesCompoundKnownValue() {
         VCImplication implication = vc("∀x:int. x == y + 1", "x > y");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
         assertSimplifiedVC(result, simplified("y + 1 > y", "x > y", "x:int"));
     }
@@ -45,7 +45,7 @@ void substitutesCompoundKnownValue() {
     void usesFirstSubstitutionFoundInChain() {
         VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
         assertSimplifiedVC(result, simplified("x > 0", "x > 0", ""), simplified("x + 4 > 0", "x + y > 0", "y:int"));
     }
@@ -54,7 +54,7 @@ void usesFirstSubstitutionFoundInChain() {
     void substitutesInnerKnownValueAcrossNestedImplications() {
         VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
         assertSimplifiedVC(result, simplified("true", "true", ""), simplified("z > 1", "z > y", "y:int"),
                 simplified("1 + z > 0", "y + z > 0", "y:int"));
@@ -64,16 +64,17 @@ void substitutesInnerKnownValueAcrossNestedImplications() {
     void substitutesOuterKnownValueIntoNestedBinderRefinements() {
         VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
-        assertSimplifiedVC(result, simplified("3 + 1 > 3", "y > x", "x:int, y:int"));
+        assertSimplifiedVC(result, simplified("y == 3 + 1", "y == x + 1", "x:int"),
+                simplified("y > 3", "y > x", "x:int"));
     }
 
     @Test
     void ignoresRecursiveBinderEquality() {
         VCImplication implication = vc("∀x:int. x == x + 1", "x > 0");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
         assertNotSame(implication, result);
         assertVC(result, "x == x + 1", "x > 0");
@@ -83,7 +84,7 @@ void ignoresRecursiveBinderEquality() {
     void ignoresNonEqualityBinderRefinement() {
         VCImplication implication = vc("∀x:int. x > 3", "x > 0");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
         assertNotSame(implication, result);
         assertVC(result, "x > 3", "x > 0");
@@ -93,7 +94,7 @@ void ignoresNonEqualityBinderRefinement() {
     void ignoresEqualityWithoutBinder() {
         VCImplication implication = vc("x == 3", "x > 0");
 
-        VCImplication result = VCSubstitution.apply(implication);
+        VCImplication result = VCSubstitution.applyOnce(implication);
 
         assertVC(result, "x == 3", "x > 0");
     }