Name: z3 Version: 4.2.0 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the Z3 4./x/ Theorem Prover (). . * "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: . Changelog: . 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.) Homepage: http://bitbucket.org/iago/z3-haskell License: BSD3 License-file: LICENSE Author: Iago Abal , David Castro Maintainer: Iago Abal Copyright: 2012-2018, Iago Abal, David Castro Category: Math, SMT, Theorem Provers, Formal Methods, Bit vectors Build-type: Simple Cabal-version: >= 1.8 Extra-source-files: README.md CHANGES.md HACKING.md source-repository head type: mercurial location: https://bitbucket.org/iago/z3-haskell Library hs-source-dirs: src Exposed-modules: Z3.Base Z3.Base.C Z3.Opts Z3.Monad -- TODO: Add flag to compile with -Werror, Hackage doesn't like it. ghc-options: -Wall -- Ban to mtl-2.1: modify in MonadState causes <> in mtl-2.1 Build-depends: base >= 4.5 && <5, containers, mtl > 2.1 Build-tools: hsc2hs Extensions: FlexibleInstances FlexibleContexts ForeignFunctionInterface MultiParamTypeClasses Other-extensions: DeriveDataTypeable EmptyDataDecls GeneralizedNewtypeDeriving PatternGuards includes: z3.h -- In OS X libz3 is linked statically against libgomp. -- In Windows Z3 is compiled using MS C++. if os(darwin) || os(windows) extra-libraries: z3 else extra-libraries: gomp z3 gomp Flag examples Description: Build examples. Default: False Manual: True Executable examples if flag(examples) Buildable: True Build-depends: base >=4.5, z3 >=0.4, containers, mtl >2.1 else Buildable: False Hs-source-dirs: examples Main-Is: Examples.hs Other-Modules: Example.Monad.Queens4 Example.Monad.Queens4All Example.Monad.DataTypes Example.Monad.FuncModel Example.Monad.Interpolation Example.Monad.MutuallyRecursive Example.Monad.Quantifiers Example.Monad.QuantifierElimination Example.Monad.ToSMTLib Example.Monad.Tuple Test-suite spec Type: exitcode-stdio-1.0 Ghc-options: -Wall Extensions: ScopedTypeVariables Hs-source-dirs: test Main-is: Spec.hs Other-modules: Z3.Base.Spec Build-depends: base >= 4.5, z3, hspec >= 2.1, QuickCheck >= 2.5.1