Name:           smtlib2
Version:        0.3.1
Author:         Henning Günther <guenther@forsyte.at>
Maintainer:     guenther@forsyte.at
Synopsis:       A type-safe interface to communicate with an SMT solver.
Stability:      provisional
Category:       SMT, Formal Methods, Theorem Provers, Symbolic Computation
License:        GPL-3
License-File:   LICENSE
Build-Type:     Simple
Cabal-Version:  >=1.6

Source-Repository head
  Type:         git
  Location:     https://github.com/hguenther/smtlib2.git

Flag WithConstraints
  Description: Enables the use of the constraint-kind extension which is needed to parse 'map'-expressions.
  Default: True
Flag WithDataKinds
  Description: Enables the use of the data-kinds extension which is needed for typed bitvectors.
  Default: False

Library
  Build-Depends:        base >= 4 && < 5,text,mtl,process,blaze-builder,bytestring,
                        attoparsec,atto-lisp >= 0.2 && < 0.3,array,
                        containers, transformers, data-fix, tagged
  Extensions: GADTs,RankNTypes,CPP,ScopedTypeVariables,
              MultiParamTypeClasses,FlexibleContexts,OverloadedStrings,
              DeriveFunctor,FlexibleInstances,DeriveTraversable,DeriveFoldable,
              DeriveDataTypeable
  GHC-Options: -fcontext-stack=100
  if flag(WithConstraints)
    Build-Depends:      constraints
    CPP-Options: -DSMTLIB2_WITH_CONSTRAINTS
  if flag(WithDataKinds)
    Extensions: DataKinds,PolyKinds
    CPP-Options: -DSMTLIB2_WITH_DATAKINDS
  
  GHC-Options: -fwarn-unused-imports
  Exposed-Modules:
    Language.SMTLib2
    Language.SMTLib2.Solver
    Language.SMTLib2.Connection
    Language.SMTLib2.Internals
    Language.SMTLib2.Internals.Instances
    Language.SMTLib2.Internals.Interface
    Language.SMTLib2.Internals.Optimize
    Language.SMTLib2.Internals.Operators
    Language.SMTLib2.Pipe
    Language.SMTLib2.Strategy
    Data.Unit