VC Simplification Refactoring

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

@@ -1,12 +1,12 @@
 package liquidjava.rj_language.opt;
 
-import java.util.ArrayList;
-import java.util.List;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
 
 import liquidjava.processor.SimplifiedVCImplication;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.LiteralBoolean;
 
 /**
@@ -88,31 +88,4 @@ private boolean isTrueBinder(VCImplication implication) {
     private boolean isFalseBinder(VCImplication implication) {
         return implication.hasBinder() && isFalse(implication.getRefinement().getExpression());
     }
-
-    /**
-     * Checks whether an expression is true
-     */
-    private boolean isTrue(Expression expression) {
-        return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
-    }
-
-    /**
-     * Checks whether an expression is false
-     */
-    private boolean isFalse(Expression expression) {
-        return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue();
-    }
-
-    /**
-     * Checks whether a VC suffix contains a variable name
-     */
-    private boolean containsVar(VCImplication implication, String name) {
-        for (VCImplication current = implication; current != null; current = current.getNext()) {
-            List<String> names = new ArrayList<>();
-            current.getRefinement().getExpression().getVariableNames(names);
-            if (names.contains(name))
-                return true;
-        }
-        return false;
-    }
 }

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

@@ -1,5 +1,8 @@
 package liquidjava.rj_language.opt;
 
+import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
+
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.GroupExpression;
@@ -199,20 +202,6 @@ private Expression simplifyImplication(Expression left, Expression right) {
         return null;
     }
 
-    /**
-     * Checks whether an expression is true
-     */
-    private boolean isTrue(Expression expression) {
-        return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
-    }
-
-    /**
-     * Checks whether an expression is false
-     */
-    private boolean isFalse(Expression expression) {
-        return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue();
-    }
-
     /**
      * Checks whether an expression is unary logical negation
      */

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

@@ -0,0 +1,33 @@
+package liquidjava.rj_language.opt;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.LiteralBoolean;
+
+public final class VCSimplificationUtils {
+
+    public static boolean containsVar(Expression expression, String name) {
+        List<String> names = new ArrayList<>();
+        expression.getVariableNames(names);
+        return names.contains(name);
+    }
+
+    public static boolean containsVar(VCImplication implication, String name) {
+        for (VCImplication current = implication; current != null; current = current.getNext()) {
+            if (containsVar(current.getRefinement().getExpression(), name))
+                return true;
+        }
+        return false;
+    }
+
+    public static boolean isTrue(Expression expression) {
+        return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
+    }
+
+    public static boolean isFalse(Expression expression) {
+        return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue();
+    }
+}

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

@@ -1,7 +1,7 @@
 package liquidjava.rj_language.opt;
 
-import java.util.ArrayList;
-import java.util.List;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar;
+
 import java.util.Optional;
 
 import liquidjava.processor.SimplifiedVCImplication;
@@ -113,23 +113,4 @@ private boolean isVar(Expression expression, String name) {
         return expression instanceof Var var && name.equals(var.getName());
     }
 
-    /**
-     * Checks whether an expression contains a variable name
-     */
-    private boolean containsVar(Expression expression, String name) {
-        List<String> names = new ArrayList<>();
-        expression.getVariableNames(names);
-        return names.contains(name);
-    }
-
-    /**
-     * Checks whether a VC suffix contains a variable name
-     */
-    private boolean containsVar(VCImplication implication, String name) {
-        for (VCImplication current = implication; current != null; current = current.getNext()) {
-            if (containsVar(current.getRefinement().getExpression(), name))
-                return true;
-        }
-        return false;
-    }
 }