What4.Expr.GroundEval

Given a collection of assignments to the symbolic values appearing in an expression, this module computes the ground value.

Ground evaluation

type family GroundValue (tp :: BaseType) where ...

Equations

GroundValue BaseBoolType = Bool

GroundValue BaseIntegerType = Integer

GroundValue BaseRealType = Rational

GroundValue (BaseBVType w) = BV w

GroundValue (BaseFloatType fpp) = BigFloat

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

A newtype wrapper around ground value for use in a cache.

Constructors

GVW

Fields

• unGVW :: GroundValue tp

data GroundArray idx b

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)

Look up an index in an ground array.

newtype GroundEvalFn t

A function that calculates ground values for elements. Clients of solvers should use the groundEval function for computing values in models.

Constructors

GroundEvalFn

Fields

• groundEval :: forall tp. Expr t tp -> IO (GroundValue tp)

type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)

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 -> MaybeT IO (GroundValue u)) -> Expr t tp -> MaybeT IO (GroundValue tp)

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)

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 -> MaybeT IO (GroundValue u)) -> App (Expr t) tp -> MaybeT IO (GroundValue tp)

Helper function for evaluating App expressions.

This function is intended for implementers of symbolic backends.

evalGroundNonceApp :: Monad m => (forall u. Expr t u -> MaybeT m (GroundValue u)) -> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp)

Helper function for evaluating NonceApp expressions.

This function is intended for implementers of symbolic backends.

defaultValueForType :: BaseTypeRepr tp -> GroundValue tp

Construct a default value for a given base type.

groundEq :: BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool