Bitbucket is a code hosting site with unlimited public and private repositories. We're also free for small teams!

Close

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.

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

  1. Declare the functions in Z3/Lang/C.hsc.
  2. 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.
  3. Lift the function to the Z3 monad in Z3/Monad.hs, this is trivially done using one of the liftFun helpers.

Recent activity

Iago Abal

Iago Abal pushed 6 commits to iago/z3-haskell

ff421e2 - Improve marshalling support especially when converting lists to C arrays
42dc660 - Replace TypeFamilies with MultiParamTypeClasses in Z3.Base marshalling code
35a142d - Add Z3_mk_exists_comst API call and factorize out marshalling code
e2317b9 - Factorize out marshalling code for mkForall and mkExists
8153ba9 - Newtype wrapping for Z3_bool and Z3_lbool types
Iago Abal

Iago Abal pushed 4 commits to iago/z3-haskell

72afd94 - Minor rewriting: replace `maybe' with `fromMaybe'
f3a0ab6 - Clean up Z3.Opts
b3c3212 - Rewrite support for running scripts under a given environment
8b75734 - Add miscellaneous API function: Z3_get_version
Iago Abal

Iago Abal stripped f121915 from iago/z3-haskell

Run hg strip f12191523c167f24c15bbc70903944bd on your local copy

Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.