Add -a/--all flag to show all SMT verification conditions

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java

@@ -22,6 +22,9 @@ public class CommandLineArgs {
     @Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output")
     public boolean debugMode;
 
+    @Option(names = { "-a", "--all" }, description = "Show every verification condition sent to the SMT solver")
+    public boolean showAllVCs;
+
     @Option(names = { "-lsp", "--language-server" }, description = "Enable language server mode for editor support")
     public boolean lspMode;
 

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

@@ -37,12 +37,56 @@ public static boolean enabled() {
         return CommandLineLauncher.cmdArgs.debugMode;
     }
 
+    /**
+     * Gate for the SMT-query trace (verification conditions fed to Z3 and their outcomes). Enabled by either
+     * {@code --debug} / {@code -d} or the lighter {@code --all} / {@code -a}, which shows every query without the rest
+     * of the debug output (e.g. simplification passes).
+     */
+    public static boolean smtEnabled() {
+        return CommandLineLauncher.cmdArgs.debugMode || CommandLineLauncher.cmdArgs.showAllVCs;
+    }
+
+    /**
+     * Set by {@link #smtStart} (the structured / flat VC printers) and consumed by {@link #smtRawQuery}. Lets the
+     * low-level Z3 boundary trace skip a query that a higher layer already printed in full, so {@code -a} shows every
+     * query exactly once. Single-threaded: each {@code smtStart} is immediately followed by one {@code solver.check()}.
+     */
+    private static boolean structuredQueryPending = false;
+
+    /**
+     * Catch-all trace emitted at the actual {@code solver.check()} boundary so {@code -a} / {@code -d} show EVERY query
+     * sent to Z3 — including those that bypass the structured {@link #smtStart} path (the simplifier's implication
+     * checks, refinement satisfiability checks, speculative typestate checks). Suppressed for queries a structured
+     * print already covered, to avoid duplication.
+     *
+     * @param sent
+     *            the predicate actually handed to Z3
+     * @param result
+     *            the raw Z3 {@code Status}
+     */
+    public static void smtRawQuery(Predicate sent, String result) {
+        if (!smtEnabled()) {
+            return;
+        }
+        if (structuredQueryPending) {
+            structuredQueryPending = false; // already shown by the structured print that preceded this check
+            return;
+        }
+        List<Expression> conjuncts = new ArrayList<>();
+        flattenConjunction(sent.getExpression(), conjuncts);
+        System.out.println(SMT_TAG + " " + Colors.GREY + "query → Z3" + Colors.RESET);
+        for (Expression c : conjuncts) {
+            System.out.println(SMT_TAG + "   " + c);
+        }
+        System.out.println(SMT_TAG + " Result: " + Colors.CYAN + result + Colors.RESET);
+    }
+
     /**
      * 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) {
+        if (!smtEnabled() || position == null) {
             return;
         }
         String where = position.getFile().getAbsolutePath() + ":" + position.getLine();
@@ -59,9 +103,10 @@ public static void smtVerifying(SourcePosition position) {
      * 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()) {
+        if (!smtEnabled()) {
             return;
         }
+        structuredQueryPending = true;
         List<Expression> conjuncts = new ArrayList<>();
         flattenConjunction(premises.getExpression(), conjuncts);
         System.out.println(SMT_TAG);
@@ -85,9 +130,10 @@ public static void smtStart(VCImplication chain, Predicate conclusion) {
      * {@code verifySMTSubtypeStates}).
      */
     public static void smtStart(VCImplication chain, Predicate extraPremise, Predicate conclusion) {
-        if (!enabled()) {
+        if (!smtEnabled()) {
             return;
         }
+        structuredQueryPending = true;
         // Pre-compute label widths for column alignment across all printed rows.
         int labelWidth = 0;
         for (VCImplication node = chain; node != null; node = node.getNext()) {
@@ -362,14 +408,14 @@ private static void flattenConjunction(Expression e, List<Expression> out) {
     }
 
     public static void smtUnsat() {
-        if (!enabled()) {
+        if (!smtEnabled()) {
             return;
         }
         System.out.println(SMT_TAG + " Result: " + Colors.GREEN + "UNSAT (subtype holds)" + Colors.RESET);
     }
 
     public static void smtSat(Object counterexample) {
-        if (!enabled()) {
+        if (!smtEnabled()) {
             return;
         }
         String header = SMT_TAG + " Result: " + Colors.RED + "SAT (subtype fails)" + Colors.RESET;
@@ -413,7 +459,7 @@ private static String formatCounterexample(Object counterexample) {
     }
 
     public static void smtUnknown() {
-        if (!enabled()) {
+        if (!smtEnabled()) {
             return;
         }
         System.out.println(SMT_TAG + " Result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET);
@@ -424,7 +470,7 @@ public static void smtUnknown() {
      * 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()) {
+        if (!smtEnabled()) {
             return;
         }
         if (result.isError()) {
@@ -439,7 +485,7 @@ public static void smtResult(liquidjava.smt.SMTResult result) {
      * still responsible for surfacing the user-facing error.
      */
     public static void smtError(String message) {
-        if (!enabled()) {
+        if (!smtEnabled()) {
             return;
         }
         System.out.println(SMT_TAG + " Result: " + Colors.RED + "ERROR" + Colors.RESET + " — "

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -233,7 +233,7 @@ private List<GhostState> filterGhostStatesForVariables(List<GhostState> list, Li
      * chain in place; safe because {@code joinPredicates} returns a clone.
      */
     private void transformChainForDebug(VCImplication chain, List<GhostState> filtered, String[] s, Factory f) {
-        if (!DebugLog.enabled())
+        if (!DebugLog.smtEnabled())
             return;
         for (VCImplication n = chain; n != null; n = n.getNext()) {
             if (n.getRefinement() == null)

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -41,6 +41,7 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
                 Expr<?> e = exp.accept(visitor);
                 Solver solver = tz3.makeSolverForExpression(e);
                 Status result = solver.check();
+                DebugLog.smtRawQuery(toVerify, result.toString());
 
                 // subRef is not a subtype of supRef
                 if (result.equals(Status.SATISFIABLE)) {
@@ -75,7 +76,9 @@ public boolean isUnsatisfiable(Predicate predicate, Context context) throws Exce
                 ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
                 Expr<?> e = exp.accept(visitor);
                 Solver solver = tz3.makeSolverForExpression(e);
-                return solver.check().equals(Status.UNSATISFIABLE);
+                Status result = solver.check();
+                DebugLog.smtRawQuery(predicate, result.toString());
+                return result.equals(Status.UNSATISFIABLE);
             }
         } catch (Z3Exception e) {
             throw new Z3Exception(e.getLocalizedMessage());