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.Internal.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.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int16 -> SymbolSet Source #
ExtractSymbolics Int32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int32 -> SymbolSet Source #
ExtractSymbolics Int64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int64 -> SymbolSet Source #
ExtractSymbolics Int8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int8 -> SymbolSet Source #
ExtractSymbolics Word16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word16 -> SymbolSet Source #
ExtractSymbolics Word32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word32 -> SymbolSet Source #
ExtractSymbolics Word64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word64 -> SymbolSet Source #
ExtractSymbolics Word8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word8 -> SymbolSet Source #
ExtractSymbolics ByteString Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: ByteString -> SymbolSet Source #
ExtractSymbolics AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: AssertionError -> SymbolSet Source #
ExtractSymbolics VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: VerificationConditions -> SymbolSet Source #
ExtractSymbolics SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SymBool -> SymbolSet Source #
ExtractSymbolics SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SymInteger -> SymbolSet Source #
ExtractSymbolics Text Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Text -> SymbolSet Source #
ExtractSymbolics Integer Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Integer -> SymbolSet Source #
ExtractSymbolics () Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: () -> SymbolSet Source #
ExtractSymbolics Bool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Bool -> SymbolSet Source #
ExtractSymbolics Char Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Char -> SymbolSet Source #
ExtractSymbolics Int Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Int -> SymbolSet Source #
ExtractSymbolics Word Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Word -> SymbolSet Source #
ExtractSymbolics a => ExtractSymbolics (Identity a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Identity a -> SymbolSet Source #
(Generic a, ExtractSymbolics' (Rep a)) => ExtractSymbolics (Default a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Default a -> SymbolSet Source #
ExtractSymbolics a => ExtractSymbolics (UnionM a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods extractSymbolics :: UnionM a -> SymbolSet Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: IntN n -> SymbolSet Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: WordN n -> SymbolSet Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ExtractSymbolics (bv n)) => ExtractSymbolics (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods extractSymbolics :: SomeBV bv -> SymbolSet Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SymIntN n -> SymbolSet Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SymWordN n -> SymbolSet Source #
ExtractSymbolics a => ExtractSymbolics (Maybe a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Maybe a -> SymbolSet Source #
ExtractSymbolics a => ExtractSymbolics [a] Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: [a] -> SymbolSet Source #
(ExtractSymbolics a, ExtractSymbolics b) => ExtractSymbolics (Either a b) Source #
Instance details Defined in Grisette.Internal.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.Internal.Core.Control.Monad.CBMCExcept Methods extractSymbolics :: CBMCEither a b -> 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 #
(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 Methods extractSymbolics :: MaybeT m a -> SymbolSet Source #
(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 Methods extractSymbolics :: CBMCExceptT e m a -> SymbolSet Source #
ExtractSymbolics (m (Either e a)) => ExtractSymbolics (ExceptT e m a) Source #
Instance details Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.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 Methods extractSymbolics :: Sum f g a -> SymbolSet Source #
(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 #