MLIR  19.0.0git
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
mlir::presburger::SimplexBase Class Referenceabstract

The Simplex class implements a version of the Simplex and Generalized Basis Reduction algorithms, which can perform analysis of integer sets with affine inequalities and equalities. More...

#include "mlir/Analysis/Presburger/Simplex.h"

+ Inheritance diagram for mlir::presburger::SimplexBase:

Classes

struct  Pivot
 
struct  Unknown
 An Unknown is either a variable or a constraint. More...
 

Public Member Functions

 SimplexBase ()=delete
 
virtual ~SimplexBase ()=default
 
bool isEmpty () const
 Returns true if the tableau is empty (has conflicting constraints), false otherwise. More...
 
virtual void addInequality (ArrayRef< MPInt > coeffs)=0
 Add an inequality to the tableau. 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
 

Protected Types

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

 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...
 
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)
 
virtual void undoLastConstraint ()=0
 Undo the addition of the last constraint. More...
 
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

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 implements a version of the Simplex and Generalized Basis Reduction algorithms, which can perform analysis of integer sets with affine inequalities and equalities.

A Simplex can be constructed by specifying the dimensionality of the set. It supports adding affine inequalities and equalities, and can perform emptiness checks, i.e., it can find a solution to the set of constraints if one exists, or say that the set is empty if no solution exists. Furthermore, it can find a subset of these constraints that are redundant, i.e. a subset of constraints that doesn't constrain the affine set further after adding the non-redundant constraints. The LexSimplex class provides support for computing the lexicographic minimum of an IntegerRelation. The SymbolicLexOpt class provides support for computing symbolic lexicographic minimums. All of these classes can be constructed from an IntegerRelation, and all inherit common functionality from SimplexBase.

The implementations of the Simplex and SimplexBase classes, other than the functionality for obtaining an integer sample, are based on the paper "Simplify: A Theorem Prover for Program Checking" by D. Detlefs, G. Nelson, J. B. Saxe.

We define variables, constraints, and unknowns. Consider the example of a two-dimensional set defined by 1 + 2x + 3y >= 0 and 2x - 3y >= 0. Here, x, y, are variables while 1 + 2x + 3y >= 0, 2x - 3y >= 0 are constraints. Unknowns are either variables or constraints, i.e., x, y, 1 + 2x + 3y >= 0, 2x - 3y >= 0 are all unknowns.

The implementation involves a matrix called a tableau, which can be thought of as a 2D matrix of rational numbers having number of rows equal to the number of constraints and number of columns equal to one plus the number of variables. In our implementation, instead of storing rational numbers, we store a common denominator for each row, so it is in fact a matrix of integers with number of rows equal to number of constraints and number of columns equal to two plus the number of variables. For example, instead of storing a row of three rationals [1/2, 2/3, 3], we would store [6, 3, 4, 18] since 3/6 = 1/2, 4/6 = 2/3, and 18/6 = 3.

Every row and column except the first and second columns is associated with an unknown and every unknown is associated with a row or column. An unknown associated with a row or column is said to be in row or column orientation respectively. As described above, the first column is the common denominator. The second column represents the constant term, explained in more detail below. These two are fixed columns; they always retain their position as the first and second columns. Additionally, LexSimplexBase stores a so-call big M parameter (explained below) in the third column, so LexSimplexBase has three fixed columns. Finally, SymbolicLexSimplex has nSymbol variables designated as symbols. These occupy the next nSymbol columns, viz. the columns [3, 3 + nSymbol). For more information on symbols, see LexSimplexBase and SymbolicLexSimplex.

LexSimplexBase does not directly support variables which can be negative, so we introduce the so-called big M parameter, an artificial variable that is considered to have an arbitrarily large value. We then transform the variables, say x, y, z, ... to M, M + x, M + y, M + z. Since M has been added to these variables, they are now known to have non-negative values. For more details, see the documentation for LexSimplexBase. The big M parameter is not considered a real unknown and is not stored in the var data structure; rather the tableau just has an extra fixed column for it just like the constant term.

The vectors var and con store information about the variables and constraints respectively, namely, whether they are in row or column position, which row or column they are associated with, and whether they correspond to a variable or a constraint.

An unknown is addressed by its index. If the index i is non-negative, then the variable var[i] is being addressed. If the index i is negative, then the constraint con[~i] is being addressed. Effectively this maps 0 -> var[0], 1 -> var[1], -1 -> con[0], -2 -> con[1], etc. rowUnknown[r] and colUnknown[c] are the indexes of the unknowns associated with row r and column c, respectively.

The unknowns in column position are together called the basis. Initially the basis is the set of variables – in our example above, the initial basis is x, y.

The unknowns in row position are represented in terms of the basis unknowns. If the basis unknowns are u_1, u_2, ... u_m, and a row in the tableau is d, c, a_1, a_2, ... a_m, this represents the unknown for that row as (c + a_1*u_1 + a_2*u_2 + ... + a_m*u_m)/d. In our running example, if the basis is the initial basis of x, y, then the constraint 1 + 2x + 3y >= 0 would be represented by the row [1, 1, 2, 3].

The association of unknowns to rows and columns can be changed by a process called pivoting, where a row unknown and a column unknown exchange places and the remaining row variables' representation is changed accordingly by eliminating the old column unknown in favour of the new column unknown. If we had pivoted the column for x with the row for 2x - 3y >= 0, the new row for x would be [2, 1, 3] since x = (1*(2x - 3y) + 3*y)/2. See the documentation for the pivot member function for details.

The association of unknowns to rows and columns is called the tableau configuration. The sample value of an unknown in a particular tableau configuration is its value if all the column unknowns were set to zero. Concretely, for unknowns in column position the sample value is zero; when the big M parameter is not used, for unknowns in row position the sample value is the constant term divided by the common denominator. When the big M parameter is used, if d is the denominator, p is the big M coefficient, and c is the constant term, then the sample value is (p*M + c)/d. Since M is considered to be positive infinity, this is positive (negative) infinity when p is positive or negative, and c/d when p is zero.

The tableau configuration is called consistent if the sample value of all restricted unknowns is non-negative. Initially there are no constraints, and the tableau is consistent. When a new constraint is added, its sample value in the current tableau configuration may be negative. In that case, we try to find a series of pivots to bring us to a consistent tableau configuration, i.e. we try to make the new constraint's sample value non-negative without making that of any other constraints negative. (See findPivot and findPivotRow for details.) If this is not possible, then the set of constraints is mutually contradictory and the tableau is marked empty, which means the set of constraints has no solution.

This SimplexBase class also supports taking snapshots of the current state and rolling back to prior snapshots. This works by maintaining an undo log of operations. Snapshots are just pointers to a particular location in the log, and rolling back to a snapshot is done by reverting each log entry's operation from the end until we reach the snapshot's location. SimplexBase also supports taking a snapshot including the exact set of basis unknowns; if this functionality is used, then on rolling back the exact basis will also be restored. This is used by LexSimplexBase because the lex algorithm, unlike Simplex, is sensitive to the exact basis used at a point.

Definition at line 157 of file Simplex.h.

Member Enumeration Documentation

◆ Orientation

Enumerator
Row 
Column 

Definition at line 229 of file Simplex.h.

◆ UndoLogEntry

Enum to denote operations that need to be undone during rollback.

Enumerator
RemoveLastConstraint 
RemoveLastVariable 
UnmarkEmpty 
UnmarkLastRedundant 
RestoreBasis 

Definition at line 305 of file Simplex.h.

Constructor & Destructor Documentation

◆ SimplexBase() [1/3]

mlir::presburger::SimplexBase::SimplexBase ( )
delete

◆ ~SimplexBase()

virtual mlir::presburger::SimplexBase::~SimplexBase ( )
virtualdefault

◆ SimplexBase() [2/3]

SimplexBase::SimplexBase ( unsigned  nVar,
bool  mustUseBigM 
)
protected

Construct a SimplexBase with the specified number of variables and fixed columns.

The first overload should be used when there are nosymbols. With the second overload, the specified range of vars will be marked as symbols. With the third overload, isSymbol is a bitmask denoting which vars are symbols. The size of isSymbol must be nVar.

For example, Simplex uses two fixed columns: the denominator and the constant term, whereas LexSimplex has an extra fixed column for the so-called big M parameter. For more information see the documentation for LexSimplex.

Definition at line 50 of file Simplex.cpp.

References Column, colUnknown, getNumFixedCols(), nullIndex, and var.

◆ SimplexBase() [3/3]

SimplexBase::SimplexBase ( unsigned  nVar,
bool  mustUseBigM,
const llvm::SmallBitVector &  isSymbol 
)
protected

Definition at line 61 of file Simplex.cpp.

References getNumFixedCols(), nSymbol, swapColumns(), and var.

Member Function Documentation

◆ addDivisionVariable()

void SimplexBase::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.

We add the usual floor division constraints: 0 <= coeffs - denom*q <= denom - 1, where q is the new division variable.

denom must be positive.

This constrains the remainder coeffs - denom*q to be in the range [0, denom - 1], which fixes the integer value of the quotient q.

Definition at line 1298 of file Simplex.cpp.

References addInequality(), and appendVariable().

◆ addEquality()

void SimplexBase::addEquality ( ArrayRef< MPInt coeffs)

Add an equality to the tableau.

If coeffs is c_0, c_1, ... c_n, where n is the current number of variables, then the corresponding equality is c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0.

If coeffs is c_0, c_1, ... c_n, where n is the current number of variables, then the corresponding equality is c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0.

We simply add two opposing inequalities, which force the expression to be zero.

Definition at line 1119 of file Simplex.cpp.

References addInequality().

Referenced by mlir::presburger::Simplex::findIntegerSample(), and intersectIntegerRelation().

◆ addInequality()

virtual void mlir::presburger::SimplexBase::addInequality ( ArrayRef< MPInt coeffs)
pure virtual

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.

Implemented in mlir::presburger::Simplex, and mlir::presburger::LexSimplexBase.

Referenced by addDivisionVariable(), addEquality(), and intersectIntegerRelation().

◆ addRow()

unsigned SimplexBase::addRow ( ArrayRef< MPInt coeffs,
bool  makeRestricted = false 
)
protected

Add a new row to the tableau and the associated data structures.

Add a new row to the tableau corresponding to the given constant term and list of coefficients.

The new row is considered to be a constraint; the new Unknown lives in con.

Returns the index of the new Unknown in con.

The coefficients are specified as a vector of (variable index, coefficient) pairs.

Definition at line 119 of file Simplex.cpp.

References addZeroRow(), Column, con, getNumColumns(), getNumFixedCols(), mlir::presburger::lcm(), mlir::presburger::IntMatrix::normalizeRow(), tableau, usingBigM, and var.

Referenced by mlir::presburger::LexSimplexBase::addInequality(), mlir::presburger::Simplex::addInequality(), and mlir::presburger::Simplex::computeOptimum().

◆ addZeroRow()

unsigned SimplexBase::addZeroRow ( bool  makeRestricted = false)
protected

Add a new row to the tableau and the associated data structures.

The row is initialized to zero. Returns the index of the added row.

Definition at line 105 of file Simplex.cpp.

References mlir::presburger::Matrix< T >::appendExtraRow(), con, getNumRows(), RemoveLastConstraint, Row, rowUnknown, tableau, and undoLog.

Referenced by mlir::presburger::LexSimplexBase::addCut(), and addRow().

◆ appendVariable()

void SimplexBase::appendVariable ( unsigned  count = 1)

Add new variables to the end of the list of variables.

Definition at line 1315 of file Simplex.cpp.

References Column, colUnknown, getNumColumns(), RemoveLastVariable, mlir::presburger::Matrix< T >::resizeHorizontally(), tableau, undoLog, and var.

Referenced by addDivisionVariable(), and mlir::presburger::LexSimplexBase::appendSymbol().

◆ dump()

void SimplexBase::dump ( ) const

Definition at line 2155 of file Simplex.cpp.

References print().

◆ findAnyPivotRow()

std::optional< unsigned > SimplexBase::findAnyPivotRow ( unsigned  col)
protected

Return any row that this column can be pivoted with, ignoring tableau consistency.

Returns an empty optional if no pivot is possible, which happens only when the column unknown is a variable and no constraint has a non-zero coefficient for it.

Definition at line 1169 of file Simplex.cpp.

References getNumRows(), nRedundant, and tableau.

Referenced by mlir::presburger::LexSimplexBase::undoLastConstraint().

◆ getNumColumns()

unsigned mlir::presburger::SimplexBase::getNumColumns ( ) const
inlineprotected

◆ getNumConstraints()

unsigned SimplexBase::getNumConstraints ( ) const

Returns the number of constraints in the tableau.

Definition at line 1128 of file Simplex.cpp.

References con.

Referenced by mlir::presburger::Simplex::makeProduct().

◆ getNumFixedCols()

unsigned mlir::presburger::SimplexBase::getNumFixedCols ( ) const
inlineprotected

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.

Definition at line 325 of file Simplex.h.

References usingBigM.

Referenced by addRow(), pivot(), SimplexBase(), and undo().

◆ getNumRows()

unsigned mlir::presburger::SimplexBase::getNumRows ( ) const
inlineprotected

◆ getNumVariables()

unsigned SimplexBase::getNumVariables ( ) const

Returns the number of variables in the tableau.

Definition at line 1127 of file Simplex.cpp.

References var.

Referenced by intersectIntegerRelation(), and mlir::presburger::Simplex::makeProduct().

◆ getSnapshot()

unsigned SimplexBase::getSnapshot ( ) const

Get a snapshot of the current state.

Return a snapshot of the current state.

This is used for rolling back. The same basis will not necessarily be restored on rolling back. The snapshot only captures the set of variables and constraints present in the Simplex.

This is just the current size of the undo log.

Definition at line 1132 of file Simplex.cpp.

References undoLog.

Referenced by mlir::presburger::Simplex::findIntegerSample(), getSetDifference(), and mlir::presburger::SimplexRollbackScopeExit::SimplexRollbackScopeExit().

◆ getSnapshotBasis()

unsigned SimplexBase::getSnapshotBasis ( )

Get a snapshot of the current state including the basis.

When rolling back, the exact basis will be restored.

Definition at line 1134 of file Simplex.cpp.

References colUnknown, nullIndex, RestoreBasis, savedBases, and undoLog.

Referenced by mlir::presburger::LexSimplexBase::getSnapshot().

◆ intersectIntegerRelation()

void SimplexBase::intersectIntegerRelation ( const IntegerRelation rel)

◆ isEmpty()

bool SimplexBase::isEmpty ( ) const

◆ markEmpty()

void SimplexBase::markEmpty ( )

Mark the tableau as being empty.

Mark this tableau empty and push an entry to the undo stack.

Definition at line 1089 of file Simplex.cpp.

References empty, undoLog, and UnmarkEmpty.

Referenced by mlir::presburger::Simplex::addInequality(), and mlir::presburger::LexSimplex::findRationalLexMin().

◆ pivot() [1/2]

void SimplexBase::pivot ( Pivot  pair)
protected

◆ pivot() [2/2]

void SimplexBase::pivot ( unsigned  pivotRow,
unsigned  pivotCol 
)
protected

Pivot the row with the column.

Pivot pivotRow and pivotCol.

Let R be the pivot row unknown and let C be the pivot col unknown. Since initially R = a*C + sum b_i * X_i (where the sum is over the other column's unknowns, x_i) C = (R - (sum b_i * X_i))/a

Let u be some other row unknown. u = c*C + sum d_i * X_i So u = c*(R - sum b_i * X_i)/a + sum d_i * X_i

This results in the following transform: pivot col other col pivot col other col pivot row a b -> pivot row 1/a -b/a other row c d other row c/a d - bc/a

Taking into account the common denominators p and q:

       pivot col    other col                    pivot col   other col

pivot row a/p b/p -> pivot row p/a -b/a other row c/q d/q other row cp/aq (da - bc)/aq

The pivot row transform is accomplished be swapping a with the pivot row's common denominator and negating the pivot row except for the pivot column element.

Definition at line 947 of file Simplex.cpp.

References getNumColumns(), getNumFixedCols(), getNumRows(), mlir::presburger::IntMatrix::normalizeRow(), swapRowWithCol(), tableau, and unknownFromColumn().

Referenced by mlir::presburger::Simplex::computeRowOptimum(), mlir::presburger::Simplex::detectRedundant(), mlir::presburger::LexSimplexBase::moveRowUnknownToColumn(), pivot(), undo(), and mlir::presburger::LexSimplexBase::undoLastConstraint().

◆ print()

void SimplexBase::print ( raw_ostream &  os) const

Print the tableau's internal state.

Definition at line 2120 of file Simplex.cpp.

References colUnknown, con, empty, getNumColumns(), getNumRows(), rowUnknown, tableau, and var.

Referenced by dump().

◆ removeLastConstraintRowOrientation()

void SimplexBase::removeLastConstraintRowOrientation ( )
protected

Remove the last constraint, which must be in row orientation.

Definition at line 1146 of file Simplex.cpp.

References con, getNumRows(), mlir::presburger::Matrix< T >::resizeVertically(), Row, rowUnknown, swapRows(), and tableau.

Referenced by mlir::presburger::LexSimplexBase::undoLastConstraint().

◆ rollback()

void SimplexBase::rollback ( unsigned  snapshot)

Rollback to a snapshot. This invalidates all later snapshots.

Rollback to the specified snapshot.

We undo all the log entries until the log size when the snapshot was taken is reached.

Definition at line 1285 of file Simplex.cpp.

References undo(), and undoLog.

Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), and mlir::presburger::Simplex::findIntegerSample().

◆ swapColumns()

void SimplexBase::swapColumns ( unsigned  i,
unsigned  j 
)
protected

◆ swapRows()

void SimplexBase::swapRows ( unsigned  i,
unsigned  j 
)
protected

Swap the two rows/columns in the tableau and associated data structures.

Definition at line 1068 of file Simplex.cpp.

References mlir::presburger::SimplexBase::Unknown::pos, rowUnknown, mlir::presburger::Matrix< T >::swapRows(), tableau, and unknownFromRow().

Referenced by removeLastConstraintRowOrientation().

◆ swapRowWithCol()

void SimplexBase::swapRowWithCol ( unsigned  row,
unsigned  col 
)
protected

Swap the row with the column in the tableau's data structures but not the tableau itself.

Swap the associated unknowns for the row and the column.

This is used by pivot.

First we swap the index associated with the row and column. Then we update the unknowns to reflect their new position and orientation.

Definition at line 910 of file Simplex.cpp.

References Column, colUnknown, mlir::presburger::SimplexBase::Unknown::orientation, mlir::presburger::SimplexBase::Unknown::pos, Row, rowUnknown, unknownFromColumn(), and unknownFromRow().

Referenced by pivot().

◆ undo()

void SimplexBase::undo ( UndoLogEntry  entry)
protected

◆ undoLastConstraint()

virtual void mlir::presburger::SimplexBase::undoLastConstraint ( )
protectedpure virtual

Undo the addition of the last constraint.

This will only be called from undo, when rolling back.

Implemented in mlir::presburger::LexSimplexBase.

Referenced by undo().

◆ unknownFromColumn() [1/2]

Simplex::Unknown & SimplexBase::unknownFromColumn ( unsigned  col)
protected

Returns the unknown associated with col.

Definition at line 95 of file Simplex.cpp.

References colUnknown, getNumColumns(), and unknownFromIndex().

◆ unknownFromColumn() [2/2]

const Simplex::Unknown & SimplexBase::unknownFromColumn ( unsigned  col) const
protected

Returns the unknown associated with col.

Definition at line 80 of file Simplex.cpp.

References colUnknown, getNumColumns(), and unknownFromIndex().

Referenced by pivot(), swapColumns(), and swapRowWithCol().

◆ unknownFromIndex() [1/2]

Simplex::Unknown & SimplexBase::unknownFromIndex ( int  index)
protected

Returns the unknown associated with index.

Definition at line 90 of file Simplex.cpp.

References con, nullIndex, and var.

◆ unknownFromIndex() [2/2]

const Simplex::Unknown & SimplexBase::unknownFromIndex ( int  index) const
protected

Returns the unknown associated with index.

Definition at line 75 of file Simplex.cpp.

References con, nullIndex, and var.

Referenced by mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::makeProduct(), undo(), unknownFromColumn(), and unknownFromRow().

◆ unknownFromRow() [1/2]

Simplex::Unknown & SimplexBase::unknownFromRow ( unsigned  row)
protected

Returns the unknown associated with row.

Definition at line 100 of file Simplex.cpp.

References getNumRows(), rowUnknown, and unknownFromIndex().

◆ unknownFromRow() [2/2]

const Simplex::Unknown & SimplexBase::unknownFromRow ( unsigned  row) const
protected

Returns the unknown associated with row.

Definition at line 85 of file Simplex.cpp.

References getNumRows(), rowUnknown, and unknownFromIndex().

Referenced by swapRows(), and swapRowWithCol().

Member Data Documentation

◆ colUnknown

SmallVector<int, 8> mlir::presburger::SimplexBase::colUnknown
protected

◆ con

SmallVector<Unknown, 8> mlir::presburger::SimplexBase::con
protected

◆ empty

bool mlir::presburger::SimplexBase::empty
protected

◆ nRedundant

unsigned mlir::presburger::SimplexBase::nRedundant
protected

The number of redundant rows in the tableau.

These are the first nRedundant rows.

Definition at line 334 of file Simplex.h.

Referenced by findAnyPivotRow(), mlir::presburger::Simplex::isMarkedRedundant(), mlir::presburger::Simplex::makeProduct(), and undo().

◆ nSymbol

unsigned mlir::presburger::SimplexBase::nSymbol
protected

The number of parameters.

This must be consistent with the number of Unknowns in var below that have isSymbol set to true.

Definition at line 338 of file Simplex.h.

Referenced by mlir::presburger::LexSimplexBase::addCut(), mlir::presburger::LexSimplexBase::appendSymbol(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::LexSimplexBase::moveRowUnknownToColumn(), SimplexBase(), and undo().

◆ rowUnknown

SmallVector<int, 8> mlir::presburger::SimplexBase::rowUnknown
protected

These hold the indexes of the unknown at a given row or column position.

We keep these as signed integers since that makes it convenient to check if an index corresponds to a variable or a constraint by checking the sign.

colUnknown is padded with two null indexes at the front since the first two columns don't correspond to any unknowns.

Definition at line 362 of file Simplex.h.

Referenced by addZeroRow(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::Simplex::makeProduct(), print(), removeLastConstraintRowOrientation(), swapRows(), swapRowWithCol(), and unknownFromRow().

◆ savedBases

SmallVector<SmallVector<int, 8>, 8> mlir::presburger::SimplexBase::savedBases
protected

Holds a vector of bases.

The ith saved basis is the basis that should be restored when processing the ith occurrance of UndoLogEntry::RestoreBasis in undoLog. This is used by getSnapshotBasis.

Definition at line 353 of file Simplex.h.

Referenced by getSnapshotBasis(), and undo().

◆ tableau

IntMatrix mlir::presburger::SimplexBase::tableau
protected

◆ undoLog

SmallVector<UndoLogEntry, 8> mlir::presburger::SimplexBase::undoLog
protected

Holds a log of operations, used for rolling back to a previous state.

Definition at line 348 of file Simplex.h.

Referenced by addZeroRow(), appendVariable(), getSnapshot(), getSnapshotBasis(), markEmpty(), and rollback().

◆ usingBigM

bool mlir::presburger::SimplexBase::usingBigM
protected

Stores whether or not a big M column is present in the tableau.

Definition at line 330 of file Simplex.h.

Referenced by addRow(), and getNumFixedCols().

◆ var

SmallVector<Unknown, 8> mlir::presburger::SimplexBase::var
protected

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