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

Grisette.Core.Data.Class.Evaluate

Contents

Evaluating symbolic values with model

Description

Synopsis

class EvaluateSym a where
- evaluateSym :: Bool -> Model -> a -> a
evaluateSymToCon :: (ToCon a b, EvaluateSym a) => Model -> a -> b

Evaluating symbolic values with model

class EvaluateSym a where Source #

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

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

Instances

Instances details

EvaluateSym Int16 Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Int16 -> Int16 Source #
EvaluateSym Int32 Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Int32 -> Int32 Source #
EvaluateSym Int64 Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Int64 -> Int64 Source #
EvaluateSym Int8 Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Int8 -> Int8 Source #
EvaluateSym Word16 Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Word16 -> Word16 Source #
EvaluateSym Word32 Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Word32 -> Word32 Source #
EvaluateSym Word64 Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Word64 -> Word64 Source #
EvaluateSym Word8 Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Word8 -> Word8 Source #
EvaluateSym ByteString Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> ByteString -> ByteString Source #
EvaluateSym AssertionError Source #
Instance details Defined in Grisette.Core.Control.Exception Methods evaluateSym :: Bool -> Model -> AssertionError -> AssertionError Source #
EvaluateSym VerificationConditions Source #
Instance details Defined in Grisette.Core.Control.Exception Methods evaluateSym :: Bool -> Model -> VerificationConditions -> VerificationConditions Source #
EvaluateSym SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> SomeIntN -> SomeIntN Source #
EvaluateSym SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> SomeWordN -> SomeWordN Source #
EvaluateSym SomeSymIntN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods evaluateSym :: Bool -> Model -> SomeSymIntN -> SomeSymIntN Source #
EvaluateSym SomeSymWordN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods evaluateSym :: Bool -> Model -> SomeSymWordN -> SomeSymWordN Source #
EvaluateSym SymBool Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods evaluateSym :: Bool -> Model -> SymBool -> SymBool Source #
EvaluateSym SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods evaluateSym :: Bool -> Model -> SymInteger -> SymInteger Source #
EvaluateSym Integer Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Integer -> Integer Source #
EvaluateSym () Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> () -> () Source #
EvaluateSym Bool Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Bool -> Bool Source #
EvaluateSym Char Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Char -> Char Source #
EvaluateSym Int Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Int -> Int Source #
EvaluateSym Word Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Word -> Word Source #
EvaluateSym a => EvaluateSym (Identity a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Identity a -> Identity a Source #
(Generic a, EvaluateSym' (Rep a)) => EvaluateSym (Default a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Default a -> Default a Source #
(Mergeable a, EvaluateSym a) => EvaluateSym (UnionM a) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods evaluateSym :: Bool -> Model -> UnionM a -> UnionM a Source #
(KnownNat n, 1 <= n) => EvaluateSym (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => EvaluateSym (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> WordN n -> WordN n Source #
(KnownNat n, 1 <= n) => EvaluateSym (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods evaluateSym :: Bool -> Model -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => EvaluateSym (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods evaluateSym :: Bool -> Model -> SymWordN n -> SymWordN n Source #
EvaluateSym a => EvaluateSym (Maybe a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Maybe a -> Maybe a Source #
EvaluateSym a => EvaluateSym [a] Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> [a] -> [a] Source #
(EvaluateSym a, EvaluateSym b) => EvaluateSym (Either a b) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Either a b -> Either a b Source #
(EvaluateSym a, EvaluateSym b) => EvaluateSym (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods evaluateSym :: Bool -> Model -> CBMCEither a b -> CBMCEither a b Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => EvaluateSym (sa -~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods evaluateSym :: Bool -> Model -> (sa -~> sb) -> sa -~> sb Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => EvaluateSym (sa =~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods evaluateSym :: Bool -> Model -> (sa =~> sb) -> sa =~> sb Source #
EvaluateSym (m (Maybe a)) => EvaluateSym (MaybeT m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> MaybeT m a -> MaybeT m a Source #
(EvaluateSym a, EvaluateSym b) => EvaluateSym (a, b) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> (a, b) -> (a, b) Source #
EvaluateSym (m (CBMCEither e a)) => EvaluateSym (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods evaluateSym :: Bool -> Model -> CBMCExceptT e m a -> CBMCExceptT e m a Source #
EvaluateSym (m (Either e a)) => EvaluateSym (ExceptT e m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> ExceptT e m a -> ExceptT e m a Source #
EvaluateSym (m a) => EvaluateSym (IdentityT m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> IdentityT m a -> IdentityT m a Source #
EvaluateSym (m (a, s)) => EvaluateSym (WriterT s m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> WriterT s m a -> WriterT s m a Source #
EvaluateSym (m (a, s)) => EvaluateSym (WriterT s m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> WriterT s m a -> WriterT s m a Source #
(EvaluateSym a, EvaluateSym b, EvaluateSym c) => EvaluateSym (a, b, c) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> (a, b, c) -> (a, b, c) Source #
(EvaluateSym (f a), EvaluateSym (g a)) => EvaluateSym (Sum f g a) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> Sum f g a -> Sum f g a Source #
(EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d) => EvaluateSym (a, b, c, d) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> (a, b, c, d) -> (a, b, c, d) Source #
(EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e) => EvaluateSym (a, b, c, d, e) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> (a, b, c, d, e) -> (a, b, c, d, e) Source #
(EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e, EvaluateSym f) => EvaluateSym (a, b, c, d, e, f) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source #
(EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e, EvaluateSym f, EvaluateSym g) => EvaluateSym (a, b, c, d, e, f, g) Source #
Instance details 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) Source #
(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) Source #
Instance details 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) Source #

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

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]