From b97aa413d166c064db65051cae97068c83319a6b Mon Sep 17 00:00:00 2001 From: Arjun P Date: Wed, 30 Mar 2022 23:24:00 +0100 Subject: [PATCH] Revert "[MLIR][Presburger] LexSimplex::addEquality: add equalities as fixed columns" This reverts commit 5630143af33f7e6e0dabdf38982cc9800140bb75. The implementation in this commit was incorrect. Also, handling this representation of equalities in the upcoming support for symbolic lexicographic minimization makes that patch much more complex. It will be easier to review that without this representaiton and then reintroduce the fixed column representation later, hence the revert rather than a bug fix. --- .../mlir/Analysis/Presburger/Simplex.h | 42 +++++------------ mlir/lib/Analysis/Presburger/Simplex.cpp | 45 +++---------------- .../Analysis/Presburger/SimplexTest.cpp | 7 --- 3 files changed, 18 insertions(+), 76 deletions(-) diff --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h b/mlir/include/mlir/Analysis/Presburger/Simplex.h index 235b794c6bd7..90f092ff39ac 100644 --- a/mlir/include/mlir/Analysis/Presburger/Simplex.h +++ b/mlir/include/mlir/Analysis/Presburger/Simplex.h @@ -166,21 +166,21 @@ public: /// false otherwise. bool isEmpty() const; + /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n + /// is the current number of variables, then the corresponding inequality is + /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0. + virtual void addInequality(ArrayRef coeffs) = 0; + /// Returns the number of variables in the tableau. unsigned getNumVariables() const; /// Returns the number of constraints in the tableau. unsigned getNumConstraints() const; - /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n - /// is the current number of variables, then the corresponding inequality is - /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0. - virtual void addInequality(ArrayRef coeffs) = 0; - /// Add an equality to the tableau. If coeffs is c_0, c_1, ... c_n, where n /// is the current number of variables, then the corresponding equality is /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0. - virtual void addEquality(ArrayRef coeffs) = 0; + void addEquality(ArrayRef coeffs); /// Add new variables to the end of the list of variables. void appendVariable(unsigned count = 1); @@ -249,14 +249,6 @@ protected: /// coefficient for it. Optional findAnyPivotRow(unsigned col); - /// Return any column that this row can be pivoted with, ignoring tableau - /// consistency. Equality rows are not considered. - /// - /// Returns an empty optional if no pivot is possible, which happens only when - /// the column unknown is a variable and no constraint has a non-zero - /// coefficient for it. - Optional findAnyPivotCol(unsigned row); - /// Swap the row with the column in the tableau's data structures but not the /// tableau itself. This is used by pivot. void swapRowWithCol(unsigned row, unsigned col); @@ -303,7 +295,6 @@ protected: RemoveLastVariable, UnmarkEmpty, UnmarkLastRedundant, - UnmarkLastEquality, RestoreBasis }; @@ -317,14 +308,13 @@ protected: /// Undo the operation represented by the log entry. void undo(UndoLogEntry entry); - unsigned getNumFixedCols() const { return numFixedCols; } + /// Return the number of fixed columns, as described in the constructor above, + /// this is the number of columns beyond those for the variables in var. + unsigned getNumFixedCols() const { return usingBigM ? 3u : 2u; } /// Stores whether or not a big M column is present in the tableau. bool usingBigM; - /// denom + const + maybe M + equality columns - unsigned numFixedCols; - /// The number of rows in the tableau. unsigned nRow; @@ -445,12 +435,9 @@ public: /// /// This just adds the inequality to the tableau and does not try to create a /// consistent tableau configuration. - void addInequality(ArrayRef coeffs) final; - - /// Add an equality to the tableau. If coeffs is c_0, c_1, ... c_n, where n - /// is the current number of variables, then the corresponding equality is - /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0. - void addEquality(ArrayRef coeffs) final; + void addInequality(ArrayRef coeffs) final { + addRow(coeffs, /*makeRestricted=*/true); + } /// Get a snapshot of the current state. This is used for rolling back. unsigned getSnapshot() { return SimplexBase::getSnapshotBasis(); } @@ -546,11 +533,6 @@ public: /// state and marks the Simplex empty if this is not possible. void addInequality(ArrayRef coeffs) final; - /// Add an equality to the tableau. If coeffs is c_0, c_1, ... c_n, where n - /// is the current number of variables, then the corresponding equality is - /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0. - void addEquality(ArrayRef coeffs) final; - /// Compute the maximum or minimum value of the given row, depending on /// direction. The specified row is never pivoted. On return, the row may /// have a negative sample value if the direction is down. diff --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp index 33ccfe1d83db..b0d00aea443d 100644 --- a/mlir/lib/Analysis/Presburger/Simplex.cpp +++ b/mlir/lib/Analysis/Presburger/Simplex.cpp @@ -19,12 +19,12 @@ using Direction = Simplex::Direction; const int nullIndex = std::numeric_limits::max(); SimplexBase::SimplexBase(unsigned nVar, bool mustUseBigM) - : usingBigM(mustUseBigM), numFixedCols(mustUseBigM ? 3 : 2), nRow(0), - nCol(numFixedCols + nVar), nRedundant(0), tableau(0, nCol), empty(false) { - colUnknown.insert(colUnknown.begin(), numFixedCols, nullIndex); + : usingBigM(mustUseBigM), nRow(0), nCol(getNumFixedCols() + nVar), + nRedundant(0), tableau(0, nCol), empty(false) { + colUnknown.insert(colUnknown.begin(), getNumFixedCols(), nullIndex); for (unsigned i = 0; i < nVar; ++i) { var.emplace_back(Orientation::Column, /*restricted=*/false, - /*pos=*/numFixedCols + i); + /*pos=*/getNumFixedCols() + i); colUnknown.push_back(i); } } @@ -309,7 +309,7 @@ void LexSimplex::restoreRationalConsistency() { // minimizes the change in sample value. LogicalResult LexSimplex::moveRowUnknownToColumn(unsigned row) { Optional maybeColumn; - for (unsigned col = getNumFixedCols(); col < nCol; ++col) { + for (unsigned col = 3; col < nCol; ++col) { if (tableau(row, col) <= 0) continue; maybeColumn = @@ -648,7 +648,7 @@ void Simplex::addInequality(ArrayRef coeffs) { /// /// We simply add two opposing inequalities, which force the expression to /// be zero. -void Simplex::addEquality(ArrayRef coeffs) { +void SimplexBase::addEquality(ArrayRef coeffs) { addInequality(coeffs); SmallVector negatedCoeffs; for (int64_t coeff : coeffs) @@ -705,15 +705,6 @@ Optional SimplexBase::findAnyPivotRow(unsigned col) { return {}; } -// This doesn't find a pivot column only if the row has zero coefficients for -// every column not marked as an equality. -Optional SimplexBase::findAnyPivotCol(unsigned row) { - for (unsigned col = getNumFixedCols(); col < nCol; ++col) - if (tableau(row, col) != 0) - return col; - return {}; -} - // It's not valid to remove the constraint by deleting the column since this // would result in an invalid basis. void Simplex::undoLastConstraint() { @@ -789,10 +780,6 @@ void SimplexBase::undo(UndoLogEntry entry) { empty = false; } else if (entry == UndoLogEntry::UnmarkLastRedundant) { nRedundant--; - } else if (entry == UndoLogEntry::UnmarkLastEquality) { - numFixedCols--; - assert(getNumFixedCols() >= 2 + usingBigM && - "The denominator, constant, big M and symbols are always fixed!"); } else if (entry == UndoLogEntry::RestoreBasis) { assert(!savedBases.empty() && "No bases saved!"); @@ -1123,26 +1110,6 @@ Optional> Simplex::getRationalSample() const { return sample; } -void LexSimplex::addInequality(ArrayRef coeffs) { - addRow(coeffs, /*makeRestricted=*/true); -} - -/// Try to make the equality a fixed column by finding any pivot and performing -/// it. The only time this is not possible is when the given equality's -/// direction is already in the span of the existing fixed column equalities. In -/// that case, we just leave it in row position. -void LexSimplex::addEquality(ArrayRef coeffs) { - const Unknown &u = con[addRow(coeffs, /*makeRestricted=*/true)]; - Optional pivotCol = findAnyPivotCol(u.pos); - if (!pivotCol) - return; - - pivot(u.pos, *pivotCol); - swapColumns(*pivotCol, getNumFixedCols()); - numFixedCols++; - undoLog.push_back(UndoLogEntry::UnmarkLastEquality); -} - MaybeOptimum> LexSimplex::getRationalSample() const { if (empty) return OptimumKind::Empty; diff --git a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp index ce5dad77819c..e605c89b4692 100644 --- a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp +++ b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp @@ -548,10 +548,3 @@ TEST(SimplexTest, addDivisionVariable) { ASSERT_TRUE(sample.hasValue()); EXPECT_EQ((*sample)[0] / 2, (*sample)[1]); } - -TEST(LexSimplexTest, addEquality) { - IntegerRelation rel(/*numDomain=*/0, /*numRange=*/1); - rel.addEquality({1, 0}); - LexSimplex simplex(rel); - EXPECT_EQ(simplex.getNumConstraints(), 1u); -}