Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Core.Data.Class.ExtractSymbolics

Contents

Extracting symbolic constant set from a value

Description

Synopsis

class ExtractSymbolics a where
- extractSymbolics :: a -> SymbolSet

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)

Methods

extractSymbolics :: a -> SymbolSet Source #

Instances

Instances details

ExtractSymbolics Int16 Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int16 -> SymbolSet Source #
ExtractSymbolics Int32 Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int32 -> SymbolSet Source #
ExtractSymbolics Int64 Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int64 -> SymbolSet Source #
ExtractSymbolics Int8 Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int8 -> SymbolSet Source #
ExtractSymbolics Word16 Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word16 -> SymbolSet Source #
ExtractSymbolics Word32 Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word32 -> SymbolSet Source #
ExtractSymbolics Word64 Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word64 -> SymbolSet Source #
ExtractSymbolics ByteString Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: ByteString -> SymbolSet Source #
ExtractSymbolics AssertionError Source #
Instance details Defined in Grisette.Core.Control.Exception Methods extractSymbolics :: AssertionError -> SymbolSet Source #
ExtractSymbolics VerificationConditions Source #
Instance details Defined in Grisette.Core.Control.Exception Methods extractSymbolics :: VerificationConditions -> SymbolSet Source #
ExtractSymbolics SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods extractSymbolics :: SymbolSet -> SymbolSet Source #
ExtractSymbolics Word8 Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word8 -> SymbolSet Source #
ExtractSymbolics Integer Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Integer -> SymbolSet Source #
ExtractSymbolics () Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: () -> SymbolSet Source #
ExtractSymbolics Bool Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Bool -> SymbolSet Source #
ExtractSymbolics Char Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Char -> SymbolSet Source #
ExtractSymbolics Int Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int -> SymbolSet Source #
ExtractSymbolics Word Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word -> SymbolSet Source #
ExtractSymbolics a => ExtractSymbolics (Identity a) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Identity a -> SymbolSet Source #
(Generic a, ExtractSymbolics' (Rep a)) => ExtractSymbolics (Default a) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Default a -> SymbolSet Source #
ExtractSymbolics a => ExtractSymbolics (UnionM a) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods extractSymbolics :: UnionM a -> SymbolSet Source #
SupportedPrim a => ExtractSymbolics (Sym a) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods extractSymbolics :: Sym a -> SymbolSet Source #
ExtractSymbolics a => ExtractSymbolics (Maybe a) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Maybe a -> SymbolSet Source #
ExtractSymbolics a => ExtractSymbolics [a] Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: [a] -> SymbolSet Source #
(ExtractSymbolics a, ExtractSymbolics b) => ExtractSymbolics (Either a b) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Either a b -> SymbolSet Source #
(ExtractSymbolics a, ExtractSymbolics b) => ExtractSymbolics (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods extractSymbolics :: CBMCEither a b -> SymbolSet Source #
ExtractSymbolics (m (Maybe a)) => ExtractSymbolics (MaybeT m a) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: MaybeT m a -> SymbolSet Source #
(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 Methods extractSymbolics :: CBMCExceptT e m a -> SymbolSet Source #
ExtractSymbolics (m (Either e a)) => ExtractSymbolics (ExceptT e m a) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: ExceptT e m a -> SymbolSet Source #
ExtractSymbolics (m a) => ExtractSymbolics (IdentityT m a) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: IdentityT m a -> SymbolSet Source #
ExtractSymbolics (m (a, s)) => ExtractSymbolics (WriterT s m a) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: WriterT s m a -> SymbolSet Source #
ExtractSymbolics (m (a, s)) => ExtractSymbolics (WriterT s m a) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: WriterT s m a -> SymbolSet Source #
(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 Methods extractSymbolics :: Sum f g a -> SymbolSet Source #