[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