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: 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.