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

Grisette.Internal.SymPrim.AllSyms

Description

Synopsis

symSize :: forall con sym. LinkedRep con sym => sym -> Int
symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int
data SomeSym where
- SomeSym :: LinkedRep con sym => sym -> SomeSym
class AllSyms a where
- allSymsS :: a -> [SomeSym] -> [SomeSym]
- allSyms :: a -> [SomeSym]
allSymsSize :: AllSyms a => a -> Int

Documentation

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

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 Source #

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 Source #

Some symbolic value with LinkedRep constraint.

Constructors

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

class AllSyms a where Source #

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] Source #

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

allSyms :: a -> [SomeSym] Source #

Specialized allSymsS that prepends to an empty list.

Instances

Instances details

AllSyms Int16 Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Int16 -> [SomeSym] -> [SomeSym] Source # allSyms :: Int16 -> [SomeSym] Source #
AllSyms Int32 Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Int32 -> [SomeSym] -> [SomeSym] Source # allSyms :: Int32 -> [SomeSym] Source #
AllSyms Int64 Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Int64 -> [SomeSym] -> [SomeSym] Source # allSyms :: Int64 -> [SomeSym] Source #
AllSyms Int8 Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Int8 -> [SomeSym] -> [SomeSym] Source # allSyms :: Int8 -> [SomeSym] Source #
AllSyms Word16 Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Word16 -> [SomeSym] -> [SomeSym] Source # allSyms :: Word16 -> [SomeSym] Source #
AllSyms Word32 Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Word32 -> [SomeSym] -> [SomeSym] Source # allSyms :: Word32 -> [SomeSym] Source #
AllSyms Word64 Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Word64 -> [SomeSym] -> [SomeSym] Source # allSyms :: Word64 -> [SomeSym] Source #
AllSyms Word8 Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Word8 -> [SomeSym] -> [SomeSym] Source # allSyms :: Word8 -> [SomeSym] Source #
AllSyms ByteString Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: ByteString -> [SomeSym] -> [SomeSym] Source # allSyms :: ByteString -> [SomeSym] Source #
AllSyms AssertionError Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: AssertionError -> [SomeSym] -> [SomeSym] Source # allSyms :: AssertionError -> [SomeSym] Source #
AllSyms VerificationConditions Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: VerificationConditions -> [SomeSym] -> [SomeSym] Source # allSyms :: VerificationConditions -> [SomeSym] Source #
AllSyms SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Methods allSymsS :: SymBool -> [SomeSym] -> [SomeSym] Source # allSyms :: SymBool -> [SomeSym] Source #
AllSyms SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods allSymsS :: SymInteger -> [SomeSym] -> [SomeSym] Source # allSyms :: SymInteger -> [SomeSym] Source #
AllSyms Text Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Text -> [SomeSym] -> [SomeSym] Source # allSyms :: Text -> [SomeSym] Source #
AllSyms Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Integer -> [SomeSym] -> [SomeSym] Source # allSyms :: Integer -> [SomeSym] Source #
AllSyms () Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: () -> [SomeSym] -> [SomeSym] Source # allSyms :: () -> [SomeSym] Source #
AllSyms Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Bool -> [SomeSym] -> [SomeSym] Source # allSyms :: Bool -> [SomeSym] Source #
AllSyms Char Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Char -> [SomeSym] -> [SomeSym] Source # allSyms :: Char -> [SomeSym] Source #
AllSyms Int Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Int -> [SomeSym] -> [SomeSym] Source # allSyms :: Int -> [SomeSym] Source #
AllSyms Word Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Word -> [SomeSym] -> [SomeSym] Source # allSyms :: Word -> [SomeSym] Source #
AllSyms a => AllSyms (Identity a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Identity a -> [SomeSym] -> [SomeSym] Source # allSyms :: Identity a -> [SomeSym] Source #
(Generic a, AllSyms' (Rep a)) => AllSyms (Default a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Default a -> [SomeSym] -> [SomeSym] Source # allSyms :: Default a -> [SomeSym] Source #
AllSyms a => AllSyms (UnionM a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods allSymsS :: UnionM a -> [SomeSym] -> [SomeSym] Source # allSyms :: UnionM a -> [SomeSym] Source #
AllSyms a => AllSyms (Union a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Union Methods allSymsS :: Union a -> [SomeSym] -> [SomeSym] Source # allSyms :: Union a -> [SomeSym] Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n)) => AllSyms (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym] Source # allSyms :: SomeBV bv -> [SomeSym] Source #
(KnownNat n, 1 <= n) => AllSyms (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods allSymsS :: SymIntN n -> [SomeSym] -> [SomeSym] Source # allSyms :: SymIntN n -> [SomeSym] Source #
(KnownNat n, 1 <= n) => AllSyms (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods allSymsS :: SymWordN n -> [SomeSym] -> [SomeSym] Source # allSyms :: SymWordN n -> [SomeSym] Source #
AllSyms a => AllSyms (Maybe a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Maybe a -> [SomeSym] -> [SomeSym] Source # allSyms :: Maybe a -> [SomeSym] Source #
AllSyms a => AllSyms [a] Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: [a] -> [SomeSym] -> [SomeSym] Source # allSyms :: [a] -> [SomeSym] Source #
(AllSyms a, AllSyms b) => AllSyms (Either a b) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Either a b -> [SomeSym] -> [SomeSym] Source # allSyms :: Either a b -> [SomeSym] Source #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods allSymsS :: (sa -~> sb) -> [SomeSym] -> [SomeSym] Source # allSyms :: (sa -~> sb) -> [SomeSym] Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods allSymsS :: (sa =~> sb) -> [SomeSym] -> [SomeSym] Source # allSyms :: (sa =~> sb) -> [SomeSym] Source #
AllSyms (m (Maybe a)) => AllSyms (MaybeT m a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: MaybeT m a -> [SomeSym] -> [SomeSym] Source # allSyms :: MaybeT m a -> [SomeSym] Source #
(AllSyms a, AllSyms b) => AllSyms (a, b) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: (a, b) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a, b) -> [SomeSym] Source #
AllSyms (m (Either e a)) => AllSyms (ExceptT e m a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: ExceptT e m a -> [SomeSym] -> [SomeSym] Source # allSyms :: ExceptT e m a -> [SomeSym] Source #
AllSyms (m a) => AllSyms (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: IdentityT m a -> [SomeSym] -> [SomeSym] Source # allSyms :: IdentityT m a -> [SomeSym] Source #
AllSyms (m (a, s)) => AllSyms (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym] Source # allSyms :: WriterT s m a -> [SomeSym] Source #
AllSyms (m (a, s)) => AllSyms (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym] Source # allSyms :: WriterT s m a -> [SomeSym] Source #
(AllSyms a, AllSyms b, AllSyms c) => AllSyms (a, b, c) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: (a, b, c) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a, b, c) -> [SomeSym] Source #
(AllSyms (f a), AllSyms (g a)) => AllSyms (Sum f g a) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: Sum f g a -> [SomeSym] -> [SomeSym] Source # allSyms :: Sum f g a -> [SomeSym] Source #
(AllSyms a, AllSyms b, AllSyms c, AllSyms d) => AllSyms (a, b, c, d) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: (a, b, c, d) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a, b, c, d) -> [SomeSym] Source #
(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e) => AllSyms (a, b, c, d, e) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: (a, b, c, d, e) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a, b, c, d, e) -> [SomeSym] Source #
(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e, AllSyms f) => AllSyms (a, b, c, d, e, f) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: (a, b, c, d, e, f) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a, b, c, d, e, f) -> [SomeSym] Source #
(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e, AllSyms f, AllSyms g) => AllSyms (a, b, c, d, e, f, g) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: (a, b, c, d, e, f, g) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a, b, c, d, e, f, g) -> [SomeSym] Source #
(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) Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: (a, b, c, d, e, f, g, h) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a, b, c, d, e, f, g, h) -> [SomeSym] Source #

allSymsSize :: AllSyms a => a -> Int Source #

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