grisette-0.5.0.1: 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.Internal.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.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Int32 Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Int64 Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Int8 Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word16 Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word32 Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word64 Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word8 Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics ByteString Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics AssertionError Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics VerificationConditions Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics SymBool Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics SymInteger Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Text Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Integer Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics () Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Bool Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Char Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Int Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

ExtractSymbolics Word Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Control.Monad.UnionM

(KnownNat n, 1 <= n) => ExtractSymbolics (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

(KnownNat n, 1 <= n) => ExtractSymbolics (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

(forall (n :: Nat). (KnownNat n, 1 <= n) => ExtractSymbolics (bv n)) => ExtractSymbolics (SomeBV bv) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

(KnownNat n, 1 <= n) => ExtractSymbolics (SymIntN n) Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

(KnownNat n, 1 <= n) => ExtractSymbolics (SymWordN n) Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ExtractSymbolics (sa -~> sb) Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

Methods

extractSymbolics :: (sa -~> sb) -> SymbolSet Source #

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ExtractSymbolics (sa =~> sb) Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

Methods

extractSymbolics :: (sa =~> sb) -> SymbolSet Source #

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.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.Internal.Core.Control.Monad.CBMCExcept

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.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.Internal.Core.Data.Class.ExtractSymbolics

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

Methods

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

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

Methods

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

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

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

Methods

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

(ExtractSymbolics a, ExtractSymbolics b, ExtractSymbolics c, ExtractSymbolics d, ExtractSymbolics e, ExtractSymbolics f, ExtractSymbolics g) => ExtractSymbolics (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

Methods

extractSymbolics :: (a, b, c, d, e, f, g) -> SymbolSet Source #

(ExtractSymbolics a, ExtractSymbolics b, ExtractSymbolics c, ExtractSymbolics d, ExtractSymbolics e, ExtractSymbolics f, ExtractSymbolics g, ExtractSymbolics h) => ExtractSymbolics (a, b, c, d, e, f, g, h) Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics

Methods

extractSymbolics :: (a, b, c, d, e, f, g, h) -> SymbolSet Source #