A class to perform symbolic lexicographic optimization, i.e., to find, for every assignment to the symbols the specified symbolDomain, the lexicographically minimum value integer value attained by the non-symbol variables.
More...
#include "mlir/Analysis/Presburger/Simplex.h"
Inheritance diagram for mlir::presburger::SymbolicLexSimplex:
Public Member Functions | |
| SymbolicLexSimplex (const IntegerRelation &constraints, const IntegerPolyhedron &symbolDomain, const llvm::SmallBitVector &isSymbol) | |
constraints is the set for which the symbolic lexopt will be computed. More... | |
| SymbolicLexSimplex (const IntegerRelation &constraints, unsigned symbolOffset, const IntegerPolyhedron &symbolDomain) | |
| An overload to select some subrange of ids as symbols for lexopt. More... | |
| SymbolicLexSimplex (const IntegerRelation &constraints, const IntegerPolyhedron &symbolDomain) | |
An overload to select the symbols of constraints as symbols for lexopt. More... | |
| SymbolicLexOpt | computeSymbolicIntegerLexMin () |
The lexmin will be stored as a function lexopt from symbols to non-symbols in the result. More... | |
| 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 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 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 |
Detailed Description
A class to perform symbolic lexicographic optimization, i.e., to find, for every assignment to the symbols the specified symbolDomain, the lexicographically minimum value integer value attained by the non-symbol variables.
The input is a set parametrized by some symbols, i.e., the constant terms of the constraints in the set are affine expressions in the symbols, and every assignment to the symbols defines a non-symbolic set.
Accordingly, the sample values of the rows in our tableau will be affine expressions in the symbols, and every assignment to the symbols will define a non-symbolic LexSimplex. We then run the algorithm of LexSimplex::findIntegerLexMin simultaneously for every value of the symbols in the domain.
Often, the pivot to be performed is the same for all values of the symbols, in which case we just do it. For example, if the symbolic sample of a row is negative for all values in the symbol domain, the row needs to be pivoted irrespective of the precise value of the symbols. To answer queries like "Is this symbolic sample always negative in the symbol domain?", we maintain a LexSimplex domainSimplex correponding to the symbol domain.
In other cases, it may be that the symbolic sample is violated at some values in the symbol domain and not violated at others. In this case, the pivot to be performed does depend on the value of the symbols. We handle this by splitting the symbol domain. We run the algorithm for the case where the row isn't violated, and then come back and run the case where it is.
Constructor & Destructor Documentation
◆ SymbolicLexSimplex() [1/3]
|
inline |
constraints is the set for which the symbolic lexopt will be computed.
symbolDomain is the set of values of the symbols for which the lexopt will be computed. symbolDomain should have a dim var for every symbol in constraints, and no other vars. isSymbol specifies which vars of constraints should be considered as symbols.
The resulting SymbolicLexOpt's space will be compatible with that of symbolDomain.
◆ SymbolicLexSimplex() [2/3]
|
inline |
◆ SymbolicLexSimplex() [3/3]
|
inline |
An overload to select the symbols of constraints as symbols for lexopt.
Definition at line 604 of file Simplex.h.
References mlir::presburger::IntegerRelation::getNumSymbolVars(), mlir::presburger::IntegerRelation::getNumVars(), and mlir::presburger::Symbol.
Member Function Documentation
◆ computeSymbolicIntegerLexMin()
| SymbolicLexOpt SymbolicLexSimplex::computeSymbolicIntegerLexMin | ( | ) |
The lexmin will be stored as a function lexopt from symbols to non-symbols in the result.
For some values of the symbols, the lexmin may be unbounded. These parts of the symbol domain will be stored in unboundedDomain.
The spaces of the sets in the result are compatible with the symbolDomain passed in the SymbolicLexSimplex constructor.
The algorithm is more naturally expressed recursively, but we implement it iteratively here to avoid potential issues with stack overflows in the compiler. We explicitly maintain the stack frames in a vector.
To "recurse", we store the current "stack frame", i.e., state variables that we will need when we "return", into stack, increment level, and continue. To "tail recurse", we just continue. To "return", we decrement level and continue.
When there is no stack frame for the current level, this indicates that we have just "recursed" or "tail recursed". When there does exist one, this indicates that we have just "returned" from recursing. There is only one point at which non-tail calls occur so we always "return" there.
Definition at line 537 of file Simplex.cpp.
References mlir::presburger::LexSimplexBase::addInequality(), mlir::presburger::IntegerRelation::addInequality(), mlir::presburger::SimplexBase::empty, mlir::presburger::LexSimplex::findIntegerLexMin(), mlir::presburger::getComplementIneq(), mlir::presburger::IntegerRelation::getCounts(), mlir::presburger::IntegerRelation::getNumDimVars(), mlir::presburger::SimplexBase::getNumRows(), mlir::presburger::IntegerRelation::getNumSymbolVars(), mlir::presburger::PresburgerSpace::getRelationSpace(), mlir::presburger::LexSimplexBase::getSnapshot(), mlir::presburger::LexSimplex::isRedundantInequality(), mlir::presburger::LexSimplex::isSeparateInequality(), mlir::presburger::LexSimplexBase::moveRowUnknownToColumn(), mlir::presburger::normalizeRange(), mlir::presburger::SimplexBase::nSymbol, mlir::presburger::SimplexBase::Unknown::orientation, mlir::presburger::SimplexBase::Unknown::pos, mlir::presburger::SimplexBase::rollback(), mlir::presburger::SimplexBase::Row, mlir::presburger::SimplexBase::rowUnknown, mlir::presburger::SimplexBase::tableau, mlir::presburger::IntegerRelation::truncate(), mlir::presburger::SimplexBase::unknownFromIndex(), and mlir::presburger::SimplexBase::var.
Referenced by mlir::presburger::IntegerRelation::computeReprWithOnlyDivLocals(), and mlir::presburger::IntegerRelation::findSymbolicIntegerLexMin().
The documentation for this class was generated from the following files:
- include/mlir/Analysis/Presburger/Simplex.h
- lib/Analysis/Presburger/Simplex.cpp
