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.

omega@cs.umd.edu