hz3 alternatives and similar packages
Based on the "Bit Vectors" category.
Alternatively, view hz3 alternatives based on common mentions on social networks and blogs.
Do you think we are missing an alternative of hz3 or a related project?
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.
[Do you want to contribute?](HACKING.md)
State of maintenance
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.
Supported versions and version policy
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> 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 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