Grisette.Core.Data.Class.ToSym

Converting to symbolic values

class ToSym a b where

Convert a concrete value to symbolic value.

Methods

toSym :: a -> b

Convert a concrete value to symbolic value.

>>> toSym False :: SymBool
false

>>> toSym [False, True] :: [SymBool]
[false,true]

Instances

ToSym Int16 Int16

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int16 -> Int16

ToSym Int32 Int32

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int32 -> Int32

ToSym Int64 Int64

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int64 -> Int64

ToSym Int8 Int8

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int8 -> Int8

ToSym Word16 Word16

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word16 -> Word16

ToSym Word32 Word32

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word32 -> Word32

ToSym Word64 Word64

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word64 -> Word64

ToSym ByteString ByteString

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: ByteString -> ByteString

ToSym AssertionError AssertionError

Defined in Grisette.Core.Control.Exception

Methods

toSym :: AssertionError -> AssertionError

ToSym VerificationConditions VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

toSym :: VerificationConditions -> VerificationConditions

ToSym Word8 Word8

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word8 -> Word8

ToSym Integer Integer

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Integer -> Integer

ToSym () ()

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: () -> ()

ToSym Bool Bool

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Bool -> Bool

ToSym Char Char

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Char -> Char

ToSym Int Int

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int -> Int

ToSym Word Word

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word -> Word

ToSym Int16 (Sym (IntN 16))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int16 -> Sym (IntN 16)

ToSym Int32 (Sym (IntN 32))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int32 -> Sym (IntN 32)

ToSym Int64 (Sym (IntN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int64 -> Sym (IntN 64)

ToSym Int8 (Sym (IntN 8))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int8 -> Sym (IntN 8)

ToSym Word16 (Sym (WordN 16))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word16 -> Sym (WordN 16)

ToSym Word32 (Sym (WordN 32))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word32 -> Sym (WordN 32)

ToSym Word64 (Sym (WordN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word64 -> Sym (WordN 64)

ToSym Word8 (Sym (WordN 8))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word8 -> Sym (WordN 8)

ToSym Int (Sym (IntN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int -> Sym (IntN 64)

ToSym Word (Sym (WordN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word -> Sym (WordN 64)

(Generic a, Generic b, ToSym' (Rep a) (Rep b)) => ToSym a (Default b)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: a -> Default b

(ToSym a b, Mergeable b) => ToSym a (UnionM b)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: a -> UnionM b

SupportedPrim a => ToSym a (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: a -> Sym a

ToSym a b => ToSym (Identity a) (Identity b)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Identity a -> Identity b

(ToSym a b, Mergeable b) => ToSym (UnionM a) (UnionM b)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM a -> UnionM b

SupportedPrim a => ToSym (Sym a) (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Sym a -> Sym a

ToSym a b => ToSym (Maybe a) (Maybe b)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Maybe a -> Maybe b

ToSym a b => ToSym [a] [b]

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: [a] -> [b]

(ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (Either e2 a2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Either e1 a1 -> Either e2 a2

(ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (CBMCEither e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: Either e1 a1 -> CBMCEither e2 a2

(ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (Either e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCEither e1 a1 -> Either e2 a2

(ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (CBMCEither e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2

ToSym (m1 (Maybe a)) (m2 (Maybe b)) => ToSym (MaybeT m1 a) (MaybeT m2 b)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: MaybeT m1 a -> MaybeT m2 b

ToSym a b => ToSym (v -> a) (v -> b)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (v -> a) -> v -> b

(ToSym a1 b1, ToSym a2 b2) => ToSym (a1, a2) (b1, b2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, a2) -> (b1, b2)

ToSym (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) => ToSym (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCExceptT e1 m1 a -> CBMCExceptT e2 m2 b

ToSym (m1 (Either e1 a)) (m2 (Either e2 b)) => ToSym (ExceptT e1 m1 a) (ExceptT e2 m2 b)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: ExceptT e1 m1 a -> ExceptT e2 m2 b

ToSym (m a) (m1 b) => ToSym (IdentityT m a) (IdentityT m1 b)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: IdentityT m a -> IdentityT m1 b

ToSym (s1 -> m1 a1) (s2 -> m2 a2) => ToSym (ReaderT s1 m1 a1) (ReaderT s2 m2 a2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: ReaderT s1 m1 a1 -> ReaderT s2 m2 a2

ToSym (s1 -> m1 (a1, s1)) (s2 -> m2 (a2, s2)) => ToSym (StateT s1 m1 a1) (StateT s2 m2 a2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: StateT s1 m1 a1 -> StateT s2 m2 a2

ToSym (s1 -> m1 (a1, s1)) (s2 -> m2 (a2, s2)) => ToSym (StateT s1 m1 a1) (StateT s2 m2 a2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: StateT s1 m1 a1 -> StateT s2 m2 a2

ToSym (m1 (a1, s1)) (m2 (a2, s2)) => ToSym (WriterT s1 m1 a1) (WriterT s2 m2 a2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: WriterT s1 m1 a1 -> WriterT s2 m2 a2

ToSym (m1 (a1, s1)) (m2 (a2, s2)) => ToSym (WriterT s1 m1 a1) (WriterT s2 m2 a2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: WriterT s1 m1 a1 -> WriterT s2 m2 a2

(ToSym a1 b1, ToSym a2 b2, ToSym a3 b3) => ToSym (a1, a2, a3) (b1, b2, b3)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, a2, a3) -> (b1, b2, b3)

(ToSym (f a) (f1 a1), ToSym (g a) (g1 a1)) => ToSym (Sum f g a) (Sum f1 g1 a1)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Sum f g a -> Sum f1 g1 a1

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2) => ToSym (a1, b1, c1, d1) (a2, b2, c2, d2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1) -> (a2, b2, c2, d2)

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2, ToSym e1 e2) => ToSym (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1, e1) -> (a2, b2, c2, d2, e2)

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2, ToSym e1 e2, ToSym f1 f2) => ToSym (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1, e1, f1) -> (a2, b2, c2, d2, e2, f2)

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2, ToSym e1 e2, ToSym f1 f2, ToSym g1 g2) => ToSym (a1, b1, c1, d1, e1, f1, g1) (a2, b2, c2, d2, e2, f2, g2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1, e1, f1, g1) -> (a2, b2, c2, d2, e2, f2, g2)

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2, ToSym e1 e2, ToSym f1 f2, ToSym g1 g2, ToSym h1 h2) => ToSym (a1, b1, c1, d1, e1, f1, g1, h1) (a2, b2, c2, d2, e2, f2, g2, h2)

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1, e1, f1, g1, h1) -> (a2, b2, c2, d2, e2, f2, g2, h2)