# Haskell bindings for Microsoft's Z3 (unofficial)

These are Haskell bindings for the Z3 theorem prover.

A changelog is available here.

## Example

We offer several interfaces to the Z3 API, the most widely used is Z3.Monad, here is an example script that solves the 4-queen puzzle:

script :: Z3 (Maybe [Integer]) script = do intSort <- mkIntSort q1 <- flip mkConst intSort =<< mkStringSymbol "q1" q2 <- flip mkConst intSort =<< mkStringSymbol "q2" q3 <- flip mkConst intSort =<< mkStringSymbol "q3" q4 <- flip mkConst intSort =<< mkStringSymbol "q4" _1 <- mkInt 1 _4 <- mkInt 4 -- the ith-queen is in the ith-row. -- qi is the column of the ith-queen assertCnstr =<< mkAnd =<< T.sequence [mkLe _1 q1, mkLe q1 _4] assertCnstr =<< mkAnd =<< T.sequence [mkLe _1 q2, mkLe q2 _4] assertCnstr =<< mkAnd =<< T.sequence [mkLe _1 q3, mkLe q3 _4] assertCnstr =<< mkAnd =<< T.sequence [mkLe _1 q4, mkLe q4 _4] -- different columns assertCnstr =<< mkDistinct [q1,q2,q3,q4] -- avoid diagonal attacks assertCnstr =<< mkNot =<< diagonal 1 q1 q2 assertCnstr =<< mkNot =<< diagonal 2 q1 q3 assertCnstr =<< mkNot =<< diagonal 3 q1 q4 assertCnstr =<< mkNot =<< diagonal 1 q2 q3 assertCnstr =<< mkNot =<< diagonal 2 q2 q4 assertCnstr =<< mkNot =<< diagonal 1 q3 q4 -- check and get solution fmap snd $ withModel $ \m -> do mb_cs <- evalT m [q1,q2,q3,q4] mapM getInt $ fromJust mb_cs where mkAbs :: AST -> Z3 AST mkAbs x = do _0 <- mkInt 0 join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x diagonal d c c' = join $ mkEq <$> (mkAbs =<< mkSub [c',c]) <*> (mkInt d)

## Installation

Preferably use the z3 package.

- Download and install a
**stable**Z3 release. We don't test this package with unstable versions. -
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

## Contributing

Some modules include a HACKING documentation section at the top that you should read before.

We appreciate your contact before contributing to the project, in order to avoid duplication of work and agree on possible design decisions.

Please follow roughly the same coding style than us.

### Adding support an API function

- Declare the functions in Z3/Lang/C.hsc.
- Lift the function to the IO monad in Z3/Base.hs, there is a bunch of marshalling helpers that should make this trivial in most cases.
- Lift the function to the Z3 monad in Z3/Monad.hs, this is trivially done using one of the
*liftFun*helpers.