grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.Evaluate

Description

 
Synopsis

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

EvaluateSym Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

EvaluateSym Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

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

EvaluateSym AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

EvaluateSym VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

EvaluateSym SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

EvaluateSym SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

EvaluateSym SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

EvaluateSym SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

EvaluateSym SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

EvaluateSym SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

EvaluateSym Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

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]