grisette-0.11.0.0: Symbolic evaluation as a library
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.
The Grisette module exports all the core APIs for building a symbolic evaluation tool. A high-level overview of the module structures are available there.
A detailed introduction to Grisette is available at Grisette.Core. More
lifted libraries are provided in Grisette.Lib.*
modules.
The Grisette.Unified module offers an experimental unified interface for symbolic and concrete evaluation. This module should be imported qualified.
For more details, please checkout the README and tutorials.
Modules
grisette-0.11.0.0
- Grisette
- Grisette.Backend
- Grisette.Core
- Grisette.Experimental
- Internal
- Backend
- Core
- Control
- Data
- Class
- Grisette.Internal.Core.Data.Class.BitCast
- Grisette.Internal.Core.Data.Class.BitVector
- Grisette.Internal.Core.Data.Class.CEGISSolver
- Grisette.Internal.Core.Data.Class.Error
- Grisette.Internal.Core.Data.Class.EvalSym
- Grisette.Internal.Core.Data.Class.ExtractSym
- Grisette.Internal.Core.Data.Class.Function
- Grisette.Internal.Core.Data.Class.GenSym
- Grisette.Internal.Core.Data.Class.IEEEFP
- 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.PPrint
- Grisette.Internal.Core.Data.Class.PlainUnion
- Grisette.Internal.Core.Data.Class.SafeBitCast
- Grisette.Internal.Core.Data.Class.SafeDiv
- Grisette.Internal.Core.Data.Class.SafeFdiv
- Grisette.Internal.Core.Data.Class.SafeFromFP
- Grisette.Internal.Core.Data.Class.SafeLinearArith
- Grisette.Internal.Core.Data.Class.SafeLogBase
- Grisette.Internal.Core.Data.Class.SafeSymRotate
- Grisette.Internal.Core.Data.Class.SafeSymShift
- 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.SubstSym
- Grisette.Internal.Core.Data.Class.SymEq
- Grisette.Internal.Core.Data.Class.SymFiniteBits
- Grisette.Internal.Core.Data.Class.SymFromIntegral
- Grisette.Internal.Core.Data.Class.SymIEEEFP
- Grisette.Internal.Core.Data.Class.SymOrd
- 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.SExpr
- Grisette.Internal.Core.Data.Symbol
- Grisette.Internal.Core.Data.UnionBase
- Class
- SymPrim
- Grisette.Internal.SymPrim.AlgReal
- Grisette.Internal.SymPrim.AllSyms
- Grisette.Internal.SymPrim.BV
- Grisette.Internal.SymPrim.FP
- Grisette.Internal.SymPrim.FunInstanceGen
- Grisette.Internal.SymPrim.GeneralFun
- Grisette.Internal.SymPrim.IntBitwidth
- Grisette.Internal.SymPrim.ModelRep
- Prim
- Internal
- Grisette.Internal.SymPrim.Prim.Internal.Caches
- Instances
- Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval
- Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm
- Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm
- Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm
- Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
- Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm
- Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm
- Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm
- Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm
- 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.PartialEval
- Grisette.Internal.SymPrim.Prim.Internal.Serialize
- 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.Pattern
- Grisette.Internal.SymPrim.Prim.SomeTerm
- Grisette.Internal.SymPrim.Prim.Term
- Grisette.Internal.SymPrim.Prim.TermUtils
- Internal
- Grisette.Internal.SymPrim.Quantifier
- Grisette.Internal.SymPrim.SomeBV
- Grisette.Internal.SymPrim.SymAlgReal
- Grisette.Internal.SymPrim.SymBV
- Grisette.Internal.SymPrim.SymBool
- Grisette.Internal.SymPrim.SymFP
- Grisette.Internal.SymPrim.SymGeneralFun
- Grisette.Internal.SymPrim.SymInteger
- Grisette.Internal.SymPrim.SymPrim
- Grisette.Internal.SymPrim.SymTabularFun
- Grisette.Internal.SymPrim.TabularFun
- TH
- Ctor
- Derivation
- Grisette.Internal.TH.Derivation.BinaryOpCommon
- Grisette.Internal.TH.Derivation.Common
- Grisette.Internal.TH.Derivation.ConvertOpCommon
- Grisette.Internal.TH.Derivation.Derive
- Grisette.Internal.TH.Derivation.DeriveAllSyms
- Grisette.Internal.TH.Derivation.DeriveBinary
- Grisette.Internal.TH.Derivation.DeriveCereal
- Grisette.Internal.TH.Derivation.DeriveEq
- Grisette.Internal.TH.Derivation.DeriveEvalSym
- Grisette.Internal.TH.Derivation.DeriveExtractSym
- Grisette.Internal.TH.Derivation.DeriveHashable
- Grisette.Internal.TH.Derivation.DeriveMergeable
- Grisette.Internal.TH.Derivation.DeriveNFData
- Grisette.Internal.TH.Derivation.DeriveOrd
- Grisette.Internal.TH.Derivation.DerivePPrint
- Grisette.Internal.TH.Derivation.DeriveSerial
- Grisette.Internal.TH.Derivation.DeriveShow
- Grisette.Internal.TH.Derivation.DeriveSimpleMergeable
- Grisette.Internal.TH.Derivation.DeriveSubstSym
- Grisette.Internal.TH.Derivation.DeriveSymEq
- Grisette.Internal.TH.Derivation.DeriveSymOrd
- Grisette.Internal.TH.Derivation.DeriveToCon
- Grisette.Internal.TH.Derivation.DeriveToSym
- Grisette.Internal.TH.Derivation.DeriveUnifiedSimpleMergeable
- Grisette.Internal.TH.Derivation.DeriveUnifiedSymEq
- Grisette.Internal.TH.Derivation.DeriveUnifiedSymOrd
- Grisette.Internal.TH.Derivation.SerializeCommon
- Grisette.Internal.TH.Derivation.ShowPPrintCommon
- Grisette.Internal.TH.Derivation.UnaryOpCommon
- Grisette.Internal.TH.Derivation.UnifiedOpCommon
- Grisette.Internal.TH.Util
- Unified
- Grisette.Internal.Unified.BVBVConversion
- Grisette.Internal.Unified.BVFPConversion
- Grisette.Internal.Unified.BaseConstraint
- Grisette.Internal.Unified.BaseMonad
- Class
- Grisette.Internal.Unified.Class.UnifiedFiniteBits
- Grisette.Internal.Unified.Class.UnifiedFromIntegral
- Grisette.Internal.Unified.Class.UnifiedITEOp
- Grisette.Internal.Unified.Class.UnifiedRep
- Grisette.Internal.Unified.Class.UnifiedSafeBitCast
- Grisette.Internal.Unified.Class.UnifiedSafeDiv
- Grisette.Internal.Unified.Class.UnifiedSafeFdiv
- Grisette.Internal.Unified.Class.UnifiedSafeFromFP
- Grisette.Internal.Unified.Class.UnifiedSafeLinearArith
- Grisette.Internal.Unified.Class.UnifiedSafeSymRotate
- Grisette.Internal.Unified.Class.UnifiedSafeSymShift
- Grisette.Internal.Unified.Class.UnifiedSimpleMergeable
- Grisette.Internal.Unified.Class.UnifiedSolvable
- Grisette.Internal.Unified.Class.UnifiedSymEq
- Grisette.Internal.Unified.Class.UnifiedSymOrd
- Grisette.Internal.Unified.EvalMode
- Grisette.Internal.Unified.EvalModeTag
- Grisette.Internal.Unified.FPFPConversion
- Grisette.Internal.Unified.Theories
- Grisette.Internal.Unified.UnifiedAlgReal
- Grisette.Internal.Unified.UnifiedBV
- Grisette.Internal.Unified.UnifiedBool
- Grisette.Internal.Unified.UnifiedData
- Grisette.Internal.Unified.UnifiedFP
- Grisette.Internal.Unified.UnifiedFun
- Grisette.Internal.Unified.UnifiedInteger
- Grisette.Internal.Unified.UnifiedPrim
- Grisette.Internal.Unified.Util
- Utils
- Lib
- Grisette.SymPrim
- Grisette.TH
- Grisette.Unified
- Grisette.Utils