Int package:what4

Lift an integer.

Defines interface between the simulator and terms that are sent to the SAT or SMT solver. The simulator can use a richer set of types, but the symbolic values must be representable by types supported by this interface. A solver backend is defined in terms of a type parameter sym, which is the type that tracks whatever state or context is needed by that particular backend. To instantiate the solver interface, one must provide several type family definitions and class instances for sym:

• type SymExpr sym :: BaseType -> * Type of symbolic expressions.
• type BoundVar sym :: BaseType -> * Representation of bound variables in symbolic expressions.
• type SymFn sym :: Ctx BaseType -> BaseType -> * Representation of symbolic functions.
• instance IsExprBuilder sym Functions for building expressions of various types.
• instance IsSymExprBuilder sym Functions for building expressions with bound variables and quantifiers.
• instance IsExpr (SymExpr sym) Recognizers for various kinds of literal expressions.
• instance OrdF (SymExpr sym)
• instance TestEquality (SymExpr sym)
• instance HashableF (SymExpr sym)
• instance OrdF (BoundVar sym)
• instance TestEquality (BoundVar sym)
• instance HashableF (BoundVar sym)

The canonical implementation of these interface classes is found in What4.Expr.Builder.

The number is between the given lower and upper bounds.

Generated internally by the simulator, or otherwise unknown.

IntTerm v denotes the SMTLIB expression v if v >= 0 and @(- `(negate v)) otherwise.

Standard option style for integral-valued configuration options

Option style for integer-valued options with an upper bound

Option style for integer-valued options with a lower bound

Option style for integer-valued options with upper and lower bounds

Evaluate a weighted sum of integer values.