Eliminates variable at the specified position using Fourier-Motzkin variable elimination. More...

Detailed Description

Eliminates variable at the specified position using Fourier-Motzkin variable elimination.

This technique is exact for rational spaces but conservative (in "rare" cases) for integer spaces. The operation corresponds to a projection operation yielding the (convex) set of integer points contained in the rational shadow of the set. An emptiness test that relies on this method will guarantee emptiness, i.e., it disproves the existence of a solution if it says it's empty. If a non-null isResultIntegerExact is passed, it is set to true if the result is also integer exact. If it's set to false, the obtained solution may not be exact, i.e., it may contain integer points that do not have an integer pre-image in the original set.

Eg: j >= 0, j <= i + 1 i >= 0, i <= N + 1 Eliminating i yields, j >= 0, 0 <= N + 1, j - 1 <= N + 1

If darkShadow = true, this method computes the dark shadow on elimination; the dark shadow is a convex integer subset of the exact integer shadow. A non-empty dark shadow proves the existence of an integer solution. The elimination in such a case could however be an under-approximation, and thus should not be used for scanning sets or used by itself for dependence checking.

Eg: 2-d set, * represents grid points, 'o' represents a point in the set. ^ | | * * * * o o i | * * o o o o | o * * * * * ------------—> j ->

Eliminating i from this system (projecting on the j dimension): rational shadow / integer light shadow: 1 <= j <= 6 dark shadow: 3 <= j <= 6 exact integer shadow: j = 1 holes/splinters: j = 2

darkShadow = false, isResultIntegerExact = nullptr are default values.

The documentation for this union was generated from the following file:

lib/Analysis/Presburger/IntegerRelation.cpp