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