[Mlir-commits] [mlir] 33f5746 - [MLIR] Redundancy detection for FlatAffineConstraints using Simplex

Uday Bondhugula llvmlistbot at llvm.org
Thu Aug 20 01:13:27 PDT 2020


Author: Arjun P
Date: 2020-08-20T13:38:51+05:30
New Revision: 33f574672f40fb94c818901208824303350df55e

URL: https://github.com/llvm/llvm-project/commit/33f574672f40fb94c818901208824303350df55e
DIFF: https://github.com/llvm/llvm-project/commit/33f574672f40fb94c818901208824303350df55e.diff

LOG: [MLIR] Redundancy detection for FlatAffineConstraints using Simplex

This patch adds the capability to perform constraint redundancy checks for `FlatAffineConstraints` using `Simplex`, via a new member function `FlatAffineConstraints::removeRedundantConstraints`. The pre-existing redundancy detection algorithm runs a full rational emptiness check for each inequality separately for checking redundancy. Leveraging the existing `Simplex` infrastructure, in this patch we have an algorithm for redundancy checks that can check each constraint by performing pivots on the tableau, which provides an alternative to running Fourier-Motzkin elimination for each constraint separately.

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

Added: 
    

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

Removed: 
    


################################################################################
diff  --git a/mlir/include/mlir/Analysis/AffineStructures.h b/mlir/include/mlir/Analysis/AffineStructures.h
index 14a19827902f..e7b10c37825b 100644
--- a/mlir/include/mlir/Analysis/AffineStructures.h
+++ b/mlir/include/mlir/Analysis/AffineStructures.h
@@ -546,6 +546,13 @@ class FlatAffineConstraints {
   /// removeTrivialRedundancy.
   void removeRedundantInequalities();
 
+  /// Removes redundant constraints using Simplex. Although the algorithm can
+  /// theoretically take exponential time in the worst case (rare), it is known
+  /// to perform much better in the average case. If V is the number of vertices
+  /// in the polytope and C is the number of constraints, the algorithm takes
+  /// O(VC) time.
+  void removeRedundantConstraints();
+
   // Removes all equalities and inequalities.
   void clearConstraints();
 

diff  --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h b/mlir/include/mlir/Analysis/Presburger/Simplex.h
index f6344a62d214..c094f8c59313 100644
--- a/mlir/include/mlir/Analysis/Presburger/Simplex.h
+++ b/mlir/include/mlir/Analysis/Presburger/Simplex.h
@@ -7,7 +7,7 @@
 //===----------------------------------------------------------------------===//
 //
 // Functionality to perform analysis on FlatAffineConstraints. In particular,
-// support for performing emptiness checks.
+// support for performing emptiness checks and redundancy checks.
 //
 //===----------------------------------------------------------------------===//
 
@@ -34,7 +34,10 @@ class GBRSimplex;
 /// inequalities and equalities, and can perform emptiness checks, i.e., it can
 /// find a solution to the set of constraints if one exists, or say that the
 /// set is empty if no solution exists. Currently, this only works for bounded
-/// sets. Simplex can also be constructed from a FlatAffineConstraints object.
+/// sets. Furthermore, it can find a subset of these constraints that are
+/// redundant, i.e. a subset of constraints that doesn't constrain the affine
+/// set further after adding the non-redundant constraints. Simplex can also be
+/// constructed from a FlatAffineConstraints object.
 ///
 /// The implementation of this Simplex class, other than the functionality
 /// for sampling, is based on the paper
@@ -112,6 +115,15 @@ class GBRSimplex;
 /// set of constraints is mutually contradictory and the tableau is marked
 /// _empty_, which means the set of constraints has no solution.
 ///
+/// The Simplex class supports redundancy checking via detectRedundant and
+/// isMarkedRedundant. A redundant constraint is one which is never violated as
+/// long as the other constrants are not violated, i.e., removing a redundant
+/// constraint does not change the set of solutions to the constraints. As a
+/// heuristic, constraints that have been marked redundant can be ignored for
+/// most operations. Therefore, these constraints are kept in rows 0 to
+/// nRedundant - 1, where nRedundant is a member variable that tracks the number
+/// of constraints that have been marked redundant.
+///
 /// This Simplex class also supports taking snapshots of the current state
 /// and rolling back to prior snapshots. This works by maintaing an undo log
 /// of operations. Snapshots are just pointers to a particular location in the
@@ -158,7 +170,7 @@ class Simplex {
   void rollback(unsigned snapshot);
 
   /// Compute the maximum or minimum value of the given row, depending on
-  /// direction.
+  /// direction. The specified row is never pivoted.
   ///
   /// Returns a (num, den) pair denoting the optimum, or None if no
   /// optimum exists, i.e., if the expression is unbounded in this direction.
@@ -172,6 +184,18 @@ class Simplex {
   Optional<Fraction> computeOptimum(Direction direction,
                                     ArrayRef<int64_t> coeffs);
 
+  /// Returns whether the specified constraint has been marked as redundant.
+  /// Constraints are numbered from 0 starting at the first added inequality.
+  /// Equalities are added as a pair of inequalities and so correspond to two
+  /// inequalities with successive indices.
+  bool isMarkedRedundant(unsigned constraintIndex) const;
+
+  /// Finds a subset of constraints that is redundant, i.e., such that
+  /// the set of solutions does not change if these constraints are removed.
+  /// Marks these constraints as redundant. Whether a specific constraint has
+  /// been marked redundant can be queried using isMarkedRedundant.
+  void detectRedundant();
+
   /// Returns a (min, max) pair denoting the minimum and maximum integer values
   /// of the given expression.
   std::pair<int64_t, int64_t> computeIntegerBounds(ArrayRef<int64_t> coeffs);
@@ -272,7 +296,17 @@ class Simplex {
   /// sample value, false otherwise.
   LogicalResult restoreRow(Unknown &u);
 
-  enum class UndoLogEntry { RemoveLastConstraint, UnmarkEmpty };
+  /// Mark the specified unknown redundant. This operation is added to the undo
+  /// log and will be undone by rollbacks. The specified unknown must be in row
+  /// orientation.
+  void markRowRedundant(Unknown &u);
+
+  /// Enum to denote operations that need to be undone during rollback.
+  enum class UndoLogEntry {
+    RemoveLastConstraint,
+    UnmarkEmpty,
+    UnmarkLastRedundant
+  };
 
   /// Undo the operation represented by the log entry.
   void undo(UndoLogEntry entry);
@@ -299,6 +333,10 @@ class Simplex {
   /// and the constant column.
   unsigned nCol;
 
+  /// The number of redundant rows in the tableau. These are the first
+  /// nRedundant rows.
+  unsigned nRedundant;
+
   /// The matrix representing the tableau.
   Matrix tableau;
 

diff  --git a/mlir/lib/Analysis/AffineStructures.cpp b/mlir/lib/Analysis/AffineStructures.cpp
index d3a4c2ed216e..b712b2cef45e 100644
--- a/mlir/lib/Analysis/AffineStructures.cpp
+++ b/mlir/lib/Analysis/AffineStructures.cpp
@@ -1422,6 +1422,51 @@ void FlatAffineConstraints::removeRedundantInequalities() {
   inequalities.resize(numReservedCols * pos);
 }
 
+// A more complex check to eliminate redundant inequalities and equalities. Uses
+// Simplex to check if a constraint is redundant.
+void FlatAffineConstraints::removeRedundantConstraints() {
+  // First, we run GCDTightenInequalities. This allows us to catch some
+  // constraints which are not redundant when considering rational solutions
+  // but are redundant in terms of integer solutions.
+  GCDTightenInequalities();
+  Simplex simplex(*this);
+  simplex.detectRedundant();
+
+  auto copyInequality = [&](unsigned src, unsigned dest) {
+    if (src == dest)
+      return;
+    for (unsigned c = 0, e = getNumCols(); c < e; c++)
+      atIneq(dest, c) = atIneq(src, c);
+  };
+  unsigned pos = 0;
+  unsigned numIneqs = getNumInequalities();
+  // Scan to get rid of all inequalities marked redundant, in-place. In Simplex,
+  // the first constraints added are the inequalities.
+  for (unsigned r = 0; r < numIneqs; r++) {
+    if (!simplex.isMarkedRedundant(r))
+      copyInequality(r, pos++);
+  }
+  inequalities.resize(numReservedCols * pos);
+
+  // Scan to get rid of all equalities marked redundant, in-place. In Simplex,
+  // after the inequalities, a pair of constraints for each equality is added.
+  // An equality is redundant if both the inequalities in its pair are
+  // redundant.
+  auto copyEquality = [&](unsigned src, unsigned dest) {
+    if (src == dest)
+      return;
+    for (unsigned c = 0, e = getNumCols(); c < e; c++)
+      atEq(dest, c) = atEq(src, c);
+  };
+  pos = 0;
+  for (unsigned r = 0, e = getNumEqualities(); r < e; r++) {
+    if (!(simplex.isMarkedRedundant(numIneqs + 2 * r) &&
+          simplex.isMarkedRedundant(numIneqs + 2 * r + 1)))
+      copyEquality(r, pos++);
+  }
+  equalities.resize(numReservedCols * pos);
+}
+
 std::pair<AffineMap, AffineMap> FlatAffineConstraints::getLowerAndUpperBound(
     unsigned pos, unsigned offset, unsigned num, unsigned symStartPos,
     ArrayRef<AffineExpr> localExprs, MLIRContext *context) const {

diff  --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp
index cd13f80fb9b9..db1e48f50e8e 100644
--- a/mlir/lib/Analysis/Presburger/Simplex.cpp
+++ b/mlir/lib/Analysis/Presburger/Simplex.cpp
@@ -17,7 +17,7 @@ const int nullIndex = std::numeric_limits<int>::max();
 
 /// Construct a Simplex object with `nVar` variables.
 Simplex::Simplex(unsigned nVar)
-    : nRow(0), nCol(2), tableau(0, 2 + nVar), empty(false) {
+    : nRow(0), nCol(2), nRedundant(0), tableau(0, 2 + nVar), empty(false) {
   colUnknown.push_back(nullIndex);
   colUnknown.push_back(nullIndex);
   for (unsigned i = 0; i < nVar; ++i) {
@@ -239,7 +239,7 @@ void Simplex::pivot(unsigned pivotRow, unsigned pivotCol) {
   }
   normalizeRow(pivotRow);
 
-  for (unsigned row = 0; row < nRow; ++row) {
+  for (unsigned row = nRedundant; row < nRow; ++row) {
     if (row == pivotRow)
       continue;
     if (tableau(row, pivotCol) == 0) // Nothing to do.
@@ -303,7 +303,7 @@ Optional<unsigned> Simplex::findPivotRow(Optional<unsigned> skipRow,
                                          unsigned col) const {
   Optional<unsigned> retRow;
   int64_t retElem, retConst;
-  for (unsigned row = 0; row < nRow; ++row) {
+  for (unsigned row = nRedundant; row < nRow; ++row) {
     if (skipRow && row == *skipRow)
       continue;
     int64_t elem = tableau(row, col);
@@ -413,7 +413,7 @@ void Simplex::undo(UndoLogEntry entry) {
         // coefficients for every row. But the unknown is a constraint,
         // so it was added initially as a row. Such a row could never have been
         // pivoted to a column. So a pivot row will always be found.
-        for (unsigned i = 0; i < nRow; ++i) {
+        for (unsigned i = nRedundant; i < nRow; ++i) {
           if (tableau(i, column) != 0) {
             row = i;
             break;
@@ -435,6 +435,8 @@ void Simplex::undo(UndoLogEntry entry) {
     con.pop_back();
   } else if (entry == UndoLogEntry::UnmarkEmpty) {
     empty = false;
+  } else if (entry == UndoLogEntry::UnmarkLastRedundant) {
+    nRedundant--;
   }
 }
 
@@ -480,6 +482,65 @@ Optional<Fraction> Simplex::computeOptimum(Direction direction,
   return optimum;
 }
 
+/// Redundant constraints are those that are in row orientation and lie in
+/// rows 0 to nRedundant - 1.
+bool Simplex::isMarkedRedundant(unsigned constraintIndex) const {
+  const Unknown &u = con[constraintIndex];
+  return u.orientation == Orientation::Row && u.pos < nRedundant;
+}
+
+/// Mark the specified row redundant.
+///
+/// This is done by moving the unknown to the end of the block of redundant
+/// rows (namely, to row nRedundant) and incrementing nRedundant to
+/// accomodate the new redundant row.
+void Simplex::markRowRedundant(Unknown &u) {
+  assert(u.orientation == Orientation::Row &&
+         "Unknown should be in row position!");
+  swapRows(u.pos, nRedundant);
+  ++nRedundant;
+  undoLog.emplace_back(UndoLogEntry::UnmarkLastRedundant);
+}
+
+/// Find a subset of constraints that is redundant and mark them redundant.
+void Simplex::detectRedundant() {
+  // It is not meaningful to talk about redundancy for empty sets.
+  if (empty)
+    return;
+
+  // Iterate through the constraints and check for each one if it can attain
+  // negative sample values. If it can, it's not redundant. Otherwise, it is.
+  // We mark redundant constraints redundant.
+  //
+  // Constraints that get marked redundant in one iteration are not respected
+  // when checking constraints in later iterations. This prevents, for example,
+  // two identical constraints both being marked redundant since each is
+  // redundant given the other one. In this example, only the first of the
+  // constraints that is processed will get marked redundant, as it should be.
+  for (Unknown &u : con) {
+    if (u.orientation == Orientation::Column) {
+      unsigned column = u.pos;
+      Optional<unsigned> pivotRow = findPivotRow({}, Direction::Down, column);
+      // If no downward pivot is returned, the constraint is unbounded below
+      // and hence not redundant.
+      if (!pivotRow)
+        continue;
+      pivot(*pivotRow, column);
+    }
+
+    unsigned row = u.pos;
+    Optional<Fraction> minimum = computeRowOptimum(Direction::Down, row);
+    if (!minimum || *minimum < Fraction(0, 1)) {
+      // Constraint is unbounded below or can attain negative sample values and
+      // hence is not redundant.
+      restoreRow(u);
+      continue;
+    }
+
+    markRowRedundant(u);
+  }
+}
+
 bool Simplex::isUnbounded() {
   if (empty)
     return false;
@@ -506,7 +567,7 @@ bool Simplex::isUnbounded() {
 /// The product constraints and variables are stored as: first A's, then B's.
 ///
 /// The product tableau has row layout:
-///   A's rows, B's rows.
+///   A's redundant rows, B's redundant rows, A's other rows, B's other rows.
 ///
 /// It has column layout:
 ///   denominator, constant, A's columns, B's columns.
@@ -569,9 +630,14 @@ Simplex Simplex::makeProduct(const Simplex &a, const Simplex &b) {
     result.nRow++;
   };
 
-  for (unsigned row = 0; row < a.nRow; ++row)
+  result.nRedundant = a.nRedundant + b.nRedundant;
+  for (unsigned row = 0; row < a.nRedundant; ++row)
+    appendRowFromA(row);
+  for (unsigned row = 0; row < b.nRedundant; ++row)
+    appendRowFromB(row);
+  for (unsigned row = a.nRedundant; row < a.nRow; ++row)
     appendRowFromA(row);
-  for (unsigned row = 0; row < b.nRow; ++row)
+  for (unsigned row = b.nRedundant; row < b.nRow; ++row)
     appendRowFromB(row);
 
   return result;

diff  --git a/mlir/unittests/Analysis/AffineStructuresTest.cpp b/mlir/unittests/Analysis/AffineStructuresTest.cpp
index 4ad977d7351f..eded4a889c7b 100644
--- a/mlir/unittests/Analysis/AffineStructuresTest.cpp
+++ b/mlir/unittests/Analysis/AffineStructuresTest.cpp
@@ -274,4 +274,117 @@ TEST(FlatAffineConstraintsTest, IsIntegerEmptyTest) {
                   .isIntegerEmpty());
 }
 
+TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) {
+  FlatAffineConstraints fac = makeFACFromConstraints(1,
+                                                     {
+                                                         {1, -2}, // x >= 2.
+                                                         {-1, 2}  // x <= 2.
+                                                     },
+                                                     {{1, -2}}); // x == 2.
+  fac.removeRedundantConstraints();
+
+  // Both inequalities are redundant given the equality. Both have been removed.
+  EXPECT_EQ(fac.getNumInequalities(), 0u);
+  EXPECT_EQ(fac.getNumEqualities(), 1u);
+
+  FlatAffineConstraints fac2 =
+      makeFACFromConstraints(2,
+                             {
+                                 {1, 0, -3}, // x >= 3.
+                                 {0, 1, -2}  // y >= 2 (redundant).
+                             },
+                             {{1, -1, 0}}); // x == y.
+  fac2.removeRedundantConstraints();
+
+  // The second inequality is redundant and should have been removed. The
+  // remaining inequality should be the first one.
+  EXPECT_EQ(fac2.getNumInequalities(), 1u);
+  EXPECT_THAT(fac2.getInequality(0), testing::ElementsAre(1, 0, -3));
+  EXPECT_EQ(fac2.getNumEqualities(), 1u);
+
+  FlatAffineConstraints fac3 =
+      makeFACFromConstraints(3, {},
+                             {{1, -1, 0, 0},   // x == y.
+                              {1, 0, -1, 0},   // x == z.
+                              {0, 1, -1, 0}}); // y == z.
+  fac3.removeRedundantConstraints();
+
+  // One of the three equalities can be removed.
+  EXPECT_EQ(fac3.getNumInequalities(), 0u);
+  EXPECT_EQ(fac3.getNumEqualities(), 2u);
+
+  FlatAffineConstraints fac4 = makeFACFromConstraints(
+      17,
+      {{0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
+       {0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 500},
+       {0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
+       {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
+       {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998},
+       {0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15},
+       {0, 0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
+       {0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
+       {0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998},
+       {0, 0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15},
+       {0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
+       {0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 500},
+       {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 16, 0, 0, 0, 0, 0, 15},
+       {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -16, 0, 0, 0, 0, 0, 0},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -16, 0, 1, 0, 0, 0},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 998},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16, 0, -1, 0, 0, 15},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 1},
+       {0, 0, 0, 0, 0, 0, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, 8, 8},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, -8, -1},
+       {0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, -8, -1},
+       {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0},
+       {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, -10},
+       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 10},
+       {0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, -13},
+       {0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 13},
+       {0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -10},
+       {0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10},
+       {1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -13},
+       {-1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 13}},
+      {});
+
+  // The above is a large set of constraints without any redundant constraints,
+  // as verified by the Fourier-Motzkin based removeRedundantInequalities.
+  unsigned nIneq = fac4.getNumInequalities();
+  unsigned nEq = fac4.getNumEqualities();
+  fac4.removeRedundantInequalities();
+  ASSERT_EQ(fac4.getNumInequalities(), nIneq);
+  ASSERT_EQ(fac4.getNumEqualities(), nEq);
+  // Now we test that removeRedundantConstraints does not find any constraints
+  // to be redundant either.
+  fac4.removeRedundantConstraints();
+  EXPECT_EQ(fac4.getNumInequalities(), nIneq);
+  EXPECT_EQ(fac4.getNumEqualities(), nEq);
+
+  FlatAffineConstraints fac5 =
+      makeFACFromConstraints(2,
+                             {
+                                 {128, 0, 127}, // [0]: 128x >= -127.
+                                 {-1, 0, 7},    // [1]: x <= 7.
+                                 {-128, 1, 0},  // [2]: y >= 128x.
+                                 {0, 1, 0}      // [3]: y >= 0.
+                             },
+                             {});
+  // [0] implies that 128x >= 0, since x has to be an integer. (This should be
+  // caught by GCDTightenInqualities().)
+  // So [2] and [0] imply [3] since we have y >= 128x >= 0.
+  fac5.removeRedundantConstraints();
+  EXPECT_EQ(fac5.getNumInequalities(), 3u);
+  SmallVector<int64_t, 8> redundantConstraint = {0, 1, 0};
+  for (unsigned i = 0; i < 3; ++i) {
+    // Ensure that the removed constraint was the redundant constraint [3].
+    EXPECT_NE(fac5.getInequality(i), ArrayRef<int64_t>(redundantConstraint));
+  }
+}
+
 } // namespace mlir

diff  --git a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp
index b40b01bbc47b..51cd8fd8e638 100644
--- a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp
@@ -216,4 +216,171 @@ TEST(SimplexTest, getSamplePointIfIntegral) {
                    .hasValue());
 }
 
+/// Some basic sanity checks involving zero or one variables.
+TEST(SimplexTest, isMarkedRedundant_no_var_ge_zero) {
+  Simplex simplex(0);
+  simplex.addInequality({0}); // 0 >= 0.
+
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_TRUE(simplex.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_no_var_eq) {
+  Simplex simplex(0);
+  simplex.addEquality({0}); // 0 == 0.
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_TRUE(simplex.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_pos_var_eq) {
+  Simplex simplex(1);
+  simplex.addEquality({1, 0}); // x == 0.
+
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_FALSE(simplex.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_zero_var_eq) {
+  Simplex simplex(1);
+  simplex.addEquality({0, 0}); // 0x == 0.
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_TRUE(simplex.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_neg_var_eq) {
+  Simplex simplex(1);
+  simplex.addEquality({-1, 0}); // -x == 0.
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_FALSE(simplex.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_pos_var_ge) {
+  Simplex simplex(1);
+  simplex.addInequality({1, 0}); // x >= 0.
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_FALSE(simplex.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_zero_var_ge) {
+  Simplex simplex(1);
+  simplex.addInequality({0, 0}); // 0x >= 0.
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_TRUE(simplex.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_neg_var_ge) {
+  Simplex simplex(1);
+  simplex.addInequality({-1, 0}); // x <= 0.
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_FALSE(simplex.isMarkedRedundant(0));
+}
+
+/// None of the constraints are redundant. Slightly more complicated test
+/// involving an equality.
+TEST(SimplexTest, isMarkedRedundant_no_redundant) {
+  Simplex simplex(3);
+
+  simplex.addEquality({-1, 0, 1, 0});     // u = w.
+  simplex.addInequality({-1, 16, 0, 15}); // 15 - (u - 16v) >= 0.
+  simplex.addInequality({1, -16, 0, 0});  //      (u - 16v) >= 0.
+
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+
+  for (unsigned i = 0; i < simplex.numConstraints(); ++i)
+    EXPECT_FALSE(simplex.isMarkedRedundant(i)) << "i = " << i << "\n";
+}
+
+TEST(SimplexTest, isMarkedRedundant_repeated_constraints) {
+  Simplex simplex(3);
+
+  // [4] to [7] are repeats of [0] to [3].
+  simplex.addInequality({0, -1, 0, 1}); // [0]: y <= 1.
+  simplex.addInequality({-1, 0, 8, 7}); // [1]: 8z >= x - 7.
+  simplex.addInequality({1, 0, -8, 0}); // [2]: 8z <= x.
+  simplex.addInequality({0, 1, 0, 0});  // [3]: y >= 0.
+  simplex.addInequality({-1, 0, 8, 7}); // [4]: 8z >= 7 - x.
+  simplex.addInequality({1, 0, -8, 0}); // [5]: 8z <= x.
+  simplex.addInequality({0, 1, 0, 0});  // [6]: y >= 0.
+  simplex.addInequality({0, -1, 0, 1}); // [7]: y <= 1.
+
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+
+  EXPECT_EQ(simplex.isMarkedRedundant(0), true);
+  EXPECT_EQ(simplex.isMarkedRedundant(1), true);
+  EXPECT_EQ(simplex.isMarkedRedundant(2), true);
+  EXPECT_EQ(simplex.isMarkedRedundant(3), true);
+  EXPECT_EQ(simplex.isMarkedRedundant(4), false);
+  EXPECT_EQ(simplex.isMarkedRedundant(5), false);
+  EXPECT_EQ(simplex.isMarkedRedundant(6), false);
+  EXPECT_EQ(simplex.isMarkedRedundant(7), false);
+}
+
+TEST(SimplexTest, isMarkedRedundant) {
+  Simplex simplex(3);
+  simplex.addInequality({0, -1, 0, 1}); // [0]: y <= 1.
+  simplex.addInequality({1, 0, 0, -1}); // [1]: x >= 1.
+  simplex.addInequality({-1, 0, 0, 2}); // [2]: x <= 2.
+  simplex.addInequality({-1, 0, 2, 7}); // [3]: 2z >= x - 7.
+  simplex.addInequality({1, 0, -2, 0}); // [4]: 2z <= x.
+  simplex.addInequality({0, 1, 0, 0});  // [5]: y >= 0.
+  simplex.addInequality({0, 1, -2, 1}); // [6]: y >= 2z - 1.
+  simplex.addInequality({-1, 1, 0, 1}); // [7]: y >= x - 1.
+
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+
+  // [0], [1], [3], [4], [7] together imply [2], [5], [6] must hold.
+  //
+  // From [7], [0]: x <= y + 1 <= 2, so we have [2].
+  // From [7], [1]: y >= x - 1 >= 0, so we have [5].
+  // From [4], [7]: 2z - 1 <= x - 1 <= y, so we have [6].
+  EXPECT_FALSE(simplex.isMarkedRedundant(0));
+  EXPECT_FALSE(simplex.isMarkedRedundant(1));
+  EXPECT_TRUE(simplex.isMarkedRedundant(2));
+  EXPECT_FALSE(simplex.isMarkedRedundant(3));
+  EXPECT_FALSE(simplex.isMarkedRedundant(4));
+  EXPECT_TRUE(simplex.isMarkedRedundant(5));
+  EXPECT_TRUE(simplex.isMarkedRedundant(6));
+  EXPECT_FALSE(simplex.isMarkedRedundant(7));
+}
+
+TEST(SimplexTest, isMarkedRedundantTiledLoopNestConstraints) {
+  Simplex simplex(3);                     // Variables are x, y, N.
+  simplex.addInequality({1, 0, 0, 0});    // [0]: x >= 0.
+  simplex.addInequality({-32, 0, 1, -1}); // [1]: 32x <= N - 1.
+  simplex.addInequality({0, 1, 0, 0});    // [2]: y >= 0.
+  simplex.addInequality({-32, 1, 0, 0});  // [3]: y >= 32x.
+  simplex.addInequality({32, -1, 0, 31}); // [4]: y <= 32x + 31.
+  simplex.addInequality({0, -1, 1, -1});  // [5]: y <= N - 1.
+  // [3] and [0] imply [2], as we have y >= 32x >= 0.
+  // [3] and [5] imply [1], as we have 32x <= y <= N - 1.
+  simplex.detectRedundant();
+  EXPECT_FALSE(simplex.isMarkedRedundant(0));
+  EXPECT_TRUE(simplex.isMarkedRedundant(1));
+  EXPECT_TRUE(simplex.isMarkedRedundant(2));
+  EXPECT_FALSE(simplex.isMarkedRedundant(3));
+  EXPECT_FALSE(simplex.isMarkedRedundant(4));
+  EXPECT_FALSE(simplex.isMarkedRedundant(5));
+}
+
+TEST(SimplexTest, addInequality_already_redundant) {
+  Simplex simplex(1);
+  simplex.addInequality({1, -1}); // x >= 1.
+  simplex.addInequality({1, 0});  // x >= 0.
+  simplex.detectRedundant();
+  ASSERT_FALSE(simplex.isEmpty());
+  EXPECT_FALSE(simplex.isMarkedRedundant(0));
+  EXPECT_TRUE(simplex.isMarkedRedundant(1));
+}
+
 } // namespace mlir


        


More information about the Mlir-commits mailing list