cabal-version:         3.0

name:                  hasmtlib
version:               2.5.1
synopsis:              A monad for interfacing with external SMT solvers
description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
  It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
  It is highly inspired by ekmett/ersatz which does the same for QSAT.
  Communication with external solvers is handled by tweag/smtlib-backends.
homepage:              https://github.com/bruderj15/Hasmtlib
bug-reports:           https://github.com/bruderj15/Hasmtlib/issues
license:               GPL-3.0-only
license-file:          LICENSE
author:                Julian Bruder
maintainer:            julian.bruder@outlook.com
copyright:             © 2024 Julian Bruder
category:              SMT, Logic
build-type:            Simple
extra-source-files:    README.md
extra-doc-files:       CHANGELOG.md
tested-with:           GHC == 9.4.8
                     , GHC == 9.6.4
                     , GHC == 9.8.2

library
  hs-source-dirs:      src
  default-language:    GHC2021
  default-extensions:  DataKinds, GADTs, TypeFamilies, OverloadedStrings

  exposed-modules:     Language.Hasmtlib
                     , Language.Hasmtlib.Codec
                     , Language.Hasmtlib.Boolean
                     , Language.Hasmtlib.Variable
                     , Language.Hasmtlib.Counting
                     , Language.Hasmtlib.Internal.Parser
                     , Language.Hasmtlib.Internal.Bitvec
                     , Language.Hasmtlib.Internal.Render
                     , Language.Hasmtlib.Internal.Sharing
                     , Language.Hasmtlib.Internal.Uniplate1
                     , Language.Hasmtlib.Internal.Constraint
                     , Language.Hasmtlib.Solver.Common
                     , Language.Hasmtlib.Solver.Bitwuzla
                     , Language.Hasmtlib.Solver.CVC5
                     , Language.Hasmtlib.Solver.MathSAT
                     , Language.Hasmtlib.Solver.OpenSMT
                     , Language.Hasmtlib.Solver.Yices
                     , Language.Hasmtlib.Solver.Z3
                     , Language.Hasmtlib.Type.Expr
                     , Language.Hasmtlib.Type.Value
                     , Language.Hasmtlib.Type.MonadSMT
                     , Language.Hasmtlib.Type.SMT
                     , Language.Hasmtlib.Type.OMT
                     , Language.Hasmtlib.Type.Pipe
                     , Language.Hasmtlib.Type.SMTSort
                     , Language.Hasmtlib.Type.Solution
                     , Language.Hasmtlib.Type.Solver
                     , Language.Hasmtlib.Type.Option
                     , Language.Hasmtlib.Type.ArrayMap

  build-depends:       attoparsec                   >= 0.14.4 && < 1
                     , base                         >= 4.17.2 && < 5
                     , bytestring                   >= 0.11.5 && < 1
                     , containers                   >= 0.6.7  && < 1
                     , unordered-containers         >= 0.2.20 && < 0.3
                     , dependent-map                >= 0.4    && < 1
                     , mtl                          >= 2.2.2  && < 3
                     , text                         >= 2.0.2  && < 3
                     , data-default                 >= 0.7.1  && < 1
                     , lens                         >= 5      && < 6
                     , smtlib-backends              >= 0.4    && < 0.5
                     , smtlib-backends-process      >= 0.3    && < 0.4
                     , some                         >= 1.0.6  && < 1.1
                     , utf8-string                  >= 1.0.2  && < 2
                     , bitvec                       >= 1.1.5  && < 2
                     , finite-typelits              >= 0.1.0  && < 1
                     , vector-sized                 >= 1      && < 2

  ghc-options:       -O2
                     -Wall
                     -Wcompat
                     -Widentities
                     -Wincomplete-record-updates
                     -Wincomplete-uni-patterns
                     -Wpartial-fields
                     -Wredundant-constraints
                     -Wno-type-defaults
                     -Wno-orphans