From 4fa96b7eca73b6b235e22f18371dba8c20ed715a Mon Sep 17 00:00:00 2001 From: Arjun P Date: Thu, 16 Dec 2021 18:11:31 +0530 Subject: [PATCH] [MLIR] Simplex: split some basic functionality out into a SimplexBase class This is a purely mechanical patch moving some functionality out from the `Simplex` class out into a `SimplexBase` class. This pavees the way for a future patch adding support for lexicographic optimization with a class `LexSimplex`, which will inherit from `SimplexBase`. Inheriting directly from `Simplex` would bring many additional functions that would not work in `LexSimplex` because it operates slighty differently from `Simplex`. So We split out only the basic functionality it needs to inherit into `SimplexBase`. Reviewed By: Groverkss Differential Revision: https://reviews.llvm.org/D115831 --- mlir/include/mlir/Analysis/Presburger/Simplex.h | 187 +++++++++++++----------- mlir/lib/Analysis/Presburger/Simplex.cpp | 76 +++++----- 2 files changed, 140 insertions(+), 123 deletions(-) diff --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h b/mlir/include/mlir/Analysis/Presburger/Simplex.h index 87217cd..a04f0b0 100644 --- a/mlir/include/mlir/Analysis/Presburger/Simplex.h +++ b/mlir/include/mlir/Analysis/Presburger/Simplex.h @@ -29,7 +29,7 @@ namespace mlir { class GBRSimplex; -/// This class implements a version of the Simplex and Generalized Basis +/// The Simplex class implements a version of the Simplex and Generalized Basis /// Reduction algorithms, which can perform analysis of integer sets with affine /// inequalities and equalities. A Simplex can be constructed /// by specifying the dimensionality of the set. It supports adding affine @@ -41,8 +41,8 @@ class GBRSimplex; /// 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 +/// The implementation of the Simplex and SimplexBase classes, other than the +/// functionality for sampling, is based on the paper /// "Simplify: A Theorem Prover for Program Checking" /// by D. Detlefs, G. Nelson, J. B. Saxe. /// @@ -134,13 +134,19 @@ class GBRSimplex; /// /// Finding an integer sample is done with the Generalized Basis Reduction /// algorithm. See the documentation for findIntegerSample and reduceBasis. -class Simplex { +/// +/// The SimplexBase class contains some basic functionality. In the future, +/// lexicographic optimization will be supported by a class inheriting from +/// SimplexBase. Functionality that will not supported by that class is placed +/// in `Simplex`. + +class SimplexBase { public: enum class Direction { Up, Down }; - Simplex() = delete; - explicit Simplex(unsigned nVar); - explicit Simplex(const FlatAffineConstraints &constraints); + SimplexBase() = delete; + explicit SimplexBase(unsigned nVar); + explicit SimplexBase(const FlatAffineConstraints &constraints); /// Returns true if the tableau is empty (has conflicting constraints), /// false otherwise. @@ -177,50 +183,6 @@ public: /// Add all the constraints from the given FlatAffineConstraints. void intersectFlatAffineConstraints(const FlatAffineConstraints &fac); - /// 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. - /// - /// Returns a Fraction denoting the optimum, or a null value if no optimum - /// exists, i.e., if the expression is unbounded in this direction. - Optional computeRowOptimum(Direction direction, unsigned row); - - /// Compute the maximum or minimum value of the given expression, depending on - /// direction. Should not be called when the Simplex is empty. - /// - /// Returns a Fraction denoting the optimum, or a null value if no optimum - /// exists, i.e., if the expression is unbounded in this direction. - Optional computeOptimum(Direction direction, - ArrayRef coeffs); - - /// Returns whether the perpendicular of the specified constraint - /// is a direction along which the polytope is bounded. - bool isBoundedAlongConstraint(unsigned constraintIndex); - - /// 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); - - /// Returns true if the polytope is unbounded, i.e., extends to infinity in - /// some direction. Otherwise, returns false. - bool isUnbounded(); - - /// Make a tableau to represent a pair of points in the given tableaus, one in - /// tableau A and one in B. - static Simplex makeProduct(const Simplex &a, const Simplex &b); - /// Returns a rational sample point. This should not be called when Simplex is /// empty. SmallVector getRationalSample() const; @@ -229,27 +191,11 @@ public: /// None. Optional> getSamplePointIfIntegral() const; - /// Returns an integer sample point if one exists, or None - /// otherwise. This should only be called for bounded sets. - Optional> findIntegerSample(); - /// Print the tableau's internal state. void print(raw_ostream &os) const; void dump() const; - /// Check if the specified inequality already holds in the polytope. - bool isRedundantInequality(ArrayRef coeffs); - - /// Check if the specified equality already holds in the polytope. - bool isRedundantEquality(ArrayRef coeffs); - - /// Returns true if this Simplex's polytope is a rational subset of `fac`. - /// Otherwise, returns false. - bool isRationalSubsetOf(const FlatAffineConstraints &fac); - -private: - friend class GBRSimplex; - +protected: enum class Orientation { Row, Column }; /// An Unknown is either a variable or a constraint. It is always associated @@ -324,20 +270,6 @@ private: /// sample value, failure otherwise. LogicalResult restoreRow(Unknown &u); - /// Compute the maximum or minimum of the specified Unknown, depending on - /// direction. The specified unknown may be pivoted. If the unknown is - /// restricted, it will have a non-negative sample value on return. - /// Should not be called if the Simplex is empty. - /// - /// Returns a Fraction denoting the optimum, or a null value if no optimum - /// exists, i.e., if the expression is unbounded in this direction. - Optional computeOptimum(Direction direction, Unknown &u); - - /// 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, @@ -360,10 +292,6 @@ private: Optional findPivotRow(Optional skipRow, Direction direction, unsigned col) const; - /// Reduce the given basis, starting at the specified level, using general - /// basis reduction. - void reduceBasis(Matrix &basis, unsigned level); - /// The number of rows in the tableau. unsigned nRow; @@ -398,6 +326,93 @@ private: SmallVector con, var; }; +class Simplex : public SimplexBase { +public: + Simplex() = delete; + explicit Simplex(unsigned nVar) : SimplexBase(nVar) {} + explicit Simplex(const FlatAffineConstraints &constraints) + : SimplexBase(constraints) {} + + /// 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. + /// + /// Returns a Fraction denoting the optimum, or a null value if no optimum + /// exists, i.e., if the expression is unbounded in this direction. + Optional computeRowOptimum(Direction direction, unsigned row); + + /// Compute the maximum or minimum value of the given expression, depending on + /// direction. Should not be called when the Simplex is empty. + /// + /// Returns a Fraction denoting the optimum, or a null value if no optimum + /// exists, i.e., if the expression is unbounded in this direction. + Optional computeOptimum(Direction direction, + ArrayRef coeffs); + + /// Returns whether the perpendicular of the specified constraint is a + /// is a direction along which the polytope is bounded. + bool isBoundedAlongConstraint(unsigned constraintIndex); + + /// 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); + + /// Returns true if the polytope is unbounded, i.e., extends to infinity in + /// some direction. Otherwise, returns false. + bool isUnbounded(); + + /// Make a tableau to represent a pair of points in the given tableaus, one in + /// tableau A and one in B. + static Simplex makeProduct(const Simplex &a, const Simplex &b); + + /// Returns an integer sample point if one exists, or None + /// otherwise. This should only be called for bounded sets. + Optional> findIntegerSample(); + + /// Check if the specified inequality already holds in the polytope. + bool isRedundantInequality(ArrayRef coeffs); + + /// Check if the specified equality already holds in the polytope. + bool isRedundantEquality(ArrayRef coeffs); + + /// Returns true if this Simplex's polytope is a rational subset of `fac`. + /// Otherwise, returns false. + bool isRationalSubsetOf(const FlatAffineConstraints &fac); + +private: + friend class GBRSimplex; + + /// Compute the maximum or minimum of the specified Unknown, depending on + /// direction. The specified unknown may be pivoted. If the unknown is + /// restricted, it will have a non-negative sample value on return. + /// Should not be called if the Simplex is empty. + /// + /// Returns a Fraction denoting the optimum, or a null value if no optimum + /// exists, i.e., if the expression is unbounded in this direction. + Optional computeOptimum(Direction direction, Unknown &u); + + /// 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); + + /// Reduce the given basis, starting at the specified level, using general + /// basis reduction. + void reduceBasis(Matrix &basis, unsigned level); +}; + } // namespace mlir #endif // MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H diff --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp index a52712a..ed3232d 100644 --- a/mlir/lib/Analysis/Presburger/Simplex.cpp +++ b/mlir/lib/Analysis/Presburger/Simplex.cpp @@ -17,7 +17,7 @@ using Direction = Simplex::Direction; const int nullIndex = std::numeric_limits::max(); /// Construct a Simplex object with `nVar` variables. -Simplex::Simplex(unsigned nVar) +SimplexBase::SimplexBase(unsigned nVar) : nRow(0), nCol(2), nRedundant(0), tableau(0, 2 + nVar), empty(false) { colUnknown.push_back(nullIndex); colUnknown.push_back(nullIndex); @@ -28,8 +28,8 @@ Simplex::Simplex(unsigned nVar) } } -Simplex::Simplex(const FlatAffineConstraints &constraints) - : Simplex(constraints.getNumIds()) { +SimplexBase::SimplexBase(const FlatAffineConstraints &constraints) + : SimplexBase(constraints.getNumIds()) { for (unsigned i = 0, numIneqs = constraints.getNumInequalities(); i < numIneqs; ++i) addInequality(constraints.getInequality(i)); @@ -37,32 +37,32 @@ Simplex::Simplex(const FlatAffineConstraints &constraints) addEquality(constraints.getEquality(i)); } -const Simplex::Unknown &Simplex::unknownFromIndex(int index) const { +const Simplex::Unknown &SimplexBase::unknownFromIndex(int index) const { assert(index != nullIndex && "nullIndex passed to unknownFromIndex"); return index >= 0 ? var[index] : con[~index]; } -const Simplex::Unknown &Simplex::unknownFromColumn(unsigned col) const { +const Simplex::Unknown &SimplexBase::unknownFromColumn(unsigned col) const { assert(col < nCol && "Invalid column"); return unknownFromIndex(colUnknown[col]); } -const Simplex::Unknown &Simplex::unknownFromRow(unsigned row) const { +const Simplex::Unknown &SimplexBase::unknownFromRow(unsigned row) const { assert(row < nRow && "Invalid row"); return unknownFromIndex(rowUnknown[row]); } -Simplex::Unknown &Simplex::unknownFromIndex(int index) { +Simplex::Unknown &SimplexBase::unknownFromIndex(int index) { assert(index != nullIndex && "nullIndex passed to unknownFromIndex"); return index >= 0 ? var[index] : con[~index]; } -Simplex::Unknown &Simplex::unknownFromColumn(unsigned col) { +Simplex::Unknown &SimplexBase::unknownFromColumn(unsigned col) { assert(col < nCol && "Invalid column"); return unknownFromIndex(colUnknown[col]); } -Simplex::Unknown &Simplex::unknownFromRow(unsigned row) { +Simplex::Unknown &SimplexBase::unknownFromRow(unsigned row) { assert(row < nRow && "Invalid row"); return unknownFromIndex(rowUnknown[row]); } @@ -70,7 +70,7 @@ Simplex::Unknown &Simplex::unknownFromRow(unsigned row) { /// Add a new row to the tableau corresponding to the given constant term and /// list of coefficients. The coefficients are specified as a vector of /// (variable index, coefficient) pairs. -unsigned Simplex::addRow(ArrayRef coeffs) { +unsigned SimplexBase::addRow(ArrayRef coeffs) { assert(coeffs.size() == 1 + var.size() && "Incorrect number of coefficients!"); @@ -121,7 +121,7 @@ unsigned Simplex::addRow(ArrayRef coeffs) { /// Normalize the row by removing factors that are common between the /// denominator and all the numerator coefficients. -void Simplex::normalizeRow(unsigned row) { +void SimplexBase::normalizeRow(unsigned row) { int64_t gcd = 0; for (unsigned col = 0; col < nCol; ++col) { if (gcd == 1) @@ -155,8 +155,8 @@ Direction flippedDirection(Direction direction) { /// /// If multiple columns are valid, we break ties by considering a lexicographic /// ordering where we prefer unknowns with lower index. -Optional Simplex::findPivot(int row, - Direction direction) const { +Optional SimplexBase::findPivot(int row, + Direction direction) const { Optional col; for (unsigned j = 2; j < nCol; ++j) { int64_t elem = tableau(row, j); @@ -183,7 +183,7 @@ Optional Simplex::findPivot(int row, /// /// First we swap the index associated with the row and column. Then we update /// the unknowns to reflect their new position and orientation. -void Simplex::swapRowWithCol(unsigned row, unsigned col) { +void SimplexBase::swapRowWithCol(unsigned row, unsigned col) { std::swap(rowUnknown[row], colUnknown[col]); Unknown &uCol = unknownFromColumn(col); Unknown &uRow = unknownFromRow(row); @@ -193,7 +193,7 @@ void Simplex::swapRowWithCol(unsigned row, unsigned col) { uRow.pos = row; } -void Simplex::pivot(Pivot pair) { pivot(pair.row, pair.column); } +void SimplexBase::pivot(Pivot pair) { pivot(pair.row, pair.column); } /// Pivot pivotRow and pivotCol. /// @@ -220,7 +220,7 @@ void Simplex::pivot(Pivot pair) { pivot(pair.row, pair.column); } /// The pivot row transform is accomplished be swapping a with the pivot row's /// common denominator and negating the pivot row except for the pivot column /// element. -void Simplex::pivot(unsigned pivotRow, unsigned pivotCol) { +void SimplexBase::pivot(unsigned pivotRow, unsigned pivotCol) { assert(pivotCol >= 2 && "Refusing to pivot invalid column"); swapRowWithCol(pivotRow, pivotCol); @@ -261,7 +261,7 @@ void Simplex::pivot(unsigned pivotRow, unsigned pivotCol) { /// Perform pivots until the unknown has a non-negative sample value or until /// no more upward pivots can be performed. Return success if we were able to /// bring the row to a non-negative sample value, and failure otherwise. -LogicalResult Simplex::restoreRow(Unknown &u) { +LogicalResult SimplexBase::restoreRow(Unknown &u) { assert(u.orientation == Orientation::Row && "unknown should be in row position"); @@ -299,9 +299,9 @@ LogicalResult Simplex::restoreRow(Unknown &u) { /// 0 and hence saturates the bound it imposes. We break ties between rows that /// impose the same bound by considering a lexicographic ordering where we /// prefer unknowns with lower index value. -Optional Simplex::findPivotRow(Optional skipRow, - Direction direction, - unsigned col) const { +Optional SimplexBase::findPivotRow(Optional skipRow, + Direction direction, + unsigned col) const { Optional retRow; int64_t retElem, retConst; for (unsigned row = nRedundant; row < nRow; ++row) { @@ -334,9 +334,9 @@ Optional Simplex::findPivotRow(Optional skipRow, return retRow; } -bool Simplex::isEmpty() const { return empty; } +bool SimplexBase::isEmpty() const { return empty; } -void Simplex::swapRows(unsigned i, unsigned j) { +void SimplexBase::swapRows(unsigned i, unsigned j) { if (i == j) return; tableau.swapRows(i, j); @@ -345,7 +345,7 @@ void Simplex::swapRows(unsigned i, unsigned j) { unknownFromRow(j).pos = j; } -void Simplex::swapColumns(unsigned i, unsigned j) { +void SimplexBase::swapColumns(unsigned i, unsigned j) { assert(i < nCol && j < nCol && "Invalid columns provided!"); if (i == j) return; @@ -356,7 +356,7 @@ void Simplex::swapColumns(unsigned i, unsigned j) { } /// Mark this tableau empty and push an entry to the undo stack. -void Simplex::markEmpty() { +void SimplexBase::markEmpty() { // If the set is already empty, then we shouldn't add another UnmarkEmpty log // entry, since in that case the Simplex will be erroneously marked as // non-empty when rolling back past this point. @@ -373,7 +373,7 @@ void Simplex::markEmpty() { /// We add the inequality and mark it as restricted. We then try to make its /// sample value non-negative. If this is not possible, the tableau has become /// empty and we mark it as such. -void Simplex::addInequality(ArrayRef coeffs) { +void SimplexBase::addInequality(ArrayRef coeffs) { unsigned conIndex = addRow(coeffs); Unknown &u = con[conIndex]; u.restricted = true; @@ -388,7 +388,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) @@ -396,14 +396,14 @@ void Simplex::addEquality(ArrayRef coeffs) { addInequality(negatedCoeffs); } -unsigned Simplex::getNumVariables() const { return var.size(); } -unsigned Simplex::getNumConstraints() const { return con.size(); } +unsigned SimplexBase::getNumVariables() const { return var.size(); } +unsigned SimplexBase::getNumConstraints() const { return con.size(); } /// Return a snapshot of the current state. This is just the current size of the /// undo log. -unsigned Simplex::getSnapshot() const { return undoLog.size(); } +unsigned SimplexBase::getSnapshot() const { return undoLog.size(); } -void Simplex::undo(UndoLogEntry entry) { +void SimplexBase::undo(UndoLogEntry entry) { if (entry == UndoLogEntry::RemoveLastConstraint) { Unknown &constraint = con.back(); if (constraint.orientation == Orientation::Column) { @@ -480,14 +480,14 @@ void Simplex::undo(UndoLogEntry entry) { /// /// We undo all the log entries until the log size when the snapshot was taken /// is reached. -void Simplex::rollback(unsigned snapshot) { +void SimplexBase::rollback(unsigned snapshot) { while (undoLog.size() > snapshot) { undo(undoLog.back()); undoLog.pop_back(); } } -void Simplex::appendVariable(unsigned count) { +void SimplexBase::appendVariable(unsigned count) { if (count == 0) return; var.reserve(var.size() + count); @@ -503,7 +503,8 @@ void Simplex::appendVariable(unsigned count) { } /// Add all the constraints from the given FlatAffineConstraints. -void Simplex::intersectFlatAffineConstraints(const FlatAffineConstraints &fac) { +void SimplexBase::intersectFlatAffineConstraints( + const FlatAffineConstraints &fac) { assert(fac.getNumIds() == getNumVariables() && "FlatAffineConstraints must have same dimensionality as simplex"); for (unsigned i = 0, e = fac.getNumInequalities(); i < e; ++i) @@ -736,7 +737,7 @@ Simplex Simplex::makeProduct(const Simplex &a, const Simplex &b) { return result; } -SmallVector Simplex::getRationalSample() const { +SmallVector SimplexBase::getRationalSample() const { assert(!empty && "This should not be called when Simplex is empty."); SmallVector sample; @@ -756,7 +757,8 @@ SmallVector Simplex::getRationalSample() const { return sample; } -Optional> Simplex::getSamplePointIfIntegral() const { +Optional> +SimplexBase::getSamplePointIfIntegral() const { // If the tableau is empty, no sample point exists. if (empty) return {}; @@ -1246,7 +1248,7 @@ Simplex::computeIntegerBounds(ArrayRef coeffs) { return {minRoundedUp, maxRoundedDown}; } -void Simplex::print(raw_ostream &os) const { +void SimplexBase::print(raw_ostream &os) const { os << "rows = " << nRow << ", columns = " << nCol << "\n"; if (empty) os << "Simplex marked empty!\n"; @@ -1281,7 +1283,7 @@ void Simplex::print(raw_ostream &os) const { os << '\n'; } -void Simplex::dump() const { print(llvm::errs()); } +void SimplexBase::dump() const { print(llvm::errs()); } bool Simplex::isRationalSubsetOf(const FlatAffineConstraints &fac) { if (isEmpty()) -- 2.7.4