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.5.0.1 x-revision: 2 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.4 , GHC == 9.8.2 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.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.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.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.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.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.11 && <11 , 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 && <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.11 && <11 , 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.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.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.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.Core.Data.SomeBVTests 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.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.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.11 && <11 , 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