# 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.

## Installation

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.

- Otherwise use the

## Example

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