Module integer_thresholds 

This module defines abstract types for linear arithmetic constraints over parameters, variables and other Atomic values, that can be safely encoded into integer arithmetic SMT constraints.

A type that can be safely encoded into integer constraints will implement the IntoNoDivBooleanExpr trait. Expressions implementing this trait will always be expanded to the least common multiple of the denominators appearing in the expression, thus removing the rational constants in the encoded expression while preserving the satisfying assignments-

This is important as SMTLIB-2 defines integer division analog to how integer division is usually implemented on a computer (see Theory of Ints).

This means for example that the expressions 1 / 2 == 0 is True. In our case, this is not the intended definition. Therefore, if fractions appear as part of boolean expressions, these expressions are expanded until all fractions can be represented as an integer.

For example, an expression of the form x = 1/3 * n will be encoded as 3 * x = n.

Structs

Threshold

WeightedSum of Parameters with additional constant summand

ThresholdConstraint

Threshold in combination with a comparison operator

ThresholdConstraintOver 🔒

This struct represents a Threshold constraint over an object of type T

WeightedSum

Weighted sum of Atomic values

Enums

ThresholdCompOp

Restricted form of ComparisonOp

Traits

IntoNoDivBooleanExpr

Trait for objects that can be encoded into boolean expressions that do not contain any integer divisions or real numbers.

Functions

display_factor_pair_omit_one 🔒

Display a scaled pair but omit factor if it is one