[MLIR] Redundancy detection for FlatAffineConstraints using Simplex

[arjunp]

Summary

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.

[arjunp]

Improved documentation.

[bondhugula]

Thanks for implementing this functionality. Some superfluous comments on documentation to start with.

mlir/include/mlir/Analysis/AffineStructures.h

540

Triple doc comment please.

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

117

Nit: . i.e., -> , i.e.,

184

constraint or inequality? The signature indicates inequality.

296

Missing doc comment.

mlir/lib/Analysis/AffineStructures.cpp

1413

inequalities or inequalities and equalities?

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

219

Comment above on what these tests are testing.

299

Comment here on what you are trying to test.

336

Use i = 0, e = ...; i < e form please.

[bondhugula]

mlir/lib/Analysis/Presburger/Simplex.cpp

501

General comment here on the implementation.

mlir/unittests/Analysis/AffineStructuresTest.cpp

275

Could you add this test case? It's a common pattern.

i >= 0, 32*i <= N - 1, 
ii >= 32i, ii >= 0, ii <= 32ii + 31, ii <= N-1

This fourth constraint is redundant.

[bondhugula]

mlir/include/mlir/Analysis/AffineStructures.h

540

A check using Simplex ... -> Removes redundant constraints using Simplex.

It would be good to add a couple of lines to say something about its complexity even if its high level.

[arjunp]

Addressed comments. Also changed the names of some Simplex objects to simplex for uniformity.

[arjunp]

clang-format.

[arjunp]

mlir/unittests/Analysis/AffineStructuresTest.cpp

275

Added in SimplexTest.

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

299

Moved to AffineStructuresTest.

[arjunp]

clang-format again. Mention redundancy checks in the Simplex.h header comment and first paragraph of the Simplex class documentation.

[bondhugula]

mlir/include/mlir/Analysis/AffineStructures.h

541

Actually, the worst case here is rare and 'n' doesn't keep growing for the use cases as it is tied to loop nest and array dimensionalities - so you may want to just use (rare) in parentheses or to that effect. Otherwise, users may think it's more expensive than it really is. We are looking at a small number of variables and vertices here. Any upper bound in terms of the number of vertices and the number of constraints will also be helpful.

[bondhugula]

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

301

Comment here please.

mlir/lib/Analysis/AffineStructures.cpp

1437

is -> if

mlir/lib/Analysis/Presburger/Simplex.cpp

507–508

You can move these comments inline into the body of the function.

514

Comment here.

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

357

Can you rename isMarkedRedundant2? (These are typical constraints from a tiled loop nest.)

[bondhugula]

Looks great overall - ideally, I'd like to some more test case patterns - the additional tests can be small. Consider this one:

128x >= -127
x <= 7
y >= 128x
y >= 0

The last constraint should be redundant.

[bondhugula]

Please add an [MLIR] tag to the commit title.

[arjunp]

Address inline review comments.

[arjunp]

Add suggested test.

[arjunp]

Thanks for your review!

In the test you suggested, was the first constraint meant to be 128x >= 127 rather than 128x >= -127? I see that when x is constrained to integers, 128x >= -127 does imply 128x >= 0. Currently, the implementation doesn't use the integrality of the variables at all. This case could be caught by internally running FlatAffineConstraints::GCDTightenInequalities()before constructing the Simplex. Should this be done?

Also, I forgot to mention that in the previous test you suggested, I assumed that the penultimate constraint was meant to be ii <= 32i + 31 rather than ii <= 32ii + 31 (in which ii occurs twice). Was this correct?

[arjunp]

Run GCDTightenInequalities() before the redundancy check in order to catch some constraints which are not rational-redundant but are integer-redundant, i.e. the constraint is valid for all integer solutions of the other constraints even though it is not valid for all rational solutions.

[arjunp]

Also, I don't have commit access yet, so someone else will need to land this.

[bondhugula]

In D84935#2200124, @arjunp wrote:

Thanks for your review!

In the test you suggested, was the first constraint meant to be 128x >= 127 rather than 128x >= -127? I see that when x is constrained to integers, 128x >= -127 does imply 128x >= 0. Currently, the implementation doesn't use the integrality of the variables at all. This case could be caught by internally running

I actually meant 128x >= -127 to stress on the integrality part. I now see your comment on the implementation not using integrality in any way.

FlatAffineConstraints::GCDTightenInequalities()before constructing the Simplex. Should this be done?

Well, in this case, GCD tighten inequalities will help tighten it to x >= 0, but that's just a stop gap / best effor thing in that it won't help in other non-trivial / general cases. So I guess one gets the desired simplified result here only by doing this tightening before using the proposed redundancy check?

Also, I forgot to mention that in the previous test you suggested, I assumed that the penultimate constraint was meant to be ii <= 32i + 31 rather than ii <= 32ii + 31 (in which ii occurs twice). Was this correct?

That's right - that was a typo.

[bondhugula]

mlir/unittests/Analysis/AffineStructuresTest.cpp

382

Random comment: for a stronger test, is there a way you can check in addition that a specific inequality doesn't exist in the set? (in this case that y >= 0 doesn't exist).

[bondhugula]

In D84935#2223424, @arjunp wrote:

Also, I don't have commit access yet, so someone else will need to land this.

I can commit this for you. Do you have anything more to update? Could you look at the last question?

[arjunp]

Ensure that the removed constraint is the redundant one.

[arjunp]

Well, in this case, GCD tighten inequalities will help tighten it to x >= 0, but that's just a stop gap / best effor thing in that it won't help in other non-trivial / general cases. So I guess one gets the desired simplified result here only by doing this tightening before using the proposed redundancy check?

Yes, we have to tighten before running the redundancy check. I don't think it's possible to have a general integer-exact redundancy check without using an integer-exact emptiness check.

mlir/include/mlir/Analysis/AffineStructures.h

public:
   /// constraints, does a single scan, and updates in place. It also normalizes
   /// constraints by their GCD and performs GCD tightening on inequalities.
   void removeTrivialRedundancy();
 
   /// A more expensive check to detect redundant inequalities thatn
   /// removeTrivialRedundancy.
   void removeRedundantInequalities();
 
+  // A check using Simplex to eliminate redundant constraints.
+  void removeRedundantConstraints();
+
   // Removes all equalities and inequalities.
   void clearConstraints();
 
   void print(raw_ostream &os) const;
   void dump() const;
 
 private:
   /// Returns false if the fields corresponding to various identifier counts, or

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

 /// in the current tableau configuration may be negative. In that case, we try
 /// to find a series of pivots to bring us to a consistent tableau
 /// configuration, i.e. we try to make the new constraint's sample value
 /// non-negative without making that of any other constraints negative. (See
 /// findPivot and findPivotRow for details.) If this is not possible, then the
 /// 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
 /// log, and rolling back to a snapshot is done by reverting each log entry's
 /// operation from the end until we reach the snapshot's location.
 ///
 /// Finding an integer sample is done with the Generalized Basis Reduction
 /// algorithm. See the documentation for findIntegerSample and reduceBasis.
public:
 
   /// Get a snapshot of the current state. This is used for rolling back.
   unsigned getSnapshot() const;
 
   /// Rollback to a snapshot. This invalidates all later snapshots.
   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.
   Optional<Fraction> computeRowOptimum(Direction direction, unsigned row);
 
   /// Compute the maximum or minimum value of the given expression, depending on
   /// direction.
   ///
   /// Returns a (num, den) pair denoting the optimum, or a null value if no
   /// optimum exists, i.e., if the expression is unbounded in this direction.
   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 inequalityIndex) const;
+
+  /// Finds a maximal 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);
 
   /// Returns true if the polytope is unbounded, i.e., extends to infinity in
   /// some direction. Otherwise, returns false.
   bool isUnbounded();
 
private:
   void swapRows(unsigned i, unsigned j);
 
   /// Restore the unknown to a non-negative sample value.
   ///
   /// Returns true if the unknown was successfully restored to a non-negative
   /// sample value, false otherwise.
   LogicalResult restoreRow(Unknown &u);
 
-  enum class UndoLogEntry { RemoveLastConstraint, UnmarkEmpty };
+  void markRowRedundant(Unknown &u);
+
+  enum class UndoLogEntry {
+    RemoveLastConstraint,
+    UnmarkEmpty,
+    UnmarkLastRedundant
+  };
 
   /// Undo the operation represented by the log entry.
   void undo(UndoLogEntry entry);
 
   /// Find a row that can be used to pivot the column in the specified
   /// direction. If skipRow is not null, then this row is excluded
   /// from consideration. The returned pivot will maintain all constraints
   /// except the column itself and skipRow, if it is set. (if these unknowns
private:
 
   /// The number of rows in the tableau.
   unsigned nRow;
 
   /// The number of columns in the tableau, including the common denominator
   /// 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;
 
   /// This is true if the tableau has been detected to be empty, false
   /// otherwise.
   bool empty;
 
   /// Holds a log of operations, used for rolling back to a previous state.

mlir/lib/Analysis/AffineStructures.cpp

void FlatAffineConstraints::removeRedundantInequalities() {
   unsigned pos = 0;
   for (unsigned r = 0, e = getNumInequalities(); r < e; r++) {
     if (!redun[r])
       copyRow(r, pos++);
   }
   inequalities.resize(numReservedCols * pos);
 }
 
+// A more complex check to eliminate redundant inequalities. Uses Simplex
+// to check if a constraint is redundant.
+void FlatAffineConstraints::removeRedundantConstraints() {
+  Simplex simplex(*this);
+  simplex.detectRedundant();
+
+  // Scan to get rid of all inequalities marked redundant, in-place.
+  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();
+  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.
+  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 {
   assert(pos + offset < getNumDimIds() && "invalid dim start pos");
   assert(symStartPos >= (pos + offset) && "invalid sym start pos");
   assert(getNumLocalIds() == localExprs.size() &&
          "incorrect local exprs count");
 

mlir/lib/Analysis/Presburger/Simplex.cpp

 
 namespace mlir {
 using Direction = Simplex::Direction;
 
 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) {
     var.emplace_back(Orientation::Column, /*restricted=*/false, /*pos=*/nCol);
     colUnknown.push_back(i);
     nCol++;
   }
 }
if (tableau(pivotRow, 0) < 0) {
     for (unsigned col = 1; col < nCol; ++col) {
       if (col == pivotCol)
         continue;
       tableau(pivotRow, col) = -tableau(pivotRow, col);
     }
   }
   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.
       continue;
     tableau(row, 0) *= tableau(pivotRow, 0);
     for (unsigned j = 1; j < nCol; ++j) {
       if (j == pivotCol)
         continue;

 /// 0 and hence saturates the bound it imposes. We break ties between rows that
 /// impose the same bound by considering a lexicographic ordering where we
 /// prefer unknowns with lower index value.
 Optional<unsigned> Simplex::findPivotRow(Optional<unsigned> skipRow,
                                          Direction direction,
                                          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);
     if (elem == 0)
       continue;
     if (!unknownFromRow(row).restricted)
       continue;
     if (signMatchesDirection(elem, direction))
if (constraint.orientation == Orientation::Column) {
       } else if (Optional<unsigned> maybeRow =
                      findPivotRow({}, Direction::Down, column)) {
         row = *maybeRow;
       } else {
         // The loop doesn't find a pivot row only if the column has zero
         // 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;
           }
         }
       }
       assert(row.hasValue() && "No pivot row found!");
       pivot(*row, column);
     }
 
     // Move this unknown to the last row and remove the last row from the
     // tableau.
     swapRows(constraint.pos, nRow - 1);
     // It is not strictly necessary to shrink the tableau, but for now we
     // maintain the invariant that the tableau has exactly nRow rows.
     tableau.resizeVertically(nRow - 1);
     nRow--;
     rowUnknown.pop_back();
     con.pop_back();
   } else if (entry == UndoLogEntry::UnmarkEmpty) {
     empty = false;
+  } else if (entry == UndoLogEntry::UnmarkLastRedundant) {
+    nRedundant--;
   }
 }
 
 /// Rollback to the specified snapshot.
 ///
 /// We undo all the log entries until the log size when the snapshot was taken
 /// is reached.
 void Simplex::rollback(unsigned snapshot) {
Optional<Fraction> Simplex::computeOptimum(Direction direction,
   unsigned snapshot = getSnapshot();
   unsigned conIndex = addRow(coeffs);
   unsigned row = con[conIndex].pos;
   Optional<Fraction> optimum = computeRowOptimum(direction, row);
   rollback(snapshot);
   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;
+}
+
+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);
+}
+
+void Simplex::detectRedundant() {
+  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;
 
   SmallVector<int64_t, 8> dir(var.size() + 1);
   for (unsigned i = 0; i < var.size(); ++i) {
     dir[i] = 1;
 
bool Simplex::isUnbounded() {
   return false;
 }
 
 /// Make a tableau to represent a pair of points in the original tableau.
 ///
 /// 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 redundan rows, A's other rows, B's other rows.
 ///
 /// It has column layout:
 ///   denominator, constant, A's columns, B's columns.
 Simplex Simplex::makeProduct(const Simplex &a, const Simplex &b) {
   unsigned numVar = a.numVariables() + b.numVariables();
   unsigned numCon = a.numConstraints() + b.numConstraints();
   Simplex result(numVar);
 
auto appendRowFromB = [&](unsigned row) {
     for (unsigned col = 2; col < b.nCol; ++col)
       result.tableau(result.nRow, offset + col) = b.tableau(row, col);
     result.rowUnknown.push_back(indexFromBIndex(b.rowUnknown[row]));
     result.unknownFromIndex(result.rowUnknown.back()).pos =
         result.rowUnknown.size() - 1;
     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;
 }
 
 Optional<SmallVector<int64_t, 8>> Simplex::getSamplePointIfIntegral() const {
   // The tableau is empty, so no sample point exists.
   if (empty)

mlir/unittests/Analysis/AffineStructuresTest.cpp

EXPECT_TRUE(makeFACFromConstraints(
                   {
                       {1, 0, 0, 0, 0},
                       {-1, 0, 0, 0, 100},
                       {0, 1, 0, 0, 0},
                       {0, -1, 0, 0, 100},
                   },
                   {{2, -3, 0, 0, 0}, {1, -1, 6, 0, -1}, {1, 1, 0, -6, -2}})
                   .isIntegerEmpty());
 }
 
+TEST(FlatAffineConstraintsTest, removeRedundantTest) {
+  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);
+}
+
 } // namespace mlir

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

EXPECT_FALSE(simplexFromConstraints(1,
                                       {// 2x = 1. (no integer solutions)
                                        {2, -1},
                                        {-2, +1}},
                                       {})
                    .getSamplePointIfIntegral()
                    .hasValue());
 }
 
+TEST(SimplexTest, isMarkedRedundant_no_var_ge_zero) {
+  Simplex tab(0);
+  tab.addInequality({0}); // 0 >= 0
+
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_TRUE(tab.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_no_var_eq) {
+  Simplex tab(0);
+  tab.addEquality({0}); // 0 == 0
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_TRUE(tab.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_pos_var_eq) {
+  Simplex tab(1);
+  tab.addEquality({1, 0}); // x == 0
+
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_FALSE(tab.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_zero_var_eq) {
+  Simplex tab(1);
+  tab.addEquality({0, 0}); // 0x == 0
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_TRUE(tab.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_neg_var_eq) {
+  Simplex tab(1);
+  tab.addEquality({-1, 0}); // -x == 0
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_FALSE(tab.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_pos_var_ge) {
+  Simplex tab(1);
+  tab.addInequality({1, 0}); // x >= 0
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_FALSE(tab.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_zero_var_ge) {
+  Simplex tab(1);
+  tab.addInequality({0, 0}); // 0x >= 0
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_TRUE(tab.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_neg_var_ge) {
+  Simplex tab(1);
+  tab.addInequality({-1, 0}); // x <= 0
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_FALSE(tab.isMarkedRedundant(0));
+}
+
+TEST(SimplexTest, isMarkedRedundant_no_redundant) {
+  Simplex tab(3);
+
+  tab.addEquality({-1, 0, 1, 0});     // u = w
+  tab.addInequality({-1, 16, 0, 15}); // 15 - (u - 16v) >= 0
+  tab.addInequality({1, -16, 0, 0});  //      (u - 16v) >= 0
+
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+
+  for (unsigned i = 0; i < tab.numConstraints(); ++i)
+    EXPECT_FALSE(tab.isMarkedRedundant(i)) << "i = " << i << "\n";
+}
+
+TEST(SimplexTest, isMarkedRedundant_regression_test) {
+  Simplex tab(17);
+
+  tab.addEquality({0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0});
+  tab.addEquality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, -10});
+  tab.addEquality({0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, -13});
+  tab.addEquality({0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -10});
+  tab.addEquality({1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -13});
+  tab.addInequality({0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1});
+  tab.addInequality({0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 500});
+  tab.addInequality({0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0});
+  tab.addInequality({0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1});
+  tab.addInequality({0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998});
+  tab.addInequality({0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15});
+  tab.addInequality({0, 0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1});
+  tab.addInequality({0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998});
+  tab.addInequality({0, 0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 500});
+  tab.addInequality({0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 16, 0, 0, 0, 0, 0, 15});
+  tab.addInequality({0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -16, 0, 0, 0, 0, 0, 0});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -16, 0, 1, 0, 0, 0});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 998});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16, 0, -1, 0, 0, 15});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 1});
+  tab.addInequality({0, 0, 0, 0, 0, 0, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, 8, 8});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, -8, -1});
+  tab.addInequality({0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, -8, -1});
+
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  for (unsigned i = 0; i < tab.numConstraints(); ++i)
+    EXPECT_FALSE(tab.isMarkedRedundant(i)) << "i = " << i << '\n';
+}
+
+TEST(SimplexTest, isMarkedRedundant_repeated_constraints) {
+  Simplex tab(3);
+
+  // [4] to [7] are repeats of [0] to [3].
+  tab.addInequality({0, -1, 0, 1}); // [0]: y <= 1
+  tab.addInequality({-1, 0, 8, 7}); // [1]: 8z >= x - 7
+  tab.addInequality({1, 0, -8, 0}); // [2]: 8z <= x
+  tab.addInequality({0, 1, 0, 0});  // [3]: y >= 0
+  tab.addInequality({-1, 0, 8, 7}); // [4]: 8z >= 7 - x
+  tab.addInequality({1, 0, -8, 0}); // [5]: 8z <= x
+  tab.addInequality({0, 1, 0, 0});  // [6]: y >= 0
+  tab.addInequality({0, -1, 0, 1}); // [7]: y <= 1
+
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+
+  EXPECT_EQ(tab.isMarkedRedundant(0), true);
+  EXPECT_EQ(tab.isMarkedRedundant(1), true);
+  EXPECT_EQ(tab.isMarkedRedundant(2), true);
+  EXPECT_EQ(tab.isMarkedRedundant(3), true);
+  EXPECT_EQ(tab.isMarkedRedundant(4), false);
+  EXPECT_EQ(tab.isMarkedRedundant(5), false);
+  EXPECT_EQ(tab.isMarkedRedundant(6), false);
+  EXPECT_EQ(tab.isMarkedRedundant(7), false);
+}
+
+TEST(SimplexTest, isMarkedRedundant) {
+  Simplex tab(3);
+  tab.addInequality({0, -1, 0, 1}); // [0]: y <= 1
+  tab.addInequality({1, 0, 0, -1}); // [1]: x >= 1
+  tab.addInequality({-1, 0, 0, 2}); // [2]: x <= 2
+  tab.addInequality({-1, 0, 2, 7}); // [3]: 2z >= x - 7
+  tab.addInequality({1, 0, -2, 0}); // [4]: 2z <= x
+  tab.addInequality({0, 1, 0, 0});  // [5]: y >= 0
+  tab.addInequality({0, 1, -2, 1}); // [6]: y >= 2z - 1
+  tab.addInequality({-1, 1, 0, 1}); // [7]: y >= x - 1
+
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.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(tab.isMarkedRedundant(0));
+  EXPECT_FALSE(tab.isMarkedRedundant(1));
+  EXPECT_TRUE(tab.isMarkedRedundant(2));
+  EXPECT_FALSE(tab.isMarkedRedundant(3));
+  EXPECT_FALSE(tab.isMarkedRedundant(4));
+  EXPECT_TRUE(tab.isMarkedRedundant(5));
+  EXPECT_TRUE(tab.isMarkedRedundant(6));
+  EXPECT_FALSE(tab.isMarkedRedundant(7));
+}
+
+TEST(SimplexTest, addInequality_already_redundant) {
+  Simplex tab(1);
+  tab.addInequality({1, -1}); // x >= 1
+  tab.addInequality({1, 0});  // x >= 0
+  tab.detectRedundant();
+  ASSERT_FALSE(tab.isEmpty());
+  EXPECT_FALSE(tab.isMarkedRedundant(0));
+  EXPECT_TRUE(tab.isMarkedRedundant(1));
+}
+
 } // namespace mlir