Many-SMT

This is an SMT-LIB frontend that runs multiple backend solvers in parallel, returning the first result. Like an ordinary SMT-LIB solver, it accepts SMT-LIB v2.6 input on stdin and writes output to stdout.

Currently, Many-SMT knows how to use Boolector, CVC4, CVC5, Yices, and Z3. It can be extended with additional solvers using environment variables; run with --doc for extended documentation on how.

Pull requests are welcome!

Use/Install

The script requires Python 3. It has no dependencies beyond the Python 3 standard libraries.

The script is small enough to be entirely self-contained. You can use it directly out of this folder:

./many-smt <test.smt2

Or install it by copying it to a folder on your PATH.

For a quick usage summary, pass --help:

./many-smt --help

For extended documentation, pass --doc:

./many-smt --doc

Details and Caveats

On startup, Many-SMT spawns multiple solver processes. Using separate processes has advantages over using libraries:

• ManySMT is insulated from memory corruption and resource leaks in the underlying solvers.
• ManySMT discovers available solvers dynamically, and requires no configuration or compilation.
• ManySMT itself is single-threaded and very simple. It uses I/O multiplexing to interact with multiple solvers concurrently.

When you write a complete command to stdin, Many-SMT broadcasts that command to all the underlying solvers. Solvers that return an error are killed, and others continue running. When this happens, Many-SMT writes a message to stderr to help you diagnose the problem. Many-SMT returns an error when no more solvers are left running.

Some commands are handled specially:

• (check-sat) and (check-sat-assuming ...) are sent to all solvers, but ManySMT returns as quickly as possible the first non-unknown non-error output by any of them. The other solvers are quietly interrupted (using SIGKILL, restart, and replay).
• Inspection commands (get-value, get-assignment, get-model, get-unsat-assumptions, get-proof, and get-unsat-core) are only sent to the solver that returned from the most recent (check-sat*) command. That solver's output is returned unaltered. Because different solvers output models in different formats, the output of these commands can be surprising!

Different solvers have different default sets of options. For example, CVC4 starts with :produce-models false while Z3 starts with it true. It is a good idea to explicitly set options to insulate yourself from these differences.

Similar Projects

metaSMT abstracts over multiple solvers, but it is a library and not a tool that takes SMT-LIB input.

Par4 is exactly the same idea, but does not seem to be publicly available.

Poolector is exactly the same idea, but only runs instances of the Boolector solver and does not support interaction.

PySMT can invoke multiple solvers in parallel (see "portfolio solving").