This library provides a pure haskell interface to many SMT solvers by implementing the [[http://www.smtlib.org/][SMTLib2 language]]. SMT solving is done by spawning a SMT solver process and communicating with it.

• Features

  • 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).

• Installation To install this package, you need [[http://www.haskell.org/haskellwiki/Cabal-Install][cabal-install]]. The first package to install must be "smtlib2":

  +BEGIN_SRC sh

  cabal install

  +END_SRC

  After 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 |

• Supported solvers For the moment, only [[http://research.microsoft.com/en-us/um/redmond/projects/z3/][Z3]] supports every feature implemented in this interface. [[http://mathsat4.disi.unitn.it/][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 |