MLIR
20.0.0git

A class for lexicographic optimization without any symbols. More...
#include "mlir/Analysis/Presburger/Simplex.h"
Public Member Functions  
LexSimplex (unsigned nVar)  
LexSimplex (const IntegerRelation &constraints)  
MaybeOptimum< SmallVector< Fraction, 8 > >  findRationalLexMin () 
Return the lexicographically minimum rational solution to the constraints. More...  
MaybeOptimum< SmallVector< DynamicAPInt, 8 > >  findIntegerLexMin () 
Return the lexicographically minimum integer solution to the constraints. More...  
bool  isSeparateInequality (ArrayRef< DynamicAPInt > coeffs) 
Return whether the specified inequality is redundant/separate for the polytope. More...  
bool  isRedundantInequality (ArrayRef< DynamicAPInt > coeffs) 
Public Member Functions inherited from mlir::presburger::LexSimplexBase  
~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 
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 Member Functions inherited from mlir::presburger::LexSimplexBase  
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< 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 
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 
A class for lexicographic optimization without any symbols.
This also provides support for integerexact redundancy and separateness checks.

inlineexplicit 

inlineexplicit 
MaybeOptimum< SmallVector< DynamicAPInt, 8 > > LexSimplex::findIntegerLexMin  (  ) 
Return the lexicographically minimum integer solution to the constraints.
Note: this should be used only when the lexmin is really needed. To obtain any integer sample, use Simplex::findIntegerSample as that is more robust.
Definition at line 306 of file Simplex.cpp.
References mlir::presburger::LexSimplexBase::addCut(), mlir::presburger::Empty, mlir::presburger::Fraction::getAsInteger(), mlir::presburger::MaybeOptimum< T >::isEmpty(), mlir::presburger::MaybeOptimum< T >::isUnbounded(), and mlir::presburger::Unbounded.
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::IntegerRelation::findIntegerLexMin(), and isSeparateInequality().
MaybeOptimum< SmallVector< Fraction, 8 > > LexSimplex::findRationalLexMin  (  ) 
Return the lexicographically minimum rational solution to the constraints.
We simply make the tableau consistent while maintaining a lexicopositive basis transform, and then return the sample value.
If the tableau becomes empty, we return empty.
Let the variables be x = (x_1, ... x_n). Let the basis unknowns be y = (y_1, ... y_n). We have that x = A*y + b for some n x n matrix A and n x 1 column vector b.
As we will show below, A*y is either zero or lexicopositive. Adding a lexicopositive vector to b will make it lexicographically greater, so A*y + b is always equal to or lexicographically greater than b. Thus, since we can attain x = b, that is the lexicographic minimum.
We have that every column in A is lexicopositive, i.e., has at least one nonzero element, with the first such element being positive. Since for the tableau to be consistent we must have nonnegative sample values not only for the constraints but also for the variables, we also have x >= 0 and y >= 0, by which we mean every element in these vectors is nonnegative.
Proof that if every column in A is lexicopositive, and y >= 0, then A*y is zero or lexicopositive. Begin by considering A_1, the first row of A. If this row is all zeros, then (A*y)_1 = (A_1)*y = 0; proceed to the next row. If we run out of rows, A*y is zero and we are done; otherwise, we encounter some row A_i that has a nonzero element. Every column is lexicopositive and so has some positive element before any negative elements occur, so the element in this row for any column, if nonzero, must be positive. Consider (A*y)_i = (A_i)*y. All the elements in both vectors are nonnegative, so if this is nonzero then it must be positive. Then the first nonzero element of A*y is positive so A*y is lexicopositive.
Otherwise, if (A_i)*y is zero, then for every column j that had a nonzero element in A_i, y_j is zero. Thus these columns have no contribution to A*y and we can completely ignore these columns of A. We now continue downwards, looking for rows of A that have a nonzero element other than in the ignored columns. If we find one, say A_k, once again these elements must be positive since they are the first nonzero element in each of these columns, so if (A_k)*y is not zero then we have that A*y is lexicopositive and if not we add these to the set of ignored columns and continue to the next row. If we run out of rows, then A*y is zero and we are done.
Definition at line 235 of file Simplex.cpp.
References mlir::presburger::Empty, and mlir::presburger::SimplexBase::markEmpty().
Referenced by mlir::presburger::IntegerRelation::findRationalLexMin().
bool LexSimplex::isRedundantInequality  (  ArrayRef< DynamicAPInt >  coeffs  ) 
Definition at line 343 of file Simplex.cpp.
References mlir::presburger::getComplementIneq(), and isSeparateInequality().
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin().
bool LexSimplex::isSeparateInequality  (  ArrayRef< DynamicAPInt >  coeffs  ) 
Return whether the specified inequality is redundant/separate for the polytope.
Redundant means every point satisfies the given inequality, and separate means no point satisfies it.
These checks are integerexact.
Definition at line 337 of file Simplex.cpp.
References mlir::presburger::LexSimplexBase::addInequality(), and findIntegerLexMin().
Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), and isRedundantInequality().