MLIR
17.0.0git

Simplex class using the lexicographic pivot rule. More...
#include "mlir/Analysis/Presburger/Simplex.h"
Public Member Functions  
~LexSimplexBase () override=default  
void  addInequality (ArrayRef< MPInt > 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< MPInt > 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< MPInt > coeffs, const MPInt &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 noninteger 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< MPInt > 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...  
Matrix  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 
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 negativevalued variables, so it uses the big M parameter trick to make all the variables nonnegative. 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 nonnegative. 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 nonzero 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 nonnegative 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 nonnegative. (note that this is a different concept from lexicopositivity!)

overridedefault 

inlineprotected 

inlineprotected 

inlineexplicitprotected 
Definition at line 435 of file Simplex.h.
References mlir::presburger::SimplexBase::intersectIntegerRelation().

inlineexplicitprotected 
Definition at line 439 of file Simplex.h.
References mlir::presburger::SimplexBase::intersectIntegerRelation().

protected 
Given a row that has a noninteger 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 noninteger 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 nonnegative. Also, all the unknowns are nonnegative here as both constraints and variables are nonnegative in LexSimplexBase. (We used the big M trick to make the variables nonnegative). Therefore, the LHS here is nonnegative. Since 0 <= (cd) < d, k is the quotient of dividing the LHS by d and is therefore nonnegative 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 263 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addZeroRow(), mlir::presburger::SimplexBase::getNumColumns(), mlir::presburger::mod(), moveRowUnknownToColumn(), mlir::presburger::SimplexBase::nSymbol, and mlir::presburger::SimplexBase::tableau.
Referenced by mlir::presburger::LexSimplex::findIntegerLexMin().
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_{n1}*x_{n1} >= 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 1571 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addRow().
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), and mlir::presburger::LexSimplex::isSeparateInequality().

protected 
Add new symbolic variables to the end of the list of variables.
Definition at line 347 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.

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 774 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Column, mlir::presburger::SimplexBase::tableau, and mlir::presburger::SimplexBase::var.
Referenced by moveRowUnknownToColumn().

inline 
Get a snapshot of the current state. This is used for rolling back.
Definition at line 429 of file Simplex.h.
References mlir::presburger::SimplexBase::getSnapshotBasis().
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin().

protected 
Try to move the specified row to column orientation while preserving the lexicopositivity of the basis transform.
The row must have a nonpositive 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 758 of file Simplex.cpp.
References mlir::failure(), getLexMinPivotColumn(), mlir::presburger::SimplexBase::getNumColumns(), mlir::presburger::SimplexBase::nSymbol, mlir::presburger::SimplexBase::pivot(), mlir::success(), and mlir::presburger::SimplexBase::tableau.
Referenced by addCut(), and mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin().

finalprotectedvirtual 
Undo the addition of the last constraint.
This is only called while rolling back.
Implements mlir::presburger::SimplexBase.
Definition at line 1192 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().