Name:                hz3
Version:             96.0.0.0
x-revision: 3
Synopsis:            Bindings for the Z3 Theorem Prover
Description:
    Fork of <https://hackage.haskell.org/package/z3 z3> with future-proof version-numbering scheme
    .
    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/strake/z3.hs/tree/master/examples>
    .
    Changelog: <https://github.com/strake/z3.hs/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.)

Homepage:            https://github.com/strake/z3.hs
Bug-reports:         https://github.com/strake/z3.hs
License:             BSD3
License-file:        LICENSE
Author:              Iago Abal <mail@iagoabal.eu>,
                     David Castro <david.castro.dcp@gmail.com>
Maintainer:          None
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:     git
  location: https://github.com/strake/z3.hs

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 <<loop>> in mtl-2.1
    Build-depends:       base >= 4.5 && <5,
                         containers,
                         transformers >= 0.2

    Build-tools:         hsc2hs
    Extensions:          FlexibleInstances
                         FlexibleContexts
                         ForeignFunctionInterface
                         MultiParamTypeClasses

    Other-extensions:    CPP
                         DeriveDataTypeable
                         EmptyDataDecls
                         GeneralizedNewtypeDeriving
                         PatternGuards

    includes:            z3.h

    extra-libraries:     z3

Flag examples
     Description: Build examples.
     Default: False
     Manual: True

Executable examples
  if flag(examples)
    Buildable:         True
    Build-depends:     hz3,
                       base >=4.5,
                       containers,
                       transformers >= 0.2
  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.MutuallyRecursive
                       Example.Monad.ParserInterface
                       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:      hz3,
                        base >= 4.5,
                        hspec >= 2.1,
                        QuickCheck >= 2.5.1