Cleanup ExpressionSimplifier

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java

@@ -2,15 +2,12 @@
 
 import java.util.ArrayList;
 import java.util.List;
-import java.util.stream.Collectors;
-
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.GroupExpression;
-import liquidjava.smt.Counterexample;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.reference.CtTypeReference;
@@ -156,33 +153,45 @@ private static void printSplitConjunction(String header, String color, Expressio
 
     private static final String PASS_NAME_COLOR = Colors.GOLD;
     private static final int PASS_NAME_WIDTH = 28;
+    private static int simplificationPass;
+    private static String previousSimplification;
 
     /**
-     * One line per simplifier phase. {@code pass} is a running counter inside a single {@code simplify()} call.
+     * Start a simplification log. DebugLog owns the running pass number and the previous expression snapshot because
+     * both are only needed for debug output.
      */
-    public static void simplificationPass(int pass, String name, Expression result) {
+    public static void simplificationStart(Expression input) {
         if (!enabled()) {
             return;
         }
-        System.out.printf("%s pass %02d: %s%n %s%n", SMP_TAG, pass, paintPassName(name), result);
+        previousSimplification = input.toString();
+        simplificationPass = 0;
+        printSimplificationPass(simplificationPass, "initial expression", previousSimplification);
     }
 
     /**
-     * Same as {@link #simplificationPass(int, String, Expression)} but prints {@code (no change)} when the step left
-     * the expression unchanged, and otherwise emits a unified-diff-style pair (red {@code -} for the previous
-     * expression with removed tokens highlighted, green {@code +} for the new one with added tokens highlighted), so
-     * substitutions inside a long predicate are obvious at a glance.
+     * One line per simplifier phase.
+     */
+    public static void simplificationPass(String name, Expression result) {
+        if (!enabled()) {
+            return;
+        }
+        String resultStr = result.toString();
+        printSimplificationPass(++simplificationPass, name, previousSimplification, resultStr);
+        previousSimplification = resultStr;
+    }
+
+    /**
+     * Prints {@code (no change)} when the step left the expression unchanged, and otherwise emits a unified-diff-style
+     * pair (red {@code -} for the previous expression with removed tokens highlighted, green {@code +} for the new one
+     * with added tokens highlighted), so substitutions inside a long predicate are obvious at a glance.
      *
      * <p>
      * {@code previous} is taken as a string rather than an {@link Expression} because the simplifier mutates the AST in
      * place: caching an {@code Expression} reference and re-stringifying it after a later pass would yield the
-     * already-mutated form, masking real changes as "no change". The caller is expected to snapshot the printed form at
-     * the moment the previous pass ran.
+     * already-mutated form, masking real changes as "no change".
      */
-    public static void simplificationPass(int pass, String name, String previous, String result) {
-        if (!enabled()) {
-            return;
-        }
+    private static void printSimplificationPass(int pass, String name, String previous, String result) {
         if (previous != null && previous.equals(result)) {
             System.out.printf("%s pass %02d: %s %s(no change)%s%n", SMP_TAG, pass, paintPassName(name), Colors.GREY,
                     Colors.RESET);
@@ -198,6 +207,10 @@ public static void simplificationPass(int pass, String name, String previous, St
         System.out.printf("%s   %s+%s %s%n", SMP_TAG, Colors.GREEN, Colors.RESET, diff[1]);
     }
 
+    private static void printSimplificationPass(int pass, String name, String result) {
+        System.out.printf("%s pass %02d: %s%n %s%n", SMP_TAG, pass, paintPassName(name), result);
+    }
+
     /**
      * Color the pass name without breaking column alignment: pad to {@link #PASS_NAME_WIDTH} first, then wrap only the
      * visible characters in {@link #PASS_NAME_COLOR}. The trailing spaces stay uncolored so {@code printf}'s width

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

@@ -24,48 +24,28 @@ public class ExpressionSimplifier {
      * expanding aliases Returns a derivation node representing the tree of simplifications applied
      */
     public static ValDerivationNode simplify(Expression exp, Map<String, AliasDTO> aliases) {
-        int[] pass = { 0 };
-        // String, not Expression: the simplification passes mutate the AST in place, so storing an Expression
-        // reference would always compare equal to itself after the next pass runs. Snapshot the printed form instead.
-        String[] prev = { null };
-        DebugLog.simplificationPass(0, "initial expression", exp);
-        prev[0] = exp.toString();
-        ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp, pass, prev);
-        logStep(pass, prev, "fixed-point reached", fixedPoint.getValue());
+        DebugLog.simplificationStart(exp);
+        ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp);
+        DebugLog.simplificationPass("fixed-point reached", fixedPoint.getValue());
         ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint);
-        logStep(pass, prev, "remove redundant &&", simplified.getValue());
+        DebugLog.simplificationPass("remove redundant &&", simplified.getValue());
         ValDerivationNode unwrapped = unwrapBooleanLiterals(simplified);
-        logStep(pass, prev, "unwrap boolean literals", unwrapped.getValue());
+        DebugLog.simplificationPass("unwrap boolean literals", unwrapped.getValue());
         ValDerivationNode expanded = AliasExpansion.expand(unwrapped, aliases);
-        logStep(pass, prev, "expand aliases", expanded.getValue());
+        DebugLog.simplificationPass("expand aliases", expanded.getValue());
         return expanded;
     }
 
     public static ValDerivationNode simplify(Expression exp) {
         return simplify(exp, Map.of());
     }
 
-    private static void logStep(int[] pass, String[] prev, String name, Expression result) {
-        String resultStr = result.toString();
-        DebugLog.simplificationPass(++pass[0], name, prev[0], resultStr);
-        prev[0] = resultStr;
-    }
-
     /**
      * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the
-     * expression simplifies to a boolean literal, which means we've simplified too much. {@code pass} and {@code prev}
-     * are running counters shared with {@link #simplify} so debug output keeps a single monotonic numbering and can
-     * detect no-op steps.
+     * expression simplifies to a boolean literal, which means we've simplified too much.
      */
-    private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp, int[] pass,
-            String[] prev) {
-        // apply propagation and folding
-        ValDerivationNode prop = VariablePropagation.propagate(prevExp, current);
-        logStep(pass, prev, "variable propagation", prop.getValue());
-        ValDerivationNode fold = ExpressionFolding.fold(prop);
-        logStep(pass, prev, "expression folding", fold.getValue());
-        ValDerivationNode simplified = simplifyValDerivationNode(fold);
-        logStep(pass, prev, "remove redundant && (loop)", simplified.getValue());
+    private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) {
+        ValDerivationNode simplified = simplifyOnce(current, prevExp);
         Expression currExp = simplified.getValue();
 
         // fixed point reached — compare on toString() because propagate/fold/reduce mutate the AST in place, so a
@@ -80,7 +60,17 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current,
         }
 
         // continue simplifying
-        return simplifyToFixedPoint(simplified, simplified.getValue(), pass, prev);
+        return simplifyToFixedPoint(simplified, simplified.getValue());
+    }
+
+    private static ValDerivationNode simplifyOnce(ValDerivationNode current, Expression prevExp) {
+        ValDerivationNode prop = VariablePropagation.propagate(prevExp, current);
+        DebugLog.simplificationPass("variable propagation", prop.getValue());
+        ValDerivationNode fold = ExpressionFolding.fold(prop);
+        DebugLog.simplificationPass("expression folding", fold.getValue());
+        ValDerivationNode simplified = simplifyValDerivationNode(fold);
+        DebugLog.simplificationPass("remove redundant && (loop)", simplified.getValue());
+        return simplified;
     }
 
     /**