What4.Expr.VarIdentification

CollectedVarInfo

data CollectedVarInfo t

uninterpConstants :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))

latches :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))

data QuantifierInfo t tp

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

Constructors

ForallBound

ExistBound

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

problemFeatures :: Simple Lens (CollectedVarInfo t) ProblemFeatures

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

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

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)

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 :: Simple Lens (CollectedVarInfo t) (Seq (Doc Void))

CollectedVarInfo generation

data Scope

Information about bound variables outside this context.

Constructors

ExistsOnly

ExistsForall

data Polarity

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

Constructors

Positive

Negative

Instances

Eq Polarity

Defined in What4.Expr.BoolMap

Methods

(==) :: Polarity -> Polarity -> Bool

(/=) :: Polarity -> Polarity -> Bool

Ord Polarity

Defined in What4.Expr.BoolMap

Methods

compare :: Polarity -> Polarity -> Ordering

(<) :: Polarity -> Polarity -> Bool

(<=) :: Polarity -> Polarity -> Bool

(>) :: Polarity -> Polarity -> Bool

(>=) :: Polarity -> Polarity -> Bool

max :: Polarity -> Polarity -> Polarity

min :: Polarity -> Polarity -> Polarity

Show Polarity

Defined in What4.Expr.BoolMap

Methods

showsPrec :: Int -> Polarity -> ShowS

show :: Polarity -> String

showList :: [Polarity] -> ShowS

Hashable Polarity

Defined in What4.Expr.BoolMap

Methods

hashWithSalt :: Int -> Polarity -> Int

hash :: Polarity -> Int

data VarRecorder s t a

Instances

MonadST s (VarRecorder s t)

Defined in What4.Expr.VarIdentification

Methods

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

Monad (VarRecorder s t)

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

Functor (VarRecorder s t)

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)

Defined in What4.Expr.VarIdentification

Methods

fail :: String -> VarRecorder s t a

Applicative (VarRecorder s t)

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

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

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

Record the variables in an element.

predicateVarInfo :: Expr t BaseBoolType -> CollectedVarInfo t

Return variables needed to define element as a predicate