[Mlir-commits] [mlir] 45ea542 - [MLIR] Introduce coalesce for PresburgerSet

Arjun P llvmlistbot at llvm.org
Thu Dec 9 02:20:25 PST 2021


Author: Michel Weber
Date: 2021-12-09T15:46:31+05:30
New Revision: 45ea542dd82216364a144324c44ff82caf905a58

URL: https://github.com/llvm/llvm-project/commit/45ea542dd82216364a144324c44ff82caf905a58
DIFF: https://github.com/llvm/llvm-project/commit/45ea542dd82216364a144324c44ff82caf905a58.diff

LOG: [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

Added: 
    

Modified: 
    mlir/include/mlir/Analysis/Presburger/Simplex.h
    mlir/include/mlir/Analysis/PresburgerSet.h
    mlir/lib/Analysis/Presburger/Simplex.cpp
    mlir/lib/Analysis/PresburgerSet.cpp
    mlir/unittests/Analysis/Presburger/CMakeLists.txt
    mlir/unittests/Analysis/Presburger/SimplexTest.cpp
    mlir/unittests/Analysis/PresburgerSetTest.cpp

Removed: 
    


################################################################################
diff  --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h b/mlir/include/mlir/Analysis/Presburger/Simplex.h
index 893f0d66b613f..87217cd7e13c3 100644
--- a/mlir/include/mlir/Analysis/Presburger/Simplex.h
+++ b/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;
 

diff  --git a/mlir/include/mlir/Analysis/PresburgerSet.h b/mlir/include/mlir/Analysis/PresburgerSet.h
index 41dfc0018efab..41190be42b0ea 100644
--- a/mlir/include/mlir/Analysis/PresburgerSet.h
+++ b/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)

diff  --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp
index 0e7ab343a2e1c..68ee63043306f 100644
--- a/mlir/lib/Analysis/Presburger/Simplex.cpp
+++ b/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

diff  --git a/mlir/lib/Analysis/PresburgerSet.cpp b/mlir/lib/Analysis/PresburgerSet.cpp
index 26ebed1444a08..50976e2fd76e9 100644
--- a/mlir/lib/Analysis/PresburgerSet.cpp
+++ b/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
+    // 
diff erent 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) {

diff  --git a/mlir/unittests/Analysis/Presburger/CMakeLists.txt b/mlir/unittests/Analysis/Presburger/CMakeLists.txt
index 5dd69edfad089..818dc934c1004 100644
--- a/mlir/unittests/Analysis/Presburger/CMakeLists.txt
+++ b/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
+  )

diff  --git a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp
index cf67193ad8b6b..df36992792c5d 100644
--- a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp
+++ b/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

diff  --git a/mlir/unittests/Analysis/PresburgerSetTest.cpp b/mlir/unittests/Analysis/PresburgerSetTest.cpp
index e146a770c0c83..09973fda12609 100644
--- a/mlir/unittests/Analysis/PresburgerSetTest.cpp
+++ b/mlir/unittests/Analysis/PresburgerSetTest.cpp
@@ -15,6 +15,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "mlir/Analysis/PresburgerSet.h"
+#include "./AffineStructuresParser.h"
 
 #include <gmock/gmock.h>
 #include <gtest/gtest.h>
@@ -645,4 +646,191 @@ TEST(SetTest, divisions) {
   expectEqual(multiples3.intersect(evens), multiples6);
 }
 
+/// Parses a FlatAffineConstraints from a StringRef. It is expected that the
+/// string represents a valid IntegerSet, otherwise it will violate a gtest
+/// assertion.
+static FlatAffineConstraints parseFAC(StringRef str, MLIRContext *context) {
+  FailureOr<FlatAffineConstraints> fac = parseIntegerSetToFAC(str, context);
+
+  EXPECT_TRUE(succeeded(fac));
+
+  return *fac;
+}
+
+/// Coalesce `set` and check that the `newSet` is equal to `set and that
+/// `expectedNumFACs` matches the number of FACs in the coalesced set.
+/// If one of the two
+void expectCoalesce(size_t expectedNumFACs, const PresburgerSet set) {
+  PresburgerSet newSet = set.coalesce();
+  EXPECT_TRUE(set.isEqual(newSet));
+  EXPECT_TRUE(expectedNumFACs == newSet.getNumFACs());
+}
+
+TEST(SetTest, coalesceNoFAC) {
+  PresburgerSet set = makeSetFromFACs(0, {});
+  expectCoalesce(0, set);
+}
+
+TEST(SetTest, coalesceContainedOneDim) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      1, {parseFAC("(x) : (x >= 0, -x + 4 >= 0)", &context),
+          parseFAC("(x) : (x - 1 >= 0, -x + 2 >= 0)", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceFirstEmpty) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      1, {
+             parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context),
+             parseFAC("(x) : ( x - 1 >= 0, -x + 2 >= 0)", &context),
+         });
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceSecondEmpty) {
+  MLIRContext context;
+  PresburgerSet set =
+      makeSetFromFACs(1, {parseFAC("(x) : (x - 1 >= 0, -x + 2 >= 0)", &context),
+                          parseFAC("(x) : (x >= 0, -x - 1 >= 0)", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceBothEmpty) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      1, {
+             parseFAC("(x) : (x - 3 >= 0, -x - 1 >= 0)", &context),
+             parseFAC("(x) : (x >= 0, -x - 1 >= 0)", &context),
+         });
+  expectCoalesce(0, set);
+}
+
+TEST(SetTest, coalesceFirstUniv) {
+  MLIRContext context;
+  PresburgerSet set =
+      makeSetFromFACs(1, {parseFAC("(x) : ()", &context),
+                          parseFAC("(x) : ( x >= 0, -x + 1 >= 0)", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceSecondUniv) {
+  MLIRContext context;
+  PresburgerSet set =
+      makeSetFromFACs(1, {parseFAC("(x) : ( x >= 0, -x + 1 >= 0)", &context),
+                          parseFAC("(x) : ()", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceBothUniv) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      1, {parseFAC("(x) : ()", &context), parseFAC("(x) : ()", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceFirstUnivSecondEmpty) {
+  MLIRContext context;
+  PresburgerSet set =
+      makeSetFromFACs(1, {parseFAC("(x) : ()", &context),
+                          parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceFirstEmptySecondUniv) {
+  MLIRContext context;
+  PresburgerSet set =
+      makeSetFromFACs(1, {parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context),
+                          parseFAC("(x) : ()", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceCutOneDim) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      1, {parseFAC("(x) : ( x >= 0, -x + 3 >= 0)", &context),
+          parseFAC("(x) : ( x - 2 >= 0, -x + 4 >= 0)", &context)});
+  expectCoalesce(2, set);
+}
+
+TEST(SetTest, coalesceSeparateOneDim) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      1, {parseFAC("(x) : ( x >= 0, -x + 2 >= 0)", &context),
+          parseFAC("(x) : ( x - 3 >= 0, -x + 4 >= 0)", &context)});
+  expectCoalesce(2, set);
+}
+
+TEST(SetTest, coalesceContainedTwoDim) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      2,
+      {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)", &context),
+       parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)",
+                &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceCutTwoDim) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      2,
+      {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)", &context),
+       parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)",
+                &context)});
+  expectCoalesce(2, set);
+}
+
+TEST(SetTest, coalesceSeparateTwoDim) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      2,
+      {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)", &context),
+       parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)",
+                &context)});
+  expectCoalesce(2, set);
+}
+
+TEST(SetTest, coalesceContainedEq) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      2, {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)", &context),
+          parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceCuttingEq) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      2, {parseFAC("(x,y) : (x - 1 >= 0, -x + 3 >= 0, x - y == 0)", &context),
+          parseFAC("(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)", &context)});
+  expectCoalesce(2, set);
+}
+
+TEST(SetTest, coalesceSeparateEq) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      2, {parseFAC("(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)", &context),
+          parseFAC("(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)", &context)});
+  expectCoalesce(2, set);
+}
+
+TEST(SetTest, coalesceContainedEqAsIneq) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      2, {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, x - y >= 0, -x + y >= 0)",
+                   &context),
+          parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)});
+  expectCoalesce(1, set);
+}
+
+TEST(SetTest, coalesceContainedEqComplex) {
+  MLIRContext context;
+  PresburgerSet set = makeSetFromFACs(
+      2, {parseFAC("(x,y) : (x - 2 == 0, x - y == 0)", &context),
+          parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)});
+  expectCoalesce(1, set);
+}
+
 } // namespace mlir


        


More information about the Mlir-commits mailing list