Improve Debug Logs

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

@@ -2,13 +2,15 @@
 
 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;
@@ -29,6 +31,7 @@ public final class DebugLog {
 
     private static final String SMT_TAG = Colors.BLUE + "[SMT]" + Colors.RESET;
     private static final String SMT_CHECK = Colors.SALMON + "[SMT CHECK]" + Colors.RESET;
+    private static final String SMP_TAG = Colors.YELLOW + "[SMP]" + Colors.RESET;
 
     private DebugLog() {
     }
@@ -123,6 +126,18 @@ public static void smtStart(VCImplication chain, Predicate extraPremise, Predica
         System.out.println(SMT_TAG + " " + formatConclusion(conclusion));
     }
 
+    /**
+     * Print the simplifier input and output side by side. This keeps the raw expression visible in debug traces while
+     * callers continue using the simplified expression for user-facing diagnostics.
+     */
+    public static void simplification(Expression input, Expression output) {
+        if (!enabled()) {
+            return;
+        }
+        System.out.println(SMP_TAG + " Before simplification: " + Colors.YELLOW + input + Colors.RESET);
+        System.out.println(SMP_TAG + " After simplification:  " + Colors.BOLD_YELLOW + output + Colors.RESET);
+    }
+
     private static String plainLabel(VCImplication node) {
         return node.getName() + " : " + simpleType(node.getType());
     }
@@ -215,14 +230,14 @@ public static void smtUnsat() {
         if (!enabled()) {
             return;
         }
-        System.out.println(SMT_TAG + " result: " + Colors.GREEN + "UNSAT (subtype holds)" + Colors.RESET);
+        System.out.println(SMT_TAG + " Result: " + Colors.GREEN + "UNSAT (subtype holds)" + Colors.RESET);
     }
 
     public static void smtSat(Object counterexample) {
         if (!enabled()) {
             return;
         }
-        String header = SMT_TAG + " result: " + Colors.RED + "SAT (subtype fails)" + Colors.RESET;
+        String header = SMT_TAG + " Result: " + Colors.RED + "SAT (subtype fails)" + Colors.RESET;
         String pretty = formatCounterexample(counterexample);
         if (pretty == null) {
             System.out.println(header);
@@ -266,7 +281,7 @@ public static void smtUnknown() {
         if (!enabled()) {
             return;
         }
-        System.out.println(SMT_TAG + " result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET);
+        System.out.println(SMT_TAG + " Result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET);
     }
 
     /**
@@ -292,7 +307,7 @@ public static void smtError(String message) {
         if (!enabled()) {
             return;
         }
-        System.out.println(SMT_TAG + " result: " + Colors.RED + "ERROR" + Colors.RESET + " — "
+        System.out.println(SMT_TAG + " Result: " + Colors.RED + "ERROR" + Colors.RESET + " — "
                 + (message == null ? "(no message)" : message));
     }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -4,7 +4,6 @@
 import java.util.List;
 import java.util.stream.Collectors;
 
-import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
@@ -53,8 +52,8 @@ public String getCounterExampleString() {
         List<String> foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList();
         String counterexampleString = counterexample.assignments().stream()
                 // only include variables that appear in the found value and are not already fixed there
-                .filter(a -> CommandLineLauncher.cmdArgs.debugMode || (foundVarNames.contains(a.first())
-                        && !foundAssignments.contains(a.first() + " == " + a.second())))
+                .filter(a -> foundVarNames.contains(a.first())
+                        && !foundAssignments.contains(a.first() + " == " + a.second()))
                 // format as "var == value"
                 .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
                 // join with "&&"

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -6,7 +6,7 @@
 import java.util.Map;
 import java.util.stream.Collectors;
 
-import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
 import liquidjava.processor.context.AliasWrapper;
@@ -257,11 +257,10 @@ public ValDerivationNode simplify(Context context) {
         for (AliasWrapper aw : context.getAliases()) {
             aliases.put(aw.getName(), aw.createAliasDTO());
         }
-        if (CommandLineLauncher.cmdArgs.debugMode) {
-            return new ValDerivationNode(exp.clone(), null);
-        }
         // simplify expression
-        return ExpressionSimplifier.simplify(exp.clone(), aliases);
+        ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases);
+        DebugLog.simplification(this.getExpression(), result.getValue());
+        return result;
     }
 
     private static boolean isBooleanLiteral(Expression expr, boolean value) {