Add Fixed Point Iteration

Author: rcosta358

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

@@ -0,0 +1,44 @@
+package liquidjava.rj_language.opt;
+
+import liquidjava.processor.VCImplication;
+
+import static liquidjava.rj_language.opt.VCSimplificationUtils.*;
+
+/**
+ * Simplifies VCImplication chains by applying various simplification steps
+ */
+public class VCSimplification {
+
+    /**
+     * Applies all available simplification steps to a VC chain
+     */
+    public static VCImplication simplify(VCImplication implication) {
+        if (implication == null)
+            return null;
+
+        // keep applying simplification steps until a fixed point is reached
+        VCImplication current = implication.clone();
+        while (true) {
+            VCImplication simplified = simplifyOnce(current);
+            if (sameVc(current, simplified)) // fixed point reached
+                return simplified;
+            current = simplified;
+        }
+    }
+
+    /**
+     * Applies one simplification step to a VC chain
+     */
+    public static VCImplication simplifyOnce(VCImplication implication) {
+        if (implication == null)
+            return null;
+
+        // first try to apply substitution, then folding
+        VCImplication substituted = VCSubstitution.applyOnce(implication);
+        if (!sameVc(implication, substituted))
+            return substituted;
+
+        // TODO: add more simplification steps here (e.g., folding)
+        return substituted;
+    }
+}

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

@@ -11,34 +11,25 @@
 
 class VCSimplificationUtils {
 
-    private VCSimplificationUtils() {
-    }
-
-    static Expression activeExpression(Predicate refinement) {
+    public static Expression activeExpression(Predicate refinement) {
         if (refinement instanceof SimplifiedPredicate simplified)
             return simplified.getSimplifiedPredicate().getExpression().clone();
         return refinement.getExpression().clone();
     }
 
-    static Predicate originPredicate(Predicate refinement) {
+    public 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) {
+    public 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) {
+    public 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

@@ -12,6 +12,8 @@
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Var;
 
+import static liquidjava.rj_language.opt.VCSimplificationUtils.*;
+
 /**
  * Simplifies VCImplication chains by replacing binder equalities with their known values
  */
@@ -134,11 +136,4 @@ public static boolean containsVariable(Expression expression, String name) {
         expression.getVariableNames(names);
         return names.contains(name);
     }
-
-    /**
-     * Returns the expression used for matching and substitution
-     */
-    public static Expression activeExpression(Predicate refinement) {
-        return VCSimplificationUtils.activeExpression(refinement);
-    }
 }

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

@@ -1,6 +1,6 @@
 package liquidjava.rj_language.opt;
 
-import static liquidjava.rj_language.opt.VCSubstitution.activeExpression;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.*;
 import static liquidjava.rj_language.opt.VCSubstitution.containsVariable;
 import static liquidjava.rj_language.opt.VCSubstitution.isVar;
 import static org.junit.jupiter.api.Assertions.assertTrue;
@@ -29,7 +29,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera
         VCImplication current = vc;
 
         for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) {
-            VCImplication simplified = VCSimplifier.simplify(current);
+            VCImplication simplified = VCSimplification.simplify(current);
             if (sameVc(current, simplified))
                 break;
 
@@ -47,10 +47,6 @@ private static void setUpContext() {
             TestUtils.addIntVariableToContext(variable);
     }
 
-    private static boolean sameVc(VCImplication left, VCImplication right) {
-        return left.toString().equals(right.toString());
-    }
-
     private static void assertEquivalent(VCImplication unsimplified, VCImplication simplified, int step) {
         Predicate premises = substitutionPremises(unsimplified);
         Predicate unsimplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(unsimplified)));