JavaSMT is a common API layer for accessing various SMT solvers. The API is optimized for performance (using JavaSMT has very little runtime overhead compared to using the solver API directly), customizability (features and settings exposed by various solvers should be visible through the wrapping layer) and type-safety (it shouldn't be possible to add boolean terms to integer ones at compile time) sometimes at the cost of verbosity.
Getting Started | Documentation | Known Issues | Documentation for Developers | Changelog | Configuration Options
- D. Baier, D. Beyer, and K. Friedberger. JavaSMT 3: Interacting with SMT Solvers in Java. In Proc. CAV, LNCS 12760, pages 1-13, 2021. Springer.
- E. G. Karpenkov, K. Friedberger, and D. Beyer. JavaSMT: A Unified Interface for SMT Solvers in Java. In Proc. VSTTE, LNCS 9971, pages 139–148, 2016. Springer.
JavaSMT can express formulas in the following theories:
- Integer
- Rational
- Bitvector
- Floating Point
- Array
- Uninterpreted Function
- String and RegEx
The concrete support for a certain theory depends on the underlying SMT solver. Only a few SMT solvers provide support for theories like Arrays, Floating Point, String or RegEx.
Currently JavaSMT supports several SMT solvers (see Getting Started for installation):
| SMT Solver | Linux64 | Windows64 | MacOS | Description |
|---|---|---|---|---|
| Boolector | ✔️ | a fast solver for bitvector logic, misses formula introspection | ||
| CVC4 | ✔️ | |||
| CVC5 | ✔️ | new! | ||
| MathSAT5 | ✔️ | ✔️ | ||
| OptiMathSAT | ✔️ | based on MathSAT5, with support for optimization | ||
| Princess | ✔️ | ✔️ | ✔️ | Java-based SMT solver |
| SMTInterpol | ✔️ | ✔️ | ✔️ | Java-based SMT solver |
| Yices2 | ✔️ | soon | ||
| Z3 | ✔️ | ✔️ | ✔️ | mature and well-known solver |
The following features are supported (depending on the used SMT solver):
- Satisfiability checking
- Quantifiers and quantifier elimination
- Incremental solving with assumptions
- Incremental solving with push/pop
- Multiple independent contexts
- Model generation
- Interpolation, including tree and sequential structure
- Formula transformation using built-in tactics
- Formula introspection using visitors
We aim for supporting more important features, more SMT solvers, and more systems. If something specific is missing, please look for or file an issue.
| SMT Solver | Concurrent context usage¹ | Concurrent prover usage² |
|---|---|---|
| Boolector | ✔️ | |
| CVC4 | ✔️ | ✔️ |
| CVC5 | ✔️ | |
| MathSAT5 | ✔️ | |
| OptiMathSAT | ✔️ | |
| Princess | ✔️ | |
| SMTInterpol | ✔️ | |
| Yices2 | ||
| Z3 | ✔️ |
Interruption using a ShutdownNotifier may be used to interrupt a a solver from any thread. Formulas are translatable in between contexts/provers/threads using FormulaManager.translateFrom().
¹ Multiple contexts, but all operations on each context only from a single thread. ² Multiple provers on one or more contexts, with each prover using its own thread.
JavaSMT exposes an API for performing garbage collection on solvers implemented in a native language. As a native solver has no way of knowing whether the created formula object is still referenced by the client application, this API is necessary to avoid leaking memory. Note that several solvers already support hash consing and thus, there is never more than one copy of an identical formula object in memory. Consequently, if all created formulas are later re-used (or re-created) in the application, it is not necessary to perform any garbage collection at all.
The parameter solver.z3.usePhantomReferences may be used to control
whether JavaSMT will attempt to decrease references on Z3 formula
objects once they are no longer referenced.
Currently we do not support performing garbage collection for MathSAT5.
Installation is possible via Maven, Ivy, or manually. Please see our Getting Started Guide.
// Instantiate JavaSMT with SMTInterpol as backend (for dependencies cf. documentation)
try (SolverContext context = SolverContextFactory.createSolverContext(
config, logger, shutdownNotifier, Solvers.SMTINTERPOL)) {
IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager();
// Create formula "a = b" with two integer variables
IntegerFormula a = imgr.makeVariable("a");
IntegerFormula b = imgr.makeVariable("b");
BooleanFormula f = imgr.equal(a, b);
// Solve formula, get model, and print variable assignment
try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
prover.addConstraint(f);
boolean isUnsat = prover.isUnsat();
assert !isUnsat;
try (Model model = prover.getModel()) {
System.out.printf("SAT with a = %s, b = %s", model.evaluate(a), model.evaluate(b));
}
}
}- Project maintainers: Karlheinz Friedberger and Philipp Wendler
- Former project maintainer: George Karpenkov
- Initial codebase, many design decisions: Philipp Wendler
- Contributions: Daniel Baier, Thomas Stieglmaier and several others.