MLIR
20.0.0git

Eliminates variable at the specified position using FourierMotzkin variable elimination. More...
Eliminates variable at the specified position using FourierMotzkin 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 nonnull 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 preimage 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 nonempty dark shadow proves the existence of an integer solution. The elimination in such a case could however be an underapproximation, and thus should not be used for scanning sets or used by itself for dependence checking.
Eg: 2d 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.