This library provides a pure haskell interface to many SMT solvers by implementing the SMTLib2 language. SMT solving is done by spawning a SMT solver process and communicating with it.
- Communication via the SMTLIB2-format with solvers who support it (Currently Z3, MathSAT and CVC4).
- Native bindings for solvers without a (proper) SMTLIB2 interface (Currently stp, boolector and yices).
- Supports haskell data types (automatic instance generation available via template-haskell).
To install this package, you need cabal-install. The first package to install must be “smtlib2”:
cabal installAfter this, you can install the extra packages in whatever order you wish.
| Package | Location |
|---|---|
| smtlib2-th | extras/th |
| smtlib2-stp | backends/stp |
| smtlib2-boolector | backends/boolector |
| smtlib2-yices | backends/yices |
For the moment, only Z3 supports every feature implemented in this interface. MathSAT implements most features, except for data types.
| Solver | Version | SMTLib2 format | Bitvectors | Integer | Enumerations | Datatypes |
|---|---|---|---|---|---|---|
| Z3 | 4.3 | yes | yes | yes | yes | yes |
| MathSAT | 5.2.10 | yes | yes | yes | no | no |
| STP | incomplete | yes | no | no | no | |
| Yices | 2.1.0 | no | yes | yes | yes | no |
| Boolector | 1.6.0 | incomplete | yes | no | no | no |
| CVC4 | 1.4 | yes | yes | yes | no | yes |