The constraints of a value-under-constraints object are interpreted as the conjunction of predicates, where each predicate is a binary relation over the ring of polynomials with variables in Symbols(vc) and with rational number coefficients.

The binary relations currently supported are of the form a = b, a <> b, a > b and a >= b, where a and b are polynomials with variables in Symbols(vc) and with rational number coefficients.

The constraints a = b, a <> b, a > b and a >= b are automatically simplified so that b is always zero. As a consequence a is called the defining polynomial of the constraint. Moreover, inequalities of the form a > 0 and a >= 0 are called positive and non-negative, respectively.

We list below some of the transformations that are applied to the constraints of a value-under-constraints object, when this object is created.

If the variables of a defining polynomial a all belong to IntegerSymbols(vc) then we say that a is integer-valued; if this the case and if the inequality a > 0 is a constraint of the value-under-constraints object vc, then this inequality is automatically replaced by an equivalent non-negative inequality.

If a <> 0 and a >= 0 are constraints of vc, then they are automatically replaced by a > 0. Similarly, if a <> 0 and -a >= 0 are constraints of vc, then they automatically replaced by -a > 0.

If a is an integer-valued polynomial, then a = 0 is replaced by the conjunction of a >= 0 and -a >= 0. If a >= 0 and -a >= 0 are constraints of vc, and a is not an integer-valued polynomial, then these constraints are replaced by a = 0.

If a is an integer-valued polynomial, and both a > 0 and 1 -a >= 0 appear both in vc when it is defined, then these two constraints are replaced by a - 1 = 0, that is, a = 1.

If a is an integer-valued polynomial, and both a > 0 and 2 -a > 0 appear both in vc when it is defined, then these two constraints are replaced by a - 1 = 0, that is, a = 1.

An important consequence of these transformations is that, if every defining polynomial is integer-valued, then every constraint is either a non-negative inequality or an inequation.