12 #include "llvm/Support/Compiler.h"
17 using namespace presburger;
27 assert(a.size() == b.size());
29 res.reserve(a.size());
30 for (
unsigned i = 0, e = a.size(); i < e; ++i)
31 res.push_back(a[i] + scale * b[i]);
36 : usingBigM(mustUseBigM), nRedundant(0), nSymbol(0),
37 tableau(0, getNumFixedCols() + nVar), empty(false) {
39 for (
unsigned i = 0; i < nVar; ++i) {
47 const llvm::SmallBitVector &isSymbol)
49 assert(isSymbol.size() == nVar &&
"invalid bitmask!");
53 for (
unsigned symbolIdx : isSymbol.set_bits()) {
54 var[symbolIdx].isSymbol =
true;
61 assert(index !=
nullIndex &&
"nullIndex passed to unknownFromIndex");
62 return index >= 0 ?
var[index] :
con[~index];
76 assert(index !=
nullIndex &&
"nullIndex passed to unknownFromIndex");
77 return index >= 0 ?
var[index] :
con[~index];
105 assert(coeffs.size() ==
var.size() + 1 &&
106 "Incorrect number of coefficients!");
108 "inconsistent column count!");
111 tableau(newRow, 1) = coeffs.back();
128 for (
unsigned i = 0; i < coeffs.size() - 1; ++i)
129 if (!
var[i].isSymbol)
130 bigMCoeff -= coeffs[i];
132 tableau(newRow, 2) = bigMCoeff;
136 for (
unsigned i = 0; i <
var.size(); ++i) {
137 unsigned pos =
var[i].pos;
159 nRowCoeff *
tableau(newRow, col) + idxRowCoeff *
tableau(pos, col);
164 return con.size() - 1;
168 bool signMatchesDirection(
const MPInt &elem,
Direction direction) {
169 assert(elem != 0 &&
"elem should not be 0");
170 return direction == Direction::Up ? elem > 0 : elem < 0;
218 if (restoreRationalConsistency().
failed()) {
222 return getRationalSample();
274 std::optional<unsigned> LexSimplex::maybeGetNonIntegralVarRow()
const {
275 for (
const Unknown &u :
var) {
281 unsigned row = u.pos;
290 if (restoreRationalConsistency().
failed())
294 while (std::optional<unsigned> maybeRow = maybeGetNonIntegralVarRow()) {
307 if (restoreRationalConsistency().
failed())
312 assert(!sample.
isEmpty() &&
"If we reached here the sample should exist!");
315 return llvm::to_vector<8>(
330 SymbolicLexSimplex::getSymbolicSampleNumerator(
unsigned row)
const {
333 for (
unsigned col = 3; col < 3 +
nSymbol; ++col)
334 sample.push_back(
tableau(row, col));
335 sample.push_back(
tableau(row, 1));
340 SymbolicLexSimplex::getSymbolicSampleIneq(
unsigned row)
const {
350 var.back().isSymbol =
true;
355 assert(divisor > 0 &&
"divisor must be positive!");
356 return llvm::all_of(range,
357 [divisor](
const MPInt &x) {
return x % divisor == 0; });
360 bool SymbolicLexSimplex::isSymbolicSampleIntegral(
unsigned row)
const {
362 return tableau(row, 1) % denom == 0 &&
399 LogicalResult SymbolicLexSimplex::addSymbolicCut(
unsigned row) {
410 divCoeffs.reserve(
nSymbol + 1);
412 for (
unsigned col = 3; col < 3 +
nSymbol; ++col)
413 divCoeffs.push_back(
mod(-
tableau(row, col), divDenom));
414 divCoeffs.push_back(
mod(-
tableau(row, 1), divDenom));
429 for (
unsigned col = 3; col < 3 +
nSymbol - 1; ++col)
438 void SymbolicLexSimplex::recordOutput(
SymbolicLexOpt &result)
const {
441 for (
const Unknown &u :
var) {
453 if (
tableau(u.pos, 2) < denom) {
460 assert(
tableau(u.pos, 2) == denom &&
461 "Coefficient of M should not be greater than 1!");
464 for (
MPInt &elem : sample) {
465 assert(elem % denom == 0 &&
"coefficients must be integral!");
468 output.appendExtraRow(sample);
480 std::optional<unsigned> SymbolicLexSimplex::maybeGetAlwaysViolatedRow() {
483 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row)
487 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row) {
498 std::optional<unsigned> SymbolicLexSimplex::maybeGetNonIntegralVarRow() {
499 for (
const Unknown &u :
var) {
502 assert(!u.isSymbol &&
"Symbol should not be in row orientation!");
503 if (!isSymbolicSampleIntegral(u.pos))
512 while (std::optional<unsigned> row = maybeGetAlwaysViolatedRow())
541 unsigned domainSnapshot;
547 assert(level >= stack.size());
548 if (level > stack.size()) {
555 if (doNonBranchingPivots().
failed()) {
562 unsigned splitRow = 0;
563 for (
unsigned e =
getNumRows(); splitRow < e; ++splitRow) {
566 assert(
tableau(splitRow, 2) == 0 &&
567 "Non-branching pivots should have been handled already!");
569 symbolicSample = getSymbolicSampleIneq(splitRow);
577 "Non-branching pivots should have been handled already!");
582 unsigned domainSnapshot = domainSimplex.
getSnapshot();
607 {splitIndex, snapshot, domainSnapshot, domainPolyCounts});
614 if (std::optional<unsigned> row = maybeGetNonIntegralVarRow()) {
615 if (addSymbolicCut(*row).
failed()) {
626 recordOutput(result);
631 if (level == stack.size()) {
633 const StackFrame &frame = stack.back();
634 domainPoly.
truncate(frame.domainPolyCounts);
635 domainSimplex.
rollback(frame.domainSnapshot);
645 "The split row should have been returned to row orientation!");
669 bool LexSimplex::rowIsViolated(
unsigned row)
const {
677 std::optional<unsigned> LexSimplex::maybeGetViolatedRow()
const {
678 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row)
679 if (rowIsViolated(row))
690 while (std::optional<unsigned> maybeViolatedRow = maybeGetViolatedRow())
759 std::optional<unsigned> maybeColumn;
770 pivot(row, *maybeColumn);
775 unsigned colB)
const {
820 auto getSampleChangeCoeffForVar = [
this, row](
unsigned col,
842 Fraction changeA = getSampleChangeCoeffForVar(colA, u);
843 Fraction changeB = getSampleChangeCoeffForVar(colB, u);
844 if (changeA < changeB)
846 if (changeA > changeB)
867 std::optional<SimplexBase::Pivot>
868 Simplex::findPivot(
int row,
Direction direction)
const {
869 std::optional<unsigned> col;
876 !signMatchesDirection(elem, direction))
886 tableau(row, *col) < 0 ? flippedDirection(direction) : direction;
887 std::optional<unsigned> maybePivotRow = findPivotRow(row, newDirection, *col);
888 return Pivot{maybePivotRow.value_or(row), *col};
933 assert(pivotCol >=
getNumFixedCols() &&
"Refusing to pivot invalid column");
939 if (
tableau(pivotRow, 0) < 0) {
945 for (
unsigned col = 1, e =
getNumColumns(); col < e; ++col) {
953 for (
unsigned row = 0, numRows =
getNumRows(); row < numRows; ++row) {
956 if (
tableau(row, pivotCol) == 0)
959 for (
unsigned col = 1, numCols =
getNumColumns(); col < numCols; ++col) {
976 "unknown should be in row position");
978 while (
tableau(u.pos, 1) < 0) {
979 std::optional<Pivot> maybePivot = findPivot(u.pos,
Direction::Up);
1012 std::optional<unsigned> Simplex::findPivotRow(std::optional<unsigned> skipRow,
1014 unsigned col)
const {
1015 std::optional<unsigned> retRow;
1020 MPInt retElem, retConst;
1022 if (skipRow && row == *skipRow)
1029 if (signMatchesDirection(elem, direction))
1036 retConst = constTerm;
1040 MPInt diff = retConst * elem - constTerm * retElem;
1042 (diff != 0 && !signMatchesDirection(diff, direction))) {
1045 retConst = constTerm;
1064 "Invalid columns provided!");
1092 unsigned conIndex =
addRow(coeffs,
true);
1107 for (
const MPInt &coeff : coeffs)
1108 negatedCoeffs.emplace_back(-coeff);
1123 basis.push_back(index);
1163 void Simplex::undoLastConstraint() {
1174 unsigned column =
con.back().pos;
1175 if (std::optional<unsigned> maybeRow =
1177 pivot(*maybeRow, column);
1178 }
else if (std::optional<unsigned> maybeRow =
1180 pivot(*maybeRow, column);
1183 assert(row &&
"Pivot should always exist for a constraint!");
1184 pivot(*row, column);
1200 unsigned column =
con.back().pos;
1202 assert(row &&
"Pivot should always exist for a constraint!");
1203 pivot(*row, column);
1224 "Variable to be removed must be in column orientation!");
1226 if (
var.back().isSymbol)
1240 assert(!
savedBases.empty() &&
"No bases saved!");
1245 for (
int index : basis) {
1252 "Column should not be a fixed column!");
1253 if (llvm::is_contained(basis,
colUnknown[col]))
1271 while (
undoLog.size() > snapshot) {
1284 const MPInt &denom) {
1285 assert(denom > 0 &&
"Denominator must be positive!");
1289 MPInt constTerm = ineq.back();
1290 ineq.back() = -denom;
1291 ineq.push_back(constTerm);
1294 for (
MPInt &coeff : ineq)
1296 ineq.back() += denom - 1;
1303 var.reserve(
var.size() + count);
1305 for (
unsigned i = 0; i < count; ++i) {
1317 "IntegerRelation must have same dimensionality as simplex");
1327 while (std::optional<Pivot> maybePivot = findPivot(row, direction)) {
1330 if (maybePivot->row == row)
1349 unsigned conIndex =
addRow(coeffs);
1350 unsigned row =
con[conIndex].pos;
1359 unsigned column = u.pos;
1360 std::optional<unsigned> pivotRow = findPivotRow({}, direction, column);
1365 pivot(*pivotRow, column);
1368 unsigned row = u.pos;
1372 if (
failed(restoreRow(u)))
1373 llvm_unreachable(
"Could not restore row!");
1379 assert(!
empty &&
"It is not meaningful to ask whether a direction is bounded "
1380 "in an empty set.");
1398 void Simplex::markRowRedundant(Unknown &u) {
1400 "Unknown should be in row position!");
1401 assert(u.pos >=
nRedundant &&
"Unknown is already marked redundant!");
1409 assert(offset + count <=
con.size() &&
"invalid range!");
1423 for (
unsigned i = 0; i < count; ++i) {
1426 unsigned column = u.
pos;
1427 std::optional<unsigned> pivotRow =
1433 pivot(*pivotRow, column);
1436 unsigned row = u.
pos;
1441 if (
failed(restoreRow(u)))
1442 llvm_unreachable(
"Could not restore non-redundant row!");
1446 markRowRedundant(u);
1455 for (
unsigned i = 0; i <
var.size(); ++i) {
1488 result.reserve(v.size() + w.size());
1489 result.insert(result.end(), v.begin(), v.end());
1490 result.insert(result.end(), w.begin(), w.end());
1496 auto indexFromBIndex = [&](
int index) {
1513 auto appendRowFromA = [&](
unsigned row) {
1515 for (
unsigned col = 0, e = a.
getNumColumns(); col < e; ++col)
1524 auto appendRowFromB = [&](
unsigned row) {
1530 for (
unsigned col = 2, e = b.
getNumColumns(); col < e; ++col)
1538 for (
unsigned row = 0; row < a.
nRedundant; ++row)
1539 appendRowFromA(row);
1540 for (
unsigned row = 0; row < b.
nRedundant; ++row)
1541 appendRowFromB(row);
1543 appendRowFromA(row);
1545 appendRowFromB(row);
1555 sample.reserve(
var.size());
1560 sample.emplace_back(0, 1);
1565 sample.emplace_back(
tableau(u.pos, 1), denom);
1580 sample.reserve(
var.size());
1582 for (
const Unknown &u :
var) {
1598 if (
tableau(u.pos, 2) != denom)
1600 sample.emplace_back(
tableau(u.pos, 1), denom);
1613 integerSample.reserve(
var.size());
1614 for (
const Fraction &coord : rationalSample) {
1616 if (coord.num % coord.den != 0)
1618 integerSample.push_back(coord.num / coord.den);
1620 return integerSample;
1638 : simplex(
Simplex::makeProduct(originalSimplex, originalSimplex)),
1639 simplexConstraintOffset(simplex.getNumConstraints()) {}
1645 assert(llvm::any_of(dir, [](
const MPInt &x) {
return x != 0; }) &&
1646 "Direction passed is the zero vector!");
1647 snapshotStack.push_back(simplex.getSnapshot());
1648 simplex.addEquality(getCoeffsForDirection(dir));
1653 simplex.computeOptimum(Direction::Up, getCoeffsForDirection(dir));
1654 assert(maybeWidth.
isBounded() &&
"Width should be bounded!");
1670 unsigned conIndex = simplex.addRow(getCoeffsForDirection(dir));
1671 unsigned row = simplex.con[conIndex].pos;
1674 assert(maybeWidth.
isBounded() &&
"Width should be bounded!");
1675 dualDenom = simplex.tableau(row, 0);
1680 for (
unsigned i = simplexConstraintOffset; i < conIndex; i += 2) {
1701 assert(!(simplex.con[i].orientation == Orientation::Column &&
1702 simplex.con[i + 1].orientation == Orientation::Column) &&
1703 "Both inequalities for the equality cannot be in column "
1705 if (simplex.con[i].orientation == Orientation::Column)
1706 dual.push_back(-simplex.tableau(row, simplex.con[i].pos));
1707 else if (simplex.con[i + 1].orientation == Orientation::Column)
1708 dual.push_back(simplex.tableau(row, simplex.con[i + 1].pos));
1710 dual.emplace_back(0);
1720 assert(!snapshotStack.empty() &&
"Snapshot stack is empty!");
1721 simplex.rollback(snapshotStack.back());
1722 snapshotStack.pop_back();
1731 assert(2 * dir.size() == simplex.getNumVariables() &&
1732 "Direction vector has wrong dimensionality");
1734 coeffs.reserve(2 * dir.size());
1735 for (
const MPInt &coeff : dir)
1736 coeffs.push_back(-coeff);
1737 coeffs.emplace_back(0);
1744 unsigned simplexConstraintOffset;
1804 void Simplex::reduceBasis(
IntMatrix &basis,
unsigned level) {
1833 auto updateBasisWithUAndGetFCandidate = [&](
unsigned i) ->
Fraction {
1834 assert(i < level + dual.size() &&
"dual_i is not known!");
1838 if (dual[i - level] % dualDenom != 0) {
1840 MPInt candidateDualDenom[2];
1844 widthI[0] = gbrSimplex.computeWidthAndDuals(
1845 basis.
getRow(i + 1), candidateDual[0], candidateDualDenom[0]);
1850 widthI[1] = gbrSimplex.computeWidthAndDuals(
1851 basis.
getRow(i + 1), candidateDual[1], candidateDualDenom[1]);
1853 unsigned j = widthI[0] < widthI[1] ? 0 : 1;
1869 "Computed u value does not minimize the width!");
1874 "Computed u value does not minimize the width!");
1876 dual = std::move(candidateDual[
j]);
1877 dualDenom = candidateDualDenom[
j];
1881 assert(i + 1 - level < width.size() &&
"width_{i+1} wasn't saved");
1885 assert(gbrSimplex.computeWidth(basis.
getRow(i + 1)) ==
1886 width[i + 1 - level]);
1887 return width[i + 1 - level];
1894 if (i >= level + width.size()) {
1899 assert((i == 0 || i - 1 < level + width.size()) &&
1900 "We are at level i but we don't know the value of width_{i-1}");
1905 assert(i == level &&
"This case should only occur when i == level");
1907 gbrSimplex.computeWidthAndDuals(basis.
getRow(i), dual, dualDenom));
1910 if (i >= level + dual.size()) {
1911 assert(i + 1 >= level + width.size() &&
1912 "We don't know dual_i but we know width_{i+1}");
1914 gbrSimplex.addEqualityForDirection(basis.
getRow(i));
1915 width.push_back(gbrSimplex.computeWidthAndDuals(basis.
getRow(i + 1), dual,
1917 gbrSimplex.removeLastEquality();
1921 Fraction widthICandidate = updateBasisWithUAndGetFCandidate(i);
1922 if (widthICandidate < epsilon * width[i - level]) {
1924 width[i - level] = widthICandidate;
1927 width.resize(i - level + 1);
1933 gbrSimplex.removeLastEquality();
1940 gbrSimplex.addEqualityForDirection(basis.
getRow(i));
1977 unsigned nDims =
var.size();
1991 while (level != -1u) {
2001 if (level >= upperBoundStack.size()) {
2007 llvm::to_vector<8>(basis.
getRow(level));
2008 basisCoeffs.emplace_back(0);
2014 if (minRoundedUp.isEmpty() || maxRoundedDown.isEmpty()) {
2015 assert((minRoundedUp.isEmpty() && maxRoundedDown.isEmpty()) &&
2016 "If one bound is empty, both should be.");
2017 snapshotStack.pop_back();
2018 nextValueStack.pop_back();
2019 upperBoundStack.pop_back();
2025 assert((minRoundedUp.isBounded() && maxRoundedDown.isBounded()) &&
2026 "Polyhedron should be bounded!");
2031 return *maybeSample;
2033 if (*minRoundedUp < *maxRoundedDown) {
2034 reduceBasis(basis, level);
2035 basisCoeffs = llvm::to_vector<8>(basis.
getRow(level));
2036 basisCoeffs.emplace_back(0);
2037 std::tie(minRoundedUp, maxRoundedDown) =
2045 nextValueStack.push_back(*minRoundedUp);
2046 upperBoundStack.push_back(*maxRoundedDown);
2049 assert((snapshotStack.size() - 1 == level &&
2050 nextValueStack.size() - 1 == level &&
2051 upperBoundStack.size() - 1 == level) &&
2052 "Mismatched variable stack sizes!");
2058 MPInt nextValue = nextValueStack.back();
2059 ++nextValueStack.back();
2060 if (nextValue > upperBoundStack.back()) {
2063 snapshotStack.pop_back();
2064 nextValueStack.pop_back();
2065 upperBoundStack.pop_back();
2072 basis.
getRow(level).end());
2073 basisCoeffs.push_back(-nextValue);
2089 return {minRoundedUp, maxRoundedDown};
2095 os <<
"Simplex marked empty!\n";
2097 for (
unsigned i = 0; i <
var.size(); ++i) {
2103 for (
unsigned i = 0; i <
con.size(); ++i) {
2109 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row) {
2115 os <<
"c0: denom, c1: const";
2117 os <<
", c" << col <<
": " <<
colUnknown[col];
2119 for (
unsigned row = 0, numRows =
getNumRows(); row < numRows; ++row) {
2120 for (
unsigned col = 0, numCols =
getNumColumns(); col < numCols; ++col)
2121 os <<
tableau(row, col) <<
'\t';
2175 "It is not meaningful to ask about redundancy in an empty set!");
2185 "It is not meaningful to ask about redundancy in an empty set!");
2189 "Optima should be non-empty for a non-empty set");
static Value max(ImplicitLocOpBuilder &builder, Value value, Value bound)
static LLVM_ATTRIBUTE_UNUSED SmallVector< MPInt, 8 > scaleAndAddForAssert(ArrayRef< MPInt > a, const MPInt &scale, ArrayRef< MPInt > b)
static bool isRangeDivisibleBy(ArrayRef< MPInt > range, const MPInt &divisor)
MPInt normalizeRow(unsigned row, unsigned nCols)
Divide the first nCols of the specified row by their GCD.
static IntMatrix identity(unsigned dimension)
Return the identity matrix of the specified dimension.
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
ArrayRef< MPInt > getEquality(unsigned idx) const
void addInequality(ArrayRef< MPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
void truncate(const CountsSnapshot &counts)
CountsSnapshot getCounts() const
unsigned getNumSymbolVars() const
void addLocalFloorDiv(ArrayRef< MPInt > dividend, const MPInt &divisor)
Adds a new local variable as the floordiv of an affine function of other variables,...
ArrayRef< MPInt > getInequality(unsigned idx) const
unsigned getNumVars() const
unsigned getNumLocalVars() const
DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const
Returns a DivisonRepr representing the division representation of local variables in the constraint s...
unsigned getNumInequalities() const
unsigned getNumEqualities() const
unsigned getNumDimVars() const
void undoLastConstraint() final
Undo the addition of the last constraint.
LogicalResult moveRowUnknownToColumn(unsigned row)
Try to move the specified row to column orientation while preserving the lexicopositivity of the basi...
void addInequality(ArrayRef< MPInt > coeffs) final
Add an inequality to the tableau.
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...
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.
MaybeOptimum< SmallVector< MPInt, 8 > > findIntegerLexMin()
Return the lexicographically minimum integer solution to the constraints.
bool isRedundantInequality(ArrayRef< MPInt > coeffs)
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin()
Return the lexicographically minimum rational solution to the constraints.
bool isSeparateInequality(ArrayRef< MPInt > coeffs)
Return whether the specified inequality is redundant/separate for the polytope.
This class provides support for multi-precision arithmetic.
unsigned getNumRows() const
void swapColumns(unsigned column, unsigned otherColumn)
Swap the given columns.
unsigned appendExtraRow()
Add an extra row at the bottom of the matrix and return its position.
MutableArrayRef< T > getRow(unsigned row)
Get a [Mutable]ArrayRef corresponding to the specified row.
void resizeVertically(unsigned newNRows)
void swapRows(unsigned row, unsigned otherRow)
Swap the given rows.
void resizeHorizontally(unsigned newNColumns)
void reserveRows(unsigned rows)
Reserve enough space to resize to the specified number of rows without reallocations.
void addToRow(unsigned sourceRow, unsigned targetRow, const T &scale)
Add scale multiples of the source row to the target row.
This class represents a multi-affine function with the domain as Z^d, where d is the number of domain...
const PresburgerSpace & getSpace() const
void addPiece(const Piece &piece)
unsigned getNumOutputs() const
void unionInPlace(const IntegerRelation &disjunct)
Mutate this set, turning it into the union of this set and the given disjunct.
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
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.
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.
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...
MaybeOptimum< Fraction > computeOptimum(Direction direction, ArrayRef< MPInt > coeffs)
Compute the maximum or minimum value of the given expression, depending on direction.
bool isMarkedRedundant(unsigned constraintIndex) const
Returns whether the specified constraint has been marked as redundant.
void addInequality(ArrayRef< MPInt > coeffs) final
Add an inequality to the tableau.
std::optional< SmallVector< MPInt, 8 > > findIntegerSample()
Returns an integer sample point if one exists, or std::nullopt otherwise.
bool isRedundantEquality(ArrayRef< MPInt > coeffs)
Check if the specified equality already holds in the polytope.
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.
MaybeOptimum< Fraction > computeRowOptimum(Direction direction, unsigned row)
Compute the maximum or minimum value of the given row, depending on direction.
bool isRationalSubsetOf(const IntegerRelation &rel)
Returns true if this Simplex's polytope is a rational subset of rel.
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.
bool isRedundantInequality(ArrayRef< MPInt > coeffs)
Check if the specified inequality already holds in the polytope.
bool isBoundedAlongConstraint(unsigned constraintIndex)
Returns whether the perpendicular of the specified constraint is a is a direction along which the pol...
bool isUnbounded()
Returns true if the polytope is unbounded, i.e., extends to infinity in some direction.
IneqType findIneqType(ArrayRef< MPInt > coeffs)
Returns the type of the inequality with coefficients coeffs.
std::optional< SmallVector< Fraction, 8 > > getRationalSample() const
Returns the current sample point, which may contain non-integer (rational) coordinates.
std::optional< SmallVector< MPInt, 8 > > getSamplePointIfIntegral() const
Returns the current sample point if it is integral.
SymbolicLexOpt computeSymbolicIntegerLexMin()
The lexmin will be stored as a function lexopt from symbols to non-symbols in the result.
Given a simplex for a polytope, construct a new simplex whose variables are identified with a pair of...
Fraction computeWidth(ArrayRef< MPInt > dir)
Compute max(dotProduct(dir, x - y)).
Fraction computeWidthAndDuals(ArrayRef< MPInt > dir, SmallVectorImpl< MPInt > &dual, MPInt &dualDenom)
Compute max(dotProduct(dir, x - y)) and save the dual variables for only the direction equalities to ...
void removeLastEquality()
Remove the last equality that was added through addEqualityForDirection.
void addEqualityForDirection(ArrayRef< MPInt > dir)
Add an equality dotProduct(dir, x - y) == 0.
GBRSimplex(const Simplex &originalSimplex)
SmallVector< AffineExpr, 4 > concat(ArrayRef< AffineExpr > a, ArrayRef< AffineExpr > b)
Return the vector that is the concatenation of a and b.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt mod(const MPInt &lhs, const MPInt &rhs)
is always non-negative.
void normalizeDiv(MutableArrayRef< MPInt > num, MPInt &denom)
Normalize the given (numerator, denominator) pair by dividing out the common factors between them.
MPInt ceil(const Fraction &f)
MPInt normalizeRange(MutableArrayRef< MPInt > range)
Divide the range by its gcd and return the gcd.
MPInt floor(const Fraction &f)
SmallVector< MPInt, 8 > getComplementIneq(ArrayRef< MPInt > ineq)
Return the complement of the given inequality.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt lcm(const MPInt &a, const MPInt &b)
Returns the least common multiple of 'a' and 'b'.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt floorDiv(const MPInt &lhs, const MPInt &rhs)
This header declares functions that assist transformations in the MemRef dialect.
LogicalResult failure(bool isFailure=true)
Utility function to generate a LogicalResult.
LogicalResult success(bool isSuccess=true)
Utility function to generate a LogicalResult.
bool failed(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a failure value.
This class represents an efficient way to signal success or failure.
bool failed() const
Returns true if the provided LogicalResult corresponds to a failure value.
A class to represent fractions.
MPInt getAsInteger() const
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type.
An Unknown is either a variable or a constraint.
Represents the result of a symbolic lexicographic optimization computation.
PWMAFunction lexopt
This maps assignments of symbols to the corresponding lexopt.
PresburgerSet unboundedDomain
Contains all assignments to the symbols that made the lexopt unbounded.
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.