MLIR
17.0.0git

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"
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< MPInt > 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< 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 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< 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) 
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...  
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 
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 nonredundant constraints. The LexSimplex class provides support for computing the lexicographic minimum of an IntegerRelation. The SymbolicLexMin 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 twodimensional 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 socall 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 socalled 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 nonnegative 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 nonnegative, 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 nonnegative. 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 nonnegative 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.

strongprotected 

strongprotected 

delete 

virtualdefault 

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 socalled big M parameter. For more information see the documentation for LexSimplex.
Definition at line 35 of file Simplex.cpp.
References Column, colUnknown, getNumFixedCols(), nullIndex, and var.

protected 
Definition at line 46 of file Simplex.cpp.
References getNumFixedCols(), nSymbol, swapColumns(), and var.
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 1283 of file Simplex.cpp.
References addInequality(), and appendVariable().
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_{n1}*x_{n1} == 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_{n1}*x_{n1} == 0.
We simply add two opposing inequalities, which force the expression to be zero.
Definition at line 1104 of file Simplex.cpp.
References addInequality().
Referenced by mlir::presburger::Simplex::findIntegerSample(), and intersectIntegerRelation().
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.
Implemented in mlir::presburger::Simplex, and mlir::presburger::LexSimplexBase.
Referenced by addDivisionVariable(), addEquality(), and intersectIntegerRelation().
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 104 of file Simplex.cpp.
References addZeroRow(), Column, con, getNumColumns(), getNumFixedCols(), mlir::presburger::lcm(), mlir::presburger::Matrix::normalizeRow(), tableau, usingBigM, and var.
Referenced by mlir::presburger::LexSimplexBase::addInequality(), mlir::presburger::Simplex::addInequality(), and mlir::presburger::Simplex::computeOptimum().

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 90 of file Simplex.cpp.
References mlir::presburger::Matrix::appendExtraRow(), con, getNumRows(), RemoveLastConstraint, Row, rowUnknown, tableau, and undoLog.
Referenced by mlir::presburger::LexSimplexBase::addCut(), and addRow().
void SimplexBase::appendVariable  (  unsigned  count = 1  ) 
Add new variables to the end of the list of variables.
Definition at line 1300 of file Simplex.cpp.
References Column, colUnknown, getNumColumns(), RemoveLastVariable, mlir::presburger::Matrix::resizeHorizontally(), tableau, undoLog, and var.
Referenced by addDivisionVariable(), mlir::presburger::LexSimplexBase::appendSymbol(), and getSetDifference().
void SimplexBase::dump  (  )  const 
Definition at line 2127 of file Simplex.cpp.
References print().

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 nonzero coefficient for it.
Definition at line 1154 of file Simplex.cpp.
References getNumRows(), nRedundant, and tableau.
Referenced by mlir::presburger::LexSimplexBase::undoLastConstraint().

inlineprotected 
Definition at line 327 of file Simplex.h.
References mlir::presburger::Matrix::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().
unsigned SimplexBase::getNumConstraints  (  )  const 
Returns the number of constraints in the tableau.
Definition at line 1113 of file Simplex.cpp.
References con.
Referenced by getSetDifference(), and mlir::presburger::Simplex::makeProduct().

inlineprotected 

inlineprotected 
Definition at line 326 of file Simplex.h.
References mlir::presburger::Matrix::getNumRows(), and tableau.
Referenced by addZeroRow(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), findAnyPivotRow(), mlir::presburger::Simplex::makeProduct(), pivot(), print(), removeLastConstraintRowOrientation(), and unknownFromRow().
unsigned SimplexBase::getNumVariables  (  )  const 
Returns the number of variables in the tableau.
Definition at line 1112 of file Simplex.cpp.
References var.
Referenced by intersectIntegerRelation(), and mlir::presburger::Simplex::makeProduct().
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 1117 of file Simplex.cpp.
References undoLog.
Referenced by mlir::presburger::Simplex::findIntegerSample(), getSetDifference(), and mlir::presburger::SimplexRollbackScopeExit::SimplexRollbackScopeExit().
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 1119 of file Simplex.cpp.
References colUnknown, nullIndex, RestoreBasis, savedBases, and undoLog.
Referenced by mlir::presburger::LexSimplexBase::getSnapshot().
void SimplexBase::intersectIntegerRelation  (  const IntegerRelation &  rel  ) 
Add all the constraints from the given IntegerRelation.
Definition at line 1315 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().
bool SimplexBase::isEmpty  (  )  const 
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
Definition at line 1051 of file Simplex.cpp.
References empty.
Referenced by mlir::presburger::IntegerRelation::computeVolume(), mlir::presburger::IntegerRelation::findIntegerSample(), mlir::presburger::IntegerRelation::getBoundedDirections(), getSetDifference(), mlir::presburger::Simplex::isRationalSubsetOf(), and mlir::presburger::SetCoalescer::SetCoalescer().
void SimplexBase::markEmpty  (  ) 
Mark the tableau as being empty.
Mark this tableau empty and push an entry to the undo stack.
Definition at line 1074 of file Simplex.cpp.
References empty, undoLog, and UnmarkEmpty.
Referenced by mlir::presburger::Simplex::addInequality(), and mlir::presburger::LexSimplex::findRationalLexMin().

protected 
Definition at line 905 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Pivot::column, pivot(), and mlir::presburger::SimplexBase::Pivot::row.

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 932 of file Simplex.cpp.
References getNumColumns(), getNumFixedCols(), getNumRows(), mlir::presburger::Matrix::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().
void SimplexBase::print  (  raw_ostream &  os  )  const 
Print the tableau's internal state.
Definition at line 2092 of file Simplex.cpp.
References colUnknown, con, empty, getNumColumns(), getNumRows(), rowUnknown, tableau, and var.
Referenced by dump().

protected 
Remove the last constraint, which must be in row orientation.
Definition at line 1131 of file Simplex.cpp.
References con, getNumRows(), mlir::presburger::Matrix::resizeVertically(), Row, rowUnknown, swapRows(), and tableau.
Referenced by mlir::presburger::LexSimplexBase::undoLastConstraint().
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 1270 of file Simplex.cpp.
References undo(), and undoLog.
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::findIntegerSample(), and getSetDifference().

protected 
Definition at line 1062 of file Simplex.cpp.
References colUnknown, getNumColumns(), mlir::presburger::SimplexBase::Unknown::pos, mlir::presburger::Matrix::swapColumns(), tableau, and unknownFromColumn().
Referenced by mlir::presburger::LexSimplexBase::appendSymbol(), SimplexBase(), and undo().

protected 
Swap the two rows/columns in the tableau and associated data structures.
Definition at line 1053 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Unknown::pos, rowUnknown, mlir::presburger::Matrix::swapRows(), tableau, and unknownFromRow().
Referenced by removeLastConstraintRowOrientation().

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 895 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().

protected 
Undo the operation represented by the log entry.
Definition at line 1208 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::resizeHorizontally(), RestoreBasis, savedBases, swapColumns(), tableau, undoLastConstraint(), unknownFromIndex(), UnmarkEmpty, UnmarkLastRedundant, and var.
Referenced by rollback().

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().

protected 
Returns the unknown associated with col.
Definition at line 80 of file Simplex.cpp.
References colUnknown, getNumColumns(), and unknownFromIndex().

protected 
Returns the unknown associated with col.
Definition at line 65 of file Simplex.cpp.
References colUnknown, getNumColumns(), and unknownFromIndex().
Referenced by pivot(), swapColumns(), and swapRowWithCol().

protected 
Returns the unknown associated with index.
Definition at line 75 of file Simplex.cpp.

protected 
Returns the unknown associated with index.
Definition at line 60 of file Simplex.cpp.
References con, nullIndex, and var.
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::makeProduct(), undo(), unknownFromColumn(), and unknownFromRow().

protected 
Returns the unknown associated with row.
Definition at line 85 of file Simplex.cpp.
References getNumRows(), rowUnknown, and unknownFromIndex().

protected 
Returns the unknown associated with row.
Definition at line 70 of file Simplex.cpp.
References getNumRows(), rowUnknown, and unknownFromIndex().
Referenced by swapRows(), and swapRowWithCol().

protected 
Definition at line 362 of file Simplex.h.
Referenced by appendVariable(), getSnapshotBasis(), mlir::presburger::Simplex::makeProduct(), print(), SimplexBase(), swapColumns(), swapRowWithCol(), undo(), and unknownFromColumn().

protected 
These hold information about each unknown.
Definition at line 365 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().

protected 
This is true if the tableau has been detected to be empty, false otherwise.
Definition at line 345 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().

protected 
The number of redundant rows in the tableau.
These are the first nRedundant rows.
Definition at line 334 of file Simplex.h.
Referenced by findAnyPivotRow(), mlir::presburger::Simplex::isMarkedRedundant(), mlir::presburger::Simplex::makeProduct(), and undo().

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 338 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().

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 362 of file Simplex.h.
Referenced by addZeroRow(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::makeProduct(), print(), removeLastConstraintRowOrientation(), swapRows(), swapRowWithCol(), and unknownFromRow().

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 353 of file Simplex.h.
Referenced by getSnapshotBasis(), and undo().

protected 
The matrix representing the tableau.
Definition at line 341 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().

protected 
Holds a log of operations, used for rolling back to a previous state.
Definition at line 348 of file Simplex.h.
Referenced by addZeroRow(), appendVariable(), getSnapshot(), getSnapshotBasis(), markEmpty(), and rollback().

protected 
Stores whether or not a big M column is present in the tableau.
Definition at line 330 of file Simplex.h.
Referenced by addRow(), and getNumFixedCols().

protected 
Definition at line 365 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().