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