Requested Changes

Author: rcosta358

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.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.smt.Counterexample;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
@@ -30,6 +32,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() {
     }
@@ -124,21 +127,31 @@ public static void smtStart(VCImplication chain, Predicate extraPremise, Predica
         System.out.println(SMT_TAG + " " + formatConclusion(conclusion));
     }
 
-    public static void simplificationInput(Predicate predicate) {
+    /**
+     * 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(SMT_TAG + " unsimplified: " + predicate);
+        System.out.println(SMP_TAG + " Simplified " + Colors.CYAN + input + Colors.RESET + " to " + Colors.YELLOW
+                + output + Colors.RESET);
     }
 
-    public static void counterexampleAssignments(Counterexample counterexample) {
+    /**
+     * Print every assignment returned by the solver before error reporting filters the user-facing counterexample down
+     * to the variables mentioned in the diagnostic.
+     */
+    public static void counterexample(Counterexample counterexample) {
         if (!enabled() || counterexample == null || counterexample.assignments().isEmpty()) {
             return;
         }
-        System.out.println(SMT_TAG + " unfiltered counterexample assignments:");
-        for (var assignment : counterexample.assignments()) {
-            System.out.println(SMT_TAG + "     " + assignment.first() + " = " + assignment.second());
-        }
+        System.out
+                .println(SMP_TAG
+                        + " Counterexample: " + Colors.RED + counterexample.assignments().stream()
+                                .map(a -> a.first() + " = " + a.second()).collect(Collectors.joining(" && "))
+                        + Colors.RESET);
     }
 
     private static String plainLabel(VCImplication node) {
@@ -233,14 +246,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);
@@ -284,7 +297,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);
     }
 
     /**
@@ -310,7 +323,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

@@ -44,7 +44,7 @@ public String getCounterExampleString() {
         if (counterexample == null || counterexample.assignments().isEmpty())
             return null;
 
-        DebugLog.counterexampleAssignments(counterexample);
+        DebugLog.counterexample(counterexample);
 
         List<String> foundVarNames = new ArrayList<>();
         found.getValue().getVariableNames(foundVarNames);

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

@@ -252,15 +252,15 @@ public Expression getExpression() {
     }
 
     public ValDerivationNode simplify(Context context) {
-        DebugLog.simplificationInput(this);
-
         // collect aliases from context
         Map<String, AliasDTO> aliases = new HashMap<>();
         for (AliasWrapper aw : context.getAliases()) {
             aliases.put(aw.getName(), aw.createAliasDTO());
         }
         // 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) {