grisette-0.3.0.0: grisette.cabal
cabal-version: 1.12
-- This file has been generated from package.yaml by hpack version 0.35.2.
--
-- see: https://github.com/sol/hpack
name: grisette
version: 0.3.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-haskell#readme
bug-reports: https://github.com/lsrcz/grisette-haskell/issues
author: Sirui Lu, Rastislav Bodík
maintainer: Sirui Lu (siruilu@cs.washington.edu)
copyright: 2021-2023 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.5
, GHC == 9.6.2
extra-source-files:
CHANGELOG.md
README.md
source-repository head
type: git
location: https://github.com/lsrcz/grisette-haskell
flag fast
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.Bool
Grisette.Core.Data.Class.CEGISSolver
Grisette.Core.Data.Class.Error
Grisette.Core.Data.Class.Evaluate
Grisette.Core.Data.Class.ExtractSymbolics
Grisette.Core.Data.Class.Function
Grisette.Core.Data.Class.GenSym
Grisette.Core.Data.Class.Mergeable
Grisette.Core.Data.Class.ModelOps
Grisette.Core.Data.Class.SafeArith
Grisette.Core.Data.Class.SimpleMergeable
Grisette.Core.Data.Class.Solvable
Grisette.Core.Data.Class.Solver
Grisette.Core.Data.Class.SOrd
Grisette.Core.Data.Class.Substitute
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.Trans
Grisette.Lib.Control.Monad.Trans.Cont
Grisette.Lib.Data.Foldable
Grisette.Lib.Data.List
Grisette.Lib.Data.Traversable
Grisette.Lib.Mtl
Grisette.Qualified.ParallelUnionDo
Grisette.Utils
Grisette.Utils.Parameterized
other-modules:
Paths_grisette
hs-source-dirs:
src
build-depends:
array >=0.5.4 && <0.6
, base >=4.14 && <5
, bytestring >=0.10.12 && <0.12
, call-stack >=0.1 && <0.5
, deepseq >=1.4.4 && <1.5
, 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
, sbv >=8.11 && <10.3
, template-haskell >=2.16 && <2.21
, th-compat >=0.1.2 && <0.2
, transformers >=0.5.6 && <0.7
, unordered-containers >=0.2.11 && <0.3
, vector >=0.12.1 && <0.14
default-language: Haskell2010
if flag(fast)
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
build-depends:
Glob
, array >=0.5.4 && <0.6
, base >=4.14 && <5
, bytestring >=0.10.12 && <0.12
, call-stack >=0.1 && <0.5
, deepseq >=1.4.4 && <1.5
, doctest >=0.18.2 && <0.22
, 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
, sbv >=8.11 && <10.3
, template-haskell >=2.16 && <2.21
, th-compat >=0.1.2 && <0.2
, transformers >=0.5.6 && <0.7
, unordered-containers >=0.2.11 && <0.3
, vector >=0.12.1 && <0.14
default-language: Haskell2010
if flag(fast)
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.Monad.UnionMTests
Grisette.Core.Data.BVTests
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
Paths_grisette
hs-source-dirs:
test
build-depends:
array >=0.5.4 && <0.6
, base >=4.14 && <5
, bytestring >=0.10.12 && <0.12
, call-stack >=0.1 && <0.5
, deepseq >=1.4.4 && <1.5
, 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
, sbv >=8.11 && <10.3
, tasty >=1.1.0.3 && <1.5
, tasty-hunit ==0.10.*
, tasty-quickcheck >=0.10.1 && <0.11
, tasty-test-reporter >=0.1.1.2 && <0.2
, template-haskell >=2.16 && <2.21
, th-compat >=0.1.2 && <0.2
, transformers >=0.5.6 && <0.7
, unordered-containers >=0.2.11 && <0.3
, vector >=0.12.1 && <0.14
default-language: Haskell2010
if flag(fast)
ghc-options: -O2
else
ghc-options: -O0