Meet the unified Kotlin/Java API for various SMT solvers.
Get the most out of SMT solving with KSMT features:
- Supporting more solvers and theories — for all popular operating systems
- Solver-agnostic formula representation and easy-to-use DSL
- Utilities to simplify and transform your expressions
- Switching between solvers and support for portfolio mode
- Running solvers in a separate process to reduce timeout-related crashes
- Streamlined solver delivery with no need for building a solver or implementing JVM bindings
To start using KSMT, install it via Gradle:
// core
implementation("io.ksmt:ksmt-core:0.5.4")
// z3 solver
implementation("io.ksmt:ksmt-z3:0.5.4")Find basic instructions in the Getting started guide and try it out with the Kotlin or Java examples.
To go beyond the basic scenarios, proceed to the Advanced usage guide and try the advanced example.
To get guided experience in KSMT, step through the detailed scenario for creating custom expressions.
Check the Roadmap to know more about current feature support and plans for the nearest future.
KSMT provides support for various solvers:
| SMT solver | Linux-x64 | Windows-x64 | macOS-aarch64 | macOS-x64 |
|---|---|---|---|---|
| Z3 | ✔️ | ✔️ | ✔️ | ✔️ |
| Bitwuzla | ✔️ | ✔️ | ✔️ | |
| Yices2 | ✔️ | ✔️ | ✔️ | |
| cvc5 | ✔️ | ✔️ | ✔️ |
You can also use SMT solvers across multiple theories:
| Theory | Z3 | Bitwuzla | Yices2 | cvc5 |
|---|---|---|---|---|
| Bitvectors | ✔️ | ✔️ | ✔️ | ✔️ |
| Arrays | ✔️ | ✔️ | ✔️ | ✔️ |
| IEEE Floats | ✔️ | ✔️ | ✔️ | |
| Uninterpreted Functions | ✔️ | ✔️ | ✔️ | ✔️ |
| Arithmetic | ✔️ | ✔️ | ✔️ |
Various scenarios are available for using SMT solvers: you can use a single solver to determine whether a formula is satisfiable, or you can apply several solvers to the same expression successively. In the latter case, you need a solver-agnostic formula representation.
We implemented it in KSMT, so you can
- transform expressions from the solver native representation to KSMT representation and vice versa,
- use formula introspection,
- manipulate expressions without involving a solver,
- use expressions even if the solver is freed.
Expression interning (hash consing) affords faster expression comparison: we do not need to compare the expression trees. Expressions are deduplicated, so we avoid redundant memory allocation.
KSMT provides you with a unified DSL for SMT expressions:
val array by mkArraySort(intSort, intSort)
val index by intSort
val value by intSort
val expr = (array.select(index - 1.expr) lt value) and
(array.select(index + 1.expr) gt value)KSMT provides a simplification engine applicable to all supported expressions for all supported theories:
- reduce expression size and complexity
- evaluate expressions (including those with free variables) — reduce your expression to a constant
- perform formula transformations
- substitute expressions
KSMT simplification engine implements more than 200 rules. By default, it attempts to apply simplifications when you create the expressions, but you can turn this feature off, if necessary. You can also simplify an arbitrary expression manually.
SMT solvers may differ in performance across different formulas: see the International Satisfiability Modulo Theories Competition.
With KSMT portfolio solving, you can run multiple solvers in parallel on the same formula — until you get the first (the fastest) result.
For detailed instructions on running multiple solvers, see Advanced usage.
Most of the SMT solvers are research projects — they are implemented via native libraries and are sometimes not production ready:
- they may ignore timeouts — they sometimes hang in a long-running operation, and you cannot interrupt it;
- they may suddenly crash interrupting the entire process — because of a pointer issue, for example.
KSMT runs each solver in a separate process, which adds to stability of your application and provides support for portfolio mode.
Many solvers do not have prebuilt binaries, or binaries are for Linux only.
KSMT is distributed as JVM library with solver binaries provided. The library has been tested against the SMT-LIB benchmarks. Documentation and examples are also available.