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.
The library is currently "maintained", meaning that I try to be responsive to new issues and pull requests. Unfortunately I do not have time to investigate issues or to do major work myself. I do try to help those who want to contribute.
If someone demonstrates willingness to maintain the library more actively in the long run, then I will be very happy to give the required permissions to become a co-maintainer. In the meantime I will do my best to keep it alive.
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:
<z3-version>.<bindings-version>[.<patch-level>]
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 use 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