Popularity
8.4
Growing
Activity
3.6
Declining
24
4
18

Monthly Downloads: 40
Programming language: Haskell
License: BSD 3-clause "New" or "Revised" License
Tags: Math     Theorem Provers     Bit Vectors     Formal Methods     SMT    
Latest version: v408.0

hz3 alternatives and similar packages

Based on the "Bit Vectors" category

Do you think we are missing an alternative of hz3 or a related project?

Add another 'Bit Vectors' Package

README

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.

[Changelog here.](CHANGES.md)

[Examples here.](examples)

[Do you want to contribute?](HACKING.md)

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

Installation

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.

Example

Most people uses 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