18 #include "llvm/ADT/STLExtras.h"
19 #include "llvm/ADT/SmallBitVector.h"
20 #include "llvm/ADT/SmallVector.h"
21 #include "llvm/Support/Compiler.h"
22 #include "llvm/Support/ErrorHandling.h"
23 #include "llvm/Support/raw_ostream.h"
32 using namespace presburger;
42 assert(a.size() == b.size());
44 res.reserve(a.size());
45 for (
unsigned i = 0, e = a.size(); i < e; ++i)
46 res.push_back(a[i] + scale * b[i]);
51 : usingBigM(mustUseBigM), nRedundant(0), nSymbol(0),
52 tableau(0, getNumFixedCols() + nVar), empty(false) {
54 for (
unsigned i = 0; i < nVar; ++i) {
62 const llvm::SmallBitVector &isSymbol)
64 assert(isSymbol.size() == nVar &&
"invalid bitmask!");
68 for (
unsigned symbolIdx : isSymbol.set_bits()) {
69 var[symbolIdx].isSymbol =
true;
76 assert(index !=
nullIndex &&
"nullIndex passed to unknownFromIndex");
77 return index >= 0 ?
var[index] :
con[~index];
91 assert(index !=
nullIndex &&
"nullIndex passed to unknownFromIndex");
92 return index >= 0 ?
var[index] :
con[~index];
120 assert(coeffs.size() ==
var.size() + 1 &&
121 "Incorrect number of coefficients!");
123 "inconsistent column count!");
126 tableau(newRow, 1) = coeffs.back();
143 for (
unsigned i = 0; i < coeffs.size() - 1; ++i)
144 if (!
var[i].isSymbol)
145 bigMCoeff -= coeffs[i];
147 tableau(newRow, 2) = bigMCoeff;
151 for (
unsigned i = 0; i <
var.size(); ++i) {
152 unsigned pos =
var[i].pos;
174 nRowCoeff *
tableau(newRow, col) + idxRowCoeff *
tableau(pos, col);
179 return con.size() - 1;
183 bool signMatchesDirection(
const MPInt &elem,
Direction direction) {
184 assert(elem != 0 &&
"elem should not be 0");
185 return direction == Direction::Up ? elem > 0 : elem < 0;
233 if (restoreRationalConsistency().
failed()) {
237 return getRationalSample();
289 std::optional<unsigned> LexSimplex::maybeGetNonIntegralVarRow()
const {
290 for (
const Unknown &u :
var) {
296 unsigned row = u.pos;
305 if (restoreRationalConsistency().
failed())
309 while (std::optional<unsigned> maybeRow = maybeGetNonIntegralVarRow()) {
322 if (restoreRationalConsistency().
failed())
327 assert(!sample.
isEmpty() &&
"If we reached here the sample should exist!");
330 return llvm::to_vector<8>(
345 SymbolicLexSimplex::getSymbolicSampleNumerator(
unsigned row)
const {
348 for (
unsigned col = 3; col < 3 +
nSymbol; ++col)
349 sample.push_back(
tableau(row, col));
350 sample.push_back(
tableau(row, 1));
355 SymbolicLexSimplex::getSymbolicSampleIneq(
unsigned row)
const {
365 var.back().isSymbol =
true;
370 assert(divisor > 0 &&
"divisor must be positive!");
371 return llvm::all_of(range,
372 [divisor](
const MPInt &x) {
return x % divisor == 0; });
375 bool SymbolicLexSimplex::isSymbolicSampleIntegral(
unsigned row)
const {
377 return tableau(row, 1) % denom == 0 &&
414 LogicalResult SymbolicLexSimplex::addSymbolicCut(
unsigned row) {
425 divCoeffs.reserve(
nSymbol + 1);
427 for (
unsigned col = 3; col < 3 +
nSymbol; ++col)
428 divCoeffs.push_back(
mod(-
tableau(row, col), divDenom));
429 divCoeffs.push_back(
mod(-
tableau(row, 1), divDenom));
444 for (
unsigned col = 3; col < 3 +
nSymbol - 1; ++col)
453 void SymbolicLexSimplex::recordOutput(
SymbolicLexOpt &result)
const {
456 for (
const Unknown &u :
var) {
468 if (
tableau(u.pos, 2) < denom) {
475 assert(
tableau(u.pos, 2) == denom &&
476 "Coefficient of M should not be greater than 1!");
479 for (
MPInt &elem : sample) {
480 assert(elem % denom == 0 &&
"coefficients must be integral!");
483 output.appendExtraRow(sample);
495 std::optional<unsigned> SymbolicLexSimplex::maybeGetAlwaysViolatedRow() {
498 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row)
502 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row) {
513 std::optional<unsigned> SymbolicLexSimplex::maybeGetNonIntegralVarRow() {
514 for (
const Unknown &u :
var) {
517 assert(!u.isSymbol &&
"Symbol should not be in row orientation!");
518 if (!isSymbolicSampleIntegral(u.pos))
527 while (std::optional<unsigned> row = maybeGetAlwaysViolatedRow())
556 unsigned domainSnapshot;
562 assert(level >= stack.size());
563 if (level > stack.size()) {
570 if (doNonBranchingPivots().
failed()) {
577 unsigned splitRow = 0;
578 for (
unsigned e =
getNumRows(); splitRow < e; ++splitRow) {
581 assert(
tableau(splitRow, 2) == 0 &&
582 "Non-branching pivots should have been handled already!");
584 symbolicSample = getSymbolicSampleIneq(splitRow);
592 "Non-branching pivots should have been handled already!");
597 unsigned domainSnapshot = domainSimplex.
getSnapshot();
622 {splitIndex, snapshot, domainSnapshot, domainPolyCounts});
629 if (std::optional<unsigned> row = maybeGetNonIntegralVarRow()) {
630 if (addSymbolicCut(*row).
failed()) {
641 recordOutput(result);
646 if (level == stack.size()) {
648 const StackFrame &frame = stack.back();
649 domainPoly.
truncate(frame.domainPolyCounts);
650 domainSimplex.
rollback(frame.domainSnapshot);
660 "The split row should have been returned to row orientation!");
684 bool LexSimplex::rowIsViolated(
unsigned row)
const {
692 std::optional<unsigned> LexSimplex::maybeGetViolatedRow()
const {
693 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row)
694 if (rowIsViolated(row))
705 while (std::optional<unsigned> maybeViolatedRow = maybeGetViolatedRow())
774 std::optional<unsigned> maybeColumn;
785 pivot(row, *maybeColumn);
790 unsigned colB)
const {
835 auto getSampleChangeCoeffForVar = [
this, row](
unsigned col,
857 Fraction changeA = getSampleChangeCoeffForVar(colA, u);
858 Fraction changeB = getSampleChangeCoeffForVar(colB, u);
859 if (changeA < changeB)
861 if (changeA > changeB)
882 std::optional<SimplexBase::Pivot>
883 Simplex::findPivot(
int row,
Direction direction)
const {
884 std::optional<unsigned> col;
891 !signMatchesDirection(elem, direction))
901 tableau(row, *col) < 0 ? flippedDirection(direction) : direction;
902 std::optional<unsigned> maybePivotRow = findPivotRow(row, newDirection, *col);
903 return Pivot{maybePivotRow.value_or(row), *col};
948 assert(pivotCol >=
getNumFixedCols() &&
"Refusing to pivot invalid column");
954 if (
tableau(pivotRow, 0) < 0) {
960 for (
unsigned col = 1, e =
getNumColumns(); col < e; ++col) {
968 for (
unsigned row = 0, numRows =
getNumRows(); row < numRows; ++row) {
971 if (
tableau(row, pivotCol) == 0)
974 for (
unsigned col = 1, numCols =
getNumColumns(); col < numCols; ++col) {
991 "unknown should be in row position");
993 while (
tableau(u.pos, 1) < 0) {
994 std::optional<Pivot> maybePivot = findPivot(u.pos,
Direction::Up);
1027 std::optional<unsigned> Simplex::findPivotRow(std::optional<unsigned> skipRow,
1029 unsigned col)
const {
1030 std::optional<unsigned> retRow;
1035 MPInt retElem, retConst;
1037 if (skipRow && row == *skipRow)
1044 if (signMatchesDirection(elem, direction))
1051 retConst = constTerm;
1055 MPInt diff = retConst * elem - constTerm * retElem;
1057 (diff != 0 && !signMatchesDirection(diff, direction))) {
1060 retConst = constTerm;
1079 "Invalid columns provided!");
1107 unsigned conIndex =
addRow(coeffs,
true);
1122 for (
const MPInt &coeff : coeffs)
1123 negatedCoeffs.emplace_back(-coeff);
1138 basis.push_back(index);
1178 void Simplex::undoLastConstraint() {
1189 unsigned column =
con.back().pos;
1190 if (std::optional<unsigned> maybeRow =
1192 pivot(*maybeRow, column);
1193 }
else if (std::optional<unsigned> maybeRow =
1195 pivot(*maybeRow, column);
1198 assert(row &&
"Pivot should always exist for a constraint!");
1199 pivot(*row, column);
1215 unsigned column =
con.back().pos;
1217 assert(row &&
"Pivot should always exist for a constraint!");
1218 pivot(*row, column);
1239 "Variable to be removed must be in column orientation!");
1241 if (
var.back().isSymbol)
1255 assert(!
savedBases.empty() &&
"No bases saved!");
1260 for (
int index : basis) {
1267 "Column should not be a fixed column!");
1268 if (llvm::is_contained(basis,
colUnknown[col]))
1286 while (
undoLog.size() > snapshot) {
1299 const MPInt &denom) {
1300 assert(denom > 0 &&
"Denominator must be positive!");
1304 MPInt constTerm = ineq.back();
1305 ineq.back() = -denom;
1306 ineq.push_back(constTerm);
1309 for (
MPInt &coeff : ineq)
1311 ineq.back() += denom - 1;
1318 var.reserve(
var.size() + count);
1320 for (
unsigned i = 0; i < count; ++i) {
1332 "IntegerRelation must have same dimensionality as simplex");
1342 while (std::optional<Pivot> maybePivot = findPivot(row, direction)) {
1345 if (maybePivot->row == row)
1364 unsigned conIndex =
addRow(coeffs);
1365 unsigned row =
con[conIndex].pos;
1374 unsigned column = u.pos;
1375 std::optional<unsigned> pivotRow = findPivotRow({}, direction, column);
1380 pivot(*pivotRow, column);
1383 unsigned row = u.pos;
1387 if (
failed(restoreRow(u)))
1388 llvm_unreachable(
"Could not restore row!");
1394 assert(!
empty &&
"It is not meaningful to ask whether a direction is bounded "
1395 "in an empty set.");
1413 void Simplex::markRowRedundant(Unknown &u) {
1415 "Unknown should be in row position!");
1416 assert(u.pos >=
nRedundant &&
"Unknown is already marked redundant!");
1424 assert(offset + count <=
con.size() &&
"invalid range!");
1438 for (
unsigned i = 0; i < count; ++i) {
1441 unsigned column = u.
pos;
1442 std::optional<unsigned> pivotRow =
1448 pivot(*pivotRow, column);
1451 unsigned row = u.
pos;
1456 if (
failed(restoreRow(u)))
1457 llvm_unreachable(
"Could not restore non-redundant row!");
1461 markRowRedundant(u);
1470 for (
unsigned i = 0; i <
var.size(); ++i) {
1503 result.reserve(v.size() + w.size());
1504 result.insert(result.end(), v.begin(), v.end());
1505 result.insert(result.end(), w.begin(), w.end());
1511 auto indexFromBIndex = [&](
int index) {
1528 auto appendRowFromA = [&](
unsigned row) {
1530 for (
unsigned col = 0, e = a.
getNumColumns(); col < e; ++col)
1539 auto appendRowFromB = [&](
unsigned row) {
1545 for (
unsigned col = 2, e = b.
getNumColumns(); col < e; ++col)
1553 for (
unsigned row = 0; row < a.
nRedundant; ++row)
1554 appendRowFromA(row);
1555 for (
unsigned row = 0; row < b.
nRedundant; ++row)
1556 appendRowFromB(row);
1558 appendRowFromA(row);
1560 appendRowFromB(row);
1570 sample.reserve(
var.size());
1575 sample.emplace_back(0, 1);
1580 sample.emplace_back(
tableau(u.pos, 1), denom);
1595 sample.reserve(
var.size());
1597 for (
const Unknown &u :
var) {
1613 if (
tableau(u.pos, 2) != denom)
1615 sample.emplace_back(
tableau(u.pos, 1), denom);
1628 integerSample.reserve(
var.size());
1629 for (
const Fraction &coord : rationalSample) {
1631 if (coord.num % coord.den != 0)
1633 integerSample.push_back(coord.num / coord.den);
1635 return integerSample;
1653 : simplex(
Simplex::makeProduct(originalSimplex, originalSimplex)),
1654 simplexConstraintOffset(simplex.getNumConstraints()) {}
1660 assert(llvm::any_of(dir, [](
const MPInt &x) {
return x != 0; }) &&
1661 "Direction passed is the zero vector!");
1662 snapshotStack.push_back(simplex.getSnapshot());
1663 simplex.addEquality(getCoeffsForDirection(dir));
1668 simplex.computeOptimum(Direction::Up, getCoeffsForDirection(dir));
1669 assert(maybeWidth.
isBounded() &&
"Width should be bounded!");
1685 unsigned conIndex = simplex.addRow(getCoeffsForDirection(dir));
1686 unsigned row = simplex.con[conIndex].pos;
1689 assert(maybeWidth.
isBounded() &&
"Width should be bounded!");
1690 dualDenom = simplex.tableau(row, 0);
1695 for (
unsigned i = simplexConstraintOffset; i < conIndex; i += 2) {
1716 assert(!(simplex.con[i].orientation == Orientation::Column &&
1717 simplex.con[i + 1].orientation == Orientation::Column) &&
1718 "Both inequalities for the equality cannot be in column "
1720 if (simplex.con[i].orientation == Orientation::Column)
1721 dual.push_back(-simplex.tableau(row, simplex.con[i].pos));
1722 else if (simplex.con[i + 1].orientation == Orientation::Column)
1723 dual.push_back(simplex.tableau(row, simplex.con[i + 1].pos));
1725 dual.emplace_back(0);
1735 assert(!snapshotStack.empty() &&
"Snapshot stack is empty!");
1736 simplex.rollback(snapshotStack.back());
1737 snapshotStack.pop_back();
1746 assert(2 * dir.size() == simplex.getNumVariables() &&
1747 "Direction vector has wrong dimensionality");
1749 coeffs.reserve(2 * dir.size());
1750 for (
const MPInt &coeff : dir)
1751 coeffs.push_back(-coeff);
1752 coeffs.emplace_back(0);
1759 unsigned simplexConstraintOffset;
1819 void Simplex::reduceBasis(
IntMatrix &basis,
unsigned level) {
1848 auto updateBasisWithUAndGetFCandidate = [&](
unsigned i) ->
Fraction {
1849 assert(i < level + dual.size() &&
"dual_i is not known!");
1853 if (dual[i - level] % dualDenom != 0) {
1855 MPInt candidateDualDenom[2];
1859 widthI[0] = gbrSimplex.computeWidthAndDuals(
1860 basis.
getRow(i + 1), candidateDual[0], candidateDualDenom[0]);
1865 widthI[1] = gbrSimplex.computeWidthAndDuals(
1866 basis.
getRow(i + 1), candidateDual[1], candidateDualDenom[1]);
1868 unsigned j = widthI[0] < widthI[1] ? 0 : 1;
1884 "Computed u value does not minimize the width!");
1889 "Computed u value does not minimize the width!");
1891 dual = std::move(candidateDual[
j]);
1892 dualDenom = candidateDualDenom[
j];
1896 assert(i + 1 - level < width.size() &&
"width_{i+1} wasn't saved");
1900 assert(gbrSimplex.computeWidth(basis.
getRow(i + 1)) ==
1901 width[i + 1 - level]);
1902 return width[i + 1 - level];
1909 if (i >= level + width.size()) {
1914 assert((i == 0 || i - 1 < level + width.size()) &&
1915 "We are at level i but we don't know the value of width_{i-1}");
1920 assert(i == level &&
"This case should only occur when i == level");
1922 gbrSimplex.computeWidthAndDuals(basis.
getRow(i), dual, dualDenom));
1925 if (i >= level + dual.size()) {
1926 assert(i + 1 >= level + width.size() &&
1927 "We don't know dual_i but we know width_{i+1}");
1929 gbrSimplex.addEqualityForDirection(basis.
getRow(i));
1930 width.push_back(gbrSimplex.computeWidthAndDuals(basis.
getRow(i + 1), dual,
1932 gbrSimplex.removeLastEquality();
1936 Fraction widthICandidate = updateBasisWithUAndGetFCandidate(i);
1937 if (widthICandidate < epsilon * width[i - level]) {
1939 width[i - level] = widthICandidate;
1942 width.resize(i - level + 1);
1948 gbrSimplex.removeLastEquality();
1955 gbrSimplex.addEqualityForDirection(basis.
getRow(i));
1992 unsigned nDims =
var.size();
2006 while (level != -1u) {
2016 if (level >= upperBoundStack.size()) {
2022 llvm::to_vector<8>(basis.
getRow(level));
2023 basisCoeffs.emplace_back(0);
2029 if (minRoundedUp.isEmpty() || maxRoundedDown.isEmpty()) {
2030 assert((minRoundedUp.isEmpty() && maxRoundedDown.isEmpty()) &&
2031 "If one bound is empty, both should be.");
2032 snapshotStack.pop_back();
2033 nextValueStack.pop_back();
2034 upperBoundStack.pop_back();
2040 assert((minRoundedUp.isBounded() && maxRoundedDown.isBounded()) &&
2041 "Polyhedron should be bounded!");
2046 return *maybeSample;
2048 if (*minRoundedUp < *maxRoundedDown) {
2049 reduceBasis(basis, level);
2050 basisCoeffs = llvm::to_vector<8>(basis.
getRow(level));
2051 basisCoeffs.emplace_back(0);
2052 std::tie(minRoundedUp, maxRoundedDown) =
2060 nextValueStack.push_back(*minRoundedUp);
2061 upperBoundStack.push_back(*maxRoundedDown);
2064 assert((snapshotStack.size() - 1 == level &&
2065 nextValueStack.size() - 1 == level &&
2066 upperBoundStack.size() - 1 == level) &&
2067 "Mismatched variable stack sizes!");
2073 MPInt nextValue = nextValueStack.back();
2074 ++nextValueStack.back();
2075 if (nextValue > upperBoundStack.back()) {
2078 snapshotStack.pop_back();
2079 nextValueStack.pop_back();
2080 upperBoundStack.pop_back();
2087 basis.
getRow(level).end());
2088 basisCoeffs.push_back(-nextValue);
2104 return {minRoundedUp, maxRoundedDown};
2108 assert(!
isEmpty() &&
"cannot check for flatness of empty simplex!");
2112 if (!upOpt.isBounded())
2114 if (!downOpt.isBounded())
2117 return *upOpt == *downOpt;
2123 os <<
"Simplex marked empty!\n";
2125 for (
unsigned i = 0; i <
var.size(); ++i) {
2131 for (
unsigned i = 0; i <
con.size(); ++i) {
2137 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row) {
2143 os <<
"c0: denom, c1: const";
2145 os <<
", c" << col <<
": " <<
colUnknown[col];
2147 for (
unsigned row = 0, numRows =
getNumRows(); row < numRows; ++row) {
2148 for (
unsigned col = 0, numCols =
getNumColumns(); col < numCols; ++col)
2149 os <<
tableau(row, col) <<
'\t';
2203 "It is not meaningful to ask about redundancy in an empty set!");
2213 "It is not meaningful to ask about redundancy in an empty set!");
2217 "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 isFlatAlong(ArrayRef< MPInt > coeffs)
Check if the simplex takes only one rational value along the direction of coeffs.
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)
Include the generated interface declarations.
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.