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

Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Expr.VarIdentification

Contents

Description

 
Synopsis

CollectedVarInfo

data QuantifierInfo t tp Source #

Contains all information about a bound variable appearing in the expression.

Constructors

BVI 

Fields

problemFeatures :: Simple Lens (CollectedVarInfo t) ProblemFeatures Source #

Describes types of functionality required by solver based on the problem.

existQuantifiers :: Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t) Source #

Expressions appearing in the problem as existentially quantified when the problem is expressed in negation normal form. This is a map from the existential quantifier element to the info.

forallQuantifiers :: Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t) Source #

Expressions appearing in the problem as existentially quantified when the problem is expressed in negation normal form. This is a map from the existential quantifier element to the info.

CollectedVarInfo generation

data Scope Source #

Information about bound variables outside this context.

Constructors

ExistsOnly 
ExistsForall 

data Polarity Source #

Describes the occurrence of a variable or expression, whether it is negated or not.

Constructors

Positive 
Negative 
Instances
Eq Polarity Source # 
Instance details

Defined in What4.Expr.BoolMap

Ord Polarity Source # 
Instance details

Defined in What4.Expr.BoolMap

Show Polarity Source # 
Instance details

Defined in What4.Expr.BoolMap

Hashable Polarity Source # 
Instance details

Defined in What4.Expr.BoolMap

Methods

hashWithSalt :: Int -> Polarity -> Int #

hash :: Polarity -> Int #

data VarRecorder s t a Source #

Instances
MonadST s (VarRecorder s t) Source # 
Instance details

Defined in What4.Expr.VarIdentification

Methods

liftST :: ST s a -> VarRecorder s t a Source #

Monad (VarRecorder s t) Source # 
Instance details

Defined in What4.Expr.VarIdentification

Methods

(>>=) :: VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b #

(>>) :: VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b #

return :: a -> VarRecorder s t a #

fail :: String -> VarRecorder s t a #

Functor (VarRecorder s t) Source # 
Instance details

Defined in What4.Expr.VarIdentification

Methods

fmap :: (a -> b) -> VarRecorder s t a -> VarRecorder s t b #

(<$) :: a -> VarRecorder s t b -> VarRecorder s t a #

MonadFail (VarRecorder s t) Source # 
Instance details

Defined in What4.Expr.VarIdentification

Methods

fail :: String -> VarRecorder s t a #

Applicative (VarRecorder s t) Source # 
Instance details

Defined in What4.Expr.VarIdentification

Methods

pure :: a -> VarRecorder s t a #

(<*>) :: VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b #

liftA2 :: (a -> b -> c) -> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c #

(*>) :: VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b #

(<*) :: VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a #

recordExprVars :: Scope -> Expr t tp -> VarRecorder s t () Source #

Record the variables in an element.

predicateVarInfo :: Expr t BaseBoolType -> CollectedVarInfo t Source #

Return variables needed to define element as a predicate