z3: Bindings for the Z3 Theorem Prover

[ bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers ] [ Propose Tags ]

Bindings for the Z3 4.x Theorem Prover (https://github.com/Z3Prover/z3).

Examples: https://github.com/IagoAbal/haskell-z3/tree/master/examples

Changelog: https://github.com/IagoAbal/haskell-z3/blob/master/CHANGES.md


(Hackage reports a build failure because Z3's library is missing.)

[Skip to Readme]
Versions [faq] 0.1.1, 0.2.0, 0.3.0, 0.3.1, 0.3.2, 4.0.0, 4.1.0, 4.1.1, 4.1.2, 4.2.0, 4.3, 4.3.1, 408.0, 408.1, 408.2
Change log CHANGES.md
Dependencies base (>=4.5 && <5), containers, transformers (>=0.2) [details]
License BSD-3-Clause
Copyright 2012-2018, Iago Abal, David Castro
Author Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>
Maintainer Iago Abal <mail@iagoabal.eu>
Category Math, SMT, Theorem Provers, Formal Methods, Bit vectors
Home page https://github.com/IagoAbal/haskell-z3
Bug tracker https://github.com/IagoAbal/haskell-z3/issues
Source repo head: git clone git@github.com:IagoAbal/haskell-z3.git
Uploaded by IagoAbal at 2019-03-31T20:33:23Z
Distributions NixOS:408.2
Executables examples
Downloads 9028 total (29 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs uploaded by user
Build status unknown [no reports yet]





Build examples.


Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info


Maintainer's Corner

For package maintainers and hackage trustees

Readme for z3-408.0

[back to package description]

Haskell bindings for Microsoft's Z3 (unofficial)

These are Haskell bindings for the Z3 theorem prover. We don't provide any high-level interface (e.g. in the form of a Haskell eDSL) here, these bindings are targeted to those who want to build verification tools on top of Z3 in Haskell.

Changelog here.

Examples here.

Do you want to contribute?

Supported versions and version policy

Z3 releases come out often and sometimes introduce backwards incompatible changes. In order to avoid #ifdef-ery, we only try to support a reasonably recent version of Z3, ideally the latest one. We use semantic versioning to reflect which version(s) are supported:


The <z3-version> indicates which version of Z3 is supported, it is computed as _x*100+y_ for Z3 x.y. For example, versions 408.y.z of these bindings are meant to support versions _4.8.*_ of Z3. This version policy is in line with Haskell's PVP.


Preferably use the z3 package.

  • Install a Z3 4.x release. (Support for Z3 3.x is provided by the 0.3.2 version of these bindings.)

  • Just type cabal install z3 if you used the standard locations for dynamic libraries (/usr/lib) and header files (/usr/include).

    • Otherwise use the --extra-lib-dirs and --extra-include-dirs Cabal flags when installing.


Most people uses the Z3.Monad interface. Here is an example script that solves the 4-queen puzzle:

import Control.Applicative
import Control.Monad ( join )
import Data.Maybe
import qualified Data.Traversable as T

import Z3.Monad

script :: Z3 (Maybe [Integer])
script = do
  q1 <- mkFreshIntVar "q1"
  q2 <- mkFreshIntVar "q2"
  q3 <- mkFreshIntVar "q3"
  q4 <- mkFreshIntVar "q4"
  _1 <- mkInteger 1
  _4 <- mkInteger 4
  -- the ith-queen is in the ith-row.
  -- qi is the column of the ith-queen
  assert =<< mkAnd =<< T.sequence
    [ mkLe _1 q1, mkLe q1 _4  -- 1 <= q1 <= 4
    , mkLe _1 q2, mkLe q2 _4
    , mkLe _1 q3, mkLe q3 _4
    , mkLe _1 q4, mkLe q4 _4
  -- different columns
  assert =<< mkDistinct [q1,q2,q3,q4]
  -- avoid diagonal attacks
  assert =<< mkNot =<< mkOr =<< T.sequence
    [ diagonal 1 q1 q2  -- diagonal line of attack between q1 and q2
    , diagonal 2 q1 q3
    , diagonal 3 q1 q4
    , diagonal 1 q2 q3
    , diagonal 2 q2 q4
    , diagonal 1 q3 q4
  -- check and get solution
  fmap snd $ withModel $ \m ->
    catMaybes <$> mapM (evalInt m) [q1,q2,q3,q4]
  where mkAbs x = do
          _0 <- mkInteger 0
          join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x
        diagonal d c c' =
          join $ mkEq <$> (mkAbs =<< mkSub [c',c]) <*> (mkInteger d)

In order to run this SMT script:

main :: IO ()
main = evalZ3 script >>= \mbSol ->
        case mbSol of
             Nothing  -> error "No solution found."
             Just sol -> putStr "Solution: " >> print sol