SMTLib2 interface implementation for Haskell
Haskell Other
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Language
backends
examples
extras
.gitignore
.travis.yml
LICENSE
README.org
install_all.sh
smtlib2.cabal
stack.yaml

README.org

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.

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 cabal-install. The first package to install must be “smtlib2”:

cabal install

After this, you can install the extra packages in whatever order you wish.

PackageLocation
smtlib2-thextras/th
smtlib2-stpbackends/stp
smtlib2-boolectorbackends/boolector
smtlib2-yicesbackends/yices

Supported solvers

For the moment, only Z3 supports every feature implemented in this interface. MathSAT implements most features, except for data types.

SolverVersionSMTLib2 formatBitvectorsIntegerEnumerationsDatatypes
Z34.3yesyesyesyesyes
MathSAT5.2.10yesyesyesnono
STPincompleteyesnonono
Yices2.1.0noyesyesyesno
Boolector1.6.0incompleteyesnonono
CVC41.4yesyesyesnoyes