MLIR  16.0.0git
Public Types | Public Member Functions | Static Public Member Functions | Friends | List of all members
mlir::presburger::Simplex Class Reference

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:
+ Collaboration diagram for mlir::presburger::Simplex:

Public Types

enum  Direction { Direction::Up, Direction::Down }
 
enum  IneqType { IneqType::Redundant, IneqType::Cut, IneqType::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< FractioncomputeRowOptimum (Direction direction, unsigned row)
 Compute the maximum or minimum value of the given row, depending on direction. More...
 
MaybeOptimum< FractioncomputeOptimum (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...
 
Optional< SmallVector< MPInt, 8 > > findIntegerSample ()
 Returns an integer sample point if one exists, or None 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...
 
Optional< SmallVector< MPInt, 8 > > getSamplePointIfIntegral () const
 Returns the current sample point if it is integral. More...
 
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  Orientation { Orientation::Row, Orientation::Column }
 
enum  UndoLogEntry {
  UndoLogEntry::RemoveLastConstraint, UndoLogEntry::RemoveLastVariable, UndoLogEntry::UnmarkEmpty, UndoLogEntry::UnmarkLastRedundant,
  UndoLogEntry::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)
 
Optional< unsignedfindAnyPivotRow (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
 
- 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

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.

Definition at line 695 of file Simplex.h.

Member Enumeration Documentation

◆ Direction

Enumerator
Up 
Down 

Definition at line 697 of file Simplex.h.

◆ IneqType

Enumerator
Redundant 
Cut 
Separate 

Definition at line 786 of file Simplex.h.

Constructor & Destructor Documentation

◆ Simplex() [1/3]

mlir::presburger::Simplex::Simplex ( )
delete

◆ Simplex() [2/3]

mlir::presburger::Simplex::Simplex ( unsigned  nVar)
inlineexplicit

Definition at line 700 of file Simplex.h.

◆ Simplex() [3/3]

mlir::presburger::Simplex::Simplex ( const IntegerRelation constraints)
inlineexplicit

◆ ~Simplex()

mlir::presburger::Simplex::~Simplex ( )
overridedefault

Member Function Documentation

◆ addInequality()

void Simplex::addInequality ( ArrayRef< MPInt coeffs)
finalvirtual

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

References mlir::presburger::ceil(), Down, mlir::presburger::floor(), and Up.

Referenced by mlir::presburger::IntegerRelation::computeVolume().

◆ 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 None 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 1342 of file Simplex.cpp.

References mlir::presburger::SimplexBase::addRow(), mlir::presburger::SimplexBase::Column, mlir::presburger::SimplexBase::con, mlir::presburger::Empty, mlir::presburger::SimplexBase::empty, mlir::failed(), mlir::presburger::MaybeOptimum< T >::isUnbounded(), mlir::presburger::SimplexBase::Unknown::orientation, mlir::presburger::SimplexBase::pivot(), mlir::presburger::SimplexBase::Unknown::pos, mlir::presburger::SimplexBase::Unknown::restricted, and mlir::presburger::Unbounded.

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

References mlir::presburger::SimplexBase::pivot(), mlir::presburger::SimplexBase::tableau, and mlir::presburger::Unbounded.

◆ detectRedundant() [1/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 1407 of file Simplex.cpp.

References mlir::presburger::SimplexBase::Column, mlir::presburger::SimplexBase::con, 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().

◆ detectRedundant() [2/3]

void mlir::presburger::Simplex::detectRedundant ( unsigned  offset)
inline

Definition at line 762 of file Simplex.h.

References mlir::presburger::SimplexBase::con.

◆ detectRedundant() [3/3]

void mlir::presburger::Simplex::detectRedundant ( )
inline

Definition at line 766 of file Simplex.h.

References mlir::presburger::SimplexBase::con, and detectRedundant().

Referenced by detectRedundant().

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

References mlir::presburger::MaybeOptimum< T >::isBounded().

Referenced by mlir::presburger::SetCoalescer::coalesce().

◆ findIntegerSample()

Optional< SmallVector< MPInt, 8 > > Simplex::findIntegerSample ( )

Returns an integer sample point if one exists, or None 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 1971 of file Simplex.cpp.

References mlir::presburger::SimplexBase::addEquality(), mlir::presburger::SimplexBase::empty, mlir::presburger::Matrix::getNumRows(), mlir::presburger::Matrix::getRow(), mlir::presburger::SimplexBase::getSnapshot(), mlir::presburger::Matrix::identity(), mlir::presburger::SimplexBase::rollback(), and mlir::presburger::SimplexBase::var.

Referenced by mlir::presburger::IntegerRelation::findIntegerSample().

◆ getRationalSample()

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

References mlir::presburger::SimplexBase::Column, mlir::presburger::SimplexBase::empty, mlir::presburger::SimplexBase::Unknown::orientation, mlir::presburger::SimplexBase::Unknown::pos, mlir::presburger::SimplexBase::tableau, and mlir::presburger::SimplexBase::var.

Referenced by mlir::presburger::IntegerRelation::findIntegerSample().

◆ getSamplePointIfIntegral()

Optional< SmallVector< MPInt, 8 > > Simplex::getSamplePointIfIntegral ( ) const

Returns the current sample point if it is integral.

Otherwise, returns None.

Definition at line 1603 of file Simplex.cpp.

References mlir::presburger::SimplexBase::empty, and mlir::presburger::SimplexBase::var.

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

References mlir::presburger::SimplexBase::con, and mlir::presburger::SimplexBase::empty.

Referenced by mlir::presburger::IntegerRelation::getBoundedDirections().

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

References mlir::presburger::SimplexBase::con, mlir::presburger::SimplexBase::nRedundant, mlir::presburger::SimplexBase::Unknown::orientation, mlir::presburger::SimplexBase::Unknown::pos, mlir::presburger::SimplexBase::Row, mlir::presburger::SimplexBase::swapRows(), mlir::presburger::SimplexBase::undoLog, and mlir::presburger::SimplexBase::UnmarkLastRedundant.

Referenced by mlir::presburger::IntegerRelation::removeRedundantConstraints().

◆ isRationalSubsetOf()

bool Simplex::isRationalSubsetOf ( const IntegerRelation rel)

◆ isRedundantEquality()

bool Simplex::isRedundantEquality ( ArrayRef< MPInt coeffs)

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

References mlir::presburger::SimplexBase::empty, mlir::presburger::MaybeOptimum< T >::isBounded(), and mlir::presburger::MaybeOptimum< T >::isEmpty().

◆ isRedundantInequality()

bool Simplex::isRedundantInequality ( ArrayRef< MPInt coeffs)

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

References mlir::presburger::SimplexBase::empty.

Referenced by mlir::presburger::SetCoalescer::coalesce().

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

References mlir::presburger::SimplexBase::empty, and mlir::presburger::SimplexBase::var.

Referenced by mlir::presburger::IntegerRelation::findIntegerSample().

◆ makeProduct()

Simplex Simplex::makeProduct ( const Simplex a,
const Simplex b 
)
static

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 1476 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.

Friends And Related Function Documentation

◆ GBRSimplex

friend class GBRSimplex
friend

Definition at line 815 of file Simplex.h.


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