[Mlir-commits] [mlir] 56bc873 - [MLIR][Presburger] Inequality Typing in coalesce

[llvmlistbot at llvm.org]

Author: Michel Weber
Date: 2022-02-20T23:19:14+05:30
New Revision: 56bc87322ccca2ae786d493410d9801cf9c87a16

URL: https://github.com/llvm/llvm-project/commit/56bc87322ccca2ae786d493410d9801cf9c87a16
DIFF: https://github.com/llvm/llvm-project/commit/56bc87322ccca2ae786d493410d9801cf9c87a16.diff

LOG: [MLIR][Presburger] Inequality Typing in coalesce

This patch adds typing of inequalities to the simplex. This is a cental part of the coalesce algorithm and will be heavily used in later coalesce patches. Currently, only the three most basic types are supported with more to be introduced when they are needed.

Reviewed By: arjunp

Differential Revision: https://reviews.llvm.org/D119925

Added: 
    

Modified: 
    mlir/include/mlir/Analysis/Presburger/Simplex.h
    mlir/lib/Analysis/Presburger/Simplex.cpp
    mlir/unittests/Analysis/Presburger/SimplexTest.cpp

Removed: 
    


################################################################################
diff  --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h b/mlir/include/mlir/Analysis/Presburger/Simplex.h
index 4f4abc1579cd2..10600064710dc 100644
--- a/mlir/include/mlir/Analysis/Presburger/Simplex.h
+++ b/mlir/include/mlir/Analysis/Presburger/Simplex.h
@@ -558,6 +558,16 @@ class Simplex : public SimplexBase {
   /// otherwise. This should only be called for bounded sets.
   Optional<SmallVector<int64_t, 8>> findIntegerSample();
 
+  enum class IneqType { Redundant, Cut, Separate };
+
+  /// Returns the type of the inequality with coefficients `coeffs`.
+  ///
+  /// Possible types are:
+  /// Redundant   The inequality is satisfied in the polytope
+  /// Cut         The inequality is satisfied by some points, but not by others
+  /// Separate    The inequality is not satisfied by any point
+  IneqType findIneqType(ArrayRef<int64_t> coeffs);
+
   /// Check if the specified inequality already holds in the polytope.
   bool isRedundantInequality(ArrayRef<int64_t> coeffs);
 

diff  --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp
index 5ba213ac9e3b4..285fa91f34a07 100644
--- a/mlir/lib/Analysis/Presburger/Simplex.cpp
+++ b/mlir/lib/Analysis/Presburger/Simplex.cpp
@@ -1605,7 +1605,7 @@ bool Simplex::isRationalSubsetOf(const IntegerPolyhedron &poly) {
     return true;
 
   for (unsigned i = 0, e = poly.getNumInequalities(); i < e; ++i)
-    if (!isRedundantInequality(poly.getInequality(i)))
+    if (findIneqType(poly.getInequality(i)) != IneqType::Redundant)
       return false;
 
   for (unsigned i = 0, e = poly.getNumEqualities(); i < e; ++i)
@@ -1615,16 +1615,39 @@ bool Simplex::isRationalSubsetOf(const IntegerPolyhedron &poly) {
   return true;
 }
 
-/// Computes the minimum value `coeffs` can take. If the value is greater than
-/// or equal to zero, the polytope entirely lies in the half-space defined by
-/// `coeffs >= 0`.
+/// Returns the type of the inequality with coefficients `coeffs`.
+/// Possible types are:
+/// Redundant   The inequality is satisfied by all points in the polytope
+/// Cut         The inequality is satisfied by some points, but not by others
+/// Separate    The inequality is not satisfied by any point
+///
+/// Internally, this computes the minimum and the maximum the inequality with
+/// coefficients `coeffs` can take. If the minimum is >= 0, the inequality holds
+/// for all points in the polytope, so it is redundant.  If the minimum is <= 0
+/// and the maximum is >= 0, the points in between the minimum and the
+/// inequality do not satisfy it, the points in between the inequality and the
+/// maximum satisfy it. Hence, it is a cut inequality. If both are < 0, no
+/// points of the polytope satisfy the inequality, which means it is a separate
+/// inequality.
+Simplex::IneqType Simplex::findIneqType(ArrayRef<int64_t> coeffs) {
+  MaybeOptimum<Fraction> minimum = computeOptimum(Direction::Down, coeffs);
+  if (minimum.isBounded() && *minimum >= Fraction(0, 1)) {
+    return IneqType::Redundant;
+  }
+  MaybeOptimum<Fraction> maximum = computeOptimum(Direction::Up, coeffs);
+  if ((!minimum.isBounded() || *minimum <= Fraction(0, 1)) &&
+      (!maximum.isBounded() || *maximum >= Fraction(0, 1))) {
+    return IneqType::Cut;
+  }
+  return IneqType::Separate;
+}
+
+/// Checks whether the type of the inequality with coefficients `coeffs`
+/// is Redundant.
 bool Simplex::isRedundantInequality(ArrayRef<int64_t> coeffs) {
   assert(!empty &&
          "It is not meaningful to ask about redundancy in an empty set!");
-  MaybeOptimum<Fraction> minimum = computeOptimum(Direction::Down, coeffs);
-  assert(!minimum.isEmpty() &&
-         "Optima should be non-empty for a non-empty set");
-  return minimum.isBounded() && *minimum >= Fraction(0, 1);
+  return findIneqType(coeffs) == IneqType::Redundant;
 }
 
 /// Check whether the equality given by `coeffs == 0` is redundant given

diff  --git a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp
index eb403adb87e0a..fbe68070f39d6 100644
--- a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp
@@ -464,6 +464,28 @@ TEST(SimplexTest, isRedundantInequality) {
   EXPECT_FALSE(simplex.isRedundantInequality({0, 1, -1}));  // y >= 1.
 }
 
+TEST(SimplexTest, ineqType) {
+  Simplex simplex(2);
+  simplex.addInequality({0, -1, 2}); // y <= 2.
+  simplex.addInequality({1, 0, 0});  // x >= 0.
+  simplex.addEquality({-1, 1, 0});   // y = x.
+
+  EXPECT_TRUE(simplex.findIneqType({-1, 0, 2}) ==
+              Simplex::IneqType::Redundant); // x <= 2.
+  EXPECT_TRUE(simplex.findIneqType({0, 1, 0}) ==
+              Simplex::IneqType::Redundant); // y >= 0.
+
+  EXPECT_TRUE(simplex.findIneqType({0, 1, -1}) ==
+              Simplex::IneqType::Cut); // y >= 1.
+  EXPECT_TRUE(simplex.findIneqType({-1, 0, 1}) ==
+              Simplex::IneqType::Cut); // x <= 1.
+  EXPECT_TRUE(simplex.findIneqType({0, 1, -2}) ==
+              Simplex::IneqType::Cut); // y >= 2.
+
+  EXPECT_TRUE(simplex.findIneqType({-1, 0, -1}) ==
+              Simplex::IneqType::Separate); // x <= -1.
+}
+
 TEST(SimplexTest, isRedundantEquality) {
   Simplex simplex(2);
   simplex.addInequality({0, -1, 2}); // y <= 2.