Skip to content

hgoes/smtlib2

Repository files navigation

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

About

SMTLib2 interface implementation for Haskell

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages