Kotlin API for various SMT solvers
Install via JitPack and Gradle
// core
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.1.0")
// z3 solver
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.1.0")See examples
Currently KSMT supports the following SMT solvers:
| SMT Solver | Linux-x64 | Windows-x64 | MacOS-x64 |
|---|---|---|---|
| Z3 | ✔️ | ✔️ | ✔️ |
| Bitwuzla | ✔️ | ✔️ |
KSMT can express formulas in the following theories:
| Theory | Z3 | Bitwuzla |
|---|---|---|
| Bitvectors | ✔️ | ✔️ |
| Arrays | ✔️ | ✔️ |
| IEEE Floats | ✔️ | |
| Uninterpreted Functions | ✔️ | ✔️ |
| Arithmetic | ✔️ |