Grisette.Core.Data.Class.Evaluate

Evaluating symbolic values with model

class EvaluateSym a where

Evaluating symbolic values with some model.

>>> let model = insertValue (SimpleSymbol "a") (1 :: Integer) emptyModel :: Model
>>> evaluateSym False model ([ssym "a", ssym "b"] :: [SymInteger])
[1,b]

If we set the first argument true, the missing variables will be filled in with some default values:

>>> evaluateSym True model ([ssym "a", ssym "b"] :: [SymInteger])
[1,0]

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 EvaluateSym via (Default X)

Methods

evaluateSym :: Bool -> Model -> a -> a

Evaluate a symbolic variable with some model, possibly fill in values for the missing variables.

Instances

EvaluateSym Int16

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Int16 -> Int16

EvaluateSym Int32

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Int32 -> Int32

EvaluateSym Int64

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Int64 -> Int64

EvaluateSym Int8

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Int8 -> Int8

EvaluateSym Word16

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Word16 -> Word16

EvaluateSym Word32

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Word32 -> Word32

EvaluateSym Word64

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Word64 -> Word64

EvaluateSym Word8

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Word8 -> Word8

EvaluateSym ByteString

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> ByteString -> ByteString

EvaluateSym AssertionError

Defined in Grisette.Core.Control.Exception

Methods

evaluateSym :: Bool -> Model -> AssertionError -> AssertionError

EvaluateSym VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

evaluateSym :: Bool -> Model -> VerificationConditions -> VerificationConditions

EvaluateSym SomeIntN

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> SomeIntN -> SomeIntN

EvaluateSym SomeWordN

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> SomeWordN -> SomeWordN

EvaluateSym SomeSymIntN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> SomeSymIntN -> SomeSymIntN

EvaluateSym SomeSymWordN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> SomeSymWordN -> SomeSymWordN

EvaluateSym SymBool

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> SymBool -> SymBool

EvaluateSym SymInteger

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> SymInteger -> SymInteger

EvaluateSym Integer

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Integer -> Integer

EvaluateSym ()

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> () -> ()

EvaluateSym Bool

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Bool -> Bool

EvaluateSym Char

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Char -> Char

EvaluateSym Int

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Int -> Int

EvaluateSym Word

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Word -> Word

EvaluateSym a => EvaluateSym (Identity a)

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Identity a -> Identity a

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Default a -> Default a

(Mergeable a, EvaluateSym a) => EvaluateSym (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

evaluateSym :: Bool -> Model -> UnionM a -> UnionM a

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> IntN n -> IntN n

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> WordN n -> WordN n

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> SymIntN n -> SymIntN n

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> SymWordN n -> SymWordN n

EvaluateSym a => EvaluateSym (Maybe a)

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Maybe a -> Maybe a

EvaluateSym a => EvaluateSym [a]

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> [a] -> [a]

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Either a b -> Either a b

(EvaluateSym a, EvaluateSym b) => EvaluateSym (CBMCEither a b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

evaluateSym :: Bool -> Model -> CBMCEither a b -> CBMCEither a b

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> (sa -~> sb) -> sa -~> sb

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> (sa =~> sb) -> sa =~> sb

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> MaybeT m a -> MaybeT m a

(EvaluateSym a, EvaluateSym b) => EvaluateSym (a, b)

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> (a, b) -> (a, b)

EvaluateSym (m (CBMCEither e a)) => EvaluateSym (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

evaluateSym :: Bool -> Model -> CBMCExceptT e m a -> CBMCExceptT e m a

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> ExceptT e m a -> ExceptT e m a

EvaluateSym (m a) => EvaluateSym (IdentityT m a)

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> IdentityT m a -> IdentityT m a

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> WriterT s m a -> WriterT s m a

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> WriterT s m a -> WriterT s m a

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> (a, b, c) -> (a, b, c)

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> Sum f g a -> Sum f g a

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> (a, b, c, d) -> (a, b, c, d)

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> (a, b, c, d, e) -> (a, b, c, d, e)

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

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

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)

evaluateSymToCon :: (ToCon a b, EvaluateSym a) => Model -> a -> b

Evaluate a symbolic variable with some model, fill in values for the missing variables, and transform to concrete ones

>>> let model = insertValue (SimpleSymbol "a") (1 :: Integer) emptyModel :: Model
>>> evaluateSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer]
[1,0]