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

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Stability | provisional
Safe Haskell | None
Language | Haskell2010

What4.Expr.VarIdentification

Contents

- CollectedVarInfo
- CollectedVarInfo generation

Description

Synopsis

- data CollectedVarInfo t
- uninterpConstants :: forall t f. Functor f => (Set (Some (ExprBoundVar t)) -> f (Set (Some (ExprBoundVar t)))) -> CollectedVarInfo t -> f (CollectedVarInfo t)
- latches :: forall t f. Functor f => (Set (Some (ExprBoundVar t)) -> f (Set (Some (ExprBoundVar t)))) -> CollectedVarInfo t -> f (CollectedVarInfo t)
- data QuantifierInfo t (tp :: BaseType) = BVI {
  - boundTopTerm :: !(NonceAppExpr t BaseBoolType)
  - boundQuant :: !BoundQuant
  - boundVar :: !(ExprBoundVar t tp)
  - boundInnerTerm :: !(Expr t BaseBoolType)
  }
- data BoundQuant
  - = ForallBound
  - | ExistBound
- type QuantifierInfoMap t = Map (NonceAppExpr t BaseBoolType) (Some (QuantifierInfo t))
- problemFeatures :: forall t f. Functor f => (ProblemFeatures -> f ProblemFeatures) -> CollectedVarInfo t -> f (CollectedVarInfo t)
- existQuantifiers :: forall t f. Functor f => (QuantifierInfoMap t -> f (QuantifierInfoMap t)) -> CollectedVarInfo t -> f (CollectedVarInfo t)
- forallQuantifiers :: forall t f. Functor f => (QuantifierInfoMap t -> f (QuantifierInfoMap t)) -> CollectedVarInfo t -> f (CollectedVarInfo t)
- varErrors :: forall t f. Functor f => (Seq (Doc Void) -> f (Seq (Doc Void))) -> CollectedVarInfo t -> f (CollectedVarInfo t)
- data Scope
  - = ExistsOnly
  - | ExistsForall
- data Polarity
  - = Positive
  - | Negative
- data VarRecorder s t a
- collectVarInfo :: VarRecorder s t () -> ST s (CollectedVarInfo t)
- recordExprVars :: forall t (tp :: BaseType) s. Scope -> Expr t tp -> VarRecorder s t ()
- predicateVarInfo :: Expr t BaseBoolType -> CollectedVarInfo t

# CollectedVarInfo

data CollectedVarInfo t Source #

uninterpConstants :: forall t f. Functor f => (Set (Some (ExprBoundVar t)) -> f (Set (Some (ExprBoundVar t)))) -> CollectedVarInfo t -> f (CollectedVarInfo t) Source #

latches :: forall t f. Functor f => (Set (Some (ExprBoundVar t)) -> f (Set (Some (ExprBoundVar t)))) -> CollectedVarInfo t -> f (CollectedVarInfo t) Source #

data QuantifierInfo t (tp :: BaseType) Source #

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

Constructors

BVI |

Fields

- boundTopTerm :: !(NonceAppExpr t BaseBoolType)

  The outer term containing the binding (e.g., Ax.f(x))

- boundQuant :: !BoundQuant

  The type of quantifier that appears

- boundVar :: !(ExprBoundVar t tp)

  The variable that is bound Variables may be bound multiple times.

- boundInnerTerm :: !(Expr t BaseBoolType)

  The term that appears inside the binding.

data BoundQuant Source #

Constructors

ForallBound |
ExistBound |

type QuantifierInfoMap t = Map (NonceAppExpr t BaseBoolType) (Some (QuantifierInfo t)) Source #

problemFeatures :: forall t f. Functor f => (ProblemFeatures -> f ProblemFeatures) -> CollectedVarInfo t -> f (CollectedVarInfo t) Source #

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

existQuantifiers :: forall t f. Functor f => (QuantifierInfoMap t -> f (QuantifierInfoMap t)) -> CollectedVarInfo t -> f (CollectedVarInfo 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 :: forall t f. Functor f => (QuantifierInfoMap t -> f (QuantifierInfoMap t)) -> CollectedVarInfo t -> f (CollectedVarInfo 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.

varErrors :: forall t f. Functor f => (Seq (Doc Void) -> f (Seq (Doc Void))) -> CollectedVarInfo t -> f (CollectedVarInfo t) Source #

# 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

Instances details

Show Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods showsPrec :: Int -> Polarity -> ShowS Source # show :: Polarity -> String Source # showList :: [Polarity] -> ShowS Source #
Eq Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods (==) :: Polarity -> Polarity -> Bool Source # (/=) :: Polarity -> Polarity -> Bool Source #
Ord Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods compare :: Polarity -> Polarity -> Ordering Source # (<) :: Polarity -> Polarity -> Bool Source # (<=) :: Polarity -> Polarity -> Bool Source # (>) :: Polarity -> Polarity -> Bool Source # (>=) :: Polarity -> Polarity -> Bool Source # max :: Polarity -> Polarity -> Polarity Source # min :: Polarity -> Polarity -> Polarity Source #
Hashable Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods hashWithSalt :: Int -> Polarity -> Int Source # hash :: Polarity -> Int Source #

data VarRecorder s t a Source #

#### Instances

Instances details

MonadST s (VarRecorder s t) Source # |
Instance details Defined in What4.Expr.VarIdentification Methods liftST :: ST s a -> VarRecorder s t a Source #
Applicative (VarRecorder s t) Source # |

Instance details

Defined in What4.Expr.VarIdentification

Methods

pure :: a -> VarRecorder s t a Source #

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

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

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

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

Functor (VarRecorder s t) Source # |
Instance details Defined in What4.Expr.VarIdentification Methods fmap :: (a -> b) -> VarRecorder s t a -> VarRecorder s t b Source # (<$) :: a -> VarRecorder s t b -> 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 Source # (>>) :: VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b Source # return :: a -> VarRecorder s t a Source #

collectVarInfo :: VarRecorder s t () -> ST s (CollectedVarInfo t) Source #

recordExprVars :: forall t (tp :: BaseType) s. 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