forked from OSchip/llvm-project
[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
This commit is contained in:
Arjun P
Uday Bondhugula
parent
33e2f69a24
commit
33f574672f
|
|
@ -546,6 +546,13 @@ public:
|
|||
/// 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();
|
||||
|
||||
|
|
|
|||
|
|
@ -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 @@ public:
|
|||
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 @@ public:
|
|||
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 @@ private:
|
|||
/// 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 @@ private:
|
|||
/// 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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -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.nRow; ++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 = b.nRedundant; row < b.nRow; ++row)
|
||||
appendRowFromB(row);
|
||||
|
||||
return result;
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue