Grisette.Internal.SymPrim.AllSyms

Get all symbolic primitive values in a value

data SomeSym where

Some symbolic value with LinkedRep constraint.

Constructors

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

Instances

Show SomeSym

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

showsPrec :: Int -> SomeSym -> ShowS

show :: SomeSym -> String

showList :: [SomeSym] -> ShowS

class AllSyms a where

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

>>> allSyms (["a" + 1 :: SymInteger, -"b"], "c" :: SymBool)
[(+ 1 a),(- b),c]

This is usually used for getting a statistical summary of the size of a symbolic value with allSymsSize.

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.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Int16 -> [SomeSym]

AllSyms Int32

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Int32 -> [SomeSym]

AllSyms Int64

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Int64 -> [SomeSym]

AllSyms Int8

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Int8 -> [SomeSym]

AllSyms Word16

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Word16 -> [SomeSym]

AllSyms Word32

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Word32 -> [SomeSym]

AllSyms Word64

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Word64 -> [SomeSym]

AllSyms Word8

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Word8 -> [SomeSym]

AllSyms ByteString

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: ByteString -> [SomeSym]

AllSyms AssertionError

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: AssertionError -> [SomeSym]

AllSyms VerificationConditions

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: VerificationConditions -> [SomeSym]

AllSyms AlgReal

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: AlgReal -> [SomeSym] -> [SomeSym]

allSyms :: AlgReal -> [SomeSym]

AllSyms FPRoundingMode

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: FPRoundingMode -> [SomeSym] -> [SomeSym]

allSyms :: FPRoundingMode -> [SomeSym]

AllSyms SymAlgReal

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

allSymsS :: SymAlgReal -> [SomeSym] -> [SomeSym]

allSyms :: SymAlgReal -> [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.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Text -> [SomeSym]

AllSyms Integer

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Integer -> [SomeSym]

AllSyms ()

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: () -> [SomeSym]

AllSyms Bool

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Bool -> [SomeSym]

AllSyms Char

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Char -> [SomeSym]

AllSyms Double

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: Double -> [SomeSym] -> [SomeSym]

allSyms :: Double -> [SomeSym]

AllSyms Float

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: Float -> [SomeSym] -> [SomeSym]

allSyms :: Float -> [SomeSym]

AllSyms Int

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Int -> [SomeSym]

AllSyms Word

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Word -> [SomeSym]

AllSyms a => AllSyms (Identity a)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Identity a -> [SomeSym]

AllSyms a => AllSyms (Ratio a)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Ratio a -> [SomeSym]

(Generic a, GAllSyms Arity0 (Rep a)) => AllSyms (Default a)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

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

allSyms :: Default a -> [SomeSym]

AllSyms a => AllSyms (Union a)

Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union

Methods

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

allSyms :: Union a -> [SomeSym]

AllSyms a => AllSyms (UnionBase a)

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

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

allSyms :: UnionBase a -> [SomeSym]

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

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: IntN n -> [SomeSym]

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

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: WordN n -> [SomeSym]

(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n), MaySomeBV bv) => 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.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Maybe a -> [SomeSym]

AllSyms a => AllSyms [a]

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: [a] -> [SomeSym]

(AllSyms a1, AllSyms a2) => AllSyms (Either a1 a2)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: Either a1 a2 -> [SomeSym] -> [SomeSym]

allSyms :: Either a1 a2 -> [SomeSym]

AllSyms (Proxy a)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: Proxy a -> [SomeSym]

(Generic1 f, GAllSyms Arity1 (Rep1 f), AllSyms a) => AllSyms (Default1 f a)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

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

allSyms :: Default1 f a -> [SomeSym]

ValidFP eb sb => AllSyms (FP eb sb)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: FP eb sb -> [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]

AllSyms (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

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

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

AllSyms (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

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

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

(AllSyms1 a1, AllSyms a2) => AllSyms (MaybeT a1 a2)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: MaybeT a1 a2 -> [SomeSym] -> [SomeSym]

allSyms :: MaybeT a1 a2 -> [SomeSym]

(AllSyms a1, AllSyms a2) => AllSyms (a1, a2)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2) -> [SomeSym]

(AllSyms a1, AllSyms1 a2, AllSyms a3) => AllSyms (ExceptT a1 a2 a3)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: ExceptT a1 a2 a3 -> [SomeSym] -> [SomeSym]

allSyms :: ExceptT a1 a2 a3 -> [SomeSym]

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

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: IdentityT m a -> [SomeSym]

(AllSyms a1, AllSyms1 a2, AllSyms a3) => AllSyms (WriterT a1 a2 a3)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: WriterT a1 a2 a3 -> [SomeSym] -> [SomeSym]

allSyms :: WriterT a1 a2 a3 -> [SomeSym]

(AllSyms a1, AllSyms1 a2, AllSyms a3) => AllSyms (WriterT a1 a2 a3)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: WriterT a1 a2 a3 -> [SomeSym] -> [SomeSym]

allSyms :: WriterT a1 a2 a3 -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3) => AllSyms (a1, a2, a3)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3) -> [SomeSym]

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

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

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

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4) => AllSyms (a1, a2, a3, a4)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5) => AllSyms (a1, a2, a3, a4, a5)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6) => AllSyms (a1, a2, a3, a4, a5, a6)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7) => AllSyms (a1, a2, a3, a4, a5, a6, a7)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13, AllSyms a14) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13, AllSyms a14, AllSyms a15) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> [SomeSym] -> [SomeSym]

allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> [SomeSym]

class (forall a. AllSyms a => AllSyms (f a)) => AllSyms1 f where

Lifting of the AllSyms class to unary type constructors.

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]

Lift the allSymsS function to unary type constructors.

Instances

AllSyms1 Identity

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Identity a -> [SomeSym] -> [SomeSym]

AllSyms1 Union

Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Union a -> [SomeSym] -> [SomeSym]

AllSyms1 UnionBase

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> UnionBase a -> [SomeSym] -> [SomeSym]

AllSyms1 Maybe

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Maybe a -> [SomeSym] -> [SomeSym]

AllSyms1 List

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> [a] -> [SomeSym] -> [SomeSym]

AllSyms a => AllSyms1 (Either a)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a0 -> [SomeSym] -> [SomeSym]) -> Either a a0 -> [SomeSym] -> [SomeSym]

AllSyms1 (Proxy :: Type -> Type)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Proxy a -> [SomeSym] -> [SomeSym]

(Generic1 f, GAllSyms Arity1 (Rep1 f)) => AllSyms1 (Default1 f)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Default1 f a -> [SomeSym] -> [SomeSym]

AllSyms1 a => AllSyms1 (MaybeT a)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a0 -> [SomeSym] -> [SomeSym]) -> MaybeT a a0 -> [SomeSym] -> [SomeSym]

AllSyms a => AllSyms1 ((,) a)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a0 -> [SomeSym] -> [SomeSym]) -> (a, a0) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms1 a2) => AllSyms1 (ExceptT a1 a2)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> ExceptT a1 a2 a -> [SomeSym] -> [SomeSym]

AllSyms1 m => AllSyms1 (IdentityT m)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> IdentityT m a -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms1 a2) => AllSyms1 (WriterT a1 a2)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> WriterT a1 a2 a -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms1 a2) => AllSyms1 (WriterT a1 a2)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> WriterT a1 a2 a -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2) => AllSyms1 ((,,) a1 a2)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a) -> [SomeSym] -> [SomeSym]

(AllSyms1 f, AllSyms1 g) => AllSyms1 (Sum f g)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Sum f g a -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3) => AllSyms1 ((,,,) a1 a2 a3)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4) => AllSyms1 ((,,,,) a1 a2 a3 a4)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5) => AllSyms1 ((,,,,,) a1 a2 a3 a4 a5)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6) => AllSyms1 ((,,,,,,) a1 a2 a3 a4 a5 a6)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7) => AllSyms1 ((,,,,,,,) a1 a2 a3 a4 a5 a6 a7)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8) => AllSyms1 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9) => AllSyms1 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10) => AllSyms1 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11) => AllSyms1 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12) => AllSyms1 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13) => AllSyms1 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13, AllSyms a14) => AllSyms1 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) -> [SomeSym] -> [SomeSym]

allSymsS1 :: (AllSyms1 f, AllSyms a) => f a -> [SomeSym] -> [SomeSym]

Lift the standard allSymsS function to unary type constructors.

class (forall a. AllSyms a => AllSyms1 (f a)) => AllSyms2 f where

Lifting of the AllSyms class to binary type constructors.

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> f a b -> [SomeSym] -> [SomeSym]

Lift the allSymsS function to binary type constructors.

Instances

AllSyms2 Either

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> Either a b -> [SomeSym] -> [SomeSym]

AllSyms2 (,)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

AllSyms a => AllSyms2 ((,,) a)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a0 -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a, a0, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2) => AllSyms2 ((,,,) a1 a2)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3) => AllSyms2 ((,,,,) a1 a2 a3)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4) => AllSyms2 ((,,,,,) a1 a2 a3 a4)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5) => AllSyms2 ((,,,,,,) a1 a2 a3 a4 a5)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6) => AllSyms2 ((,,,,,,,) a1 a2 a3 a4 a5 a6)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7) => AllSyms2 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8) => AllSyms2 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9) => AllSyms2 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10) => AllSyms2 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11) => AllSyms2 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12) => AllSyms2 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) -> [SomeSym] -> [SomeSym]

(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13) => AllSyms2 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13)

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, b) -> [SomeSym] -> [SomeSym]

allSymsS2 :: (AllSyms2 f, AllSyms a, AllSyms b) => f a b -> [SomeSym] -> [SomeSym]

Lift the standard allSymsS function to binary type constructors.

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

The 5 terms are a, b, (+ a b), c, and (* (+ a b) c).

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

Generic AllSyms

data family AllSymsArgs arity a :: Type

The arguments to the generic AllSyms function.

Instances

data AllSymsArgs Arity0 _

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

data AllSymsArgs Arity0 _ = AllSymsArgs0

newtype AllSymsArgs Arity1 a

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

newtype AllSymsArgs Arity1 a = AllSymsArgs1 (a -> [SomeSym] -> [SomeSym])

class GAllSyms arity f where

The class of types that can generically extract all symbolic primitives.

Methods

gallSymsS :: AllSymsArgs arity a -> f a -> [SomeSym] -> [SomeSym]

Instances

GAllSyms Arity1 Par1

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs Arity1 a -> Par1 a -> [SomeSym] -> [SomeSym]

GAllSyms arity (U1 :: Type -> Type)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs arity a -> U1 a -> [SomeSym] -> [SomeSym]

GAllSyms arity (V1 :: Type -> Type)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs arity a -> V1 a -> [SomeSym] -> [SomeSym]

AllSyms1 f => GAllSyms Arity1 (Rec1 f)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs Arity1 a -> Rec1 f a -> [SomeSym] -> [SomeSym]

(GAllSyms arity a, GAllSyms arity b) => GAllSyms arity (a :*: b)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs arity a0 -> (a :*: b) a0 -> [SomeSym] -> [SomeSym]

(GAllSyms arity a, GAllSyms arity b) => GAllSyms arity (a :+: b)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs arity a0 -> (a :+: b) a0 -> [SomeSym] -> [SomeSym]

AllSyms c => GAllSyms arity (K1 i c :: Type -> Type)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs arity a -> K1 i c a -> [SomeSym] -> [SomeSym]

(AllSyms1 f, GAllSyms Arity1 g) => GAllSyms Arity1 (f :.: g)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs Arity1 a -> (f :.: g) a -> [SomeSym] -> [SomeSym]

GAllSyms arity a => GAllSyms arity (M1 i c a)

Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms

Methods

gallSymsS :: AllSymsArgs arity a0 -> M1 i c a a0 -> [SomeSym] -> [SomeSym]

genericAllSymsS :: (Generic a, GAllSyms Arity0 (Rep a)) => a -> [SomeSym] -> [SomeSym]

Generic allSymsS function.

genericLiftAllSymsS :: (Generic1 f, GAllSyms Arity1 (Rep1 f)) => (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]

Generic liftAllSymsS function.