Grisette.Internal.SymPrim.AllSyms

Documentation

symSize :: forall con sym. LinkedRep con sym => sym -> Int

Get the size of a symbolic term. Duplicate sub-terms are counted for only once.

>>> symSize (1 :: SymInteger)
1
>>> symSize ("a" :: SymInteger)
1
>>> symSize ("a" + 1 :: SymInteger)
3
>>> symSize (("a" + 1) * ("a" + 1) :: SymInteger)
4

symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int

Get the sum of the sizes of a list of symbolic terms. Duplicate sub-terms are counted for only once.

>>> symsSize [1, "a" :: SymInteger, "a" + 1 :: SymInteger]
3

data SomeSym where

Some symbolic value with LinkedRep constraint.

Constructors

SomeSym :: LinkedRep con sym => sym -> SomeSym

class AllSyms a where

Extract all symbolic primitive values that are represented as SMT terms.

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

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

Minimal complete definition

allSymsS | allSyms

Methods

allSymsS :: a -> [SomeSym] -> [SomeSym]

Convert a value to a list of symbolic primitive values. It should prepend to an existing list of symbolic primitive values.

allSyms :: a -> [SomeSym]

Specialized allSymsS that prepends to an empty list.

Instances

AllSyms Int16

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int16 -> [SomeSym] -> [SomeSym]

allSyms :: Int16 -> [SomeSym]

AllSyms Int32

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int32 -> [SomeSym] -> [SomeSym]

allSyms :: Int32 -> [SomeSym]

AllSyms Int64

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int64 -> [SomeSym] -> [SomeSym]

allSyms :: Int64 -> [SomeSym]

AllSyms Int8

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int8 -> [SomeSym] -> [SomeSym]

allSyms :: Int8 -> [SomeSym]

AllSyms Word16

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word16 -> [SomeSym] -> [SomeSym]

allSyms :: Word16 -> [SomeSym]

AllSyms Word32

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word32 -> [SomeSym] -> [SomeSym]

allSyms :: Word32 -> [SomeSym]

AllSyms Word64

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word64 -> [SomeSym] -> [SomeSym]

allSyms :: Word64 -> [SomeSym]

AllSyms Word8

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word8 -> [SomeSym] -> [SomeSym]

allSyms :: Word8 -> [SomeSym]

AllSyms ByteString

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: ByteString -> [SomeSym] -> [SomeSym]

allSyms :: ByteString -> [SomeSym]

AllSyms AssertionError

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: AssertionError -> [SomeSym] -> [SomeSym]

allSyms :: AssertionError -> [SomeSym]

AllSyms VerificationConditions

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: VerificationConditions -> [SomeSym] -> [SomeSym]

allSyms :: VerificationConditions -> [SomeSym]

AllSyms SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

allSymsS :: SymBool -> [SomeSym] -> [SomeSym]

allSyms :: SymBool -> [SomeSym]

AllSyms SymFPRoundingMode

Defined in Grisette.Internal.SymPrim.SymFP

Methods

allSymsS :: SymFPRoundingMode -> [SomeSym] -> [SomeSym]

allSyms :: SymFPRoundingMode -> [SomeSym]

AllSyms SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

allSymsS :: SymInteger -> [SomeSym] -> [SomeSym]

allSyms :: SymInteger -> [SomeSym]

AllSyms Text

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Text -> [SomeSym] -> [SomeSym]

allSyms :: Text -> [SomeSym]

AllSyms Integer

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Integer -> [SomeSym] -> [SomeSym]

allSyms :: Integer -> [SomeSym]

AllSyms ()

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: () -> [SomeSym] -> [SomeSym]

allSyms :: () -> [SomeSym]

AllSyms Bool

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Bool -> [SomeSym] -> [SomeSym]

allSyms :: Bool -> [SomeSym]

AllSyms Char

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Char -> [SomeSym] -> [SomeSym]

allSyms :: Char -> [SomeSym]

AllSyms Int

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int -> [SomeSym] -> [SomeSym]

allSyms :: Int -> [SomeSym]

AllSyms Word

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word -> [SomeSym] -> [SomeSym]

allSyms :: Word -> [SomeSym]

AllSyms a => AllSyms (Identity a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Identity a -> [SomeSym] -> [SomeSym]

allSyms :: Identity a -> [SomeSym]

(Generic a, AllSyms' (Rep a)) => AllSyms (Default a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Default a -> [SomeSym] -> [SomeSym]

allSyms :: Default a -> [SomeSym]

AllSyms a => AllSyms (UnionM a)

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

Methods

allSymsS :: UnionM a -> [SomeSym] -> [SomeSym]

allSyms :: UnionM a -> [SomeSym]

AllSyms a => AllSyms (Union a)

Defined in Grisette.Internal.Core.Data.Union

Methods

allSymsS :: Union a -> [SomeSym] -> [SomeSym]

allSyms :: Union a -> [SomeSym]

(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n)) => AllSyms (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym]

allSyms :: SomeBV bv -> [SomeSym]

(KnownNat n, 1 <= n) => AllSyms (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

allSymsS :: SymIntN n -> [SomeSym] -> [SomeSym]

allSyms :: SymIntN n -> [SomeSym]

(KnownNat n, 1 <= n) => AllSyms (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

allSymsS :: SymWordN n -> [SomeSym] -> [SomeSym]

allSyms :: SymWordN n -> [SomeSym]

AllSyms a => AllSyms (Maybe a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Maybe a -> [SomeSym] -> [SomeSym]

allSyms :: Maybe a -> [SomeSym]

AllSyms a => AllSyms [a]

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: [a] -> [SomeSym] -> [SomeSym]

allSyms :: [a] -> [SomeSym]

(AllSyms a, AllSyms b) => AllSyms (Either a b)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Either a b -> [SomeSym] -> [SomeSym]

allSyms :: Either a b -> [SomeSym]

ValidFP eb sb => AllSyms (SymFP eb sb)

Defined in Grisette.Internal.SymPrim.SymFP

Methods

allSymsS :: SymFP eb sb -> [SomeSym] -> [SomeSym]

allSyms :: SymFP eb sb -> [SomeSym]

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

allSymsS :: (sa -~> sb) -> [SomeSym] -> [SomeSym]

allSyms :: (sa -~> sb) -> [SomeSym]

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

allSymsS :: (sa =~> sb) -> [SomeSym] -> [SomeSym]

allSyms :: (sa =~> sb) -> [SomeSym]

AllSyms (m (Maybe a)) => AllSyms (MaybeT m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: MaybeT m a -> [SomeSym] -> [SomeSym]

allSyms :: MaybeT m a -> [SomeSym]

(AllSyms a, AllSyms b) => AllSyms (a, b)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b) -> [SomeSym]

AllSyms (m (Either e a)) => AllSyms (ExceptT e m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: ExceptT e m a -> [SomeSym] -> [SomeSym]

allSyms :: ExceptT e m a -> [SomeSym]

AllSyms (m a) => AllSyms (IdentityT m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: IdentityT m a -> [SomeSym] -> [SomeSym]

allSyms :: IdentityT m a -> [SomeSym]

AllSyms (m (a, s)) => AllSyms (WriterT s m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym]

allSyms :: WriterT s m a -> [SomeSym]

AllSyms (m (a, s)) => AllSyms (WriterT s m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym]

allSyms :: WriterT s m a -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c) => AllSyms (a, b, c)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c) -> [SomeSym]

(AllSyms (f a), AllSyms (g a)) => AllSyms (Sum f g a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Sum f g a -> [SomeSym] -> [SomeSym]

allSyms :: Sum f g a -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d) => AllSyms (a, b, c, d)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d) -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e) => AllSyms (a, b, c, d, e)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d, e) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d, e) -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e, AllSyms f) => AllSyms (a, b, c, d, e, f)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d, e, f) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d, e, f) -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e, AllSyms f, AllSyms g) => AllSyms (a, b, c, d, e, f, g)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d, e, f, g) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d, e, f, g) -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e, AllSyms f, AllSyms g, AllSyms h) => AllSyms (a, b, c, d, e, f, g, h)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d, e, f, g, h) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d, e, f, g, h) -> [SomeSym]

allSymsSize :: AllSyms a => a -> Int

Get the total size of symbolic terms in a value. Duplicate sub-terms are counted for only once.

>>> allSymsSize ("a" :: SymInteger, "a" + "b" :: SymInteger, ("a" + "b") * "c" :: SymInteger)
5