Simplex class using the lexicographic pivot rule. More...
#include "mlir/Analysis/Presburger/Simplex.h"
Inheritance diagram for mlir::presburger::LexSimplexBase:
Public Member Functions | |
| ~LexSimplexBase () override=default | |
| void | addInequality (ArrayRef< DynamicAPInt > coeffs) final |
| Add an inequality to the tableau. More... | |
| unsigned | getSnapshot () |
| Get a snapshot of the current state. This is used for rolling back. More... | |
| Public Member Functions inherited from mlir::presburger::SimplexBase | |
| SimplexBase ()=delete | |
| virtual | ~SimplexBase ()=default |
| bool | isEmpty () const |
| Returns true if the tableau is empty (has conflicting constraints), false otherwise. More... | |
| unsigned | getNumVariables () const |
| Returns the number of variables in the tableau. More... | |
| unsigned | getNumConstraints () const |
| Returns the number of constraints in the tableau. More... | |
| void | addEquality (ArrayRef< DynamicAPInt > coeffs) |
| Add an equality to the tableau. More... | |
| void | appendVariable (unsigned count=1) |
| Add new variables to the end of the list of variables. More... | |
| void | addDivisionVariable (ArrayRef< DynamicAPInt > coeffs, const DynamicAPInt &denom) |
Append a new variable to the simplex and constrain it such that its only integer value is the floor div of coeffs and denom. More... | |
| void | markEmpty () |
| Mark the tableau as being empty. More... | |
| unsigned | getSnapshot () const |
| Get a snapshot of the current state. More... | |
| unsigned | getSnapshotBasis () |
| Get a snapshot of the current state including the basis. More... | |
| void | rollback (unsigned snapshot) |
| Rollback to a snapshot. This invalidates all later snapshots. More... | |
| void | intersectIntegerRelation (const IntegerRelation &rel) |
| Add all the constraints from the given IntegerRelation. More... | |
| void | print (raw_ostream &os) const |
| Print the tableau's internal state. More... | |
| void | dump () const |
Protected Member Functions | |
| LexSimplexBase (unsigned nVar) | |
| LexSimplexBase (unsigned nVar, const llvm::SmallBitVector &isSymbol) | |
| LexSimplexBase (const IntegerRelation &constraints) | |
| LexSimplexBase (const IntegerRelation &constraints, const llvm::SmallBitVector &isSymbol) | |
| void | appendSymbol () |
| Add new symbolic variables to the end of the list of variables. More... | |
| LogicalResult | moveRowUnknownToColumn (unsigned row) |
| Try to move the specified row to column orientation while preserving the lexicopositivity of the basis transform. More... | |
| LogicalResult | addCut (unsigned row) |
| Given a row that has a non-integer sample value, add an inequality to cut away this fractional sample value from the polytope without removing any integer points. More... | |
| void | undoLastConstraint () final |
| Undo the addition of the last constraint. More... | |
| unsigned | getLexMinPivotColumn (unsigned row, unsigned colA, unsigned colB) const |
| Given two potential pivot columns for a row, return the one that results in the lexicographically smallest sample vector. More... | |
| Protected Member Functions inherited from mlir::presburger::SimplexBase | |
| SimplexBase (unsigned nVar, bool mustUseBigM) | |
| Construct a SimplexBase with the specified number of variables and fixed columns. More... | |
| SimplexBase (unsigned nVar, bool mustUseBigM, const llvm::SmallBitVector &isSymbol) | |
| std::optional< unsigned > | findAnyPivotRow (unsigned col) |
| Return any row that this column can be pivoted with, ignoring tableau consistency. More... | |
| void | swapRowWithCol (unsigned row, unsigned col) |
| Swap the row with the column in the tableau's data structures but not the tableau itself. More... | |
| void | pivot (unsigned row, unsigned col) |
| Pivot the row with the column. More... | |
| void | pivot (Pivot pair) |
| const Unknown & | unknownFromIndex (int index) const |
| Returns the unknown associated with index. More... | |
| const Unknown & | unknownFromColumn (unsigned col) const |
| Returns the unknown associated with col. More... | |
| const Unknown & | unknownFromRow (unsigned row) const |
| Returns the unknown associated with row. More... | |
| Unknown & | unknownFromIndex (int index) |
| Returns the unknown associated with index. More... | |
| Unknown & | unknownFromColumn (unsigned col) |
| Returns the unknown associated with col. More... | |
| Unknown & | unknownFromRow (unsigned row) |
| Returns the unknown associated with row. More... | |
| unsigned | addZeroRow (bool makeRestricted=false) |
| Add a new row to the tableau and the associated data structures. More... | |
| unsigned | addRow (ArrayRef< DynamicAPInt > coeffs, bool makeRestricted=false) |
| Add a new row to the tableau and the associated data structures. More... | |
| void | swapRows (unsigned i, unsigned j) |
| Swap the two rows/columns in the tableau and associated data structures. More... | |
| void | swapColumns (unsigned i, unsigned j) |
| void | removeLastConstraintRowOrientation () |
| Remove the last constraint, which must be in row orientation. More... | |
| void | undo (UndoLogEntry entry) |
| Undo the operation represented by the log entry. More... | |
| unsigned | getNumFixedCols () const |
| 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. More... | |
| unsigned | getNumRows () const |
| unsigned | getNumColumns () const |
Additional Inherited Members | |
| Protected Types inherited from mlir::presburger::SimplexBase | |
| enum class | Orientation { Row , Column } |
| enum class | UndoLogEntry { RemoveLastConstraint , RemoveLastVariable , UnmarkEmpty , UnmarkLastRedundant , RestoreBasis } |
| Enum to denote operations that need to be undone during rollback. More... | |
| Protected Attributes inherited from mlir::presburger::SimplexBase | |
| bool | usingBigM |
| Stores whether or not a big M column is present in the tableau. More... | |
| unsigned | nRedundant |
| The number of redundant rows in the tableau. More... | |
| unsigned | nSymbol |
| The number of parameters. More... | |
| IntMatrix | tableau |
| The matrix representing the tableau. More... | |
| bool | empty |
| This is true if the tableau has been detected to be empty, false otherwise. More... | |
| SmallVector< UndoLogEntry, 8 > | undoLog |
| Holds a log of operations, used for rolling back to a previous state. More... | |
| SmallVector< SmallVector< int, 8 >, 8 > | savedBases |
| Holds a vector of bases. More... | |
| SmallVector< int, 8 > | rowUnknown |
| These hold the indexes of the unknown at a given row or column position. More... | |
| SmallVector< int, 8 > | colUnknown |
| SmallVector< Unknown, 8 > | con |
| These hold information about each unknown. More... | |
| SmallVector< Unknown, 8 > | var |
Detailed Description
Simplex class using the lexicographic pivot rule.
Used for lexicographic optimization. The implementation of this class is based on the paper "Parametric Integer Programming" by Paul Feautrier.
This does not directly support negative-valued variables, so it uses the big M parameter trick to make all the variables non-negative. Basically we introduce an artifical variable M that is considered to have a value of +infinity and instead of the variables x, y, z, we internally use variables M + x, M + y, M + z, which are now guaranteed to be non-negative. See the documentation for SimplexBase for more details. M is also considered to be an integer that is divisible by everything.
The whole algorithm is performed with M treated as a symbol; it is just considered to be infinite throughout and it never appears in the final outputs. We will deal with sample values throughout that may in general be some affine expression involving M, like pM + q or aM + b. We can compare these with each other. They have a total order:
aM + b < pM + q iff a < p or (a == p and b < q). In particular, aM + b < 0 iff a < 0 or (a == 0 and b < 0).
When performing symbolic optimization, sample values will be affine expressions in M and the symbols. For example, we could have sample values aM + bS + c and pM + qS + r, where S is a symbol. Now we have aM + bS + c < pM + qS + r iff (a < p) or (a == p and bS + c < qS + r). bS + c < qS + r can be always true, always false, or neither, depending on the set of values S can take. The symbols are always stored in columns [3, 3 + nSymbols). For more details, see the documentation for SymbolicLexSimplex.
Initially all the constraints to be added are added as rows, with no attempt to keep the tableau consistent. Pivots are only performed when some query is made, such as a call to getRationalLexMin. Care is taken to always maintain a lexicopositive basis transform, explained below.
Let the variables be x = (x_1, ... x_n). Let the symbols be s = (s_1, ... s_m). Let the basis unknowns at a particular point be y = (y_1, ... y_n). We know that x = A*y + T*s + b for some n x n matrix A, n x m matrix s, and n x 1 column vector b. We want every column in A to be lexicopositive, i.e., have at least one non-zero element, with the first such element being positive. This property is preserved throughout the operation of LexSimplexBase. Note that on construction, the basis transform A is the identity matrix and so every column is lexicopositive. Note that for LexSimplexBase, for the tableau to be consistent we must have non-negative sample values not only for the constraints but also for the variables. So if the tableau is consistent then x >= 0 and y >= 0, by which we mean every element in these vectors is non-negative. (note that this is a different concept from lexicopositivity!)
Constructor & Destructor Documentation
◆ ~LexSimplexBase()
|
overridedefault |
◆ LexSimplexBase() [1/4]
|
inlineprotected |
◆ LexSimplexBase() [2/4]
|
inlineprotected |
◆ LexSimplexBase() [3/4]
|
inlineexplicitprotected |
Definition at line 431 of file Simplex.h.
References mlir::presburger::SimplexBase::intersectIntegerRelation().
◆ LexSimplexBase() [4/4]
|
inlineexplicitprotected |
Definition at line 435 of file Simplex.h.
References mlir::presburger::SimplexBase::intersectIntegerRelation().
Member Function Documentation
◆ addCut()
|
protected |
Given a row that has a non-integer sample value, add an inequality to cut away this fractional sample value from the polytope without removing any integer points.
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 integer lexmin, if one existed, remains the same on return.
This assumes that the symbolic part of the sample is integral, i.e., if the symbolic sample is (c + aM + b_1*s_1 + ... b_n*s_n)/d, where s_1, ... s_n are symbols, this assumes that (b_1*s_1 + ... + b_n*s_n)/s is integral.
Return failure if the tableau became empty, and success if it didn't. Failure status indicates that the polytope was integer empty.
The added inequality will be such that no integer points are removed. i.e., the integer lexmin, if it exists, is the same with and without this constraint.
Let the row be (c + coeffM*M + a_1*s_1 + ... + a_m*s_m + b_1*y_1 + ... + b_n*y_n)/d, where s_1, ... s_m are the symbols and y_1, ... y_n are the other basis unknowns.
For this to be an integer, we want coeffM*M + a_1*s_1 + ... + a_m*s_m + b_1*y_1 + ... + b_n*y_n = -c (mod d) Note that this constraint must always hold, independent of the basis, becuse the row unknown's value always equals this expression, even if we later compute the sample value from a different expression based on a different basis.
Let us assume that M has a factor of d in it. Imposing this constraint on M does not in any way hinder us from finding a value of M that is big enough. Moreover, this function is only called when the symbolic part of the sample, a_1*s_1 + ... + a_m*s_m, is known to be an integer.
Also, we can safely reduce the coefficients modulo d, so we have:
(b_1d)y_1 + ... + (b_nd)y_n = (-cd) + k*d for some integer k
Note that all coefficient modulos here are non-negative. Also, all the unknowns are non-negative here as both constraints and variables are non-negative in LexSimplexBase. (We used the big M trick to make the variables non-negative). Therefore, the LHS here is non-negative. Since 0 <= (-cd) < d, k is the quotient of dividing the LHS by d and is therefore non-negative as well.
So we have ((b_1d)y_1 + ... + (b_nd)y_n - (-cd))/d >= 0.
The constraint is violated when added (it would be useless otherwise) so we immediately try to move it to a column.
Definition at line 281 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addZeroRow(), mlir::presburger::SimplexBase::getNumColumns(), moveRowUnknownToColumn(), mlir::presburger::SimplexBase::nSymbol, and mlir::presburger::SimplexBase::tableau.
Referenced by mlir::presburger::LexSimplex::findIntegerLexMin().
◆ addInequality()
|
finalvirtual |
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.
This just adds the inequality to the tableau and does not try to create a consistent tableau configuration.
Implements mlir::presburger::SimplexBase.
Definition at line 1592 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addRow().
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), and mlir::presburger::LexSimplex::isSeparateInequality().
◆ appendSymbol()
|
protected |
Add new symbolic variables to the end of the list of variables.
Definition at line 365 of file Simplex.cpp.
References mlir::presburger::SimplexBase::appendVariable(), mlir::presburger::SimplexBase::getNumColumns(), mlir::presburger::SimplexBase::nSymbol, mlir::presburger::SimplexBase::swapColumns(), and mlir::presburger::SimplexBase::var.
◆ getLexMinPivotColumn()
|
protected |
Given two potential pivot columns for a row, return the one that results in the lexicographically smallest sample vector.
The row's sample value must be negative. If symbols are involved, the sample value must be negative for all possible assignments to the symbols.
Definition at line 793 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Column, mlir::presburger::SimplexBase::tableau, and mlir::presburger::SimplexBase::var.
Referenced by moveRowUnknownToColumn().
◆ getSnapshot()
|
inline |
Get a snapshot of the current state. This is used for rolling back.
Definition at line 425 of file Simplex.h.
References mlir::presburger::SimplexBase::getSnapshotBasis().
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin().
◆ moveRowUnknownToColumn()
|
protected |
Try to move the specified row to column orientation while preserving the lexicopositivity of the basis transform.
The row must have a non-positive sample value. If this is not possible, return failure. This occurs when the constraints have no solution or the sample value is zero.
Definition at line 777 of file Simplex.cpp.
References getLexMinPivotColumn(), mlir::presburger::SimplexBase::getNumColumns(), mlir::presburger::SimplexBase::nSymbol, mlir::presburger::SimplexBase::pivot(), and mlir::presburger::SimplexBase::tableau.
Referenced by addCut(), and mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin().
◆ undoLastConstraint()
|
finalprotectedvirtual |
Undo the addition of the last constraint.
This is only called while rolling back.
Implements mlir::presburger::SimplexBase.
Definition at line 1213 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Column, mlir::presburger::SimplexBase::con, mlir::presburger::SimplexBase::findAnyPivotRow(), mlir::presburger::SimplexBase::pivot(), and mlir::presburger::SimplexBase::removeLastConstraintRowOrientation().
The documentation for this class was generated from the following files:
- include/mlir/Analysis/Presburger/Simplex.h
- lib/Analysis/Presburger/Simplex.cpp
