actually what i wanted to print as we had once upon a time

Author: CatarinaGamboa

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

@@ -11,4 +11,21 @@ public class Colors {
     public static final String CYAN = "\u001B[36m";
     public static final String BOLD_RED = "\u001B[1;31m";
     public static final String BOLD_YELLOW = "\u001B[1;33m";
+    public static final String ORANGE = "\u001B[38;5;208m";
+    public static final String PINK = "\u001B[38;5;205m";
+    public static final String CORAL = "\u001B[38;5;203m";
+    public static final String SALMON = "\u001B[38;5;209m";
+    public static final String GOLD = "\u001B[38;5;220m";
+    public static final String BRIGHT_YELLOW = "\u001B[38;5;226m";
+    public static final String LIME = "\u001B[38;5;118m";
+    public static final String BRIGHT_GREEN = "\u001B[38;5;46m";
+    public static final String TEAL = "\u001B[38;5;37m";
+    public static final String LIGHT_BLUE = "\u001B[38;5;39m";
+    public static final String BRIGHT_CYAN = "\u001B[38;5;51m";
+    public static final String PURPLE = "\u001B[38;5;129m";
+    public static final String BRIGHT_MAGENTA = "\u001B[38;5;201m";
+    public static final String BROWN = "\u001B[38;5;94m";
+    public static final String NAVY = "\u001B[38;5;17m";
+    public static final String LIGHT_GREY = "\u001B[38;5;250m";
+    public static final String DARK_GREY = "\u001B[38;5;240m";
 }

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

@@ -1,19 +1,17 @@
 package liquidjava.diagnostics;
 
 import java.util.ArrayList;
-import java.util.LinkedHashMap;
-import java.util.LinkedHashSet;
 import java.util.List;
-import java.util.Map;
-import java.util.Set;
 
 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.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.reference.CtTypeReference;
 
 /**
  * Centralised debug-mode logging for verification activity. Output is gated on the global {@code --debug} / {@code -d}
@@ -29,8 +27,8 @@
  */
 public final class DebugLog {
 
-    private static final String INFO_TAG = Colors.YELLOW + "[INFO]" + Colors.RESET;
     private static final String SMT_TAG = Colors.BLUE + "[SMT]" + Colors.RESET;
+    private static final String SMT_CHECK = Colors.SALMON + "[SMT CHECK]" + Colors.RESET;
 
     private DebugLog() {
     }
@@ -39,57 +37,165 @@ public static boolean enabled() {
         return CommandLineLauncher.cmdArgs.debugMode;
     }
 
-    public static void info(String verb, Object expected, Object found, SourcePosition position) {
-        if (!enabled()) {
+    /**
+     * One-line header for a verification check: emits the absolute file path + line so terminals (iTerm2, VS Code,
+     * WezTerm, …) make it ⌘/Ctrl-clickable. Replaces the older two-line {@code info()} prints.
+     */
+    public static void smtVerifying(SourcePosition position) {
+        if (!enabled() || position == null) {
             return;
         }
+        String where = position.getFile().getAbsolutePath() + ":" + position.getLine();
         String exp = Utils.getExpressionFromPosition(position);
-        String where = position.getFile().getName() + ":" + position.getLine();
-        System.out.println(INFO_TAG + " " + verb + ": " + found + " <: " + expected);
-        System.out.println(INFO_TAG + "   at " + where + (exp != null ? "  on '" + exp + "'" : ""));
+        System.out.println(SMT_CHECK);
+        System.out.println(SMT_TAG + " Verifying " + Colors.CYAN + where + Colors.RESET
+                + (exp != null ? "  on '" + exp + "'" : ""));
     }
 
+    private static final String SEPARATOR = Colors.GREY + "   ────────────────────────────────────────" + Colors.RESET;
+
+    /**
+     * Flat-predicate fallback: prints top-level conjuncts in order with no per-variable grouping. Used by SMT entry
+     * points that don't carry the structured per-variable {@link VCImplication} chain (e.g. ExpressionSimplifier).
+     */
     public static void smtStart(Predicate premises, Predicate conclusion) {
         if (!enabled()) {
             return;
         }
-        printPremisesByVariable(premises);
-        System.out.println(SMT_TAG + " conclusion: " + conclusion);
+        List<Expression> conjuncts = new ArrayList<>();
+        flattenConjunction(premises.getExpression(), conjuncts);
+        System.out.println(SMT_TAG);
+        for (Expression c : conjuncts) {
+            System.out.println(SMT_TAG + "   " + c);
+        }
+        System.out.println(SMT_TAG + SEPARATOR);
+        System.out.println(SMT_TAG + "   "  + formatConclusion(conclusion));
     }
 
     /**
-     * Splits the premise conjunction into top-level conjuncts and groups them by the variable they constrain. Conjuncts
-     * mentioning a single variable are printed under that variable; conjuncts mentioning zero or several variables are
-     * printed under a {@code <shared>} bucket.
+     * Structured form: walks the {@link VCImplication} chain produced by {@code joinPredicates}, printing one line per
+     * refined variable with all of its refinements together.
      */
-    private static void printPremisesByVariable(Predicate premises) {
-        Expression root = premises.getExpression();
-        List<Expression> conjuncts = new ArrayList<>();
-        flattenConjunction(root, conjuncts);
+    public static void smtStart(VCImplication chain, Predicate conclusion) {
+        smtStart(chain, null, conclusion);
+    }
 
-        Map<String, List<String>> grouped = new LinkedHashMap<>();
-        for (Expression c : conjuncts) {
-            List<String> names = new ArrayList<>();
-            c.getVariableNames(names);
-            Set<String> unique = new LinkedHashSet<>(names);
-            String key;
-            if (unique.isEmpty()) {
-                key = "";
-            } else if (unique.size() == 1) {
-                key = unique.iterator().next();
-            } else {
-                key = "<shared>";
+    /**
+     * Structured form with an extra unattributed premise (e.g. the "found" type appended in
+     * {@code verifySMTSubtypeStates}).
+     */
+    public static void smtStart(VCImplication chain, Predicate extraPremise, Predicate conclusion) {
+        if (!enabled()) {
+            return;
+        }
+        // Pre-compute label widths for column alignment across all printed rows.
+        int labelWidth = 0;
+        for (VCImplication node = chain; node != null; node = node.getNext()) {
+            if (node.getName() == null && node.getType() == null) {
+                continue;
+            }
+            labelWidth = Math.max(labelWidth, plainLabel(node).length());
+        }
+        if (extraPremise != null && !extraPremise.isBooleanTrue()) {
+            labelWidth = Math.max(labelWidth, "found".length());
+        }
+
+        System.out.println(SMT_TAG + " ");
+        List<String> printedRefinements = new ArrayList<>();
+        for (VCImplication node = chain; node != null; node = node.getNext()) {
+            if (node.getName() == null && node.getType() == null) {
+                continue; // skip the empty trailing tail node
+            }
+            String refinement = formatRefinement(node.getRefinement());
+            printedRefinements.add(refinement);
+            System.out.println(SMT_TAG + "   " + paintLabel(node, labelWidth) + "  " + refinement);
+        }
+        if (extraPremise != null && !extraPremise.isBooleanTrue()) {
+            String extra = formatRefinement(extraPremise);
+            // Skip when the appended "found" type is identical to a premise we just printed
+            // (common in verifySMTSubtypeStates when `type` IS the variable's current refinement).
+            if (!printedRefinements.contains(extra)) {
+                String label = Colors.GREY + padRight("found", labelWidth) + Colors.RESET;
+                System.out.println(SMT_TAG + "   " + label + "  " + extra);
+            }
+        }
+        System.out.println(SMT_TAG + SEPARATOR);
+        System.out.println(SMT_TAG + " " + formatConclusion(conclusion));
+    }
+
+    private static String plainLabel(VCImplication node) {
+        return node.getName() + " : " + simpleType(node.getType());
+    }
+
+    private static String paintLabel(VCImplication node, int width) {
+        String name = node.getName();
+        String type = simpleType(node.getType());
+        String padded = padRight(name + " : " + type, width);
+        // Color only the name; keep alignment by computing padding on the plain string.
+        String coloredName = Colors.CYAN + name + Colors.RESET;
+        String coloredType = Colors.GREY + type + Colors.RESET;
+        String tail = padded.substring((name + " : " + type).length()); // padding spaces
+        return coloredName + Colors.GREY + " : " + Colors.RESET + coloredType + tail;
+    }
+
+    private static String simpleType(CtTypeReference<?> type) {
+        if (type == null) {
+            return "?";
+        }
+        String qual = type.getQualifiedName();
+        return qual.contains(".") ? Utils.getSimpleName(qual) : qual;
+    }
+
+    private static String padRight(String s, int width) {
+        if (s.length() >= width) {
+            return s;
+        }
+        StringBuilder sb = new StringBuilder(s);
+        for (int i = s.length(); i < width; i++) {
+            sb.append(' ');
+        }
+        return sb.toString();
+    }
+
+    /**
+     * Render a refinement so multi-conjunct predicates are unambiguous on a single line: each top-level conjunct is
+     * wrapped in parens and joined with ∧.
+     */
+    private static String formatRefinement(Predicate p) {
+        List<Expression> conjuncts = new ArrayList<>();
+        flattenConjunction(p.getExpression(), conjuncts);
+        if (conjuncts.size() <= 1) {
+            return p.toString();
+        }
+        StringBuilder sb = new StringBuilder();
+        for (int i = 0; i < conjuncts.size(); i++) {
+            if (i > 0) {
+                sb.append(Colors.GREY).append(" ∧ ").append(Colors.RESET);
             }
-            grouped.computeIfAbsent(key, k -> new ArrayList<>()).add(c.toString());
+            sb.append('(').append(conjuncts.get(i)).append(')');
         }
+        return sb.toString();
+    }
 
-        System.out.println(SMT_TAG + " premises:");
-        for (Map.Entry<String, List<String>> entry : grouped.entrySet()) {
-            String prefix = entry.getKey().isEmpty() ? "" : entry.getKey() + ": ";
-            for (String c : entry.getValue()) {
-                System.out.println(SMT_TAG + "   " + prefix + c);
+    /**
+     * Conclusion needs its own painter: nesting {@link #formatRefinement} (which already emits ANSI {@code RESET}
+     * around its operators) inside an outer color would clear the outer color after the first inner reset, leaving the
+     * tail of the line uncoloured. Paint each conjunct individually instead.
+     */
+    private static String formatConclusion(Predicate p) {
+        List<Expression> conjuncts = new ArrayList<>();
+        flattenConjunction(p.getExpression(), conjuncts);
+        if (conjuncts.size() <= 1) {
+            return Colors.BOLD_YELLOW + p + Colors.RESET;
+        }
+        StringBuilder sb = new StringBuilder();
+        for (int i = 0; i < conjuncts.size(); i++) {
+            if (i > 0) {
+                sb.append(Colors.GREY).append(" ∧ ").append(Colors.RESET);
             }
+            sb.append(Colors.BOLD_YELLOW).append('(').append(conjuncts.get(i)).append(')').append(Colors.RESET);
         }
+        return sb.toString();
     }
 
     private static void flattenConjunction(Expression e, List<Expression> out) {
@@ -126,4 +232,31 @@ public static void smtUnknown() {
         }
         System.out.println(SMT_TAG + " result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET);
     }
+
+    /**
+     * Print the result of an SMT check whose {@code smtStart} was emitted by the caller (e.g. VCChecker's structured
+     * print). {@link liquidjava.smt.SMTResult} doesn't preserve UNKNOWN, so this maps OK → UNSAT and ERROR → SAT.
+     */
+    public static void smtResult(liquidjava.smt.SMTResult result) {
+        if (!enabled()) {
+            return;
+        }
+        if (result.isError()) {
+            smtSat(result.getCounterexample());
+        } else {
+            smtUnsat();
+        }
+    }
+
+    /**
+     * Print an SMT-side failure (e.g. Z3 sort mismatch) so the trace doesn't end with a dangling header. Caller is
+     * still responsible for surfacing the user-facing error.
+     */
+    public static void smtError(String message) {
+        if (!enabled()) {
+            return;
+        }
+        System.out.println(SMT_TAG + " result: " + Colors.RED + "ERROR" + Colors.RESET + " — "
+                + (message == null ? "(no message)" : message));
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -27,6 +27,26 @@ public void setNext(VCImplication c) {
         next = c;
     }
 
+    public String getName() {
+        return name;
+    }
+
+    public CtTypeReference<?> getType() {
+        return type;
+    }
+
+    public Predicate getRefinement() {
+        return refinement;
+    }
+
+    public void setRefinement(Predicate refinement) {
+        this.refinement = refinement;
+    }
+
+    public VCImplication getNext() {
+        return next;
+    }
+
     public String toString() {
         if (name != null && type != null) {
             String qualType = type.getQualifiedName();