Commit Graph

3 Commits

Author SHA1 Message Date
Arjun P 6ebeba88f5 Support emptiness checks for unbounded FlatAffineConstraints.
With this, we have complete support for emptiness checks. This also paves the way for future support to check if two FlatAffineConstraints are equal.

Reviewed By: ftynse

Differential Revision: https://reviews.llvm.org/D94272
2021-01-14 19:33:37 +01:00
Arjun P 63dead2096 Introduce subtraction for FlatAffineConstraints
Subtraction is a foundational arithmetic operation that is often used when computing, for example, data transfer sets or cache hits. Since the result of subtraction need not be a convex polytope, a new class `PresburgerSet` is introduced to represent unions of convex polytopes.

Reviewed By: ftynse, bondhugula

Differential Revision: https://reviews.llvm.org/D87068
2020-10-07 17:31:06 +02:00
Arjun P 10a898b3ec [MLIR] Exact integer emptiness checks for FlatAffineConstraints
This patch adds the capability to perform exact integer emptiness checks for FlatAffineConstraints using the General Basis Reduction algorithm (GBR). Previously, only a heuristic was available for emptiness checks, which was not guaranteed to always give a conclusive result.

This patch adds a `Simplex` class, which can be constructed using a `FlatAffineConstraints`, and can find an integer sample point (if one exists) using the GBR algorithm. Additionally, it adds two classes `Matrix` and `Fraction`, which are used by `Simplex`.

The integer emptiness check functionality can be accessed through the new `FlatAffineConstraints::isIntegerEmpty()` function, which runs the existing heuristic first and, if that proves to be inconclusive, runs the GBR algorithm to produce a conclusive result.

Differential Revision: https://reviews.llvm.org/D80860
2020-07-02 19:53:27 +05:30