diff --git a/mlir/include/mlir/Analysis/AffineStructures.h b/mlir/include/mlir/Analysis/AffineStructures.h --- a/mlir/include/mlir/Analysis/AffineStructures.h +++ b/mlir/include/mlir/Analysis/AffineStructures.h @@ -537,6 +537,13 @@ /// 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 --- 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 @@ /// 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 @@ /// 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 @@ 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 @@ Optional computeOptimum(Direction direction, ArrayRef 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 computeIntegerBounds(ArrayRef coeffs); @@ -272,7 +296,17 @@ /// 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 @@ /// 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 --- a/mlir/lib/Analysis/AffineStructures.cpp +++ b/mlir/lib/Analysis/AffineStructures.cpp @@ -1410,6 +1410,51 @@ 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 FlatAffineConstraints::getLowerAndUpperBound( unsigned pos, unsigned offset, unsigned num, unsigned symStartPos, ArrayRef localExprs, MLIRContext *context) const { diff --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp --- a/mlir/lib/Analysis/Presburger/Simplex.cpp +++ b/mlir/lib/Analysis/Presburger/Simplex.cpp @@ -17,7 +17,7 @@ /// 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 @@ } 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 @@ unsigned col) const { Optional 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 @@ // 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 @@ con.pop_back(); } else if (entry == UndoLogEntry::UnmarkEmpty) { empty = false; + } else if (entry == UndoLogEntry::UnmarkLastRedundant) { + nRedundant--; } } @@ -480,6 +482,65 @@ 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 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 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 @@ /// 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 @@ 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 --- a/mlir/unittests/Analysis/AffineStructuresTest.cpp +++ b/mlir/unittests/Analysis/AffineStructuresTest.cpp @@ -274,4 +274,117 @@ .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 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(redundantConstraint)); + } +} + } // namespace mlir diff --git a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp --- a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp +++ b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp @@ -216,4 +216,171 @@ .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