Presburger formulas [KK67] are those formulas that can be constructed
by combining affine constraints on integer variables with the logical operations
, 
and 
, and the quantifiers 
and 
.
The affine constraints can be either equality constraints or inequality
constraints (abbreviated as EQs and GEQs respectively).
For example, the formulas in the previous section are Presburger formulas.
There are a number of algorithms for testing the satisfiability of arbitrary
Presburger formulas [KK67,Coo72,PW93].
The best known upper bound on the performance of an algorithm for
verifying Presburger formulas is 
[Opp78],
and we have no reason to believe that our method will provide better
worst-case performance.
However, our method may be more efficient for many simple cases that arise in
our applications.