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. More...
#include "mlir/Analysis/Presburger/Simplex.h"
Inheritance diagram for mlir::presburger::SimplexBase:
Classes | |
| struct | Pivot |
| struct | Unknown |
| An Unknown is either a variable or a constraint. More... | |
Public Member Functions | |
| SimplexBase ()=delete | |
| virtual | ~SimplexBase ()=default |
| bool | isEmpty () const |
| Returns true if the tableau is empty (has conflicting constraints), false otherwise. More... | |
| virtual void | addInequality (ArrayRef< DynamicAPInt > coeffs)=0 |
| Add an inequality to the tableau. 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 Types | |
| 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 Member Functions | |
| 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) |
| virtual void | undoLastConstraint ()=0 |
| Undo the addition of the last constraint. More... | |
| 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 |
Protected Attributes | |
| 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
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 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. 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. The LexSimplex class provides support for computing the lexicographic minimum of an IntegerRelation. The SymbolicLexOpt class provides support for computing symbolic lexicographic minimums. All of these classes can be constructed from an IntegerRelation, and all inherit common functionality from SimplexBase.
The implementations of the Simplex and SimplexBase classes, other than the functionality for obtaining an integer sample, are based on the paper "Simplify: A Theorem Prover for Program Checking" by D. Detlefs, G. Nelson, J. B. Saxe.
We define variables, constraints, and unknowns. Consider the example of a two-dimensional set defined by 1 + 2x + 3y >= 0 and 2x - 3y >= 0. Here, x, y, are variables while 1 + 2x + 3y >= 0, 2x - 3y >= 0 are constraints. Unknowns are either variables or constraints, i.e., x, y, 1 + 2x + 3y >= 0, 2x - 3y >= 0 are all unknowns.
The implementation involves a matrix called a tableau, which can be thought of as a 2D matrix of rational numbers having number of rows equal to the number of constraints and number of columns equal to one plus the number of variables. In our implementation, instead of storing rational numbers, we store a common denominator for each row, so it is in fact a matrix of integers with number of rows equal to number of constraints and number of columns equal to two plus the number of variables. For example, instead of storing a row of three rationals [1/2, 2/3, 3], we would store [6, 3, 4, 18] since 3/6 = 1/2, 4/6 = 2/3, and 18/6 = 3.
Every row and column except the first and second columns is associated with an unknown and every unknown is associated with a row or column. An unknown associated with a row or column is said to be in row or column orientation respectively. As described above, the first column is the common denominator. The second column represents the constant term, explained in more detail below. These two are fixed columns; they always retain their position as the first and second columns. Additionally, LexSimplexBase stores a so-call big M parameter (explained below) in the third column, so LexSimplexBase has three fixed columns. Finally, SymbolicLexSimplex has nSymbol variables designated as symbols. These occupy the next nSymbol columns, viz. the columns [3, 3 + nSymbol). For more information on symbols, see LexSimplexBase and SymbolicLexSimplex.
LexSimplexBase does not directly support variables which can be negative, so we introduce the so-called big M parameter, an artificial variable that is considered to have an arbitrarily large value. We then transform the variables, say x, y, z, ... to M, M + x, M + y, M + z. Since M has been added to these variables, they are now known to have non-negative values. For more details, see the documentation for LexSimplexBase. The big M parameter is not considered a real unknown and is not stored in the var data structure; rather the tableau just has an extra fixed column for it just like the constant term.
The vectors var and con store information about the variables and constraints respectively, namely, whether they are in row or column position, which row or column they are associated with, and whether they correspond to a variable or a constraint.
An unknown is addressed by its index. If the index i is non-negative, then the variable var[i] is being addressed. If the index i is negative, then the constraint con[~i] is being addressed. Effectively this maps 0 -> var[0], 1 -> var[1], -1 -> con[0], -2 -> con[1], etc. rowUnknown[r] and colUnknown[c] are the indexes of the unknowns associated with row r and column c, respectively.
The unknowns in column position are together called the basis. Initially the basis is the set of variables – in our example above, the initial basis is x, y.
The unknowns in row position are represented in terms of the basis unknowns. If the basis unknowns are u_1, u_2, ... u_m, and a row in the tableau is d, c, a_1, a_2, ... a_m, this represents the unknown for that row as (c + a_1*u_1 + a_2*u_2 + ... + a_m*u_m)/d. In our running example, if the basis is the initial basis of x, y, then the constraint 1 + 2x + 3y >= 0 would be represented by the row [1, 1, 2, 3].
The association of unknowns to rows and columns can be changed by a process called pivoting, where a row unknown and a column unknown exchange places and the remaining row variables' representation is changed accordingly by eliminating the old column unknown in favour of the new column unknown. If we had pivoted the column for x with the row for 2x - 3y >= 0, the new row for x would be [2, 1, 3] since x = (1*(2x - 3y) + 3*y)/2. See the documentation for the pivot member function for details.
The association of unknowns to rows and columns is called the tableau configuration. The sample value of an unknown in a particular tableau configuration is its value if all the column unknowns were set to zero. Concretely, for unknowns in column position the sample value is zero; when the big M parameter is not used, for unknowns in row position the sample value is the constant term divided by the common denominator. When the big M parameter is used, if d is the denominator, p is the big M coefficient, and c is the constant term, then the sample value is (p*M + c)/d. Since M is considered to be positive infinity, this is positive (negative) infinity when p is positive or negative, and c/d when p is zero.
The tableau configuration is called consistent if the sample value of all restricted unknowns is non-negative. Initially there are no constraints, and the tableau is consistent. When a new constraint is added, its sample value in the current tableau configuration may be negative. In that case, we try to find a series of pivots to bring us to a consistent tableau configuration, i.e. we try to make the new constraint's sample value non-negative without making that of any other constraints negative. (See findPivot and findPivotRow for details.) If this is not possible, then the set of constraints is mutually contradictory and the tableau is marked empty, which means the set of constraints has no solution.
This SimplexBase class also supports taking snapshots of the current state and rolling back to prior snapshots. This works by maintaining an undo log of operations. Snapshots are just pointers to a particular location in the log, and rolling back to a snapshot is done by reverting each log entry's operation from the end until we reach the snapshot's location. SimplexBase also supports taking a snapshot including the exact set of basis unknowns; if this functionality is used, then on rolling back the exact basis will also be restored. This is used by LexSimplexBase because the lex algorithm, unlike Simplex, is sensitive to the exact basis used at a point.
Member Enumeration Documentation
◆ Orientation
|
strongprotected |
◆ UndoLogEntry
|
strongprotected |
Constructor & Destructor Documentation
◆ SimplexBase() [1/3]
|
delete |
◆ ~SimplexBase()
|
virtualdefault |
◆ SimplexBase() [2/3]
|
protected |
Construct a SimplexBase with the specified number of variables and fixed columns.
The first overload should be used when there are nosymbols. With the second overload, the specified range of vars will be marked as symbols. With the third overload, isSymbol is a bitmask denoting which vars are symbols. The size of isSymbol must be nVar.
For example, Simplex uses two fixed columns: the denominator and the constant term, whereas LexSimplex has an extra fixed column for the so-called big M parameter. For more information see the documentation for LexSimplex.
Definition at line 50 of file Simplex.cpp.
References Column, colUnknown, getNumFixedCols(), nullIndex, and var.
◆ SimplexBase() [3/3]
|
protected |
Definition at line 63 of file Simplex.cpp.
References getNumFixedCols(), nSymbol, swapColumns(), and var.
Member Function Documentation
◆ addDivisionVariable()
| void SimplexBase::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.
We add the usual floor division constraints: 0 <= coeffs - denom*q <= denom - 1, where q is the new division variable.
denom must be positive.
This constrains the remainder coeffs - denom*q to be in the range [0, denom - 1], which fixes the integer value of the quotient q.
Definition at line 1304 of file Simplex.cpp.
References addInequality(), and appendVariable().
◆ addEquality()
| void SimplexBase::addEquality | ( | ArrayRef< DynamicAPInt > | coeffs | ) |
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.
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.
We simply add two opposing inequalities, which force the expression to be zero.
Definition at line 1123 of file Simplex.cpp.
References addInequality().
Referenced by mlir::presburger::Simplex::findIntegerSample(), and intersectIntegerRelation().
◆ addInequality()
|
pure virtual |
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.
Implemented in mlir::presburger::Simplex, and mlir::presburger::LexSimplexBase.
Referenced by addDivisionVariable(), addEquality(), and intersectIntegerRelation().
◆ addRow()
|
protected |
Add a new row to the tableau and the associated data structures.
Add a new row to the tableau corresponding to the given constant term and list of coefficients.
The new row is considered to be a constraint; the new Unknown lives in con.
Returns the index of the new Unknown in con.
The coefficients are specified as a vector of (variable index, coefficient) pairs.
Definition at line 121 of file Simplex.cpp.
References addZeroRow(), Column, con, getNumColumns(), getNumFixedCols(), mlir::presburger::IntMatrix::normalizeRow(), tableau, usingBigM, and var.
Referenced by mlir::presburger::LexSimplexBase::addInequality(), mlir::presburger::Simplex::addInequality(), and mlir::presburger::Simplex::computeOptimum().
◆ addZeroRow()
|
protected |
Add a new row to the tableau and the associated data structures.
The row is initialized to zero. Returns the index of the added row.
Definition at line 107 of file Simplex.cpp.
References mlir::presburger::Matrix< T >::appendExtraRow(), con, getNumRows(), RemoveLastConstraint, Row, rowUnknown, tableau, and undoLog.
Referenced by mlir::presburger::LexSimplexBase::addCut(), and addRow().
◆ appendVariable()
| void SimplexBase::appendVariable | ( | unsigned | count = 1 | ) |
Add new variables to the end of the list of variables.
Definition at line 1321 of file Simplex.cpp.
References Column, colUnknown, getNumColumns(), RemoveLastVariable, mlir::presburger::Matrix< T >::resizeHorizontally(), tableau, undoLog, and var.
Referenced by addDivisionVariable(), mlir::presburger::LexSimplexBase::appendSymbol(), and getSetDifference().
◆ dump()
| void SimplexBase::dump | ( | ) | const |
Definition at line 2171 of file Simplex.cpp.
References print().
◆ findAnyPivotRow()
|
protected |
Return any row that this column can be pivoted with, ignoring tableau consistency.
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.
Definition at line 1175 of file Simplex.cpp.
References getNumRows(), nRedundant, and tableau.
Referenced by mlir::presburger::LexSimplexBase::undoLastConstraint().
◆ getNumColumns()
|
inlineprotected |
Definition at line 323 of file Simplex.h.
References mlir::presburger::Matrix< T >::getNumColumns(), and tableau.
Referenced by mlir::presburger::LexSimplexBase::addCut(), addRow(), mlir::presburger::LexSimplexBase::appendSymbol(), appendVariable(), mlir::presburger::Simplex::makeProduct(), mlir::presburger::LexSimplexBase::moveRowUnknownToColumn(), pivot(), print(), swapColumns(), undo(), and unknownFromColumn().
◆ getNumConstraints()
| unsigned SimplexBase::getNumConstraints | ( | ) | const |
Returns the number of constraints in the tableau.
Definition at line 1133 of file Simplex.cpp.
References con.
Referenced by getSetDifference(), and mlir::presburger::Simplex::makeProduct().
◆ getNumFixedCols()
|
inlineprotected |
◆ getNumRows()
|
inlineprotected |
Definition at line 322 of file Simplex.h.
References mlir::presburger::Matrix< T >::getNumRows(), and tableau.
Referenced by addZeroRow(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), findAnyPivotRow(), mlir::presburger::Simplex::makeProduct(), pivot(), print(), removeLastConstraintRowOrientation(), and unknownFromRow().
◆ getNumVariables()
| unsigned SimplexBase::getNumVariables | ( | ) | const |
Returns the number of variables in the tableau.
Definition at line 1132 of file Simplex.cpp.
References var.
Referenced by intersectIntegerRelation(), and mlir::presburger::Simplex::makeProduct().
◆ getSnapshot()
| unsigned SimplexBase::getSnapshot | ( | ) | const |
Get a snapshot of the current state.
Return a snapshot of the current state.
This is used for rolling back. The same basis will not necessarily be restored on rolling back. The snapshot only captures the set of variables and constraints present in the Simplex.
This is just the current size of the undo log.
Definition at line 1137 of file Simplex.cpp.
References undoLog.
Referenced by mlir::presburger::Simplex::findIntegerSample(), getSetDifference(), and mlir::presburger::SimplexRollbackScopeExit::SimplexRollbackScopeExit().
◆ getSnapshotBasis()
| unsigned SimplexBase::getSnapshotBasis | ( | ) |
Get a snapshot of the current state including the basis.
When rolling back, the exact basis will be restored.
Definition at line 1139 of file Simplex.cpp.
References colUnknown, nullIndex, RestoreBasis, savedBases, and undoLog.
Referenced by mlir::presburger::LexSimplexBase::getSnapshot().
◆ intersectIntegerRelation()
| void SimplexBase::intersectIntegerRelation | ( | const IntegerRelation & | rel | ) |
Add all the constraints from the given IntegerRelation.
Definition at line 1336 of file Simplex.cpp.
References addEquality(), addInequality(), mlir::presburger::IntegerRelation::getEquality(), mlir::presburger::IntegerRelation::getInequality(), mlir::presburger::IntegerRelation::getNumEqualities(), mlir::presburger::IntegerRelation::getNumInequalities(), getNumVariables(), and mlir::presburger::IntegerRelation::getNumVars().
Referenced by getSetDifference(), mlir::presburger::LexSimplexBase::LexSimplexBase(), and mlir::presburger::Simplex::Simplex().
◆ isEmpty()
| bool SimplexBase::isEmpty | ( | ) | const |
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
Definition at line 1070 of file Simplex.cpp.
References empty.
Referenced by mlir::presburger::IntegerRelation::computeVolume(), mlir::presburger::IntegerRelation::findIntegerSample(), mlir::presburger::IntegerRelation::getBoundedDirections(), getSetDifference(), mlir::presburger::Simplex::isFlatAlong(), mlir::presburger::Simplex::isRationalSubsetOf(), and mlir::presburger::SetCoalescer::SetCoalescer().
◆ markEmpty()
| void SimplexBase::markEmpty | ( | ) |
Mark the tableau as being empty.
Mark this tableau empty and push an entry to the undo stack.
Definition at line 1093 of file Simplex.cpp.
References empty, undoLog, and UnmarkEmpty.
Referenced by mlir::presburger::Simplex::addInequality(), and mlir::presburger::LexSimplex::findRationalLexMin().
◆ pivot() [1/2]
|
protected |
Definition at line 924 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Pivot::column, pivot(), and mlir::presburger::SimplexBase::Pivot::row.
◆ pivot() [2/2]
|
protected |
Pivot the row with the column.
Pivot pivotRow and pivotCol.
Let R be the pivot row unknown and let C be the pivot col unknown. Since initially R = a*C + sum b_i * X_i (where the sum is over the other column's unknowns, x_i) C = (R - (sum b_i * X_i))/a
Let u be some other row unknown. u = c*C + sum d_i * X_i So u = c*(R - sum b_i * X_i)/a + sum d_i * X_i
This results in the following transform: pivot col other col pivot col other col pivot row a b -> pivot row 1/a -b/a other row c d other row c/a d - bc/a
Taking into account the common denominators p and q:
pivot col other col pivot col other col
pivot row a/p b/p -> pivot row p/a -b/a other row c/q d/q other row cp/aq (da - bc)/aq
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.
Definition at line 951 of file Simplex.cpp.
References getNumColumns(), getNumFixedCols(), getNumRows(), mlir::presburger::IntMatrix::normalizeRow(), swapRowWithCol(), tableau, and unknownFromColumn().
Referenced by mlir::presburger::Simplex::computeRowOptimum(), mlir::presburger::Simplex::detectRedundant(), mlir::presburger::LexSimplexBase::moveRowUnknownToColumn(), pivot(), undo(), and mlir::presburger::LexSimplexBase::undoLastConstraint().
◆ print()
| void SimplexBase::print | ( | raw_ostream & | os | ) | const |
Print the tableau's internal state.
Definition at line 2129 of file Simplex.cpp.
References colUnknown, con, empty, getNumColumns(), getNumRows(), rowUnknown, tableau, and var.
Referenced by dump().
◆ removeLastConstraintRowOrientation()
|
protected |
Remove the last constraint, which must be in row orientation.
Definition at line 1152 of file Simplex.cpp.
References con, getNumRows(), mlir::presburger::Matrix< T >::resizeVertically(), Row, rowUnknown, swapRows(), and tableau.
Referenced by mlir::presburger::LexSimplexBase::undoLastConstraint().
◆ rollback()
| void SimplexBase::rollback | ( | unsigned | snapshot | ) |
Rollback to a snapshot. This invalidates all later snapshots.
Rollback to the specified snapshot.
We undo all the log entries until the log size when the snapshot was taken is reached.
Definition at line 1291 of file Simplex.cpp.
References undo(), and undoLog.
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::findIntegerSample(), and getSetDifference().
◆ swapColumns()
|
protected |
Definition at line 1081 of file Simplex.cpp.
References colUnknown, getNumColumns(), mlir::presburger::SimplexBase::Unknown::pos, mlir::presburger::Matrix< T >::swapColumns(), tableau, and unknownFromColumn().
Referenced by mlir::presburger::LexSimplexBase::appendSymbol(), SimplexBase(), and undo().
◆ swapRows()
|
protected |
Swap the two rows/columns in the tableau and associated data structures.
Definition at line 1072 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Unknown::pos, rowUnknown, mlir::presburger::Matrix< T >::swapRows(), tableau, and unknownFromRow().
Referenced by removeLastConstraintRowOrientation().
◆ swapRowWithCol()
|
protected |
Swap the row with the column in the tableau's data structures but not the tableau itself.
Swap the associated unknowns for the row and the column.
This is used by pivot.
First we swap the index associated with the row and column. Then we update the unknowns to reflect their new position and orientation.
Definition at line 914 of file Simplex.cpp.
References Column, colUnknown, mlir::presburger::SimplexBase::Unknown::orientation, mlir::presburger::SimplexBase::Unknown::pos, Row, rowUnknown, unknownFromColumn(), and unknownFromRow().
Referenced by pivot().
◆ undo()
|
protected |
Undo the operation represented by the log entry.
Definition at line 1229 of file Simplex.cpp.
References Column, colUnknown, empty, getNumColumns(), getNumFixedCols(), nRedundant, nSymbol, nullIndex, mlir::presburger::SimplexBase::Unknown::orientation, pivot(), mlir::presburger::SimplexBase::Unknown::pos, RemoveLastConstraint, RemoveLastVariable, mlir::presburger::Matrix< T >::resizeHorizontally(), RestoreBasis, savedBases, swapColumns(), tableau, undoLastConstraint(), unknownFromIndex(), UnmarkEmpty, UnmarkLastRedundant, and var.
Referenced by rollback().
◆ undoLastConstraint()
|
protectedpure virtual |
Undo the addition of the last constraint.
This will only be called from undo, when rolling back.
Implemented in mlir::presburger::LexSimplexBase.
Referenced by undo().
◆ unknownFromColumn() [1/2]
|
protected |
Returns the unknown associated with col.
Definition at line 97 of file Simplex.cpp.
References colUnknown, getNumColumns(), and unknownFromIndex().
◆ unknownFromColumn() [2/2]
|
protected |
Returns the unknown associated with col.
Definition at line 82 of file Simplex.cpp.
References colUnknown, getNumColumns(), and unknownFromIndex().
Referenced by pivot(), swapColumns(), and swapRowWithCol().
◆ unknownFromIndex() [1/2]
|
protected |
Returns the unknown associated with index.
Definition at line 92 of file Simplex.cpp.
◆ unknownFromIndex() [2/2]
|
protected |
Returns the unknown associated with index.
Definition at line 77 of file Simplex.cpp.
References con, nullIndex, and var.
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::makeProduct(), undo(), unknownFromColumn(), and unknownFromRow().
◆ unknownFromRow() [1/2]
|
protected |
Returns the unknown associated with row.
Definition at line 102 of file Simplex.cpp.
References getNumRows(), rowUnknown, and unknownFromIndex().
◆ unknownFromRow() [2/2]
|
protected |
Returns the unknown associated with row.
Definition at line 87 of file Simplex.cpp.
References getNumRows(), rowUnknown, and unknownFromIndex().
Referenced by swapRows(), and swapRowWithCol().
Member Data Documentation
◆ colUnknown
|
protected |
Definition at line 358 of file Simplex.h.
Referenced by appendVariable(), getSnapshotBasis(), mlir::presburger::Simplex::makeProduct(), print(), SimplexBase(), swapColumns(), swapRowWithCol(), undo(), and unknownFromColumn().
◆ con
|
protected |
These hold information about each unknown.
Definition at line 361 of file Simplex.h.
Referenced by mlir::presburger::Simplex::addInequality(), addRow(), addZeroRow(), mlir::presburger::Simplex::computeOptimum(), mlir::presburger::Simplex::detectRedundant(), getNumConstraints(), mlir::presburger::Simplex::isBoundedAlongConstraint(), mlir::presburger::Simplex::isMarkedRedundant(), mlir::presburger::Simplex::makeProduct(), print(), removeLastConstraintRowOrientation(), mlir::presburger::LexSimplexBase::undoLastConstraint(), and unknownFromIndex().
◆ empty
|
protected |
This is true if the tableau has been detected to be empty, false otherwise.
Definition at line 341 of file Simplex.h.
Referenced by mlir::presburger::Simplex::computeOptimum(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::detectRedundant(), mlir::presburger::Simplex::findIntegerSample(), mlir::presburger::Simplex::getRationalSample(), mlir::presburger::Simplex::getSamplePointIfIntegral(), mlir::presburger::Simplex::isBoundedAlongConstraint(), isEmpty(), mlir::presburger::Simplex::isRedundantEquality(), mlir::presburger::Simplex::isRedundantInequality(), mlir::presburger::Simplex::isUnbounded(), mlir::presburger::Simplex::makeProduct(), markEmpty(), print(), and undo().
◆ nRedundant
|
protected |
The number of redundant rows in the tableau.
These are the first nRedundant rows.
Definition at line 330 of file Simplex.h.
Referenced by findAnyPivotRow(), mlir::presburger::Simplex::isMarkedRedundant(), mlir::presburger::Simplex::makeProduct(), and undo().
◆ nSymbol
|
protected |
The number of parameters.
This must be consistent with the number of Unknowns in var below that have isSymbol set to true.
Definition at line 334 of file Simplex.h.
Referenced by mlir::presburger::LexSimplexBase::addCut(), mlir::presburger::LexSimplexBase::appendSymbol(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::LexSimplexBase::moveRowUnknownToColumn(), SimplexBase(), and undo().
◆ rowUnknown
|
protected |
These hold the indexes of the unknown at a given row or column position.
We keep these as signed integers since that makes it convenient to check if an index corresponds to a variable or a constraint by checking the sign.
colUnknown is padded with two null indexes at the front since the first two columns don't correspond to any unknowns.
Definition at line 358 of file Simplex.h.
Referenced by addZeroRow(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::makeProduct(), print(), removeLastConstraintRowOrientation(), swapRows(), swapRowWithCol(), and unknownFromRow().
◆ savedBases
|
protected |
Holds a vector of bases.
The ith saved basis is the basis that should be restored when processing the ith occurrance of UndoLogEntry::RestoreBasis in undoLog. This is used by getSnapshotBasis.
Definition at line 349 of file Simplex.h.
Referenced by getSnapshotBasis(), and undo().
◆ tableau
|
protected |
The matrix representing the tableau.
Definition at line 337 of file Simplex.h.
Referenced by mlir::presburger::LexSimplexBase::addCut(), addRow(), addZeroRow(), appendVariable(), mlir::presburger::Simplex::computeRowOptimum(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), findAnyPivotRow(), mlir::presburger::LexSimplexBase::getLexMinPivotColumn(), getNumColumns(), getNumRows(), mlir::presburger::Simplex::getRationalSample(), mlir::presburger::Simplex::makeProduct(), mlir::presburger::LexSimplexBase::moveRowUnknownToColumn(), pivot(), print(), removeLastConstraintRowOrientation(), swapColumns(), swapRows(), and undo().
◆ undoLog
|
protected |
Holds a log of operations, used for rolling back to a previous state.
Definition at line 344 of file Simplex.h.
Referenced by addZeroRow(), appendVariable(), getSnapshot(), getSnapshotBasis(), markEmpty(), and rollback().
◆ usingBigM
|
protected |
Stores whether or not a big M column is present in the tableau.
Definition at line 326 of file Simplex.h.
Referenced by addRow(), and getNumFixedCols().
◆ var
|
protected |
Definition at line 361 of file Simplex.h.
Referenced by addRow(), mlir::presburger::LexSimplexBase::appendSymbol(), appendVariable(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::findIntegerSample(), mlir::presburger::LexSimplexBase::getLexMinPivotColumn(), getNumVariables(), mlir::presburger::Simplex::getRationalSample(), mlir::presburger::Simplex::getSamplePointIfIntegral(), mlir::presburger::Simplex::isUnbounded(), mlir::presburger::Simplex::makeProduct(), print(), SimplexBase(), undo(), and unknownFromIndex().
The documentation for this class was generated from the following files:
- include/mlir/Analysis/Presburger/Simplex.h
- lib/Analysis/Presburger/Simplex.cpp
