15 #ifndef MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
16 #define MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
24 #include "llvm/ADT/ArrayRef.h"
25 #include "llvm/ADT/SmallBitVector.h"
26 #include "llvm/ADT/SmallVector.h"
27 #include "llvm/Support/StringSaver.h"
28 #include "llvm/Support/raw_ostream.h"
32 namespace presburger {
211 void print(raw_ostream &os)
const;
227 const llvm::SmallBitVector &isSymbol);
240 bool oIsSymbol =
false)
273 void pivot(
unsigned row,
unsigned col);
291 unsigned addZeroRow(
bool makeRestricted =
false);
440 const llvm::SmallBitVector &isSymbol)
477 unsigned colB) const;
521 bool rowIsViolated(
unsigned row)
const;
525 std::optional<unsigned> maybeGetViolatedRow()
const;
529 std::optional<unsigned> maybeGetNonIntegralVarRow()
const;
536 unboundedDomain(
PresburgerSet::getEmpty(space.getDomainSpace())) {}
588 const llvm::SmallBitVector &isSymbol)
589 :
LexSimplexBase(constraints, isSymbol), domainPoly(symbolDomain),
590 domainSimplex(symbolDomain) {
593 assert(domainPoly.getNumVars() > 0 &&
594 "there must be some non-symbols to optimize!");
605 symbolDomain.getNumVars())) {}
614 "symbolDomain must have as many vars as constraints has symbols!");
636 std::optional<unsigned> maybeGetAlwaysViolatedRow();
640 std::optional<unsigned> maybeGetNonIntegralVarRow();
669 bool isSymbolicSampleIntegral(
unsigned row)
const;
702 :
Simplex(constraints.getNumVars()) {
733 bool isBoundedAlongConstraint(
unsigned constraintIndex);
739 bool isMarkedRedundant(
unsigned constraintIndex)
const;
761 void detectRedundant(
unsigned offset,
unsigned count);
763 assert(offset <=
con.size() &&
"invalid offset!");
764 detectRedundant(offset,
con.size() - offset);
784 std::optional<SmallVector<MPInt, 8>> findIntegerSample();
808 std::optional<SmallVector<MPInt, 8>> getSamplePointIfIntegral()
const;
812 std::optional<SmallVector<Fraction, 8>> getRationalSample()
const;
831 std::optional<Pivot> findPivot(
int row,
Direction direction)
const;
841 std::optional<unsigned> findPivotRow(std::optional<unsigned> skipRow,
842 Direction direction,
unsigned col)
const;
860 void markRowRedundant(
Unknown &u);
864 void reduceBasis(
IntMatrix &basis,
unsigned level);
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
unsigned getNumSymbolVars() const
unsigned getNumVars() const
Simplex class using the lexicographic pivot rule.
void undoLastConstraint() final
Undo the addition of the last constraint.
LexSimplexBase(const IntegerRelation &constraints)
LogicalResult moveRowUnknownToColumn(unsigned row)
Try to move the specified row to column orientation while preserving the lexicopositivity of the basi...
~LexSimplexBase() override=default
void addInequality(ArrayRef< MPInt > coeffs) final
Add an inequality to the tableau.
LexSimplexBase(const IntegerRelation &constraints, const llvm::SmallBitVector &isSymbol)
LexSimplexBase(unsigned nVar, const llvm::SmallBitVector &isSymbol)
LogicalResult addCut(unsigned row)
Given a row that has a non-integer sample value, add an inequality to cut away this fractional sample...
unsigned getLexMinPivotColumn(unsigned row, unsigned colA, unsigned colB) const
Given two potential pivot columns for a row, return the one that results in the lexicographically sma...
LexSimplexBase(unsigned nVar)
unsigned getSnapshot()
Get a snapshot of the current state. This is used for rolling back.
void appendSymbol()
Add new symbolic variables to the end of the list of variables.
A class for lexicographic optimization without any symbols.
LexSimplex(const IntegerRelation &constraints)
LexSimplex(unsigned nVar)
This class provides support for multi-precision arithmetic.
unsigned getNumRows() const
unsigned getNumColumns() const
This class represents a piece-wise MultiAffineFunction.
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
The Simplex class implements a version of the Simplex and Generalized Basis Reduction algorithms,...
unsigned addZeroRow(bool makeRestricted=false)
Add a new row to the tableau and the associated data structures.
bool isEmpty() const
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
void appendVariable(unsigned count=1)
Add new variables to the end of the list of variables.
virtual void undoLastConstraint()=0
Undo the addition of the last constraint.
SmallVector< int, 8 > rowUnknown
These hold the indexes of the unknown at a given row or column position.
SmallVector< SmallVector< int, 8 >, 8 > savedBases
Holds a vector of bases.
void intersectIntegerRelation(const IntegerRelation &rel)
Add all the constraints from the given IntegerRelation.
SmallVector< UndoLogEntry, 8 > undoLog
Holds a log of operations, used for rolling back to a previous state.
bool usingBigM
Stores whether or not a big M column is present in the tableau.
unsigned getSnapshot() const
Get a snapshot of the current state.
void print(raw_ostream &os) const
Print the tableau's internal state.
UndoLogEntry
Enum to denote operations that need to be undone during rollback.
unsigned getNumRows() const
unsigned addRow(ArrayRef< MPInt > coeffs, bool makeRestricted=false)
Add a new row to the tableau and the associated data structures.
const Unknown & unknownFromRow(unsigned row) const
Returns the unknown associated with row.
SmallVector< int, 8 > colUnknown
SmallVector< Unknown, 8 > var
virtual void addInequality(ArrayRef< MPInt > coeffs)=0
Add an inequality to the tableau.
unsigned getSnapshotBasis()
Get a snapshot of the current state including the basis.
unsigned getNumFixedCols() const
Return the number of fixed columns, as described in the constructor above, this is the number of colu...
SmallVector< Unknown, 8 > con
These hold information about each unknown.
void markEmpty()
Mark the tableau as being empty.
bool empty
This is true if the tableau has been detected to be empty, false otherwise.
void swapColumns(unsigned i, unsigned j)
void removeLastConstraintRowOrientation()
Remove the last constraint, which must be in row orientation.
virtual ~SimplexBase()=default
std::optional< unsigned > findAnyPivotRow(unsigned col)
Return any row that this column can be pivoted with, ignoring tableau consistency.
void addEquality(ArrayRef< MPInt > coeffs)
Add an equality to the tableau.
const Unknown & unknownFromColumn(unsigned col) const
Returns the unknown associated with col.
void rollback(unsigned snapshot)
Rollback to a snapshot. This invalidates all later snapshots.
IntMatrix tableau
The matrix representing the tableau.
void pivot(unsigned row, unsigned col)
Pivot the row with the column.
void swapRows(unsigned i, unsigned j)
Swap the two rows/columns in the tableau and associated data structures.
void undo(UndoLogEntry entry)
Undo the operation represented by the log entry.
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 d...
const Unknown & unknownFromIndex(int index) const
Returns the unknown associated with index.
unsigned nSymbol
The number of parameters.
unsigned nRedundant
The number of redundant rows in the tableau.
unsigned getNumVariables() const
Returns the number of variables in the tableau.
void swapRowWithCol(unsigned row, unsigned col)
Swap the row with the column in the tableau's data structures but not the tableau itself.
unsigned getNumColumns() const
unsigned getNumConstraints() const
Returns the number of constraints in the tableau.
Takes a snapshot of the simplex state on construction and rolls back to the snapshot on destruction.
SimplexRollbackScopeExit(SimplexBase &simplex)
~SimplexRollbackScopeExit()
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...
void detectRedundant(unsigned offset)
Simplex(const IntegerRelation &constraints)
~Simplex() override=default
A class to perform symbolic lexicographic optimization, i.e., to find, for every assignment to the sy...
SymbolicLexSimplex(const IntegerRelation &constraints, const IntegerPolyhedron &symbolDomain, const llvm::SmallBitVector &isSymbol)
constraints is the set for which the symbolic lexopt will be computed.
SymbolicLexSimplex(const IntegerRelation &constraints, unsigned symbolOffset, const IntegerPolyhedron &symbolDomain)
An overload to select some subrange of ids as symbols for lexopt.
SymbolicLexSimplex(const IntegerRelation &constraints, const IntegerPolyhedron &symbolDomain)
An overload to select the symbols of constraints as symbols for lexopt.
Given a simplex for a polytope, construct a new simplex whose variables are identified with a pair of...
llvm::SmallBitVector getSubrangeBitVector(unsigned len, unsigned setOffset, unsigned numSet)
Include the generated interface declarations.
This class represents an efficient way to signal success or failure.
A class to represent fractions.
An Unknown is either a variable or a constraint.
void print(raw_ostream &os) const
Unknown(Orientation oOrientation, bool oRestricted, unsigned oPos, bool oIsSymbol=false)
Represents the result of a symbolic lexicographic optimization computation.
PWMAFunction lexopt
This maps assignments of symbols to the corresponding lexopt.
SymbolicLexOpt(const PresburgerSpace &space)
PresburgerSet unboundedDomain
Contains all assignments to the symbols that made the lexopt unbounded.
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.