cabal-version: 1.12 -- This file has been generated from package.yaml by hpack version 0.35.0. -- -- see: https://github.com/sol/hpack name: grisette version: 0.1.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 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.Union Grisette.Core.Control.Monad.UnionM 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.Integer Grisette.Core.Data.Class.Mergeable Grisette.Core.Data.Class.ModelOps 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.Internal.Backend.SBV Grisette.Internal.Core Grisette.Internal.IR.SymPrim Grisette.IR.SymPrim Grisette.IR.SymPrim.Data.BV 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.Integer 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 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.3 , once >=0.2 && <0.5 , sbv >=8.11 && <9.1 , template-haskell >=2.16 && <2.20 , th-compat >=0.1.2 && <0.2 , transformers >=0.5.6 && <0.6 , 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.21 , 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.3 , once >=0.2 && <0.5 , sbv >=8.11 && <9.1 , template-haskell >=2.16 && <2.20 , th-compat >=0.1.2 && <0.2 , transformers >=0.5.6 && <0.6 , 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.IR.SymPrim.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.IntegerTests 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.3 , once >=0.2 && <0.5 , sbv >=8.11 && <9.1 , 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.20 , th-compat >=0.1.2 && <0.2 , transformers >=0.5.6 && <0.6 , 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