z3

Bindings for the Z3 Theorem Prover

https://github.com/IagoAbal/haskell-z3

Latest on Hackage:408.2

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

BSD-3-Clause licensed by Iago Abal, David Castro
Maintained by Iago Abal

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

  • Z3.Base.C provides the raw foreign imports from Z3's C API.

  • Z3.Base does the marshaling of values between Haskell and C, and transparently handles reference counting of Z3 objects for you.

  • Z3.Monad provides a convenient monadic wrapper for the common usage scenario.

Examples: https://github.com/IagoAbal/haskell-z3/tree/master/examples

Changelog: https://github.com/IagoAbal/haskell-z3/blob/master/CHANGES.md

Installation:

  • Unix-like: Just be sure to use the standard locations for dynamic libraries (/usr/lib) and header files (/usr/include), or else use the --extra-lib-dirs and --extra-include-dirs Cabal flags.

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