15 #include "llvm/ADT/DynamicAPInt.h"
16 #include "llvm/ADT/STLExtras.h"
17 #include "llvm/ADT/SmallBitVector.h"
18 #include "llvm/ADT/SmallVector.h"
19 #include "llvm/Support/Compiler.h"
20 #include "llvm/Support/ErrorHandling.h"
21 #include "llvm/Support/raw_ostream.h"
30 using namespace presburger;
41 assert(a.size() == b.size());
43 res.reserve(a.size());
44 for (
unsigned i = 0, e = a.size(); i < e; ++i)
45 res.emplace_back(a[i] + scale * b[i]);
50 : usingBigM(mustUseBigM), nRedundant(0), nSymbol(0),
51 tableau(0, getNumFixedCols() + nVar), empty(false) {
55 for (
unsigned i = 0; i < nVar; ++i) {
63 const llvm::SmallBitVector &isSymbol)
65 assert(isSymbol.size() == nVar &&
"invalid bitmask!");
69 for (
unsigned symbolIdx : isSymbol.set_bits()) {
70 var[symbolIdx].isSymbol =
true;
77 assert(index !=
nullIndex &&
"nullIndex passed to unknownFromIndex");
78 return index >= 0 ?
var[index] :
con[~index];
92 assert(index !=
nullIndex &&
"nullIndex passed to unknownFromIndex");
93 return index >= 0 ?
var[index] :
con[~index];
121 bool makeRestricted) {
122 assert(coeffs.size() ==
var.size() + 1 &&
123 "Incorrect number of coefficients!");
125 "inconsistent column count!");
128 tableau(newRow, 1) = coeffs.back();
144 DynamicAPInt bigMCoeff(0);
145 for (
unsigned i = 0; i < coeffs.size() - 1; ++i)
146 if (!
var[i].isSymbol)
147 bigMCoeff -= coeffs[i];
149 tableau(newRow, 2) = bigMCoeff;
153 for (
unsigned i = 0; i <
var.size(); ++i) {
154 unsigned pos =
var[i].pos;
170 DynamicAPInt lcm = llvm::lcm(
tableau(newRow, 0),
tableau(pos, 0));
171 DynamicAPInt nRowCoeff = lcm /
tableau(newRow, 0);
172 DynamicAPInt idxRowCoeff = coeffs[i] * (lcm /
tableau(pos, 0));
176 nRowCoeff *
tableau(newRow, col) + idxRowCoeff *
tableau(pos, col);
181 return con.size() - 1;
185 bool signMatchesDirection(
const DynamicAPInt &elem,
Direction direction) {
186 assert(elem != 0 &&
"elem should not be 0");
187 return direction == Direction::Up ? elem > 0 : elem < 0;
235 if (restoreRationalConsistency().
failed()) {
239 return getRationalSample();
281 DynamicAPInt d =
tableau(row, 0);
291 std::optional<unsigned> LexSimplex::maybeGetNonIntegralVarRow()
const {
292 for (
const Unknown &u :
var) {
298 unsigned row = u.pos;
307 if (restoreRationalConsistency().
failed())
311 while (std::optional<unsigned> maybeRow = maybeGetNonIntegralVarRow()) {
322 if (
addCut(*maybeRow).failed())
324 if (restoreRationalConsistency().
failed())
329 assert(!sample.
isEmpty() &&
"If we reached here the sample should exist!");
332 return llvm::to_vector<8>(
347 SymbolicLexSimplex::getSymbolicSampleNumerator(
unsigned row)
const {
350 for (
unsigned col = 3; col < 3 +
nSymbol; ++col)
351 sample.emplace_back(
tableau(row, col));
352 sample.emplace_back(
tableau(row, 1));
357 SymbolicLexSimplex::getSymbolicSampleIneq(
unsigned row)
const {
367 var.back().isSymbol =
true;
372 const DynamicAPInt &divisor) {
373 assert(divisor > 0 &&
"divisor must be positive!");
375 range, [divisor](
const DynamicAPInt &x) {
return x % divisor == 0; });
378 bool SymbolicLexSimplex::isSymbolicSampleIntegral(
unsigned row)
const {
379 DynamicAPInt denom =
tableau(row, 0);
380 return tableau(row, 1) % denom == 0 &&
417 LogicalResult SymbolicLexSimplex::addSymbolicCut(
unsigned row) {
418 DynamicAPInt d =
tableau(row, 0);
428 divCoeffs.reserve(
nSymbol + 1);
429 DynamicAPInt divDenom = d;
430 for (
unsigned col = 3; col < 3 +
nSymbol; ++col)
431 divCoeffs.emplace_back(mod(-
tableau(row, col), divDenom));
432 divCoeffs.emplace_back(mod(-
tableau(row, 1), divDenom));
447 for (
unsigned col = 3; col < 3 +
nSymbol - 1; ++col)
456 void SymbolicLexSimplex::recordOutput(
SymbolicLexOpt &result)
const {
459 for (
const Unknown &u :
var) {
470 DynamicAPInt denom =
tableau(u.pos, 0);
471 if (
tableau(u.pos, 2) < denom) {
478 assert(
tableau(u.pos, 2) == denom &&
479 "Coefficient of M should not be greater than 1!");
482 for (DynamicAPInt &elem : sample) {
483 assert(elem % denom == 0 &&
"coefficients must be integral!");
486 output.appendExtraRow(sample);
498 std::optional<unsigned> SymbolicLexSimplex::maybeGetAlwaysViolatedRow() {
501 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row)
505 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row) {
516 std::optional<unsigned> SymbolicLexSimplex::maybeGetNonIntegralVarRow() {
517 for (
const Unknown &u :
var) {
520 assert(!u.isSymbol &&
"Symbol should not be in row orientation!");
521 if (!isSymbolicSampleIntegral(u.pos))
529 LogicalResult SymbolicLexSimplex::doNonBranchingPivots() {
530 while (std::optional<unsigned> row = maybeGetAlwaysViolatedRow())
559 unsigned domainSnapshot;
565 assert(level >= stack.size());
566 if (level > stack.size()) {
573 if (doNonBranchingPivots().
failed()) {
580 unsigned splitRow = 0;
581 for (
unsigned e =
getNumRows(); splitRow < e; ++splitRow) {
584 assert(
tableau(splitRow, 2) == 0 &&
585 "Non-branching pivots should have been handled already!");
587 symbolicSample = getSymbolicSampleIneq(splitRow);
595 "Non-branching pivots should have been handled already!");
600 unsigned domainSnapshot = domainSimplex.
getSnapshot();
625 StackFrame{splitIndex, snapshot, domainSnapshot, domainPolyCounts});
632 if (std::optional<unsigned> row = maybeGetNonIntegralVarRow()) {
633 if (addSymbolicCut(*row).failed()) {
644 recordOutput(result);
649 if (level == stack.size()) {
651 const StackFrame &frame = stack.back();
652 domainPoly.
truncate(frame.domainPolyCounts);
653 domainSimplex.
rollback(frame.domainSnapshot);
663 "The split row should have been returned to row orientation!");
687 bool LexSimplex::rowIsViolated(
unsigned row)
const {
695 std::optional<unsigned> LexSimplex::maybeGetViolatedRow()
const {
696 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row)
697 if (rowIsViolated(row))
705 LogicalResult LexSimplex::restoreRationalConsistency() {
708 while (std::optional<unsigned> maybeViolatedRow = maybeGetViolatedRow())
777 std::optional<unsigned> maybeColumn;
788 pivot(row, *maybeColumn);
793 unsigned colB)
const {
838 auto getSampleChangeCoeffForVar = [
this, row](
unsigned col,
840 DynamicAPInt a =
tableau(row, col);
855 DynamicAPInt c =
tableau(u.pos, col);
860 Fraction changeA = getSampleChangeCoeffForVar(colA, u);
861 Fraction changeB = getSampleChangeCoeffForVar(colB, u);
862 if (changeA < changeB)
864 if (changeA > changeB)
885 std::optional<SimplexBase::Pivot>
886 Simplex::findPivot(
int row,
Direction direction)
const {
887 std::optional<unsigned> col;
889 DynamicAPInt elem =
tableau(row,
j);
894 !signMatchesDirection(elem, direction))
904 tableau(row, *col) < 0 ? flippedDirection(direction) : direction;
905 std::optional<unsigned> maybePivotRow = findPivotRow(row, newDirection, *col);
906 return Pivot{maybePivotRow.value_or(row), *col};
951 assert(pivotCol >=
getNumFixedCols() &&
"Refusing to pivot invalid column");
957 if (
tableau(pivotRow, 0) < 0) {
963 for (
unsigned col = 1, e =
getNumColumns(); col < e; ++col) {
971 for (
unsigned row = 0, numRows =
getNumRows(); row < numRows; ++row) {
974 if (
tableau(row, pivotCol) == 0)
977 for (
unsigned col = 1, numCols =
getNumColumns(); col < numCols; ++col) {
992 LogicalResult Simplex::restoreRow(Unknown &u) {
994 "unknown should be in row position");
996 while (
tableau(u.pos, 1) < 0) {
997 std::optional<Pivot> maybePivot = findPivot(u.pos,
Direction::Up);
1005 return success(
tableau(u.pos, 1) >= 0);
1030 std::optional<unsigned> Simplex::findPivotRow(std::optional<unsigned> skipRow,
1032 unsigned col)
const {
1033 std::optional<unsigned> retRow;
1038 DynamicAPInt retElem, retConst;
1040 if (skipRow && row == *skipRow)
1042 DynamicAPInt elem =
tableau(row, col);
1047 if (signMatchesDirection(elem, direction))
1049 DynamicAPInt constTerm =
tableau(row, 1);
1054 retConst = constTerm;
1058 DynamicAPInt diff = retConst * elem - constTerm * retElem;
1060 (diff != 0 && !signMatchesDirection(diff, direction))) {
1063 retConst = constTerm;
1082 "Invalid columns provided!");
1110 unsigned conIndex =
addRow(coeffs,
true);
1111 LogicalResult result = restoreRow(
con[conIndex]);
1112 if (result.failed())
1125 negatedCoeffs.reserve(coeffs.size());
1126 for (
const DynamicAPInt &coeff : coeffs)
1127 negatedCoeffs.emplace_back(-coeff);
1143 basis.emplace_back(index);
1183 void Simplex::undoLastConstraint() {
1194 unsigned column =
con.back().pos;
1195 if (std::optional<unsigned> maybeRow =
1197 pivot(*maybeRow, column);
1198 }
else if (std::optional<unsigned> maybeRow =
1200 pivot(*maybeRow, column);
1203 assert(row &&
"Pivot should always exist for a constraint!");
1204 pivot(*row, column);
1220 unsigned column =
con.back().pos;
1222 assert(row &&
"Pivot should always exist for a constraint!");
1223 pivot(*row, column);
1244 "Variable to be removed must be in column orientation!");
1246 if (
var.back().isSymbol)
1260 assert(!
savedBases.empty() &&
"No bases saved!");
1265 for (
int index : basis) {
1272 "Column should not be a fixed column!");
1273 if (llvm::is_contained(basis,
colUnknown[col]))
1291 while (
undoLog.size() > snapshot) {
1304 const DynamicAPInt &denom) {
1305 assert(denom > 0 &&
"Denominator must be positive!");
1309 DynamicAPInt constTerm = ineq.back();
1310 ineq.back() = -denom;
1311 ineq.emplace_back(constTerm);
1314 for (DynamicAPInt &coeff : ineq)
1316 ineq.back() += denom - 1;
1323 var.reserve(
var.size() + count);
1325 for (
unsigned i = 0; i < count; ++i) {
1337 "IntegerRelation must have same dimensionality as simplex");
1347 while (std::optional<Pivot> maybePivot = findPivot(row, direction)) {
1350 if (maybePivot->row == row)
1369 unsigned conIndex =
addRow(coeffs);
1370 unsigned row =
con[conIndex].pos;
1379 unsigned column = u.pos;
1380 std::optional<unsigned> pivotRow = findPivotRow({}, direction, column);
1385 pivot(*pivotRow, column);
1388 unsigned row = u.pos;
1392 if (restoreRow(u).
failed())
1393 llvm_unreachable(
"Could not restore row!");
1399 assert(!
empty &&
"It is not meaningful to ask whether a direction is bounded "
1400 "in an empty set.");
1418 void Simplex::markRowRedundant(Unknown &u) {
1420 "Unknown should be in row position!");
1421 assert(u.pos >=
nRedundant &&
"Unknown is already marked redundant!");
1429 assert(offset + count <=
con.size() &&
"invalid range!");
1443 for (
unsigned i = 0; i < count; ++i) {
1446 unsigned column = u.
pos;
1447 std::optional<unsigned> pivotRow =
1453 pivot(*pivotRow, column);
1456 unsigned row = u.
pos;
1461 if (restoreRow(u).
failed())
1462 llvm_unreachable(
"Could not restore non-redundant row!");
1466 markRowRedundant(u);
1475 for (
unsigned i = 0; i <
var.size(); ++i) {
1508 result.reserve(v.size() + w.size());
1509 llvm::append_range(result, v);
1510 llvm::append_range(result, w);
1516 auto indexFromBIndex = [&](
int index) {
1533 auto appendRowFromA = [&](
unsigned row) {
1535 for (
unsigned col = 0, e = a.
getNumColumns(); col < e; ++col)
1544 auto appendRowFromB = [&](
unsigned row) {
1550 for (
unsigned col = 2, e = b.
getNumColumns(); col < e; ++col)
1558 for (
unsigned row = 0; row < a.
nRedundant; ++row)
1559 appendRowFromA(row);
1560 for (
unsigned row = 0; row < b.
nRedundant; ++row)
1561 appendRowFromB(row);
1563 appendRowFromA(row);
1565 appendRowFromB(row);
1575 sample.reserve(
var.size());
1580 sample.emplace_back(0, 1);
1584 DynamicAPInt denom =
tableau(u.pos, 0);
1585 sample.emplace_back(
tableau(u.pos, 1), denom);
1600 sample.reserve(
var.size());
1602 for (
const Unknown &u :
var) {
1616 DynamicAPInt denom =
tableau(u.pos, 0);
1618 if (
tableau(u.pos, 2) != denom)
1620 sample.emplace_back(
tableau(u.pos, 1), denom);
1625 std::optional<SmallVector<DynamicAPInt, 8>>
1634 integerSample.reserve(
var.size());
1635 for (
const Fraction &coord : rationalSample) {
1637 if (coord.num % coord.den != 0)
1639 integerSample.emplace_back(coord.num / coord.den);
1641 return integerSample;
1659 : simplex(
Simplex::makeProduct(originalSimplex, originalSimplex)),
1660 simplexConstraintOffset(simplex.getNumConstraints()) {}
1666 assert(llvm::any_of(dir, [](
const DynamicAPInt &X) {
return X != 0; }) &&
1667 "Direction passed is the zero vector!");
1668 snapshotStack.emplace_back(simplex.getSnapshot());
1669 simplex.addEquality(getCoeffsForDirection(dir));
1674 simplex.computeOptimum(Direction::Up, getCoeffsForDirection(dir));
1675 assert(maybeWidth.
isBounded() &&
"Width should be bounded!");
1683 DynamicAPInt &dualDenom) {
1691 unsigned conIndex = simplex.addRow(getCoeffsForDirection(dir));
1692 unsigned row = simplex.con[conIndex].pos;
1695 assert(maybeWidth.
isBounded() &&
"Width should be bounded!");
1696 dualDenom = simplex.tableau(row, 0);
1698 dual.reserve((conIndex - simplexConstraintOffset) / 2);
1702 for (
unsigned i = simplexConstraintOffset; i < conIndex; i += 2) {
1723 assert((simplex.con[i].orientation != Orientation::Column ||
1724 simplex.con[i + 1].orientation != Orientation::Column) &&
1725 "Both inequalities for the equality cannot be in column "
1727 if (simplex.con[i].orientation == Orientation::Column)
1728 dual.emplace_back(-simplex.tableau(row, simplex.con[i].pos));
1729 else if (simplex.con[i + 1].orientation == Orientation::Column)
1730 dual.emplace_back(simplex.tableau(row, simplex.con[i + 1].pos));
1732 dual.emplace_back(0);
1742 assert(!snapshotStack.empty() &&
"Snapshot stack is empty!");
1743 simplex.rollback(snapshotStack.back());
1744 snapshotStack.pop_back();
1754 assert(2 * dir.size() == simplex.getNumVariables() &&
1755 "Direction vector has wrong dimensionality");
1757 coeffs.reserve(dir.size() + 1);
1758 for (
const DynamicAPInt &coeff : dir)
1759 coeffs.emplace_back(-coeff);
1760 coeffs.emplace_back(0);
1767 unsigned simplexConstraintOffset;
1827 void Simplex::reduceBasis(
IntMatrix &basis,
unsigned level) {
1836 DynamicAPInt dualDenom;
1856 auto updateBasisWithUAndGetFCandidate = [&](
unsigned i) ->
Fraction {
1857 assert(i < level + dual.size() &&
"dual_i is not known!");
1859 DynamicAPInt u = floorDiv(dual[i - level], dualDenom);
1861 if (dual[i - level] % dualDenom != 0) {
1863 DynamicAPInt candidateDualDenom[2];
1867 widthI[0] = gbrSimplex.computeWidthAndDuals(
1868 basis.
getRow(i + 1), candidateDual[0], candidateDualDenom[0]);
1873 widthI[1] = gbrSimplex.computeWidthAndDuals(
1874 basis.
getRow(i + 1), candidateDual[1], candidateDualDenom[1]);
1876 unsigned j = widthI[0] < widthI[1] ? 0 : 1;
1890 basis.
getRow(i + 1), DynamicAPInt(-1), basis.
getRow(i))) >=
1892 "Computed u value does not minimize the width!");
1895 basis.
getRow(i + 1), DynamicAPInt(+1), basis.
getRow(i))) >=
1897 "Computed u value does not minimize the width!");
1899 dual = std::move(candidateDual[
j]);
1900 dualDenom = candidateDualDenom[
j];
1904 assert(i + 1 - level < width.size() &&
"width_{i+1} wasn't saved");
1908 assert(gbrSimplex.computeWidth(basis.
getRow(i + 1)) ==
1909 width[i + 1 - level]);
1910 return width[i + 1 - level];
1917 if (i >= level + width.size()) {
1922 assert((i == 0 || i - 1 < level + width.size()) &&
1923 "We are at level i but we don't know the value of width_{i-1}");
1928 assert(i == level &&
"This case should only occur when i == level");
1930 gbrSimplex.computeWidthAndDuals(basis.
getRow(i), dual, dualDenom));
1933 if (i >= level + dual.size()) {
1934 assert(i + 1 >= level + width.size() &&
1935 "We don't know dual_i but we know width_{i+1}");
1937 gbrSimplex.addEqualityForDirection(basis.
getRow(i));
1938 width.emplace_back(gbrSimplex.computeWidthAndDuals(basis.
getRow(i + 1),
1940 gbrSimplex.removeLastEquality();
1944 Fraction widthICandidate = updateBasisWithUAndGetFCandidate(i);
1945 if (widthICandidate < epsilon * width[i - level]) {
1947 width[i - level] = widthICandidate;
1950 width.resize(i - level + 1);
1956 gbrSimplex.removeLastEquality();
1963 gbrSimplex.addEqualityForDirection(basis.
getRow(i));
2000 unsigned nDims =
var.size();
2014 while (level != -1u) {
2024 if (level >= upperBoundStack.size()) {
2030 llvm::to_vector<8>(basis.
getRow(level));
2031 basisCoeffs.emplace_back(0);
2037 if (minRoundedUp.isEmpty() || maxRoundedDown.isEmpty()) {
2038 assert((minRoundedUp.isEmpty() && maxRoundedDown.isEmpty()) &&
2039 "If one bound is empty, both should be.");
2040 snapshotStack.pop_back();
2041 nextValueStack.pop_back();
2042 upperBoundStack.pop_back();
2048 assert((minRoundedUp.isBounded() && maxRoundedDown.isBounded()) &&
2049 "Polyhedron should be bounded!");
2054 return *maybeSample;
2056 if (*minRoundedUp < *maxRoundedDown) {
2057 reduceBasis(basis, level);
2058 basisCoeffs = llvm::to_vector<8>(basis.
getRow(level));
2059 basisCoeffs.emplace_back(0);
2060 std::tie(minRoundedUp, maxRoundedDown) =
2068 nextValueStack.emplace_back(*minRoundedUp);
2069 upperBoundStack.emplace_back(*maxRoundedDown);
2072 assert((snapshotStack.size() - 1 == level &&
2073 nextValueStack.size() - 1 == level &&
2074 upperBoundStack.size() - 1 == level) &&
2075 "Mismatched variable stack sizes!");
2081 DynamicAPInt nextValue = nextValueStack.back();
2082 ++nextValueStack.back();
2083 if (nextValue > upperBoundStack.back()) {
2086 snapshotStack.pop_back();
2087 nextValueStack.pop_back();
2088 upperBoundStack.pop_back();
2095 basis.
getRow(level).end());
2096 basisCoeffs.emplace_back(-nextValue);
2112 return {minRoundedUp, maxRoundedDown};
2116 assert(!
isEmpty() &&
"cannot check for flatness of empty simplex!");
2120 if (!upOpt.isBounded())
2122 if (!downOpt.isBounded())
2125 return *upOpt == *downOpt;
2131 os <<
"Simplex marked empty!\n";
2133 for (
unsigned i = 0; i <
var.size(); ++i) {
2139 for (
unsigned i = 0; i <
con.size(); ++i) {
2145 for (
unsigned row = 0, e =
getNumRows(); row < e; ++row) {
2151 os <<
"c0: denom, c1: const";
2153 os <<
", c" << col <<
": " <<
colUnknown[col];
2156 for (
unsigned row = 0, numRows =
getNumRows(); row < numRows; ++row)
2157 for (
unsigned col = 0, numCols =
getNumColumns(); col < numCols; ++col)
2158 updatePrintMetrics<DynamicAPInt>(
tableau(row, col), ptm);
2159 unsigned minSpacing = 1;
2160 for (
unsigned row = 0, numRows =
getNumRows(); row < numRows; ++row) {
2161 for (
unsigned col = 0, numCols =
getNumColumns(); col < numCols; ++col) {
2162 printWithPrintMetrics<DynamicAPInt>(os,
tableau(row, col), minSpacing,
2218 "It is not meaningful to ask about redundancy in an empty set!");
2228 "It is not meaningful to ask about redundancy in an empty set!");
2232 "Optima should be non-empty for a non-empty set");
static Value max(ImplicitLocOpBuilder &builder, Value value, Value bound)
static bool isRangeDivisibleBy(ArrayRef< DynamicAPInt > range, const DynamicAPInt &divisor)
static LLVM_ATTRIBUTE_UNUSED SmallVector< DynamicAPInt, 8 > scaleAndAddForAssert(ArrayRef< DynamicAPInt > a, const DynamicAPInt &scale, ArrayRef< DynamicAPInt > b)
static IntMatrix identity(unsigned dimension)
Return the identity matrix of the specified dimension.
DynamicAPInt normalizeRow(unsigned row, unsigned nCols)
Divide the first nCols of the specified row by their GCD.
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
void truncate(const CountsSnapshot &counts)
CountsSnapshot getCounts() const
unsigned getNumSymbolVars() const
ArrayRef< DynamicAPInt > getInequality(unsigned idx) const
unsigned getNumVars() const
unsigned addLocalFloorDiv(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
Adds a new local variable as the floordiv of an affine function of other variables,...
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...
void addInequality(ArrayRef< DynamicAPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
ArrayRef< DynamicAPInt > getEquality(unsigned idx) const
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...
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...
void addInequality(ArrayRef< DynamicAPInt > coeffs) final
Add an inequality to the tableau.
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< Fraction, 8 > > findRationalLexMin()
Return the lexicographically minimum rational solution to the constraints.
bool isSeparateInequality(ArrayRef< DynamicAPInt > coeffs)
Return whether the specified inequality is redundant/separate for the polytope.
bool isRedundantInequality(ArrayRef< DynamicAPInt > coeffs)
MaybeOptimum< SmallVector< DynamicAPInt, 8 > > findIntegerLexMin()
Return the lexicographically minimum integer solution to the constraints.
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
const Unknown & unknownFromRow(unsigned row) const
Returns the unknown associated with row.
SmallVector< int, 8 > colUnknown
SmallVector< Unknown, 8 > var
void addEquality(ArrayRef< DynamicAPInt > coeffs)
Add an equality 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 addDivisionVariable(ArrayRef< DynamicAPInt > coeffs, const DynamicAPInt &denom)
Append a new variable to the simplex and constrain it such that its only integer value is the floor d...
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.
virtual void addInequality(ArrayRef< DynamicAPInt > coeffs)=0
Add an inequality 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.
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 addRow(ArrayRef< DynamicAPInt > coeffs, bool makeRestricted=false)
Add a new row to the tableau and the associated data structures.
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...
std::pair< MaybeOptimum< DynamicAPInt >, MaybeOptimum< DynamicAPInt > > computeIntegerBounds(ArrayRef< DynamicAPInt > coeffs)
Returns a (min, max) pair denoting the minimum and maximum integer values of the given expression.
bool isMarkedRedundant(unsigned constraintIndex) const
Returns whether the specified constraint has been marked as redundant.
std::optional< SmallVector< DynamicAPInt, 8 > > getSamplePointIfIntegral() const
Returns the current sample point if it is integral.
bool isFlatAlong(ArrayRef< DynamicAPInt > coeffs)
Check if the simplex takes only one rational value along the direction of coeffs.
bool isRedundantEquality(ArrayRef< DynamicAPInt > coeffs)
Check if the specified equality already holds in the polytope.
IneqType findIneqType(ArrayRef< DynamicAPInt > coeffs)
Returns the type of the inequality with coefficients coeffs.
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.
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.
bool isRedundantInequality(ArrayRef< DynamicAPInt > coeffs)
Check if the specified inequality already holds in the polytope.
void addInequality(ArrayRef< DynamicAPInt > coeffs) final
Add an inequality to the tableau.
MaybeOptimum< Fraction > computeOptimum(Direction direction, ArrayRef< DynamicAPInt > coeffs)
Compute the maximum or minimum value of the given expression, depending on direction.
std::optional< SmallVector< Fraction, 8 > > getRationalSample() const
Returns the current sample point, which may contain non-integer (rational) coordinates.
std::optional< SmallVector< DynamicAPInt, 8 > > findIntegerSample()
Returns an integer sample point if one exists, or std::nullopt otherwise.
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 computeWidthAndDuals(ArrayRef< DynamicAPInt > dir, SmallVectorImpl< DynamicAPInt > &dual, DynamicAPInt &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.
Fraction computeWidth(ArrayRef< DynamicAPInt > dir)
Compute max(dotProduct(dir, x - y)).
GBRSimplex(const Simplex &originalSimplex)
void addEqualityForDirection(ArrayRef< DynamicAPInt > dir)
Add an equality dotProduct(dir, x - y) == 0.
SmallVector< AffineExpr, 4 > concat(ArrayRef< AffineExpr > a, ArrayRef< AffineExpr > b)
Return the vector that is the concatenation of a and b.
void normalizeDiv(MutableArrayRef< DynamicAPInt > num, DynamicAPInt &denom)
Normalize the given (numerator, denominator) pair by dividing out the common factors between them.
DynamicAPInt floor(const Fraction &f)
DynamicAPInt ceil(const Fraction &f)
DynamicAPInt normalizeRange(MutableArrayRef< DynamicAPInt > range)
Divide the range by its gcd and return the gcd.
SmallVector< DynamicAPInt, 8 > getComplementIneq(ArrayRef< DynamicAPInt > ineq)
Return the complement of the given inequality.
Include the generated interface declarations.
A class to represent fractions.
DynamicAPInt getAsInteger() const
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type.
Example usage: Print .12, 3.4, 56.7 preAlign = ".", minSpacing = 1, .12 .12 3.4 3....
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.