smtlib2

A type-safe interface to communicate with an SMT solver.

Latest on Hackage:1.0

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

GPL-3 licensed by Henning G√ľnther
Maintained by guenther@forsyte.at
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 |
comments powered byDisqus