grisette-0.6.0.0: grisette.cabal

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.6.0.0
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.
                .
                This "Grisette" module exports all you need for building a symbolic evaluation
                tool.
                .
                For more details, please checkout the README.
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.Union
      Grisette.Internal.Core.Control.Monad.UnionM
      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.EvaluateSym
      Grisette.Internal.Core.Data.Class.ExtractSymbolics
      Grisette.Internal.Core.Data.Class.Function
      Grisette.Internal.Core.Data.Class.GenSym
      Grisette.Internal.Core.Data.Class.GPretty
      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.SafeDivision
      Grisette.Internal.Core.Data.Class.SafeLinearArith
      Grisette.Internal.Core.Data.Class.SafeSymRotate
      Grisette.Internal.Core.Data.Class.SafeSymShift
      Grisette.Internal.Core.Data.Class.SEq
      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.SOrd
      Grisette.Internal.Core.Data.Class.SubstituteSym
      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.Union
      Grisette.Internal.Core.TH.MergeConstructor
      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.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.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
    , deepseq >=1.4.4 && <1.6
    , generic-deriving >=1.14.1 && <1.15
    , hashable >=1.2.3 && <1.5
    , 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-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
    , 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.5
    , 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-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.UnionMTests
      Grisette.Core.Control.Monad.UnionTests
      Grisette.Core.Data.Class.BoolTests
      Grisette.Core.Data.Class.EvaluateSymTests
      Grisette.Core.Data.Class.ExtractSymbolicsTests
      Grisette.Core.Data.Class.GenSymTests
      Grisette.Core.Data.Class.GPrettyTests
      Grisette.Core.Data.Class.MergeableTests
      Grisette.Core.Data.Class.PlainUnionTests
      Grisette.Core.Data.Class.SafeDivisionTests
      Grisette.Core.Data.Class.SafeLinearArithTests
      Grisette.Core.Data.Class.SafeSymRotateTests
      Grisette.Core.Data.Class.SafeSymShiftTests
      Grisette.Core.Data.Class.SEqTests
      Grisette.Core.Data.Class.SimpleMergeableTests
      Grisette.Core.Data.Class.SOrdTests
      Grisette.Core.Data.Class.SubstituteSymTests
      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.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
      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
    , deepseq >=1.4.4 && <1.6
    , generic-deriving >=1.14.1 && <1.15
    , grisette
    , hashable >=1.2.3 && <1.5
    , 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-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