The z3 package

[Tags: bsd3, library]

Bindings for the (now open source!) Z3 4.x Theorem Prover (https://github.com/Z3Prover/z3).

Examples: https://bitbucket.org/iago/z3-haskell/src/tip/examples

Changelog: https://bitbucket.org/iago/z3-haskell/src/tip/CHANGES.md

Installation:

(Hackage reports a build failure because Z3's library is missing.)


[Skip to ReadMe]

Properties

Versions0.1.1, 0.2.0, 0.3.0, 0.3.1, 0.3.2, 4.0.0, 4.1.0
Change logCHANGES.md
Dependenciesbase (>=4.5 && <5), containers, mtl (>2.1), z3 (>=0.4) [details]
LicenseBSD3
Copyright2012-2015, Iago Abal, David Castro
AuthorIago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>
MaintainerIago Abal <mail@iagoabal.eu>
CategoryMath, SMT, Theorem Provers, Formal Methods, Bit vectors
Home pagehttp://bitbucket.org/iago/z3-haskell
Source repositoryhead: hg clone https://bitbucket.org/iago/z3-haskell
Executablesexamples
UploadedSat Jul 18 21:30:04 UTC 2015 by IagoAbal
DistributionsNixOS:4.1.0
Downloads1084 total (75 in last 30 days)
Votes
0 []
StatusDocs uploaded by user
Build status unknown [no reports yet]

Modules

[Index]

Flags

NameDescriptionDefault
examplesBuild examples.Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainers' corner

For package maintainers and hackage trustees

Readme for z3-4.1.0

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.

Examples here.

Do you want to contribute?

Installation

Preferably use the z3 package.

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 = evalZ3With Nothing opts script >>= \mbSol ->
        case mbSol of
             Nothing  -> error "No solution found."
             Just sol -> putStr "Solution: " >> print sol
  where opts = opt "MODEL" True +? opt "MODEL_COMPLETION" True