grisette-0.4.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.4.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.3
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.SBV
      Grisette.Backend.SBV.Data.SMT.Lowering
      Grisette.Backend.SBV.Data.SMT.Solving
      Grisette.Backend.SBV.Data.SMT.SymBiMap
      Grisette.Core
      Grisette.Core.BuiltinUnionWrappers
      Grisette.Core.Control.Exception
      Grisette.Core.Control.Monad.CBMCExcept
      Grisette.Core.Control.Monad.Class.MonadParallelUnion
      Grisette.Core.Control.Monad.Union
      Grisette.Core.Control.Monad.UnionM
      Grisette.Core.Data.BV
      Grisette.Core.Data.Class.BitVector
      Grisette.Core.Data.Class.CEGISSolver
      Grisette.Core.Data.Class.Error
      Grisette.Core.Data.Class.EvaluateSym
      Grisette.Core.Data.Class.ExtractSymbolics
      Grisette.Core.Data.Class.Function
      Grisette.Core.Data.Class.GenSym
      Grisette.Core.Data.Class.GPretty
      Grisette.Core.Data.Class.ITEOp
      Grisette.Core.Data.Class.LogicalOp
      Grisette.Core.Data.Class.Mergeable
      Grisette.Core.Data.Class.ModelOps
      Grisette.Core.Data.Class.SafeDivision
      Grisette.Core.Data.Class.SafeLinearArith
      Grisette.Core.Data.Class.SafeSymRotate
      Grisette.Core.Data.Class.SafeSymShift
      Grisette.Core.Data.Class.SEq
      Grisette.Core.Data.Class.SignConversion
      Grisette.Core.Data.Class.SimpleMergeable
      Grisette.Core.Data.Class.Solvable
      Grisette.Core.Data.Class.Solver
      Grisette.Core.Data.Class.SOrd
      Grisette.Core.Data.Class.SubstituteSym
      Grisette.Core.Data.Class.SymRotate
      Grisette.Core.Data.Class.SymShift
      Grisette.Core.Data.Class.ToCon
      Grisette.Core.Data.Class.ToSym
      Grisette.Core.Data.FileLocation
      Grisette.Core.Data.MemoUtils
      Grisette.Core.Data.Union
      Grisette.Core.TH
      Grisette.Core.THCompat
      Grisette.Experimental
      Grisette.Experimental.GenSymConstrained
      Grisette.Internal.Backend.SBV
      Grisette.Internal.Core
      Grisette.Internal.IR.SymPrim
      Grisette.IR.SymPrim
      Grisette.IR.SymPrim.Data.IntBitwidth
      Grisette.IR.SymPrim.Data.Prim.Helpers
      Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches
      Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
      Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
      Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
      Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
      Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
      Grisette.IR.SymPrim.Data.Prim.Model
      Grisette.IR.SymPrim.Data.Prim.ModelValue
      Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
      Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
      Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
      Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
      Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
      Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
      Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval
      Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
      Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
      Grisette.IR.SymPrim.Data.Prim.Utils
      Grisette.IR.SymPrim.Data.SymPrim
      Grisette.IR.SymPrim.Data.TabularFun
      Grisette.Lib.Base
      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.State
      Grisette.Lib.Control.Monad.Trans.State.Lazy
      Grisette.Lib.Control.Monad.Trans.State.Strict
      Grisette.Lib.Data.Foldable
      Grisette.Lib.Data.List
      Grisette.Lib.Data.Traversable
      Grisette.Qualified.ParallelUnionDo
      Grisette.Utils
      Grisette.Utils.Parameterized
  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.*
    , 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.11 && <10.4
    , stm ==2.5.*
    , template-haskell >=2.16 && <2.22
    , 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.*
    , 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.11 && <10.4
    , stm ==2.5.*
    , template-haskell >=2.16 && <2.22
    , 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.SBV.Data.SMT.CEGISTests
      Grisette.Backend.SBV.Data.SMT.LoweringTests
      Grisette.Backend.SBV.Data.SMT.TermRewritingGen
      Grisette.Backend.SBV.Data.SMT.TermRewritingTests
      Grisette.Core.Control.ExceptionTests
      Grisette.Core.Control.Monad.UnionMTests
      Grisette.Core.Control.Monad.UnionTests
      Grisette.Core.Data.BVTests
      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.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.UnionLikeTests
      Grisette.IR.SymPrim.Data.Prim.BitsTests
      Grisette.IR.SymPrim.Data.Prim.BoolTests
      Grisette.IR.SymPrim.Data.Prim.BVTests
      Grisette.IR.SymPrim.Data.Prim.IntegralTests
      Grisette.IR.SymPrim.Data.Prim.ModelTests
      Grisette.IR.SymPrim.Data.Prim.NumTests
      Grisette.IR.SymPrim.Data.Prim.TabularFunTests
      Grisette.IR.SymPrim.Data.SymPrimTests
      Grisette.IR.SymPrim.Data.TabularFunTests
      Grisette.Lib.Control.Monad.ExceptTests
      Grisette.Lib.Control.Monad.State.ClassTests
      Grisette.Lib.Control.Monad.Trans.ClassTests
      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.TraversableTests
      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.*
    , 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.11 && <10.4
    , stm ==2.5.*
    , template-haskell >=2.16 && <2.22
    , 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