grisette-0.1.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.ExtractSymbolics

Description

 
Synopsis

Extracting symbolic constant set from a value

class ExtractSymbolics a where Source #

Extracts all the symbolic variables that are transitively contained in the given value.

>>> extractSymbolics ("a" :: SymBool) :: SymbolSet
SymbolSet {a :: Bool}
>>> extractSymbolics (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: UnionM [SymBool]) :: SymbolSet
SymbolSet {a :: Bool, b :: Bool, c :: Bool, d :: Bool}

Note 1: This type class can be derived for algebraic data types. You may need the DerivingVia and DerivingStrategies extensions.

data X = ... deriving Generic deriving ExtractSymbolics via (Default X)

Instances

Instances details
ExtractSymbolics Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ExtractSymbolics VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ExtractSymbolics SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ExtractSymbolics Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics () Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics a => ExtractSymbolics (Identity a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

(Generic a, ExtractSymbolics' (Rep a)) => ExtractSymbolics (Default a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics a => ExtractSymbolics (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

SupportedPrim a => ExtractSymbolics (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ExtractSymbolics a => ExtractSymbolics (Maybe a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics a => ExtractSymbolics [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

(ExtractSymbolics a, ExtractSymbolics b) => ExtractSymbolics (Either a b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

(ExtractSymbolics a, ExtractSymbolics b) => ExtractSymbolics (CBMCEither a b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

ExtractSymbolics (m (Maybe a)) => ExtractSymbolics (MaybeT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

(ExtractSymbolics a, ExtractSymbolics b) => ExtractSymbolics (a, b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

Methods

extractSymbolics :: (a, b) -> SymbolSet Source #

ExtractSymbolics (m (CBMCEither e a)) => ExtractSymbolics (CBMCExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

ExtractSymbolics (m (Either e a)) => ExtractSymbolics (ExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics (m a) => ExtractSymbolics (IdentityT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics (m (a, s)) => ExtractSymbolics (WriterT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

ExtractSymbolics (m (a, s)) => ExtractSymbolics (WriterT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

(ExtractSymbolics a, ExtractSymbolics b, ExtractSymbolics c) => ExtractSymbolics (a, b, c) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

Methods

extractSymbolics :: (a, b, c) -> SymbolSet Source #

(ExtractSymbolics (f a), ExtractSymbolics (g a)) => ExtractSymbolics (Sum f g a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics