z3-408.1: z3.cabal

Name:                z3
Version:             408.1
Synopsis:            Bindings for the Z3 Theorem Prover
Description:
    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.)

Homepage:            https://github.com/IagoAbal/haskell-z3
Bug-reports:         https://github.com/IagoAbal/haskell-z3/issues
License:             BSD3
License-file:        LICENSE
Author:              Iago Abal <mail@iagoabal.eu>,
                     David Castro <david.castro.dcp@gmail.com>
Maintainer:          Iago Abal <mail@iagoabal.eu>
Copyright:           2012-2019, 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: git@github.com:IagoAbal/haskell-z3.git

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
    if impl(ghc < 8)
      Build-depends:     semigroups >= 0.5

    Build-tools:         hsc2hs
    Extensions:          FlexibleInstances
                         FlexibleContexts
                         ForeignFunctionInterface
                         MultiParamTypeClasses

    Other-extensions:    CPP
                         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,
                       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:      base >= 4.5,
                        z3,
                        hspec >= 2.1,
                        QuickCheck >= 2.5.1