MLIR
17.0.0git

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"
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  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 noninteger (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...  
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 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.

strong 

strong 

delete 

inlineexplicit 

inlineexplicit 
Definition at line 701 of file Simplex.h.
References mlir::presburger::SimplexBase::intersectIntegerRelation().

overridedefault 
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.
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_{n1}*x_{n1} >= 0.
We add the inequality and mark it as restricted. We then try to make its sample value nonnegative. If this is not possible, the tableau has become empty and we mark it as such.
Implements mlir::presburger::SimplexBase.
Definition at line 1091 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addRow(), mlir::presburger::SimplexBase::con, mlir::failed(), and mlir::presburger::SimplexBase::markEmpty().
Referenced by getSetDifference().
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 2084 of file Simplex.cpp.
References mlir::presburger::ceil(), computeOptimum(), Down, mlir::presburger::floor(), and Up.
Referenced by mlir::presburger::IntegerRelation::computeVolume(), and findIntegerSample().
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 1343 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(), isRedundantEquality(), and isUnbounded().
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 1324 of file Simplex.cpp.
References mlir::presburger::SimplexBase::pivot(), mlir::presburger::SimplexBase::tableau, and mlir::presburger::Unbounded.
Referenced by computeOptimum(), and detectRedundant().

inline 
Definition at line 766 of file Simplex.h.
References mlir::presburger::SimplexBase::con, and detectRedundant().
Referenced by detectRedundant().

inline 
Definition at line 762 of file Simplex.h.
References mlir::presburger::SimplexBase::con.
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 1408 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 getSetDifference(), and mlir::presburger::IntegerRelation::removeRedundantConstraints().
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 2158 of file Simplex.cpp.
References computeOptimum(), Cut, Down, mlir::presburger::MaybeOptimum< T >::isBounded(), Redundant, Separate, and Up.
Referenced by isRationalSubsetOf(), and isRedundantInequality().
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 levelth 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 1973 of file Simplex.cpp.
References mlir::presburger::SimplexBase::addEquality(), computeIntegerBounds(), mlir::presburger::SimplexBase::empty, mlir::presburger::Matrix::getNumRows(), mlir::presburger::Matrix::getRow(), getSamplePointIfIntegral(), mlir::presburger::SimplexBase::getSnapshot(), mlir::presburger::Matrix::identity(), mlir::presburger::SimplexBase::rollback(), and mlir::presburger::SimplexBase::var.
Referenced by mlir::presburger::IntegerRelation::findIntegerSample().
std::optional< SmallVector< Fraction, 8 > > Simplex::getRationalSample  (  )  const 
Returns the current sample point, which may contain noninteger (rational) coordinates.
Returns an empty optional when the tableau is empty.
Definition at line 1550 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().
std::optional< SmallVector< MPInt, 8 > > Simplex::getSamplePointIfIntegral  (  )  const 
Returns the current sample point if it is integral.
Otherwise, returns std::nullopt.
Definition at line 1605 of file Simplex.cpp.
References mlir::presburger::SimplexBase::empty, getRationalSample(), and mlir::presburger::SimplexBase::var.
Referenced by findIntegerSample().
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 1378 of file Simplex.cpp.
References computeOptimum(), mlir::presburger::SimplexBase::con, mlir::presburger::SimplexBase::empty, and Up.
Referenced by mlir::presburger::IntegerRelation::getBoundedDirections().
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 1388 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 getSetDifference(), and mlir::presburger::IntegerRelation::removeRedundantConstraints().
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 2129 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.
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 2183 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().
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 2173 of file Simplex.cpp.
References mlir::presburger::SimplexBase::empty, findIneqType(), and Redundant.
bool Simplex::isUnbounded  (  ) 
Returns true if the polytope is unbounded, i.e., extends to infinity in some direction.
Otherwise, returns false.
Definition at line 1450 of file Simplex.cpp.
References computeOptimum(), Down, mlir::presburger::SimplexBase::empty, Up, and mlir::presburger::SimplexBase::var.
Referenced by mlir::presburger::IntegerRelation::findIntegerSample().
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 1478 of file Simplex.cpp.
References mlir::presburger::Matrix::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::reserveRows(), mlir::presburger::SimplexBase::rowUnknown, mlir::presburger::SimplexBase::tableau, mlir::presburger::SimplexBase::unknownFromIndex(), and mlir::presburger::SimplexBase::var.

friend 