[MLIR][Presburger] Inequality Typing in coalesce

[webmiche]

Summary

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.

[Groverkss]

mlir/include/mlir/Analysis/Presburger/Simplex.h

560–566

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

421–449

Could you write a comment here on what it's doing? I don't exactly understand what it is doing.

427–429

Use lowerCamelCase for variables, please.

435–441

You can remove the curly braces here.

[webmiche]

address review comments

[arjunp]

mlir/include/mlir/Analysis/Presburger/Simplex.h

491

I think it might be best to move this down right above ineqType

566

You should be able to drop this here

566

Maybe rename to findIneqType. Function names should represent doing something

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

421

As far as I can see, this doesn't change the functionality, but reimplements it in a different way to setup the rest of the coalesce patches? If so, I would leave it out for this patch.

421–429

Please capitalize starts of sentences and end them with full stops

422–426

I would suggest early exiting if it becomes false at any point

423–433

Is there a specific reason for using l as the iterator when k is unused?

mlir/lib/Analysis/Presburger/Simplex.cpp

1591

I would just omit all the "if it exists" stuff. If it doesn't exist, it's plus/minus infinity and people can figure out whether that's >= or <= 0. This would make the whole doc much more understandable

1593

1594

1597

Describe why the other case corresponds to the description of what "separate" means above

[webmiche]

I removed everything concerning looping strategy in coalesce. This is reduced purely to everything that concerns introducing inequality types.

[arjunp]

mlir/lib/Analysis/Presburger/Simplex.cpp

1615

1619–1623

Write "the inequality" instead of "coeffs"

[webmiche]

addressed remaining comments

[arjunp]

LGTM!

mlir/include/mlir/Analysis/Presburger/Simplex.h

 /// of constraints that have been marked redundant.
 ///
 /// Finding an integer sample is done with the Generalized Basis Reduction
 /// algorithm. See the documentation for findIntegerSample and reduceBasis.
 class Simplex : public SimplexBase {
 public:
   enum class Direction { Up, Down };
 
+  enum class IneqType { Redundant, Cut, Separate };
+
   Simplex() = delete;
   explicit Simplex(unsigned nVar) : SimplexBase(nVar, /*mustUseBigM=*/false) {}
   explicit Simplex(const IntegerPolyhedron &constraints)
       : Simplex(constraints.getNumIds()) {
     intersectIntegerPolyhedron(constraints);
   }
   ~Simplex() override = default;
 
public:
   /// Make a tableau to represent a pair of points in the given tableaus, one in
   /// tableau A and one in B.
   static Simplex makeProduct(const Simplex &a, const Simplex &b);
 
   /// Returns an integer sample point if one exists, or None
   /// otherwise. This should only be called for bounded sets.
   Optional<SmallVector<int64_t, 8>> findIntegerSample();
 
+  /// 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
+  Simplex::IneqType ineqType(ArrayRef<int64_t> coeffs);
+
   /// Check if the specified inequality already holds in the polytope.
   bool isRedundantInequality(ArrayRef<int64_t> coeffs);
 
   /// Check if the specified equality already holds in the polytope.
   bool isRedundantEquality(ArrayRef<int64_t> coeffs);
 
   /// Returns true if this Simplex's polytope is a rational subset of `poly`.
   /// Otherwise, returns false.

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

for (unsigned i = 0, e = integerPolyhedrons.size(); i < e; ++i) {
     }
 
     // Check whether `IntegerPolyhedron[i]` is contained in any Poly, that is
     // different from itself and not yet marked as redundant.
     for (unsigned j = 0, e = integerPolyhedrons.size(); j < e; ++j) {
       if (j == i || isRedundant[j])
         continue;
 
-      if (simplex.isRationalSubsetOf(integerPolyhedrons[j])) {
+      // Check whether all equalities are redundant
+      bool onlyRedundantEqs = true;
+      for (unsigned l = 0, e = integerPolyhedrons[j].getNumEqualities(); l < e;
+           ++l)
+        onlyRedundantEqs &=
+            simplex.isRedundantEquality(integerPolyhedrons[j].getEquality(l));
+
+      // type all inequalities
+      SmallVector<ArrayRef<int64_t>, 2> redundantIneqs;
+      SmallVector<ArrayRef<int64_t>, 2> cuttingIneqs;
+      SmallVector<ArrayRef<int64_t>, 2> separateIneqs;
+
+      for (unsigned l = 0, e = integerPolyhedrons[j].getNumInequalities();
+           l < e; ++l) {
+        Simplex::IneqType type =
+            simplex.ineqType(integerPolyhedrons[j].getInequality(l));
+        if (type == Simplex::IneqType::Redundant)
+          redundantIneqs.push_back(integerPolyhedrons[j].getInequality(l));
+        else if (type == Simplex::IneqType::Cut)
+          cuttingIneqs.push_back(integerPolyhedrons[j].getInequality(l));
+        else
+          separateIneqs.push_back(integerPolyhedrons[j].getInequality(l));
+      }
+
+      // If no separate and cutting inequalities exist, this can be
+      // coalesced.
+      if (onlyRedundantEqs && separateIneqs.size() == 0 &&
+          cuttingIneqs.size() == 0) {
         isRedundant[i] = true;
         break;
       }
     }
   }
 
   for (unsigned i = 0, e = integerPolyhedrons.size(); i < e; ++i)
     if (!isRedundant[i])
       newSet.unionPolyInPlace(integerPolyhedrons[i]);

mlir/lib/Analysis/Presburger/Simplex.cpp

bool Simplex::isRationalSubsetOf(const IntegerPolyhedron &poly) {
 
   for (unsigned i = 0, e = poly.getNumEqualities(); i < e; ++i)
     if (!isRedundantEquality(poly.getEquality(i)))
       return false;
 
   return true;
 }
 
+/// 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
+///
+/// Internally, this computes the minimum and the maximum `coeffs` can take. If
+/// the minimum exists and it is >= 0, the inequality holds for all points in
+/// the polytope, so `coeffs` is redundant.  If the minimum does not exists or
+/// is <= 0 and the maximum does not exists or is >= 0, the points in between
+/// the minimum and `coeffs` do not satisfy the inequality, the points in
+/// between `coeffs` and the maximum satisfy the inequality. Hence, it is a cut
+/// inequality. In any other case, separate is returned.
+Simplex::IneqType Simplex::ineqType(ArrayRef<int64_t> coeffs) {
+  Optional<Fraction> minimum = computeOptimum(Direction::Down, coeffs);
+  if (minimum && *minimum >= Fraction(0, 1)) {
+    return IneqType::Redundant;
+  }
+  Optional<Fraction> maximum = computeOptimum(Direction::Up, coeffs);
+  if ((!minimum || *minimum <= Fraction(0, 1)) &&
+      (!maximum || *maximum >= Fraction(0, 1))) {
+    return IneqType::Cut;
+  }
+  return IneqType::Separate;
+}
+
 /// 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`.
 bool Simplex::isRedundantInequality(ArrayRef<int64_t> coeffs) {
   Optional<Fraction> minimum = computeOptimum(Direction::Down, coeffs);
   return minimum && *minimum >= Fraction(0, 1);
 }
 
 /// Check whether the equality given by `coeffs == 0` is redundant given
 /// the existing constraints. This is redundant when `coeffs` is already
 /// always zero under the existing constraints. `coeffs` is always zero
 /// when the minimum and maximum value that `coeffs` can take are both zero.
 bool Simplex::isRedundantEquality(ArrayRef<int64_t> coeffs) {
   Optional<Fraction> minimum = computeOptimum(Direction::Down, coeffs);
   Optional<Fraction> maximum = computeOptimum(Direction::Up, coeffs);
   return minimum && maximum && *maximum == Fraction(0, 1) &&
          *minimum == Fraction(0, 1);
 }
 
 } // namespace mlir

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

TEST(SimplexTest, isRedundantInequality) {
   EXPECT_TRUE(simplex.isRedundantInequality({-1, 0, 2})); // x <= 2.
   EXPECT_TRUE(simplex.isRedundantInequality({0, 1, 0}));  // y >= 0.
 
   EXPECT_FALSE(simplex.isRedundantInequality({-1, 0, -1})); // x <= -1.
   EXPECT_FALSE(simplex.isRedundantInequality({0, 1, -2}));  // y >= 2.
   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.ineqType({-1, 0, 2}) ==
+              Simplex::IneqType::Redundant); // x <= 2.
+  EXPECT_TRUE(simplex.ineqType({0, 1, 0}) ==
+              Simplex::IneqType::Redundant); // y >= 0.
+
+  EXPECT_TRUE(simplex.ineqType({0, 1, -1}) ==
+              Simplex::IneqType::Cut); // y >= 1.
+  EXPECT_TRUE(simplex.ineqType({-1, 0, 1}) ==
+              Simplex::IneqType::Cut); // x <= 1.
+  EXPECT_TRUE(simplex.ineqType({0, 1, -2}) ==
+              Simplex::IneqType::Cut); // y >= 2.
+
+  EXPECT_TRUE(simplex.ineqType({-1, 0, -1}) ==
+              Simplex::IneqType::Separate); // x <= -1.
+}
+
 TEST(SimplexTest, isRedundantEquality) {
   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.isRedundantEquality({-1, 1, 0})); // y = x.
   EXPECT_TRUE(simplex.isRedundantEquality({1, -1, 0})); // x = y.