MLIR  17.0.0git
Public Member Functions | Protected Member Functions | List of all members
mlir::presburger::LexSimplexBase Class Reference

Simplex class using the lexicographic pivot rule. More...

#include "mlir/Analysis/Presburger/Simplex.h"

+ Inheritance diagram for mlir::presburger::LexSimplexBase:
+ Collaboration diagram for mlir::presburger::LexSimplexBase:

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 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 UnknownunknownFromIndex (int index) const
 Returns the unknown associated with index. More...
const UnknownunknownFromColumn (unsigned col) const
 Returns the unknown associated with col. More...
const UnknownunknownFromRow (unsigned row) const
 Returns the unknown associated with row. More...
UnknownunknownFromIndex (int index)
 Returns the unknown associated with index. More...
UnknownunknownFromColumn (unsigned col)
 Returns the unknown associated with col. More...
UnknownunknownFromRow (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 ,
 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

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!)

Definition at line 416 of file Simplex.h.

Constructor & Destructor Documentation

◆ ~LexSimplexBase()

mlir::presburger::LexSimplexBase::~LexSimplexBase ( )

◆ LexSimplexBase() [1/4]

mlir::presburger::LexSimplexBase::LexSimplexBase ( unsigned  nVar)

Definition at line 432 of file Simplex.h.

◆ LexSimplexBase() [2/4]

mlir::presburger::LexSimplexBase::LexSimplexBase ( unsigned  nVar,
const llvm::SmallBitVector &  isSymbol 

Definition at line 433 of file Simplex.h.

◆ LexSimplexBase() [3/4]

mlir::presburger::LexSimplexBase::LexSimplexBase ( const IntegerRelation constraints)

◆ LexSimplexBase() [4/4]

mlir::presburger::LexSimplexBase::LexSimplexBase ( const IntegerRelation constraints,
const llvm::SmallBitVector &  isSymbol 

Member Function Documentation

◆ addCut()

LogicalResult LexSimplexBase::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.

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

◆ addInequality()

void LexSimplexBase::addInequality ( ArrayRef< MPInt coeffs)

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 1571 of file Simplex.cpp.

References mlir::presburger::SimplexBase::addRow().

Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), and mlir::presburger::LexSimplex::isSeparateInequality().

◆ appendSymbol()

void LexSimplexBase::appendSymbol ( )

◆ getLexMinPivotColumn()

unsigned LexSimplexBase::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.

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

◆ getSnapshot()

unsigned mlir::presburger::LexSimplexBase::getSnapshot ( )

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

◆ moveRowUnknownToColumn()

LogicalResult LexSimplexBase::moveRowUnknownToColumn ( unsigned  row)

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

◆ undoLastConstraint()

void LexSimplexBase::undoLastConstraint ( )

The documentation for this class was generated from the following files: