Provide JavaSMT main to execute as solver for SMT-COMP

[gcarpio21]

Command-line interface for running JavaSMT

Adds a command-line interface so that JavaSMT can be run like a regular SMT solver on a single SMT-LIB 2 file, e.g., for SMT-COMP or for benchmarking the solvers behind JavaSMT with BenchExec.

$ javasmt --solver z3 benchmark.smt2
sat

JavaSMTMain parses the assertions with FormulaManager.parseAll, checks them in one ProverEnvironment, and prints exactly one of sat, unsat, or unknown on stdout; diagnostics got to stderr. --solver selects the solver (default SMTInterpol), --logic is forwarded to OpenSMT. The launcher javasmt in the project root builds the classpath from bin/ or the JAR and all solver runtimes, passes -X* arguments to the JVM, and shares its Java version check and platform handling with runExamples.sh.

• Input without (check-sat) is rejected.
• Unparsable input and solvers without a parser (Yices2) are reported with a message on stderr. Unexpected exceptions terminate the program with a stack trace, so that a benchmarking framework can report the exception class.
• Ctrl+C and SIGTERM request a shutdown from the solver via a JVM shutdown hook; unknown is reported and the solver is closed. Solvers that do not respond get a grace period of 10 s.
• parseAll runs before the ProverEnvironment is created, because Princess does not register symbols declared after its prover exists.

JavaSMTMainTest covers the argument parsing and the whole interface in-process with SMTInterpol and Princess, including all error cases and shutdown requests before and during solving; one test runs main in a separate JVM and sends SIGTERM.

[baierd]

We should not silently ignore all input that we can't and don't want to handle.
This includes 2 categories:

• malformed/illegal input. For example (check-sat-garbage) and (check-sat 1) are currently accepted.
• unsupported input. check-sat-assuming is not supported by parseAll, and is silently ignored.

Most of this is a problem that should be tackled by parseAll in my opinion. @daniel-raffler would you be so kind and open a issue to track this problem, and add unit tests for all allowed SMTLIB2 commands, including malformed ones, e.g. with more arguments than allowed, arguments before the command etc. Then improve the state-machine in parseAll to throw for unsupported or malformed input as long as it can change results. Example:

(declare-fun p () Bool)
(assert p)
(check-sat-assuming ((not p)))

Is UNSAT, but we return SAT currently.

@gcarpio21 what must be blocked are all pop and all resetting commands for now, as we do not properly track assertion stacks through parseAll and also ignore resets. Please add a TODO that explains the problem and that we add it later. (exit) should also throw, except for if its the very last command.

[daniel-raffler]

Hello Daniel,

We should not silently ignore all input that we can't and don't want to handle. This includes 2 categories:

* malformed/illegal input. For example `(check-sat-garbage)` and `(check-sat 1)` are currently accepted.

* unsupported input. `check-sat-assuming` is not supported by `parseAll`, and is silently ignored.

Most of this is a problem that should be tackled by parseAll in my opinion

I did some work on this a while ago, and there is an open PR here that should at least take case of your first point about illegal inputs

If we want to support commands like check-sat-assuming, pop or exit, I think it would be easiest to write a proper parser with ANTLR. The tokenizer is more of a stop-gap solution that works well enough for parsing simple formulas, but it was never meant to execute entire SMTLIB scripts

[baierd]

ANTLR may be overkill for what we want.

I opened a issue for this here, lets discuss it there.

[gcarpio21]

JavaSMTMain.checkScript now rejects (push ...), (pop ...), (reset) and (reset-assertions), any (exit) that is not the last command, anything that looks like (check-sat) but is not exactly (check-sat), and text outside a command, which the tokenizer would otherwise drop. (push ...) is included because the tokenizer's isForbiddenToken covers it and parseAll fails on it anyway.

[baierd]

Nice job!
We only need to work out some minor points before merging this.

Could you please also add a --help command that explains restrictions and allowed arguments?

[baierd]

This is currently incorrect.
Sat checks should be performed for each and every (check-sat) command. We currently perform one giant SAT check, but this violates SMTLIB2.

I propose to only allow ONE (check-sat) (i.e. use parse instead of parseAll) for now. And extend it later on.

[gcarpio21]

I kept parseAll for now. parse delegates to parseAll and then throws unless the query contains exactly one assertion. The restriction is instead enforced in JavaSMTMain.checkScript before parsing: exactly one (check-sat), no (assert ...) after it.

[baierd]

Please do not use shorthand if-then-else. They are hard to read and provide no benefit at all.

String reason = "";
if (shutdownNotifier.shouldShutdown()) {
  reason = shutdownNotifier.getReason();
}

Is much easier to read.

[PhilippWendler]

I disagree. Having a single point of assignment is typically easier to follow (less mutable state) and allows variables to be final.

[baierd]

Fair point.
But that is also quite easy.

final String reason;
if (shutdownNotifier.shouldShutdown()) {
  reason = shutdownNotifier.getReason();
} else {
  reason = "";
}

[gcarpio21]

Fair point. But that is also quite easy.

final String reason;
if (shutdownNotifier.shouldShutdown()) {
  reason = shutdownNotifier.getReason();
} else {
  reason = "";
}

I decided to replace the shorthands with this suggestion.

[baierd]

While PrintStream does not swallow IOExceptions from Appendables, System.out and System.err record these failures internally, and flushing does not report them. Thus result delivery can fail while the process reports success. Better: after the existing flushes, check both streams with checkError() and change the exit status to ERROR_EXIT_CODE on failure.

Also, redirect the launchers JVM-probe failure messages to stderr using >&2; that branch currently uses plain echo on stdout.

@PhilippWendler why are we using PrintStream in CPAchecker?

[PhilippWendler]

For example because we do not want to stop proceeding through all the code for statistics and output files if there is an I/O error for the statistics output.

[baierd]

Makes sense. Thanks for the explanation.
The question now is whether we should use PrintStream or not here as well. Do you have a strong opinion on that @PhilippWendler ?

[PhilippWendler]

This depends a lot on the use case. For I/O in most cases it is bad, but for particular situations it can be ok.

[baierd]

Please avoid Arrays.asList() (and most other default toList, asList etc. methods). Take a look at CPAcheckers StyleGuide for why and for alternatives. In this case, just use ImmutableList.of(pArgs).

[PhilippWendler]

CPAchecker's style guide definitively does not forbid Arrays.asList(), and I wouldn't know what "default toList, asList methods" are.

[baierd]

My bad, i was a little over-eager here.
Collectors.toList() should be avoided.

The code can be improved either way by using Guavas utilities from its Iterators class;
Iterator<String> argsIt = Iterators.forArray(pArgs);

[gcarpio21]

Nice job! We only need to work out some minor points before merging this.

Could you please also add a --help command that explains restrictions and allowed arguments?

the --help command is now expanded to do this.

[gcarpio21]

The main purpose of this command-line interface and the javasmt launcher is to benchmark JavaSMT with BenchExec on the SMT-COMP benchmarks, i.e., the non-incremental benchmarks of SMT-LIB 2025, using the tool-info module from sosy-lab/benchexec#1317. This is how I set up my benchmarks; none of the files described here are part of this branch.

Expected answers (task-definition files)

BenchExec only judges a result as correct or wrong if the task is given as a task-definition file (YAML) that states an expected verdict for the property file named in the benchmark definition (benchexec.md); plain input files are executed without checking the result (properties.md). Each task-definition file has exactly one set of input files (INDEX.md), so each benchmark needs its own.

SMT-LIB stores the expected answer inside each benchmark as (set-info :status …). I wrote a Python script that walks the benchmark directory recursively and writes one YAML file next to each .smt2 file, 450,472 in total. It works the same way as SMT-COMP's own setup for BenchExec (scramble_benchmarks.py, benchexec.py):

• sat becomes expected_verdict: true and unsat becomes expected_verdict: false, matching the tool-info, which reports sat as true and unsat as false.
• unknown gets no expected verdict, because it means that the answer is not known (SMT-LIB standard 2.7, p. 74). BenchExec counts a sat or unsat answer on these as "missing", neither correct nor wrong. SMT-COMP instead scores such an answer as correct (rules 2025, §7.1.2, footnote 4), which BenchExec cannot express, because an expected verdict can only be true or false.
• All YAML files refer to the same property file, smt.prp. Its content does not matter.
• Each YAML file is named after its path below the benchmark directory (e.g. QF_LIA-20210219-Dartagnan-…-03_incdec-O0.yml). SMT-LIB reuses file names across directories, and BenchExec names log files after the task-definition file, so equal names would break the results.

Benchmark definition

The benchmark definition (XML) uses tool="javasmt" and <propertyfile>smt.prp</propertyfile>, with the same limits for every run (5 min CPU time, 4 GB memory). It has one run definition per solver (smtinterpol, princess, z3, cvc5, cvc4, boolector, mathsat5, yices2, opensmt), which differ only in --solver, and one task set per logic (89 in total). With -r (run definition) and -t (task set) any combination can be chosen, e.g. -r z3 -t QF_LIA for z3 on QF_LIA only, -r z3 for z3 on all logics, or nothing for all solvers on all logics.

Results

On the Cloud, QF_LIA worked with z3 alone and with all nine solvers (13,306 tasks, 119,754 runs), and the tables from table-generator show the correct and wrong results per solver. For the full set, BenchExec found all task-definition files and their input files, but because of the number of files no results were written.

Proposal

Since this setup works, I think it would be useful to add the benchmark definition, the property file, and the script to this PR, so that others can benchmark JavaSMT the same way. The YAML files themselves would not be added, as the script generates them from the SMT-LIB release.