what4-1.0: Solver-agnostic symbolic values support for issuing queries

Copyright(c) Galois Inc 2016-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Expr.GroundEval

Contents

Description

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

Synopsis

Ground evaluation

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.