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 @@ -419,15 +419,9 @@ /// (A_k)*y is not zero then we have that A*y is lexicopositive and if not we /// ignore more columns; eventually if all these dot products become zero then /// A*y is zero and we are done. -class LexSimplex : public SimplexBase { +class LexSimplexBase : public SimplexBase { public: - explicit LexSimplex(unsigned nVar) - : SimplexBase(nVar, /*mustUseBigM=*/true) {} - explicit LexSimplex(const IntegerRelation &constraints) - : LexSimplex(constraints.getNumIds()) { - intersectIntegerRelation(constraints); - } - ~LexSimplex() override = default; + ~LexSimplexBase() override = default; /// 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 @@ -435,13 +429,52 @@ /// /// This just adds the inequality to the tableau and does not try to create a /// consistent tableau configuration. - void addInequality(ArrayRef coeffs) final { - addRow(coeffs, /*makeRestricted=*/true); - } + void addInequality(ArrayRef coeffs) final; /// Get a snapshot of the current state. This is used for rolling back. unsigned getSnapshot() { return SimplexBase::getSnapshotBasis(); } +protected: + LexSimplexBase(unsigned nVar) : SimplexBase(nVar, /*mustUseBigM=*/true) {} + explicit LexSimplexBase(const IntegerRelation &constraints) + : LexSimplexBase(constraints.getNumIds()) { + intersectIntegerRelation(constraints); + } + + /// Try to move the specified row to column orientation while preserving the + /// lexicopositivity of the basis transform. If this is not possible, return + /// failure. This only occurs when the constraints have no solution; the + /// tableau will be marked empty in such a case. + LogicalResult moveRowUnknownToColumn(unsigned row); + + /// Given a row that has a non-integer sample value, add an inequality such + /// that this fractional sample value is cut away from the polytope. The added + /// inequality will be such that no integer points are removed. + /// + /// Returns whether the cut constraint could be enforced, i.e. failure if the + /// cut made the polytope empty, and success if it didn't. Failure status + /// indicates that the polytope didn't have any integer points. + LogicalResult addCut(unsigned row); + + /// Undo the addition of the last constraint. This is only called while + /// rolling back. + void undoLastConstraint() final; + + /// Given two potential pivot columns for a row, return the one that results + /// in the lexicographically smallest sample vector. + unsigned getLexMinPivotColumn(unsigned row, unsigned colA, + unsigned colB) const; +}; + +class LexSimplex : public LexSimplexBase { +public: + explicit LexSimplex(unsigned nVar) : LexSimplexBase(nVar) {} + explicit LexSimplex(const IntegerRelation &constraints) + : LexSimplexBase(constraints) { + assert(constraints.getNumSymbolIds() == 0 && + "LexSimplex does not support symbols!"); + } + /// Return the lexicographically minimum rational solution to the constraints. MaybeOptimum> findRationalLexMin(); @@ -451,7 +484,7 @@ /// any integer sample, use Simplex::findIntegerSample as that is more robust. MaybeOptimum> findIntegerLexMin(); -protected: +private: /// Returns the current sample point, which may contain non-integer (rational) /// coordinates. Returns an empty optimum when the tableau is empty. /// @@ -460,19 +493,6 @@ /// or unbounded. MaybeOptimum> getRationalSample() const; - /// Given a row that has a non-integer sample value, add an inequality such - /// that this fractional sample value is cut away from the polytope. The added - /// inequality will be such that no integer points are removed. - /// - /// Returns whether the cut constraint could be enforced, i.e. failure if the - /// cut made the polytope empty, and success if it didn't. Failure status - /// indicates that the polytope didn't have any integer points. - LogicalResult addCut(unsigned row); - - /// Undo the addition of the last constraint. This is only called while - /// rolling back. - void undoLastConstraint() final; - /// Make the tableau configuration consistent. void restoreRationalConsistency(); @@ -491,12 +511,6 @@ /// in the lexicographically smallest sample vector. unsigned getLexMinPivotColumn(unsigned row, unsigned colA, unsigned colB) const; - - /// Try to move the specified row to column orientation while preserving the - /// lexicopositivity of the basis transform. If this is not possible, return - /// failure. This only occurs when the constraints have no solution; the - /// tableau will be marked empty in such a case. - LogicalResult moveRowUnknownToColumn(unsigned row); }; /// The Simplex class uses the Normal pivot rule and supports integer emptiness 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 @@ -169,7 +169,7 @@ return getRationalSample(); } -LogicalResult LexSimplex::addCut(unsigned row) { +LogicalResult LexSimplexBase::addCut(unsigned row) { int64_t denom = tableau(row, 0); addZeroRow(/*makeRestricted=*/true); tableau(nRow - 1, 0) = denom; @@ -307,7 +307,7 @@ // which is in contradiction to the fact that B.col(j) / B(i,j) must be // lexicographically smaller than B.col(k) / B(i,k), since it lexicographically // minimizes the change in sample value. -LogicalResult LexSimplex::moveRowUnknownToColumn(unsigned row) { +LogicalResult LexSimplexBase::moveRowUnknownToColumn(unsigned row) { Optional maybeColumn; for (unsigned col = 3; col < nCol; ++col) { if (tableau(row, col) <= 0) @@ -325,8 +325,8 @@ return success(); } -unsigned LexSimplex::getLexMinPivotColumn(unsigned row, unsigned colA, - unsigned colB) const { +unsigned LexSimplexBase::getLexMinPivotColumn(unsigned row, unsigned colA, + unsigned colB) const { // A pivot causes the following change. (in the diagram the matrix elements // are shown as rationals and there is no common denominator used) // @@ -735,7 +735,7 @@ // It's not valid to remove the constraint by deleting the column since this // would result in an invalid basis. -void LexSimplex::undoLastConstraint() { +void LexSimplexBase::undoLastConstraint() { if (con.back().orientation == Orientation::Column) { // When removing the last constraint during a rollback, we just need to find // any pivot at all, i.e., any row with non-zero coefficient for the @@ -1110,6 +1110,10 @@ return sample; } +void LexSimplexBase::addInequality(ArrayRef coeffs) { + addRow(coeffs, /*makeRestricted=*/true); +} + MaybeOptimum> LexSimplex::getRationalSample() const { if (empty) return OptimumKind::Empty;