[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

561–567

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

421–424 ↗

(On Diff #409177)

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

427–429 ↗

(On Diff #409177)

Use lowerCamelCase for variables, please.

435–441 ↗

(On Diff #409177)

You can remove the curly braces here.

[webmiche]

address review comments

[arjunp]

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

493

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

567

You should be able to drop this here

567

Maybe rename to findIneqType. Function names should represent doing something

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

421 ↗

(On Diff #409189)

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 ↗

(On Diff #409189)

Please capitalize starts of sentences and end them with full stops

422–426 ↗

(On Diff #409189)

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

423–433 ↗

(On Diff #409189)

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

mlir/lib/Analysis/Presburger/Simplex.cpp

1624

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

1626

1627

1630

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

1620

1624–1628

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 };
 
   Simplex() = delete;
   explicit Simplex(unsigned nVar) : SimplexBase(nVar, /*mustUseBigM=*/false) {}
   explicit Simplex(const IntegerPolyhedron &constraints)
       : Simplex(constraints.getNumIds()) {
     intersectIntegerPolyhedron(constraints);
   }
   ~Simplex() override = default;
 
   /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
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();
 
+  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);
 
   /// 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/Simplex.cpp

 
 void SimplexBase::dump() const { print(llvm::errs()); }
 
 bool Simplex::isRationalSubsetOf(const IntegerPolyhedron &poly) {
   if (isEmpty())
     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)
     if (!isRedundantEquality(poly.getEquality(i)))
       return false;
 
   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
 /// 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) {
   assert(!empty &&

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.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.
   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.