6. A Fifth Issue: Omega's Presburger Formulae vs Polyhedra

The domain of Presburger formulae can provide more accurate information than the polyhedral one in static program analysis. For example, dependence analysis using polyhedra is structured by Pugh as a decision problem: test simply answer yes or no . Meanwhile, using Presburger formulae, i.e. the OMEGA test, one can construct a set of constraints that describes all possible dependency distance vectors which can be used directly in deciding the validity of program transformation [PUG91].

Presburger formulae contain affine constraints, the usual logical operators, and existential and universal quantifiers. The OMEGA test cannot simplify all Presburger formulae efficiently: there is a $2^{2^n}$ non-deterministic lower bound and a $2^{2^{2^n}}$ deterministic upper bound on the time required to test Presburger formulae satisfiability, where $n$ is the length of the formulae.

Despite their worse case complexities, some algorithms implemented in Omega library are worth to be considered. For example, exact integer projection is implemented in Omega [PUG91], whereas $C^3$'s algorithm only detects exactness when the exact projection is a polyhedron: A projection of a polyhedron along a variable is exact on an integer set if the existence of an integer point in the polyhedron after the elimination of the variable implies the existence of a corresponding integer point in the initial polyhedron.

The Omega test uses the dark shadow method, which is an extension of Fourier-Motzkin method; hence its complexity is exponential. However, in practice, for dependence tests, its time complexity is polynomial [PUG91]. The $C^3$ implementation, using three sufficient conditions defined in [AI91] and in [PUG92], performs the exactness test with lower complexity, while retaining a good percentage of exact responses in experimental results: the exactness rate of the dependence test developed in PIPS for the PerfectClub benchmark is $97,95 \%$ (see [YAN93], page $70$).

We can see in the author's thesis the differences between interfaces for the Omega library and polyhedra. For example, in Omega there is a structure which represents either a relation $R$, or a set $S$. This relation can be used to model a transformer, which belongs to a higher level than the polyhedral domain. Therefore it is necessary to define different generic levels to accommodate all existing interfaces.