| Copyright | (c) Galois Inc 2016-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Stability | provisional |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Expr.GroundEval
Description
Given a collection of assignments to the symbolic values appearing in an expression, this module computes the ground value.
Synopsis
- type family GroundValue (tp :: BaseType) where ...
- newtype GroundValueWrapper tp = GVW {
- unGVW :: GroundValue tp
- data GroundArray idx b
- = ArrayMapping (Assignment GroundValueWrapper idx -> IO (GroundValue b))
- | ArrayConcrete (GroundValue b) (Map (Assignment IndexLit idx) (GroundValue b))
- lookupArray :: Assignment BaseTypeRepr idx -> GroundArray idx b -> Assignment GroundValueWrapper idx -> IO (GroundValue b)
- newtype GroundEvalFn t = GroundEvalFn {
- groundEval :: forall tp. Expr t tp -> IO (GroundValue tp)
- type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)
- tryEvalGroundExpr :: (forall u. Expr t u -> IO (GroundValue u)) -> Expr t tp -> MaybeT IO (GroundValue tp)
- evalGroundExpr :: (forall u. Expr t u -> IO (GroundValue u)) -> Expr t tp -> IO (GroundValue tp)
- evalGroundApp :: forall t tp. (forall u. Expr t u -> IO (GroundValue u)) -> App (Expr t) tp -> MaybeT IO (GroundValue tp)
- evalGroundNonceApp :: MonadFail m => (forall u. Expr t u -> MaybeT m (GroundValue u)) -> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp)
- defaultValueForType :: BaseTypeRepr tp -> GroundValue tp
Ground evaluation
type family GroundValue (tp :: BaseType) where ... Source #
Equations
| GroundValue BaseBoolType = Bool | |
| GroundValue BaseNatType = Natural | |
| GroundValue BaseIntegerType = Integer | |
| GroundValue BaseRealType = Rational | |
| GroundValue (BaseBVType w) = BV w | |
| GroundValue (BaseFloatType fpp) = BV (FloatPrecisionBits fpp) | |
| GroundValue BaseComplexType = Complex Rational | |
| GroundValue (BaseStringType si) = StringLiteral si | |
| GroundValue (BaseArrayType idx b) = GroundArray idx b | |
| GroundValue (BaseStructType ctx) = Assignment GroundValueWrapper ctx |
newtype GroundValueWrapper tp Source #
A newtype wrapper around ground value for use in a cache.
Constructors
| GVW | |
Fields
| |
data GroundArray idx b Source #
A representation of a ground-value array.
Constructors
| ArrayMapping (Assignment GroundValueWrapper idx -> IO (GroundValue b)) | Lookup function for querying by index |
| ArrayConcrete (GroundValue b) (Map (Assignment IndexLit idx) (GroundValue b)) | Default value and finite map of particular indices |
lookupArray :: Assignment BaseTypeRepr idx -> GroundArray idx b -> Assignment GroundValueWrapper idx -> IO (GroundValue b) Source #
Look up an index in an ground array.
newtype GroundEvalFn t Source #
A function that calculates ground values for elements.
Clients of solvers should use the groundEval function for computing
values in models.
Constructors
| GroundEvalFn | |
Fields
| |
type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational) Source #
Function that calculates upper and lower bounds for real-valued elements. This type is used for solvers (e.g., dReal) that give only approximate solutions.
Internal operations
tryEvalGroundExpr :: (forall u. Expr t u -> IO (GroundValue u)) -> Expr t tp -> MaybeT IO (GroundValue tp) Source #
Evaluate an element, when given an evaluation function for
subelements. Instead of recursing directly, tryEvalGroundExpr
calls into the given function on sub-elements to allow the caller
to cache results if desired.
However, sometimes we are unable to compute expressions outside
the solver. In these cases, this function will return Nothing
in the `MaybeT IO` monad. In these cases, the caller should instead
query the solver directly to evaluate the expression, if possible.
evalGroundExpr :: (forall u. Expr t u -> IO (GroundValue u)) -> Expr t tp -> IO (GroundValue tp) Source #
Helper function for evaluating Expr expressions in a model.
This function is intended for implementers of symbolic backends.
evalGroundApp :: forall t tp. (forall u. Expr t u -> IO (GroundValue u)) -> App (Expr t) tp -> MaybeT IO (GroundValue tp) Source #
Helper function for evaluating App expressions.
This function is intended for implementers of symbolic backends.
evalGroundNonceApp :: MonadFail m => (forall u. Expr t u -> MaybeT m (GroundValue u)) -> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp) Source #
Helper function for evaluating NonceApp expressions.
This function is intended for implementers of symbolic backends.
defaultValueForType :: BaseTypeRepr tp -> GroundValue tp Source #
Construct a default value for a given base type.