[MLIR] Introduce coalesce for PresburgerSet

This patch provides functionality for simplifying `PresburgerSet`s by checking if any `FlatAffineConstraints` in the set is contained in another, and removing such redundant FACs.

This is part of a series of patches to provide functionality for [integer set coalescing](http://impact.gforge.inria.fr/impact2015/papers/impact2015-verdoolaege.pdf) in MLIR.

Reviewed By: arjunp

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

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

@@ -237,6 +237,16 @@ class Simplex {
   void print(raw_ostream &os) const;
   void dump() const;
 
+  /// 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 `fac`.
+  /// Otherwise, returns false.
+  bool isRationalSubsetOf(const FlatAffineConstraints &fac);
+
 private:
   friend class GBRSimplex;
 

mlir/include/mlir/Analysis/PresburgerSet.h

@@ -94,6 +94,12 @@ class PresburgerSet {
   /// any of the FACs in the union are unbounded.
   bool findIntegerSample(SmallVectorImpl<int64_t> &sample);
 
+  /// Simplifies the representation of a PresburgerSet.
+  ///
+  /// In particular, removes all FACs which are subsets of other FACs in the
+  /// union.
+  PresburgerSet coalesce() const;
+
 private:
   /// Construct an empty PresburgerSet.
   PresburgerSet(unsigned nDim = 0, unsigned nSym = 0)

mlir/lib/Analysis/Presburger/Simplex.cpp

@@ -1246,4 +1246,38 @@ void Simplex::print(raw_ostream &os) const {
 
 void Simplex::dump() const { print(llvm::errs()); }
 
+bool Simplex::isRationalSubsetOf(const FlatAffineConstraints &fac) {
+  if (isEmpty())
+    return true;
+
+  for (unsigned i = 0, e = fac.getNumInequalities(); i < e; ++i)
+    if (!isRedundantInequality(fac.getInequality(i)))
+      return false;
+
+  for (unsigned i = 0, e = fac.getNumEqualities(); i < e; ++i)
+    if (!isRedundantEquality(fac.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`.
+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/lib/Analysis/PresburgerSet.cpp

@@ -381,6 +381,42 @@ bool PresburgerSet::findIntegerSample(SmallVectorImpl<int64_t> &sample) {
   return false;
 }
 
+PresburgerSet PresburgerSet::coalesce() const {
+  PresburgerSet newSet = PresburgerSet::getEmptySet(getNumDims(), getNumSyms());
+  llvm::SmallBitVector isRedundant(getNumFACs());
+
+  for (unsigned i = 0, e = flatAffineConstraints.size(); i < e; ++i) {
+    if (isRedundant[i])
+      continue;
+    Simplex simplex(flatAffineConstraints[i]);
+
+    // Check whether the polytope of `simplex` is empty. If so, it is trivially
+    // redundant.
+    if (simplex.isEmpty()) {
+      isRedundant[i] = true;
+      continue;
+    }
+
+    // Check whether `FlatAffineConstraints[i]` is contained in any FAC, that is
+    // different from itself and not yet marked as redundant.
+    for (unsigned j = 0, e = flatAffineConstraints.size(); j < e; ++j) {
+      if (j == i || isRedundant[j])
+        continue;
+
+      if (simplex.isRationalSubsetOf(flatAffineConstraints[j])) {
+        isRedundant[i] = true;
+        break;
+      }
+    }
+  }
+
+  for (unsigned i = 0, e = flatAffineConstraints.size(); i < e; ++i)
+    if (!isRedundant[i])
+      newSet.unionFACInPlace(flatAffineConstraints[i]);
+
+  return newSet;
+}
+
 void PresburgerSet::print(raw_ostream &os) const {
   os << getNumFACs() << " FlatAffineConstraints:\n";
   for (const FlatAffineConstraints &fac : flatAffineConstraints) {

mlir/unittests/Analysis/Presburger/CMakeLists.txt

@@ -1,8 +1,11 @@
 add_mlir_unittest(MLIRPresburgerTests
   MatrixTest.cpp
   SimplexTest.cpp
+  ../AffineStructuresParser.cpp
 )
 
 target_link_libraries(MLIRPresburgerTests
-  PRIVATE MLIRPresburger)
-
+  PRIVATE MLIRPresburger
+  MLIRLoopAnalysis
+  MLIRParser
+  )

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

@@ -7,6 +7,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "mlir/Analysis/Presburger/Simplex.h"
+#include "../AffineStructuresParser.h"
 
 #include <gmock/gmock.h>
 #include <gtest/gtest.h>
@@ -445,4 +446,84 @@ TEST(SimplexTest, appendVariable) {
   EXPECT_EQ(simplex.getNumConstraints(), 0u);
 }
 
+TEST(SimplexTest, isRedundantInequality) {
+  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.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, 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.
+
+  EXPECT_FALSE(simplex.isRedundantEquality({0, 1, -1})); // y = 1.
+
+  simplex.addEquality({0, -1, 2}); // y = 2.
+
+  EXPECT_TRUE(simplex.isRedundantEquality({-1, 0, 2})); // x = 2.
+}
+
+static FlatAffineConstraints parseFAC(StringRef str, MLIRContext *context) {
+  FailureOr<FlatAffineConstraints> fac = parseIntegerSetToFAC(str, context);
+
+  EXPECT_TRUE(succeeded(fac));
+
+  return *fac;
+}
+
+TEST(SimplexTest, IsRationalSubsetOf) {
+
+  MLIRContext context;
+
+  FlatAffineConstraints univ = FlatAffineConstraints::getUniverse(1, 0);
+  FlatAffineConstraints empty =
+      parseFAC("(x) : (x + 0 >= 0, -x - 1 >= 0)", &context);
+  FlatAffineConstraints s1 = parseFAC("(x) : ( x >= 0, -x + 4 >= 0)", &context);
+  FlatAffineConstraints s2 =
+      parseFAC("(x) : (x - 1 >= 0, -x + 3 >= 0)", &context);
+
+  Simplex simUniv(univ);
+  Simplex simEmpty(empty);
+  Simplex sim1(s1);
+  Simplex sim2(s2);
+
+  EXPECT_TRUE(simUniv.isRationalSubsetOf(univ));
+  EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty));
+  EXPECT_TRUE(sim1.isRationalSubsetOf(s1));
+  EXPECT_TRUE(sim2.isRationalSubsetOf(s2));
+
+  EXPECT_TRUE(simEmpty.isRationalSubsetOf(univ));
+  EXPECT_TRUE(simEmpty.isRationalSubsetOf(s1));
+  EXPECT_TRUE(simEmpty.isRationalSubsetOf(s2));
+  EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty));
+
+  EXPECT_TRUE(simUniv.isRationalSubsetOf(univ));
+  EXPECT_FALSE(simUniv.isRationalSubsetOf(s1));
+  EXPECT_FALSE(simUniv.isRationalSubsetOf(s2));
+  EXPECT_FALSE(simUniv.isRationalSubsetOf(empty));
+
+  EXPECT_TRUE(sim1.isRationalSubsetOf(univ));
+  EXPECT_TRUE(sim1.isRationalSubsetOf(s1));
+  EXPECT_FALSE(sim1.isRationalSubsetOf(s2));
+  EXPECT_FALSE(sim1.isRationalSubsetOf(empty));
+
+  EXPECT_TRUE(sim2.isRationalSubsetOf(univ));
+  EXPECT_TRUE(sim2.isRationalSubsetOf(s1));
+  EXPECT_TRUE(sim2.isRationalSubsetOf(s2));
+  EXPECT_FALSE(sim2.isRationalSubsetOf(empty));
+}
+
 } // namespace mlir