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.1.0 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.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 && <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.* , 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.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 && <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