The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecting redundancies. More...
#include "mlir/Analysis/Presburger/Simplex.h"
Inheritance diagram for mlir::presburger::Simplex:
Public Types | |
| enum class | Direction { Up , Down } |
| enum class | IneqType { Redundant , Cut , Separate } |
Public Member Functions | |
| Simplex ()=delete | |
| Simplex (unsigned nVar) | |
| Simplex (const IntegerRelation &constraints) | |
| ~Simplex () override=default | |
| void | addInequality (ArrayRef< MPInt > coeffs) final |
| Add an inequality to the tableau. More... | |
| MaybeOptimum< Fraction > | computeRowOptimum (Direction direction, unsigned row) |
| Compute the maximum or minimum value of the given row, depending on direction. More... | |
| MaybeOptimum< Fraction > | computeOptimum (Direction direction, ArrayRef< MPInt > coeffs) |
| Compute the maximum or minimum value of the given expression, depending on direction. More... | |
| bool | isBoundedAlongConstraint (unsigned constraintIndex) |
| Returns whether the perpendicular of the specified constraint is a is a direction along which the polytope is bounded. More... | |
| bool | isMarkedRedundant (unsigned constraintIndex) const |
| Returns whether the specified constraint has been marked as redundant. More... | |
| void | detectRedundant (unsigned offset, unsigned count) |
| Finds a subset of constraints that is redundant, i.e., such that the set of solutions does not change if these constraints are removed. More... | |
| void | detectRedundant (unsigned offset) |
| void | detectRedundant () |
| std::pair< MaybeOptimum< MPInt >, MaybeOptimum< MPInt > > | computeIntegerBounds (ArrayRef< MPInt > coeffs) |
| Returns a (min, max) pair denoting the minimum and maximum integer values of the given expression. More... | |
| bool | isFlatAlong (ArrayRef< MPInt > coeffs) |
Check if the simplex takes only one rational value along the direction of coeffs. More... | |
| bool | isUnbounded () |
| Returns true if the polytope is unbounded, i.e., extends to infinity in some direction. More... | |
| std::optional< SmallVector< MPInt, 8 > > | findIntegerSample () |
| Returns an integer sample point if one exists, or std::nullopt otherwise. More... | |
| IneqType | findIneqType (ArrayRef< MPInt > coeffs) |
Returns the type of the inequality with coefficients coeffs. More... | |
| bool | isRedundantInequality (ArrayRef< MPInt > coeffs) |
| Check if the specified inequality already holds in the polytope. More... | |
| bool | isRedundantEquality (ArrayRef< MPInt > coeffs) |
| Check if the specified equality already holds in the polytope. More... | |
| bool | isRationalSubsetOf (const IntegerRelation &rel) |
Returns true if this Simplex's polytope is a rational subset of rel. More... | |
| std::optional< SmallVector< MPInt, 8 > > | getSamplePointIfIntegral () const |
| Returns the current sample point if it is integral. More... | |
| std::optional< SmallVector< Fraction, 8 > > | getRationalSample () const |
| Returns the current sample point, which may contain non-integer (rational) coordinates. 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 |
Static Public Member Functions | |
| static Simplex | makeProduct (const Simplex &a, const Simplex &b) |
| Make a tableau to represent a pair of points in the given tableaus, one in tableau A and one in B. More... | |
Friends | |
| class | GBRSimplex |
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::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 |
| 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
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecting redundancies.
The Simplex class supports redundancy checking via detectRedundant and isMarkedRedundant. A redundant constraint is one which is never violated as long as the other constraints are not violated, i.e., removing a redundant constraint does not change the set of solutions to the constraints. As a heuristic, constraints that have been marked redundant can be ignored for most operations. Therefore, these constraints are kept in rows 0 to nRedundant - 1, where nRedundant is a member variable that tracks the number of constraints that have been marked redundant.
Finding an integer sample is done with the Generalized Basis Reduction algorithm. See the documentation for findIntegerSample and reduceBasis.
Member Enumeration Documentation
◆ Direction
|
strong |
◆ IneqType
|
strong |
Constructor & Destructor Documentation
◆ Simplex() [1/3]
|
delete |
◆ Simplex() [2/3]
|
inlineexplicit |
◆ Simplex() [3/3]
|
inlineexplicit |
Definition at line 701 of file Simplex.h.
References mlir::presburger::SimplexBase::intersectIntegerRelation().
◆ ~Simplex()
|
overridedefault |
Member Function Documentation
◆ addInequality()
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 also tries to restore the tableau configuration to a consistent state and marks the Simplex empty if this is not possible.
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.
We add the inequality and mark it as restricted. We then try to make its sample value non-negative. If this is not possible, the tableau has become empty and we mark it as such.
Implements mlir::presburger::SimplexBase.
Definition at line 1106 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addRow(), mlir::presburger::SimplexBase::con, mlir::failed(), and mlir::presburger::SimplexBase::markEmpty().
◆ computeIntegerBounds()
| std::pair< MaybeOptimum< MPInt >, MaybeOptimum< MPInt > > Simplex::computeIntegerBounds | ( | ArrayRef< MPInt > | coeffs | ) |
Returns a (min, max) pair denoting the minimum and maximum integer values of the given expression.
Compute the minimum and maximum integer values the expression can take.
If no integer value exists, both results will be of kind Empty.
We compute each separately.
Definition at line 2099 of file Simplex.cpp.
References mlir::presburger::ceil(), computeOptimum(), Down, mlir::presburger::floor(), and Up.
Referenced by mlir::presburger::IntegerRelation::computeVolume(), and findIntegerSample().
◆ computeOptimum()
| MaybeOptimum< Fraction > Simplex::computeOptimum | ( | Direction | direction, |
| ArrayRef< MPInt > | coeffs | ||
| ) |
Compute the maximum or minimum value of the given expression, depending on direction.
Compute the optimum of the specified expression in the specified direction, or std::nullopt if it is unbounded.
Should not be called when the Simplex is empty.
Returns a Fraction denoting the optimum, or a null value if no optimum exists, i.e., if the expression is unbounded in this direction.
Definition at line 1358 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addRow(), computeRowOptimum(), mlir::presburger::SimplexBase::con, mlir::presburger::SimplexBase::empty, and mlir::presburger::Empty.
Referenced by computeIntegerBounds(), findIneqType(), isBoundedAlongConstraint(), isFlatAlong(), isRedundantEquality(), and isUnbounded().
◆ computeRowOptimum()
| MaybeOptimum< Fraction > Simplex::computeRowOptimum | ( | Direction | direction, |
| unsigned | row | ||
| ) |
Compute the maximum or minimum value of the given row, depending on direction.
The specified row is never pivoted. On return, the row may have a negative sample value if the direction is down.
Returns a Fraction denoting the optimum, or a null value if no optimum exists, i.e., if the expression is unbounded in this direction.
Definition at line 1339 of file Simplex.cpp.
References mlir::presburger::SimplexBase::pivot(), mlir::presburger::SimplexBase::tableau, and mlir::presburger::Unbounded.
Referenced by computeOptimum(), and detectRedundant().
◆ detectRedundant() [1/3]
|
inline |
Definition at line 766 of file Simplex.h.
References mlir::presburger::SimplexBase::con, and detectRedundant().
Referenced by detectRedundant().
◆ detectRedundant() [2/3]
|
inline |
Definition at line 762 of file Simplex.h.
References mlir::presburger::SimplexBase::con.
◆ detectRedundant() [3/3]
| void Simplex::detectRedundant | ( | unsigned | offset, |
| unsigned | count | ||
| ) |
Finds a subset of constraints that is redundant, i.e., such that the set of solutions does not change if these constraints are removed.
Find a subset of constraints that is redundant and mark them redundant.
Marks these constraints as redundant. Whether a specific constraint has been marked redundant can be queried using isMarkedRedundant.
The first overload only tries to find redundant constraints with indices in the range [offset, offset + count), by scanning constraints from left to right in this range. If count is not provided, all constraints starting at offset are scanned, and if neither are provided, all constraints are scanned, starting from 0 and going to the last constraint.
As an example, in the set (x) : (x >= 0, x >= 0, x >= 0), calling detectRedundant with no parameters will result in the first two constraints being marked redundant. All copies cannot be marked redundant because removing all the constraints changes the set. The first two are the ones marked redundant because we scan from left to right. Thus, when there is some preference among the constraints as to which should be marked redundant with priority when there are multiple possibilities, this could be accomplished by succesive calls to detectRedundant(offset, count).
Definition at line 1423 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Column, computeRowOptimum(), mlir::presburger::SimplexBase::con, Down, mlir::presburger::SimplexBase::empty, mlir::failed(), mlir::presburger::MaybeOptimum< T >::isUnbounded(), mlir::presburger::SimplexBase::Unknown::orientation, mlir::presburger::SimplexBase::pivot(), and mlir::presburger::SimplexBase::Unknown::pos.
Referenced by mlir::presburger::IntegerRelation::removeRedundantConstraints().
◆ findIneqType()
| Simplex::IneqType Simplex::findIneqType | ( | ArrayRef< MPInt > | coeffs | ) |
Returns the type of the inequality with coefficients coeffs.
Possible types are: Redundant The inequality is satisfied in the polytope Cut The inequality is satisfied by some points, but not by others Separate The inequality is not satisfied by any point
Possible types are: Redundant The inequality is satisfied by all points in the polytope Cut The inequality is satisfied by some points, but not by others Separate The inequality is not satisfied by any point
Internally, this computes the minimum and the maximum the inequality with coefficients coeffs can take. If the minimum is >= 0, the inequality holds for all points in the polytope, so it is redundant. If the minimum is <= 0 and the maximum is >= 0, the points in between the minimum and the inequality do not satisfy it, the points in between the inequality and the maximum satisfy it. Hence, it is a cut inequality. If both are < 0, no points of the polytope satisfy the inequality, which means it is a separate inequality.
Definition at line 2186 of file Simplex.cpp.
References computeOptimum(), Cut, Down, mlir::presburger::MaybeOptimum< T >::isBounded(), Redundant, Separate, and Up.
Referenced by isRationalSubsetOf(), and isRedundantInequality().
◆ findIntegerSample()
| std::optional< SmallVector< MPInt, 8 > > Simplex::findIntegerSample | ( | ) |
Returns an integer sample point if one exists, or std::nullopt otherwise.
Search for an integer sample point using a branch and bound algorithm.
This should only be called for bounded sets.
Each row in the basis matrix is a vector, and the set of basis vectors should span the space. Initially this is the identity matrix, i.e., the basis vectors are just the variables.
In every level, a value is assigned to the level-th basis vector, as follows. Compute the minimum and maximum rational values of this direction. If only one integer point lies in this range, constrain the variable to have this value and recurse to the next variable.
If the range has multiple values, perform generalized basis reduction via reduceBasis and then compute the bounds again. Now we try constraining this direction in the first value in this range and "recurse" to the next level. If we fail to find a sample, we try assigning the direction the next value in this range, and so on.
If no integer sample is found from any of the assignments, or if the range contains no integer value, then of course the polytope is empty for the current assignment of the values in previous levels, so we return to the previous level.
If we reach the last level where all the variables have been assigned values already, then we simply return the current sample point if it is integral, and go back to the previous level otherwise.
To avoid potentially arbitrarily large recursion depths leading to stack overflows, this algorithm is implemented iteratively.
Definition at line 1988 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addEquality(), computeIntegerBounds(), mlir::presburger::SimplexBase::empty, mlir::presburger::Matrix< T >::getNumRows(), mlir::presburger::Matrix< T >::getRow(), getSamplePointIfIntegral(), mlir::presburger::SimplexBase::getSnapshot(), mlir::presburger::IntMatrix::identity(), mlir::presburger::SimplexBase::rollback(), and mlir::presburger::SimplexBase::var.
Referenced by mlir::presburger::IntegerRelation::findIntegerSample().
◆ getRationalSample()
| std::optional< SmallVector< Fraction, 8 > > Simplex::getRationalSample | ( | ) | const |
Returns the current sample point, which may contain non-integer (rational) coordinates.
Returns an empty optional when the tableau is empty.
Definition at line 1565 of file Simplex.cpp.
References mlir::presburger::SimplexBase::Column, mlir::presburger::SimplexBase::empty, mlir::presburger::SimplexBase::tableau, and mlir::presburger::SimplexBase::var.
Referenced by mlir::presburger::IntegerRelation::findIntegerSample(), and getSamplePointIfIntegral().
◆ getSamplePointIfIntegral()
| std::optional< SmallVector< MPInt, 8 > > Simplex::getSamplePointIfIntegral | ( | ) | const |
Returns the current sample point if it is integral.
Otherwise, returns std::nullopt.
Definition at line 1620 of file Simplex.cpp.
References mlir::presburger::SimplexBase::empty, getRationalSample(), and mlir::presburger::SimplexBase::var.
Referenced by findIntegerSample().
◆ isBoundedAlongConstraint()
| bool Simplex::isBoundedAlongConstraint | ( | unsigned | constraintIndex | ) |
Returns whether the perpendicular of the specified constraint is a is a direction along which the polytope is bounded.
Definition at line 1393 of file Simplex.cpp.
References computeOptimum(), mlir::presburger::SimplexBase::con, mlir::presburger::SimplexBase::empty, and Up.
Referenced by mlir::presburger::IntegerRelation::getBoundedDirections().
◆ isFlatAlong()
Check if the simplex takes only one rational value along the direction of coeffs.
this must be nonempty.
Definition at line 2107 of file Simplex.cpp.
References computeOptimum(), Down, mlir::presburger::SimplexBase::isEmpty(), and Up.
Referenced by mlir::presburger::IntegerRelation::isFullDim().
◆ isMarkedRedundant()
| bool Simplex::isMarkedRedundant | ( | unsigned | constraintIndex | ) | const |
Returns whether the specified constraint has been marked as redundant.
Redundant constraints are those that are in row orientation and lie in rows 0 to nRedundant - 1.
Constraints are numbered from 0 starting at the first added inequality. Equalities are added as a pair of inequalities and so correspond to two inequalities with successive indices.
Definition at line 1403 of file Simplex.cpp.
References mlir::presburger::SimplexBase::con, mlir::presburger::SimplexBase::nRedundant, mlir::presburger::SimplexBase::Unknown::orientation, mlir::presburger::SimplexBase::Unknown::pos, and mlir::presburger::SimplexBase::Row.
Referenced by mlir::presburger::IntegerRelation::removeRedundantConstraints().
◆ isRationalSubsetOf()
| bool Simplex::isRationalSubsetOf | ( | const IntegerRelation & | rel | ) |
Returns true if this Simplex's polytope is a rational subset of rel.
Otherwise, returns false.
Definition at line 2157 of file Simplex.cpp.
References findIneqType(), mlir::presburger::IntegerRelation::getEquality(), mlir::presburger::IntegerRelation::getInequality(), mlir::presburger::IntegerRelation::getNumEqualities(), mlir::presburger::IntegerRelation::getNumInequalities(), mlir::presburger::SimplexBase::isEmpty(), isRedundantEquality(), and Redundant.
◆ isRedundantEquality()
Check if the specified equality already holds in the polytope.
Check whether the equality given by coeffs == 0 is redundant given the existing constraints.
This is redundant when coeffs is already always zero under the existing constraints. coeffs is always zero when the minimum and maximum value that coeffs can take are both zero.
Definition at line 2211 of file Simplex.cpp.
References computeOptimum(), Down, mlir::presburger::SimplexBase::empty, mlir::presburger::MaybeOptimum< T >::isBounded(), mlir::presburger::MaybeOptimum< T >::isEmpty(), and Up.
Referenced by isRationalSubsetOf().
◆ isRedundantInequality()
Check if the specified inequality already holds in the polytope.
Checks whether the type of the inequality with coefficients coeffs is Redundant.
Definition at line 2201 of file Simplex.cpp.
References mlir::presburger::SimplexBase::empty, findIneqType(), and Redundant.
◆ isUnbounded()
| bool Simplex::isUnbounded | ( | ) |
Returns true if the polytope is unbounded, i.e., extends to infinity in some direction.
Otherwise, returns false.
Definition at line 1465 of file Simplex.cpp.
References computeOptimum(), Down, mlir::presburger::SimplexBase::empty, Up, and mlir::presburger::SimplexBase::var.
Referenced by mlir::presburger::IntegerRelation::findIntegerSample().
◆ makeProduct()
Make a tableau to represent a pair of points in the given tableaus, one in tableau A and one in B.
Make a tableau to represent a pair of points in the original tableau.
The product constraints and variables are stored as: first A's, then B's.
The product tableau has row layout: A's redundant rows, B's redundant rows, A's other rows, B's other rows.
It has column layout: denominator, constant, A's columns, B's columns.
Definition at line 1493 of file Simplex.cpp.
References mlir::presburger::Matrix< T >::appendExtraRow(), mlir::presburger::SimplexBase::colUnknown, mlir::presburger::SimplexBase::con, mlir::linalg::concat(), mlir::presburger::SimplexBase::empty, mlir::presburger::SimplexBase::getNumColumns(), mlir::presburger::SimplexBase::getNumConstraints(), mlir::presburger::SimplexBase::getNumRows(), mlir::presburger::SimplexBase::getNumVariables(), mlir::presburger::SimplexBase::nRedundant, nullIndex, mlir::presburger::Matrix< T >::reserveRows(), mlir::presburger::SimplexBase::rowUnknown, mlir::presburger::SimplexBase::tableau, mlir::presburger::SimplexBase::unknownFromIndex(), and mlir::presburger::SimplexBase::var.
Friends And Related Function Documentation
◆ GBRSimplex
|
friend |
The documentation for this class was generated from the following files:
- include/mlir/Analysis/Presburger/Simplex.h
- lib/Analysis/Presburger/Simplex.cpp
