next up previous
Next: 3.4 Relational and set Up: 3 Relational Expression syntax Previous: 3.2 Presburger formula operations

3.3 Constraints and arithmetic and comparison operations

A Presburger formula is built from constraints using the operations described in the previous subsection. In this subsection we describe the syntax of individual constraints.

A constraint is a series of expression lists, connected with the arithmetic relational operators =, !=, >, >=, <, <=. An example is 2i + 3j <= 5k,p <= 3x-z = t.

When an constraint contains a comma-separated list of expressions, it indicates that the same constraints should be introduced for each of the expressions. The constraint a,b <= c,d > e,f translates to the constraints

Expressions can be of the forms (where var is a variable, integer is an integer constant, and e, , and are expressions): var, integer, e, integer e, , , , - e, .

An important restriction is that all expressions in the constraints must be affine functions of the variables. For example, is legal, is legal, but is illegal.