cabal-version: 1.12

-- This file has been generated from package.yaml by hpack version 0.36.0.
--
-- see: https://github.com/sol/hpack

name:           grisette
version:        0.7.0.0
x-revision: 1
synopsis:       Symbolic evaluation as a library
description:    Grisette is a reusable symbolic evaluation library for Haskell. By
                translating programs into constraints, Grisette can help the development of
                program reasoning tools, including verification, synthesis, and more.
                .
                The "Grisette" module exports all the core APIs for building a symbolic
                evaluation tool. A high-level overview of the module structures are available
                there.
                .
                A detailed introduction to Grisette is available at "Grisette.Core". More
                lifted libraries are provided in @Grisette.Lib.*@ modules.
                .
                The "Grisette.Unified" module offers an experimental unified interface for
                symbolic and concrete evaluation. This module should be imported qualified.
                .
                For more details, please checkout the README and 
                [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials).
category:       Formal Methods, Theorem Provers, Symbolic Computation, SMT
homepage:       https://github.com/lsrcz/grisette#readme
bug-reports:    https://github.com/lsrcz/grisette/issues
author:         Sirui Lu, Rastislav Bodík
maintainer:     Sirui Lu (siruilu@cs.washington.edu)
copyright:      2021-2024 Sirui Lu
license:        BSD3
license-file:   LICENSE
build-type:     Simple
tested-with:
    GHC == 8.10.7
  , GHC == 9.0.2
  , GHC == 9.2.8
  , GHC == 9.4.8
  , GHC == 9.6.5
  , GHC == 9.8.2
  , GHC == 9.10.1
extra-source-files:
    CHANGELOG.md
    README.md

source-repository head
  type: git
  location: https://github.com/lsrcz/grisette

flag optimize
  description: Compile with O2 optimization
  manual: False
  default: True

library
  exposed-modules:
      Grisette
      Grisette.Backend
      Grisette.Core
      Grisette.Experimental
      Grisette.Experimental.GenSymConstrained
      Grisette.Experimental.MonadParallelUnion
      Grisette.Experimental.Qualified.ParallelUnionDo
      Grisette.Internal.Backend.Solving
      Grisette.Internal.Backend.SymBiMap
      Grisette.Internal.Core.Control.Exception
      Grisette.Internal.Core.Control.Monad.CBMCExcept
      Grisette.Internal.Core.Control.Monad.Class.Union
      Grisette.Internal.Core.Control.Monad.Union
      Grisette.Internal.Core.Data.Class.BitCast
      Grisette.Internal.Core.Data.Class.BitVector
      Grisette.Internal.Core.Data.Class.CEGISSolver
      Grisette.Internal.Core.Data.Class.Error
      Grisette.Internal.Core.Data.Class.EvalSym
      Grisette.Internal.Core.Data.Class.ExtractSym
      Grisette.Internal.Core.Data.Class.Function
      Grisette.Internal.Core.Data.Class.GenSym
      Grisette.Internal.Core.Data.Class.IEEEFP
      Grisette.Internal.Core.Data.Class.ITEOp
      Grisette.Internal.Core.Data.Class.LogicalOp
      Grisette.Internal.Core.Data.Class.Mergeable
      Grisette.Internal.Core.Data.Class.ModelOps
      Grisette.Internal.Core.Data.Class.PlainUnion
      Grisette.Internal.Core.Data.Class.PPrint
      Grisette.Internal.Core.Data.Class.SafeDivision
      Grisette.Internal.Core.Data.Class.SafeLinearArith
      Grisette.Internal.Core.Data.Class.SafeSymRotate
      Grisette.Internal.Core.Data.Class.SafeSymShift
      Grisette.Internal.Core.Data.Class.SignConversion
      Grisette.Internal.Core.Data.Class.SimpleMergeable
      Grisette.Internal.Core.Data.Class.Solvable
      Grisette.Internal.Core.Data.Class.Solver
      Grisette.Internal.Core.Data.Class.SubstSym
      Grisette.Internal.Core.Data.Class.SymEq
      Grisette.Internal.Core.Data.Class.SymOrd
      Grisette.Internal.Core.Data.Class.SymRotate
      Grisette.Internal.Core.Data.Class.SymShift
      Grisette.Internal.Core.Data.Class.ToCon
      Grisette.Internal.Core.Data.Class.ToSym
      Grisette.Internal.Core.Data.Class.TryMerge
      Grisette.Internal.Core.Data.MemoUtils
      Grisette.Internal.Core.Data.Symbol
      Grisette.Internal.Core.Data.UnionBase
      Grisette.Internal.SymPrim.AllSyms
      Grisette.Internal.SymPrim.BV
      Grisette.Internal.SymPrim.FP
      Grisette.Internal.SymPrim.GeneralFun
      Grisette.Internal.SymPrim.IntBitwidth
      Grisette.Internal.SymPrim.ModelRep
      Grisette.Internal.SymPrim.Prim.Internal.Caches
      Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm
      Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm
      Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
      Grisette.Internal.SymPrim.Prim.Internal.IsZero
      Grisette.Internal.SymPrim.Prim.Internal.PartialEval
      Grisette.Internal.SymPrim.Prim.Internal.Term
      Grisette.Internal.SymPrim.Prim.Internal.Unfold
      Grisette.Internal.SymPrim.Prim.Internal.Utils
      Grisette.Internal.SymPrim.Prim.Model
      Grisette.Internal.SymPrim.Prim.ModelValue
      Grisette.Internal.SymPrim.Prim.SomeTerm
      Grisette.Internal.SymPrim.Prim.Term
      Grisette.Internal.SymPrim.Prim.TermUtils
      Grisette.Internal.SymPrim.SomeBV
      Grisette.Internal.SymPrim.SymBool
      Grisette.Internal.SymPrim.SymBV
      Grisette.Internal.SymPrim.SymFP
      Grisette.Internal.SymPrim.SymGeneralFun
      Grisette.Internal.SymPrim.SymInteger
      Grisette.Internal.SymPrim.SymTabularFun
      Grisette.Internal.SymPrim.TabularFun
      Grisette.Internal.TH.DeriveBuiltin
      Grisette.Internal.TH.DeriveInstanceProvider
      Grisette.Internal.TH.DerivePredefined
      Grisette.Internal.TH.DeriveTypeParamHandler
      Grisette.Internal.TH.DeriveUnifiedInterface
      Grisette.Internal.TH.DeriveWithHandlers
      Grisette.Internal.TH.MergeConstructor
      Grisette.Internal.TH.UnifiedConstructor
      Grisette.Internal.TH.Util
      Grisette.Internal.Utils.Derive
      Grisette.Internal.Utils.Parameterized
      Grisette.Lib.Base
      Grisette.Lib.Control.Applicative
      Grisette.Lib.Control.Monad
      Grisette.Lib.Control.Monad.Except
      Grisette.Lib.Control.Monad.State.Class
      Grisette.Lib.Control.Monad.Trans
      Grisette.Lib.Control.Monad.Trans.Class
      Grisette.Lib.Control.Monad.Trans.Cont
      Grisette.Lib.Control.Monad.Trans.Except
      Grisette.Lib.Control.Monad.Trans.State
      Grisette.Lib.Control.Monad.Trans.State.Lazy
      Grisette.Lib.Control.Monad.Trans.State.Strict
      Grisette.Lib.Data.Bool
      Grisette.Lib.Data.Either
      Grisette.Lib.Data.Foldable
      Grisette.Lib.Data.Functor
      Grisette.Lib.Data.Functor.Sum
      Grisette.Lib.Data.List
      Grisette.Lib.Data.Maybe
      Grisette.Lib.Data.Traversable
      Grisette.Lib.Data.Tuple
      Grisette.SymPrim
      Grisette.TH
      Grisette.Unified
      Grisette.Unified.Internal.BaseConstraint
      Grisette.Unified.Internal.BaseMonad
      Grisette.Unified.Internal.Class.UnifiedITEOp
      Grisette.Unified.Internal.Class.UnifiedSafeDivision
      Grisette.Unified.Internal.Class.UnifiedSafeLinearArith
      Grisette.Unified.Internal.Class.UnifiedSafeSymRotate
      Grisette.Unified.Internal.Class.UnifiedSafeSymShift
      Grisette.Unified.Internal.Class.UnifiedSimpleMergeable
      Grisette.Unified.Internal.Class.UnifiedSymEq
      Grisette.Unified.Internal.Class.UnifiedSymOrd
      Grisette.Unified.Internal.EvalMode
      Grisette.Unified.Internal.EvalModeTag
      Grisette.Unified.Internal.MonadWithMode
      Grisette.Unified.Internal.UnifiedBool
      Grisette.Unified.Internal.UnifiedBV
      Grisette.Unified.Internal.UnifiedConstraint
      Grisette.Unified.Internal.UnifiedData
      Grisette.Unified.Internal.UnifiedInteger
      Grisette.Unified.Internal.Util
      Grisette.Unified.Lib.Control.Applicative
      Grisette.Unified.Lib.Control.Monad
      Grisette.Unified.Lib.Data.Foldable
      Grisette.Unified.Lib.Data.Functor
      Grisette.Utils
  other-modules:
      Paths_grisette
  hs-source-dirs:
      src
  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns
  build-depends:
      QuickCheck >=2.14 && <2.16
    , array >=0.5.4 && <0.6
    , async >=2.2.2 && <2.3
    , base >=4.14 && <5
    , bytestring >=0.10.12 && <0.13
    , containers >=0.4 && <0.8
    , deepseq >=1.4.4 && <1.6
    , generic-deriving >=1.14.1 && <1.15
    , hashable >=1.2.3 && <1.6
    , hashtables >=1.2.3.4 && <1.4
    , intern >=0.9.2 && <0.10
    , loch-th >=0.2.2 && <0.3
    , mtl >=2.2.2 && <2.4
    , parallel >=3.2.2.0 && <3.3
    , prettyprinter >=1.5.0 && <1.8
    , sbv >=8.17 && <11
    , stm ==2.5.*
    , template-haskell >=2.16 && <2.23
    , text >=1.2.4.1 && <2.2
    , th-abstraction >=0.4 && <0.8
    , th-compat >=0.1.2 && <0.2
    , transformers >=0.5.6 && <0.7
    , unordered-containers >=0.2.11 && <0.3
  default-language: Haskell2010
  if flag(optimize)
    ghc-options: -O2
  else
    ghc-options: -O0

test-suite doctest
  type: exitcode-stdio-1.0
  main-is: Main.hs
  other-modules:
      Paths_grisette
  hs-source-dirs:
      doctest
  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
  build-depends:
      Glob
    , QuickCheck >=2.14 && <2.16
    , array >=0.5.4 && <0.6
    , async >=2.2.2 && <2.3
    , base >=4.14 && <5
    , bytestring >=0.10.12 && <0.13
    , containers >=0.4 && <0.8
    , deepseq >=1.4.4 && <1.6
    , doctest >=0.18.2 && <0.23
    , generic-deriving >=1.14.1 && <1.15
    , grisette
    , hashable >=1.2.3 && <1.6
    , hashtables >=1.2.3.4 && <1.4
    , intern >=0.9.2 && <0.10
    , loch-th >=0.2.2 && <0.3
    , mtl >=2.2.2 && <2.4
    , parallel >=3.2.2.0 && <3.3
    , prettyprinter >=1.5.0 && <1.8
    , sbv >=8.17 && <11
    , stm ==2.5.*
    , template-haskell >=2.16 && <2.23
    , text >=1.2.4.1 && <2.2
    , th-abstraction >=0.4 && <0.8
    , th-compat >=0.1.2 && <0.2
    , transformers >=0.5.6 && <0.7
    , unordered-containers >=0.2.11 && <0.3
  default-language: Haskell2010
  if flag(optimize)
    ghc-options: -O2
  else
    ghc-options: -O0

test-suite spec
  type: exitcode-stdio-1.0
  main-is: Main.hs
  other-modules:
      Grisette.Backend.CEGISTests
      Grisette.Backend.LoweringTests
      Grisette.Backend.TermRewritingGen
      Grisette.Backend.TermRewritingTests
      Grisette.Core.Control.ExceptionTests
      Grisette.Core.Control.Monad.UnionTests
      Grisette.Core.Data.Class.BoolTests
      Grisette.Core.Data.Class.EvalSymTests
      Grisette.Core.Data.Class.ExtractSymTests
      Grisette.Core.Data.Class.GenSymTests
      Grisette.Core.Data.Class.MergeableTests
      Grisette.Core.Data.Class.PlainUnionTests
      Grisette.Core.Data.Class.PPrintTests
      Grisette.Core.Data.Class.SafeDivisionTests
      Grisette.Core.Data.Class.SafeLinearArithTests
      Grisette.Core.Data.Class.SafeSymRotateTests
      Grisette.Core.Data.Class.SafeSymShiftTests
      Grisette.Core.Data.Class.SimpleMergeableTests
      Grisette.Core.Data.Class.SubstSymTests
      Grisette.Core.Data.Class.SymEqTests
      Grisette.Core.Data.Class.SymOrdTests
      Grisette.Core.Data.Class.SymRotateTests
      Grisette.Core.Data.Class.SymShiftTests
      Grisette.Core.Data.Class.TestValues
      Grisette.Core.Data.Class.ToConTests
      Grisette.Core.Data.Class.ToSymTests
      Grisette.Core.Data.Class.TryMergeTests
      Grisette.Core.Data.UnionBaseTests
      Grisette.Core.TH.DerivationTest
      Grisette.Lib.Control.ApplicativeTest
      Grisette.Lib.Control.Monad.ExceptTests
      Grisette.Lib.Control.Monad.State.ClassTests
      Grisette.Lib.Control.Monad.Trans.ClassTests
      Grisette.Lib.Control.Monad.Trans.ExceptTests
      Grisette.Lib.Control.Monad.Trans.State.Common
      Grisette.Lib.Control.Monad.Trans.State.LazyTests
      Grisette.Lib.Control.Monad.Trans.State.StrictTests
      Grisette.Lib.Control.MonadTests
      Grisette.Lib.Data.FoldableTests
      Grisette.Lib.Data.FunctorTests
      Grisette.Lib.Data.ListTests
      Grisette.Lib.Data.TraversableTests
      Grisette.SymPrim.BVTests
      Grisette.SymPrim.FPTests
      Grisette.SymPrim.Prim.BitsTests
      Grisette.SymPrim.Prim.BoolTests
      Grisette.SymPrim.Prim.BVTests
      Grisette.SymPrim.Prim.IntegralTests
      Grisette.SymPrim.Prim.ModelTests
      Grisette.SymPrim.Prim.NumTests
      Grisette.SymPrim.Prim.TabularFunTests
      Grisette.SymPrim.SomeBVTests
      Grisette.SymPrim.SymPrimTests
      Grisette.SymPrim.TabularFunTests
      Grisette.TestUtil.NoMerge
      Grisette.TestUtil.PrettyPrint
      Grisette.TestUtil.SymbolicAssertion
      Grisette.Unified.EvalModeTest
      Grisette.Unified.UnifiedClassesTest
      Grisette.Unified.UnifiedConstructorTest
      Paths_grisette
  hs-source-dirs:
      test
  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
  build-depends:
      HUnit ==1.6.*
    , QuickCheck >=2.14 && <2.16
    , array >=0.5.4 && <0.6
    , async >=2.2.2 && <2.3
    , base >=4.14 && <5
    , bytestring >=0.10.12 && <0.13
    , containers >=0.4 && <0.8
    , deepseq >=1.4.4 && <1.6
    , generic-deriving >=1.14.1 && <1.15
    , grisette
    , hashable >=1.2.3 && <1.6
    , hashtables >=1.2.3.4 && <1.4
    , intern >=0.9.2 && <0.10
    , loch-th >=0.2.2 && <0.3
    , mtl >=2.2.2 && <2.4
    , parallel >=3.2.2.0 && <3.3
    , prettyprinter >=1.5.0 && <1.8
    , sbv >=8.17 && <11
    , stm ==2.5.*
    , template-haskell >=2.16 && <2.23
    , test-framework >=0.8.2 && <0.9
    , test-framework-hunit >=0.3.0.2 && <0.4
    , test-framework-quickcheck2 >=0.3.0.5 && <0.4
    , text >=1.2.4.1 && <2.2
    , th-abstraction >=0.4 && <0.8
    , th-compat >=0.1.2 && <0.2
    , transformers >=0.5.6 && <0.7
    , unordered-containers >=0.2.11 && <0.3
  default-language: Haskell2010
  if flag(optimize)
    ghc-options: -O2
  else
    ghc-options: -O0