MLIR  17.0.0git
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 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< 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...

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

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

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.

## ◆ Direction

 strong
Enumerator
Up
Down

Definition at line 697 of file Simplex.h.

## ◆ IneqType

 strong
Enumerator
Redundant
Cut
Separate

Definition at line 786 of file Simplex.h.

## ◆ 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

Definition at line 701 of file Simplex.h.

## ◆ ~Simplex()

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

## Member Function Documentation

 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.

Referenced by getSetDifference().

## ◆ 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 2084 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 1343 of file Simplex.cpp.

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

Referenced by computeOptimum(), and detectRedundant().

## ◆ detectRedundant() [1/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().

## ◆ 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 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.

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

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

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

## ◆ 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.

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

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

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

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

Referenced by isRationalSubsetOf().

## ◆ 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 2173 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 1450 of file Simplex.cpp.

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

## ◆ GBRSimplex

 friend class GBRSimplex
friend

Definition at line 815 of file Simplex.h.

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