Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
CatarinaGamboa wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

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

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a684f45
Change flag to dump context info
CatarinaGamboa Jun 9, 2026
baefe3d
Flag all shows both context and the debug info
CatarinaGamboa Jun 13, 2026
e593f79
less changes in utils
CatarinaGamboa Jun 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Flag all shows both context and the debug info
  • Loading branch information
@CatarinaGamboa
CatarinaGamboa committed Jun 13, 2026
commit baefe3d4ada87bfcaacd330e29099ef44fd56a85
4 changes: 2 additions & 2 deletions liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ public class CommandLineArgs {
@Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output")
public boolean debugMode;

@Option(names = { "-a", "--all-context" }, description = "Print the full context after every checked element")
public boolean printContext;
@Option(names = { "-a", "--all" }, description = "Print the full context plus the debug trace (implies -d)")
public boolean all;

@Option(names = { "-lsp", "--language-server" }, description = "Enable language server mode for editor support")
public boolean lspMode;
Expand Down
16 changes: 3 additions & 13 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@
import java.util.List;
import liquidjava.api.CommandLineLauncher;
import liquidjava.processor.VCImplication;
import liquidjava.processor.context.Context;
import liquidjava.processor.context.ContextHistory;
import liquidjava.rj_language.Predicate;
import liquidjava.rj_language.ast.BinaryExpression;
import liquidjava.rj_language.ast.Expression;
Expand Down Expand Up @@ -38,12 +36,12 @@ private DebugLog() {
}

public static boolean enabled() {
return CommandLineLauncher.cmdArgs.debugMode;
return CommandLineLauncher.cmdArgs.debugMode || CommandLineLauncher.cmdArgs.all;
}

/** Gate for the full-context dump, driven by the {@code -a} / {@code --all-context} flag (independent of debug). */
/** Gate for the full-context dump, driven by the {@code -a} / {@code --all} flag (the verbose tier of debug). */
public static boolean contextEnabled() {
return CommandLineLauncher.cmdArgs.printContext;
return CommandLineLauncher.cmdArgs.all;
}

/**
Expand Down Expand Up @@ -473,12 +471,4 @@ public static void contextAtElement(CtElement element, String contextInfo) {
System.out.println(header);
System.out.println(contextInfo);
}

public static void log(String string) {
if (!enabled()) {
return;
}
System.out.println(string);

}
}
5 changes: 2 additions & 3 deletions liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,7 @@ public void clearHistory() {
}

public void saveContext(CtElement element, Context context) {
if (!CommandLineLauncher.cmdArgs.lspMode && !CommandLineLauncher.cmdArgs.debugMode
&& !CommandLineLauncher.cmdArgs.printContext)
if (!CommandLineLauncher.cmdArgs.lspMode && !CommandLineLauncher.cmdArgs.all)
return;

String file = Utils.getFile(element);
Expand All @@ -67,7 +66,7 @@ public void saveContext(CtElement element, Context context) {
aliases.addAll(context.getAliases());
methods.addAll(context.getCtxFunctions());

// Gate lives inside DebugLog.contextAtElement (-a / --all-context); no-op unless that flag is set.
// Gate lives inside DebugLog.contextAtElement (-a / --all); no-op unless that flag is set.
DebugLog.contextAtElement(element, prettyPrint());
}

Expand Down
8 changes: 4 additions & 4 deletions ...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,10 +75,10 @@ public RefinementTypeChecker(Context context, Factory factory) {
// --------------------- Visitors -----------------------------------

/**
* Under {@code -a} / {@code --all-context}, dump the context after every top-level statement. {@code super.scan}
* runs the full {@code visitCtXxx} override first, so the statement's refinement effect is already applied to the
* context by the time we save it. The {@code STATEMENT} role filter keeps this to actual statements (direct block /
* case children), skipping sub-expressions like the {@code g(x)} in {@code f(g(x))}.
* Under {@code -a} / {@code --all}, dump the context after every top-level statement. {@code super.scan} runs the
* full {@code visitCtXxx} override first, so the statement's refinement effect is already applied to the context by
* the time we save it. The {@code STATEMENT} role filter keeps this to actual statements (direct block / case
* children), skipping sub-expressions like the {@code g(x)} in {@code f(g(x))}.
*/
@Override
public void scan(CtElement element) {
Expand Down
Loading