21 #include "llvm/ADT/DenseMap.h" 22 #include "llvm/ADT/DenseSet.h" 23 #include "llvm/Support/Debug.h" 25 #define DEBUG_TYPE "presburger" 28 using namespace presburger;
30 using llvm::SmallDenseMap;
31 using llvm::SmallDenseSet;
34 return std::make_unique<IntegerRelation>(*this);
38 return std::make_unique<IntegerPolyhedron>(*this);
47 assert(oSpace.
getNumLocalVars() == 0 &&
"no locals should be present!");
101 "Incorrect number of vars in lexMin!");
121 "Incorrect number of vars in lexMin!");
127 return llvm::all_of(range, [](int64_t x) {
return x == 0; });
131 unsigned begin,
unsigned count) {
150 assert(num <= curNum &&
"Can't truncate to more vars!");
183 unsigned numNonDivLocals = 0;
185 for (
unsigned i = 0, e = copy.
getNumLocalVars(); i < e - numNonDivLocals;) {
190 copy.
swapVar(offset + i, offset + e - numNonDivLocals - 1);
191 std::swap(reprs[i], reprs[e - numNonDivLocals - 1]);
199 if (numNonDivLocals == 0)
217 .computeSymbolicIntegerLexMin();
233 llvm::SmallBitVector isSymbol(
getNumVars(),
false);
277 for (
unsigned i = 0, e = eq.size(); i < e; ++i)
284 for (
unsigned i = 0, e = inEq.size(); i < e; ++i)
298 if (varStart >= varLimit)
313 if (varStart >= varLimit)
319 auto removeVarKindInRange = [
this](
VarKind kind,
unsigned &start,
328 unsigned relativeStart =
329 start <= offset ? 0 :
std::min(num, start - offset);
330 unsigned relativeLimit =
331 limit <= offset ? 0 :
std::min(num, limit - offset);
339 limit -= relativeLimit - relativeStart;
369 assert(posA <
getNumVars() &&
"invalid position A");
370 assert(posB <
getNumVars() &&
"invalid position B");
390 unsigned offset,
unsigned num)
const {
391 assert(pos <
getNumVars() &&
"invalid position");
392 assert(offset + num <
getNumCols() &&
"invalid range");
396 auto containsConstraintDependentOnRange = [&](
unsigned r,
bool isEq) {
399 for (c = offset, f = offset + num; c < f; ++c) {
413 if (containsConstraintDependentOnRange(r,
false))
415 if (
atIneq(r, pos) >= 1) {
417 lbIndices->push_back(r);
418 }
else if (
atIneq(r, pos) <= -1) {
420 ubIndices->push_back(r);
430 if (
atEq(r, pos) == 0)
432 if (containsConstraintDependentOnRange(r,
true))
434 eqIndices->push_back(r);
450 "invalid position or too many values");
455 for (
unsigned i = 0, numVals = values.size(); i < numVals; ++i)
457 for (
unsigned i = 0, numVals = values.size(); i < numVals; ++i)
470 unsigned *rowIdx)
const {
471 assert(colIdx <
getNumCols() &&
"position out of bounds");
472 auto at = [&](
unsigned rowIdx) -> int64_t {
473 return isEq ?
atEq(rowIdx, colIdx) :
atIneq(rowIdx, colIdx);
476 for (*rowIdx = 0; *rowIdx < e; ++(*rowIdx)) {
477 if (at(*rowIdx) != 0) {
493 auto check = [&](
bool isEq) ->
bool {
496 for (
unsigned i = 0, e = numRows; i < e; ++i) {
498 for (j = 0; j < numCols - 1; ++j) {
504 if (j < numCols - 1) {
509 int64_t v = isEq ?
atEq(i, numCols - 1) :
atIneq(i, numCols - 1);
510 if ((isEq && v != 0) || (!isEq && v < 0)) {
525 unsigned rowIdx,
unsigned pivotRow,
526 unsigned pivotCol,
unsigned elimColStart,
529 if (isEq && rowIdx == pivotRow)
531 auto at = [&](
unsigned i,
unsigned j) -> int64_t {
532 return isEq ? constraints->
atEq(i,
j) : constraints->
atIneq(i,
j);
534 int64_t leadCoeff = at(rowIdx, pivotCol);
538 int64_t pivotCoeff = constraints->
atEq(pivotRow, pivotCol);
539 int64_t sign = (leadCoeff * pivotCoeff > 0) ? -1 : 1;
541 int64_t pivotMultiplier = sign * (lcm /
std::abs(pivotCoeff));
542 int64_t rowMultiplier = lcm /
std::abs(leadCoeff);
545 for (
unsigned j = 0;
j < numCols; ++
j) {
547 if (
j >= elimColStart &&
j < pivotCol)
549 int64_t v = pivotMultiplier * constraints->
atEq(pivotRow,
j) +
550 rowMultiplier * at(rowIdx,
j);
551 isEq ? constraints->
atEq(rowIdx,
j) = v
552 : constraints->
atIneq(rowIdx,
j) = v;
562 unsigned start,
unsigned end) {
565 auto getProductOfNumLowerUpperBounds = [&](
unsigned pos) {
569 if (cst.
atIneq(r, pos) > 0) {
571 }
else if (cst.
atIneq(r, pos) < 0) {
575 return numLb * numUb;
578 unsigned minLoc = start;
579 unsigned min = getProductOfNumLowerUpperBounds(start);
580 for (
unsigned c = start + 1; c < end; c++) {
581 unsigned numLbUbProduct = getProductOfNumLowerUpperBounds(c);
582 if (numLbUbProduct < min) {
583 min = numLbUbProduct;
606 unsigned currentPos = 0;
619 for (
unsigned i = 0, e = tmpCst.
getNumVars(); i < e; i++) {
628 LLVM_DEBUG(llvm::dbgs() <<
"FM constraint explosion detected\n");
660 for (
unsigned j = 1;
j < numCols - 1; ++
j) {
661 gcd = llvm::GreatestCommonDivisor64(gcd,
std::abs(
atEq(i,
j)));
664 if (gcd > 0 && (v % gcd != 0)) {
685 assert(!simplex.
isEmpty() &&
"It is not meaningful to ask whether a " 686 "direction is bounded in an empty set.");
693 boundedIneqs.push_back(i);
703 for (
unsigned i : boundedIneqs) {
704 for (
unsigned col = 0; col < dirsNumCols; ++col)
705 dirs(row, col) =
atIneq(i, col);
711 for (
unsigned col = 0; col < dirsNumCols; ++col)
712 dirs(row, col) =
atEq(i, col);
789 std::pair<unsigned, LinearTransform> result =
798 unsigned numBoundedDims = result.first;
799 unsigned numUnboundedDims =
getNumVars() - numBoundedDims;
810 "Simplex returned an invalid sample!");
844 int64_t coeff = cone.
atIneq(i,
j);
854 Simplex shrunkenConeSimplex(cone);
855 assert(!shrunkenConeSimplex.
isEmpty() &&
"Shrunken cone cannot be empty!");
865 sample.append(coneSample.begin(), coneSample.end());
873 assert(expr.size() == 1 + point.size() &&
874 "Dimensionalities of point and expression don't match!");
875 int64_t
value = expr.back();
876 for (
unsigned i = 0; i < point.size(); ++i)
877 value += expr[i] * point[i];
907 "Point should contain all vars except locals!");
909 "This function depends on locals being stored last!");
929 if (!foundRepr[i + localOffset]) {
939 foundRepr[localOffset + i] =
true;
976 if (posStart >= posLimit)
981 unsigned pivotCol = 0;
982 for (pivotCol = posStart; pivotCol < posLimit; ++pivotCol) {
1012 posLimit = pivotCol;
1015 return posLimit - posStart;
1064 for (
unsigned r = 0; r < numIneqs; r++) {
1108 bool hasUnboundedVar =
false;
1114 assert((!
min.isEmpty() && !
max.isEmpty()) &&
1115 "Polytope should be rationally non-empty!");
1119 if (
min.isUnbounded() ||
max.isUnbounded()) {
1120 hasUnboundedVar =
true;
1126 if (
min.getBoundedOptimum() >
max.getBoundedOptimum())
1129 count *= (*
max - *
min + 1);
1134 if (hasUnboundedVar)
1144 posA += localOffset;
1145 posB += localOffset;
1172 auto merge = [&relA, &relB, oldALocals](
unsigned i,
unsigned j) ->
bool {
1184 relB.eliminateRedundantLocalVar(i,
j);
1201 auto merge = [
this](
unsigned i,
unsigned j) ->
bool {
1221 unsigned i, e,
j, f;
1240 if (
atEq(k, j) != 0) {
1257 unsigned varLimit,
VarKind dstKind,
1259 assert(varLimit <=
getNumVarKind(srcKind) &&
"Invalid id range");
1261 if (varStart >= varLimit)
1265 unsigned convertCount = varLimit - varStart;
1266 unsigned newVarsBegin =
insertVar(dstKind, pos, convertCount);
1276 for (
unsigned i = 0; i < convertCount; ++i)
1277 swapVar(offset + varStart + i, newVarsBegin + i);
1285 if (type == BoundType::EQ) {
1291 inequalities(row, pos) = type == BoundType::LB ? 1 : -1;
1299 assert(type != BoundType::EQ &&
"EQ not implemented");
1302 for (
unsigned i = 0, e = expr.size(); i < e; ++i)
1303 inequalities(row, i) = type == BoundType::LB ? expr[i] : -expr[i];
1305 type == BoundType::LB ? -value : value;
1315 assert(dividend.size() ==
getNumCols() &&
"incorrect dividend size");
1316 assert(divisor > 0 &&
"positive divisor expected");
1321 dividendCopy.insert(dividendCopy.end() - 1, 0);
1334 bool symbolic =
false) {
1335 assert(pos < cst.
getNumVars() &&
"invalid position");
1337 int64_t v = cst.
atEq(r, pos);
1343 for (c = 0; c < f; c++) {
1346 if (cst.
atEq(r, c) != 0) {
1359 assert(pos <
getNumVars() &&
"invalid position");
1365 assert(
atEq(rowIdx, pos) *
atEq(rowIdx, pos) == 1);
1372 for (
unsigned s = pos, t = pos, e = pos + num; s < e; s++) {
1395 unsigned *minUbPos)
const {
1396 assert(pos <
getNumDimVars() &&
"Invalid variable position");
1407 [](int64_t coeff) {
return coeff == 0; }))
1417 int64_t v =
atEq(eqPos, pos);
1424 (*ub)[c] = (*lb)[c];
1426 assert(boundFloorDivisor &&
1427 "both lb and divisor or none should be provided");
1428 *boundFloorDivisor = 1;
1459 unsigned minLbPosition = 0, minUbPosition = 0;
1460 for (
auto ubPos : ubIndices) {
1461 for (
auto lbPos : lbIndices) {
1469 for (j = 0, e =
getNumCols() - 1; j < e; j++)
1479 diff = std::max<int64_t>(diff, 0);
1480 if (minDiff ==
None || diff < minDiff) {
1482 minLbPosition = lbPos;
1483 minUbPosition = ubPos;
1487 if (lb && minDiff) {
1496 *boundFloorDivisor =
atIneq(minLbPosition, pos);
1497 assert(*boundFloorDivisor == -
atIneq(minUbPosition, pos));
1512 *minLbPos = minLbPosition;
1514 *minUbPos = minUbPosition;
1518 template <
bool isLower>
1521 assert(pos <
getNumVars() &&
"invalid position");
1550 }
else if (
atIneq(r, 0) >= 0) {
1555 for (c = 0, f =
getNumCols() - 1; c < f; c++)
1556 if (c != 0 &&
atIneq(r, c) != 0)
1562 int64_t boundConst =
1566 if (minOrMaxConst ==
None || boundConst > minOrMaxConst)
1567 minOrMaxConst = boundConst;
1569 if (minOrMaxConst ==
None || boundConst < minOrMaxConst)
1570 minOrMaxConst = boundConst;
1573 return minOrMaxConst;
1577 unsigned pos)
const {
1578 if (type == BoundType::LB)
1580 .computeConstantLowerOrUpperBound<
true>(pos);
1581 if (type == BoundType::UB)
1583 .computeConstantLowerOrUpperBound<
false>(pos);
1585 assert(type == BoundType::EQ &&
"expected EQ");
1591 .computeConstantLowerOrUpperBound<
false>(pos);
1601 for (
unsigned c = pos; c < pos + num; c++) {
1610 for (
unsigned c = pos; c < pos + num; c++) {
1611 if (
atEq(r, c) != 0)
1633 SmallDenseMap<ArrayRef<int64_t>, std::pair<unsigned, int64_t>>
1634 rowsWithoutConstTerm;
1636 SmallDenseSet<ArrayRef<int64_t>, 8> rowSet;
1639 auto isTriviallyValid = [&](
unsigned r) ->
bool {
1640 for (
unsigned c = 0, e =
getNumCols() - 1; c < e; c++) {
1652 if (isTriviallyValid(r) || !rowSet.insert(row).second) {
1653 redunIneq[r] =
true;
1664 rowsWithoutConstTerm.insert({rowWithoutConstTerm, {r, constTerm}});
1667 auto &val = ret.first->second;
1668 if (val.second > constTerm) {
1670 redunIneq[val.first] =
true;
1671 val = {r, constTerm};
1674 redunIneq[r] =
true;
1692 #define DEBUG_TYPE "fm" 1738 bool *isResultIntegerExact) {
1739 LLVM_DEBUG(llvm::dbgs() <<
"FM input (eliminate pos " << pos <<
"):\n");
1741 assert(pos <
getNumVars() &&
"invalid position");
1746 if (
atEq(r, pos) != 0) {
1750 assert(
succeeded(ret) &&
"Gaussian elimination guaranteed to succeed");
1751 LLVM_DEBUG(llvm::dbgs() <<
"FM output (through Gaussian elimination):\n");
1765 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
1775 std::vector<unsigned> nbIndices;
1782 if (
atIneq(r, pos) == 0) {
1784 nbIndices.push_back(r);
1785 }
else if (
atIneq(r, pos) >= 1) {
1787 lbIndices.push_back(r);
1790 ubIndices.push_back(r);
1797 newSpace.
removeVarRange(idKindRemove, relativePos, relativePos + 1);
1800 IntegerRelation newRel(lbIndices.size() * ubIndices.size() + nbIndices.size(),
1804 bool allLCMsAreOne =
true;
1816 for (
auto ubPos : ubIndices) {
1817 for (
auto lbPos : lbIndices) {
1819 ineq.reserve(newRel.getNumCols());
1820 int64_t lbCoeff =
atIneq(lbPos, pos);
1824 int64_t ubCoeff = -
atIneq(ubPos, pos);
1826 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
1829 assert(lbCoeff >= 1 && ubCoeff >= 1 &&
"bounds wrongly identified");
1831 ineq.push_back(
atIneq(ubPos, l) * (lcm / ubCoeff) +
1832 atIneq(lbPos, l) * (lcm / lbCoeff));
1833 assert(lcm > 0 &&
"lcm should be positive!");
1835 allLCMsAreOne =
false;
1840 ineq[ineq.size() - 1] += lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
1844 newRel.addInequality(ineq);
1848 LLVM_DEBUG(llvm::dbgs() <<
"FM isResultIntegerExact: " << allLCMsAreOne
1850 if (allLCMsAreOne && isResultIntegerExact)
1851 *isResultIntegerExact =
true;
1854 for (
auto nbPos : nbIndices) {
1857 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
1860 ineq.push_back(
atIneq(nbPos, l));
1862 newRel.addInequality(ineq);
1865 assert(newRel.getNumConstraints() ==
1866 lbIndices.size() * ubIndices.size() + nbIndices.size());
1871 eq.reserve(newRel.getNumCols());
1872 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
1875 eq.push_back(
atEq(r, l));
1877 newRel.addEquality(eq);
1882 newRel.gcdTightenInequalities();
1883 newRel.normalizeConstraintsByGCD();
1884 newRel.removeTrivialRedundancy();
1886 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
1891 #define DEBUG_TYPE "presburger" 1899 assert(pos + num <
getNumCols() &&
"invalid range");
1902 unsigned currentPos = pos;
1903 unsigned numToEliminate = num;
1904 unsigned numGaussianEliminated = 0;
1907 unsigned curNumEliminated =
1910 numToEliminate -= curNumEliminated + 1;
1911 numGaussianEliminated += curNumEliminated;
1915 for (
unsigned i = 0; i < num - numGaussianEliminated; i++) {
1916 unsigned numToEliminate = num - numGaussianEliminated - i;
1935 assert(a.size() == b.size());
1941 if (!std::equal(a.begin(), a.end() - 1, b.begin()))
1944 if (a.back() == b.back())
1947 return a.back() < b.back() ? Less : Greater;
1986 std::vector<SmallVector<int64_t, 8>> boundingLbs;
1987 std::vector<SmallVector<int64_t, 8>> boundingUbs;
1999 int64_t lbFloorDivisor, otherLbFloorDivisor;
2002 if (!extent.has_value())
2008 d, &otherLb, &otherLbFloorDivisor, &otherUb);
2009 if (!otherExtent.has_value() || lbFloorDivisor != otherLbFloorDivisor)
2013 assert(lbFloorDivisor > 0 &&
"divisor always expected to be positive");
2015 auto res = compareBounds(lb, otherLb);
2017 if (res == BoundCmpResult::Less || res == BoundCmpResult::Equal) {
2022 minLb.back() -= lbFloorDivisor - 1;
2023 }
else if (res == BoundCmpResult::Greater) {
2025 minLb.back() -= otherLbFloorDivisor - 1;
2030 if (!constLb.has_value() || !constOtherLb.has_value())
2032 std::fill(minLb.begin(), minLb.end(), 0);
2033 minLb.back() =
std::min(constLb.value(), constOtherLb.value());
2037 auto uRes = compareBounds(ub, otherUb);
2038 if (uRes == BoundCmpResult::Greater || uRes == BoundCmpResult::Equal) {
2040 }
else if (uRes == BoundCmpResult::Less) {
2046 if (!constUb.has_value() || !constOtherUb.has_value())
2048 std::fill(maxUb.begin(), maxUb.end(), 0);
2049 maxUb.back() =
std::max(constUb.value(), constOtherUb.value());
2052 std::fill(newLb.begin(), newLb.end(), 0);
2053 std::fill(newUb.begin(), newUb.end(), 0);
2057 newLb[d] = lbFloorDivisor;
2058 newUb[d] = -lbFloorDivisor;
2061 std::transform(newLb.begin() +
getNumDimVars(), newLb.end(),
2065 boundingLbs.push_back(newLb);
2066 boundingUbs.push_back(newUb);
2099 assert(pos < cst.
getNumVars() &&
"invalid start position");
2100 assert(pos + num <= cst.
getNumVars() &&
"invalid limit");
2105 for (c = pos; c < pos + num; ++c) {
2106 if (cst.
atIneq(r, c) != 0)
2110 nbIneqIndices.push_back(r);
2116 for (c = pos; c < pos + num; ++c) {
2117 if (cst.
atEq(r, c) != 0)
2121 nbEqIndices.push_back(r);
2126 assert(pos + num <=
getNumVars() &&
"invalid range");
2135 for (
auto nbIndex : llvm::reverse(nbIneqIndices))
2137 for (
auto nbIndex : llvm::reverse(nbEqIndices))
2170 "Domain set is not compatible with poly");
2186 "Range set is not compatible with poly");
2206 "Range of `this` should be compatible with Domain of `rel`");
2248 os <<
atEq(i,
j) <<
" ";
2266 "Domain has to be zero in a set");
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt lcm(const MPInt &a, const MPInt &b)
Returns the least common multiple of 'a' and 'b'.
int64_t normalizeRow(unsigned row, unsigned nCols)
Divide the first nCols of the specified row by their GCD.
Include the generated interface declarations.
virtual bool hasConsistentState() const
Returns false if the fields corresponding to various variable counts, or equality/inequality buffer s...
unsigned getNumLocalVars() const
void addLocalFloorDiv(ArrayRef< int64_t > dividend, int64_t divisor)
Adds a new local variable as the floordiv of an affine function of other variables, the coefficients of which are provided in dividend and with respect to a positive constant divisor.
int64_t lcm(int64_t a, int64_t b)
Returns the least common multiple of 'a' and 'b'.
Matrix inequalities
Coefficients of affine inequalities (in >= 0 form).
void removeInequalityRange(unsigned start, unsigned end)
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt ceilDiv(const MPInt &lhs, const MPInt &rhs)
LogicalResult constantFoldVar(unsigned pos)
Tries to fold the specified variable to a constant using a trivial equality detection; if successful...
Class storing division representation of local variables of a constraint system.
Optional< uint64_t > computeVolume() const
Compute an overapproximation of the number of integer points in the relation.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt abs(const MPInt &x)
SymbolicLexMin computeSymbolicIntegerLexMin()
The lexmin will be stored as a function lexmin from symbols to non-symbols in the result...
void removeDuplicateDivs(llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Removes duplicate divisions.
bool isEmpty() const
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
unsigned appendVar(VarKind kind, unsigned num=1)
Append num variables of the specified kind after the last variable.
bool hasConsistentState() const
Return whether the Matrix is in a consistent state with all its invariants satisfied.
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...
void print(llvm::raw_ostream &os) const
Optional< int64_t > computeConstantLowerOrUpperBound(unsigned pos)
Returns the constant lower bound bound if isLower is true, and the upper bound if isLower is false...
virtual void swapVar(unsigned posA, unsigned posB)
Swap the posA^th variable with the posB^th variable.
virtual void eliminateRedundantLocalVar(unsigned posA, unsigned posB)
Eliminate the posB^th local variable, replacing every instance of it with the posA^th local variable...
unsigned getNumOutputs() const
void removeRows(unsigned pos, unsigned count)
Remove the rows having positions pos, pos + 1, ...
bool isEqual(const PresburgerRelation &set) const
Return true if this set is equal to the given set, and false otherwise.
unsigned getNumRows() const
bool isHyperRectangular(unsigned pos, unsigned num) const
Returns true if the set can be trivially detected as being hyper-rectangular on the specified contigu...
void compose(const IntegerRelation &rel)
Let the relation this be R1, and the relation rel be R2.
A class to perform symbolic lexicographic optimization, i.e., to find, for every assignment to the sy...
void addEquality(ArrayRef< int64_t > eq)
Adds an equality from the coefficients specified in eq.
SmallVector< int64_t, 8 > getDivUpperBound(ArrayRef< int64_t > dividend, int64_t divisor, unsigned localVarIdx)
If q is defined to be equal to expr floordiv d, this equivalent to saying that q is an integer and q ...
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1) override
Insert num variables of the specified kind at position pos.
MaybeLocalRepr contains the indices of the constraints that can be expressed as a floordiv of an affi...
std::unique_ptr< IntegerPolyhedron > clone() const
void fillRow(unsigned row, int64_t value)
void removeEquality(unsigned pos)
IntegerPolyhedron getRangeSet() const
Return a set corresponding to all points in the range of the relation.
void clearConstraints()
Removes all equalities and inequalities.
static void copy(Location loc, Value dst, Value src, Value size, OpBuilder &builder)
Copies the given number of bytes from src to dst pointers.
unsigned getNumRangeVars() const
bool failed(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a failure value...
bool isMarkedRedundant(unsigned constraintIndex) const
Returns whether the specified constraint has been marked as redundant.
void removeDuplicateDivs()
void addToColumn(unsigned sourceColumn, unsigned targetColumn, int64_t scale)
Add scale multiples of the source column to the target column.
VarKind getVarKindAt(unsigned pos) const
Return the VarKind of the var at the specified position.
ArrayRef< int64_t > getInequality(unsigned idx) const
DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const
Returns a DivisonRepr representing the division representation of local variables in the constraint s...
bool isIntegerEmpty() const
Returns true if the set of constraints is found to have no solution, false if a solution exists...
This is a class to represent a resizable matrix.
unsigned getNumIneqs() const
void truncate(const CountsSnapshot &counts)
void applyDomain(const IntegerRelation &rel)
Given a relation rel, apply the relation to the domain of this relation.
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin() const
Get the lexicographically minimum rational point satisfying the constraints.
PresburgerSet unboundedDomain
Contains all assignments to the symbols that made the lexmin unbounded.
static void getCommonConstraints(const IntegerRelation &a, const IntegerRelation &b, IntegerRelation &c)
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of vars starts.
void clearRepr(unsigned i)
Optional< SmallVector< Fraction, 8 > > getRationalSample() const
Returns the current sample point, which may contain non-integer (rational) coordinates.
bool succeeded(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a success value...
void reserveRows(unsigned rows)
Reserve enough space to resize to the specified number of rows without reallocations.
void setAndEliminate(unsigned pos, ArrayRef< int64_t > values)
Sets the values.size() variables starting at pos to the specified values and removes them...
void mergeLocalVars(IntegerRelation &relA, IntegerRelation &relB, llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Given two relations, A and B, add additional local vars to the sets such that both have the union of ...
static int findEqualityToConstant(const IntegerRelation &cst, unsigned pos, bool symbolic=false)
Finds an equality that equates the specified variable to a constant.
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace.
int64_t atIneq(unsigned i, unsigned j) const
Returns the value at the specified inequality row and column.
SmallVector< int64_t, 8 > getDivLowerBound(ArrayRef< int64_t > dividend, int64_t divisor, unsigned localVarIdx)
LogicalResult unionBoundingBox(const IntegerRelation &other)
Updates the constraints to be the smallest bounding (enclosing) box that contains the points of this ...
virtual void fourierMotzkinEliminate(unsigned pos, bool darkShadow=false, bool *isResultIntegerExact=nullptr)
Eliminates the variable at the specified position using Fourier-Motzkin variable elimination, but uses Gaussian elimination if there is an equality involving that variable.
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
BoundType
The type of bound: equal, lower bound or upper bound.
void removeRedundantInequalities()
A more expensive check than removeTrivialRedundancy to detect redundant inequalities.
static constexpr const bool value
void swapColumns(unsigned column, unsigned otherColumn)
Swap the given columns.
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
void print(raw_ostream &os) const
void copyRow(unsigned sourceRow, unsigned targetRow)
bool isUnbounded()
Returns true if the polytope is unbounded, i.e., extends to infinity in some direction.
void removeRedundantLocalVars()
Removes local variables using equalities.
PresburgerSet unionSet(const PresburgerRelation &set) const
These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...
unsigned getNumEqualities() const
unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit)
Eliminates variables from equality and inequality constraints in column range [posStart, posLimit).
void truncateVarKind(VarKind kind, unsigned num)
Truncate the vars of the specified kind to the specified number by dropping some vars at the end...
void addInequality(ArrayRef< int64_t > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
unsigned getVarKindEnd(VarKind kind) const
Return the index at Which the specified kind of vars ends.
IntegerRelation intersect(IntegerRelation other) const
Return the intersection of the two relations.
static unsigned getBestVarToEliminate(const IntegerRelation &cst, unsigned start, unsigned end)
Returns the position of the variable that has the minimum <number of="" lower="" bounds>=""> times <n...
bool isEmptyByGCDTest() const
Runs the GCD test on all equality constraints.
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
static void eliminateFromConstraint(IntegerRelation *constraints, unsigned rowIdx, unsigned pivotRow, unsigned pivotCol, unsigned elimColStart, bool isEq)
Eliminate variable from constraint at rowIdx based on coefficient at pivotRow, pivotCol.
unsigned mergeLocalVars(IntegerRelation &other)
Adds additional local vars to the sets such that they both have the union of the local vars in each s...
LogicalResult success(bool isSuccess=true)
Utility function to generate a LogicalResult.
This class represents an efficient way to signal success or failure.
LogicalResult failure(bool isFailure=true)
Utility function to generate a LogicalResult.
void projectOut(unsigned pos, unsigned num)
Projects out (aka eliminates) num variables starting at position pos.
MutableArrayRef< int64_t > getDividend(unsigned i)
int64_t floorDiv(int64_t lhs, int64_t rhs)
Returns the result of MLIR's floordiv operation on constants.
bool isColZero(unsigned pos) const
Returns true if the pos^th column is all zero for both inequalities and equalities.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set. ...
unsigned getNumInequalities() const
void inverse()
Invert the relation i.e., swap its domain and range.
bool hasInvalidConstraint() const
Checks all rows of equality/inequality constraints for trivial contradictions (for example: 1 == 0...
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type...
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace, which should have the same number of ids as the current space.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set. ...
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
void insertColumns(unsigned pos, unsigned count)
Insert columns having positions pos, pos + 1, ...
void removeInequality(unsigned pos)
void removeRow(unsigned pos)
void truncateOutput(unsigned count)
Truncate the output dimensions to the first count dimensions.
unsigned getNumVars() const
bool isEqual(const IntegerRelation &other) const
Return whether this and other are equal.
int64_t ceilDiv(int64_t lhs, int64_t rhs)
Returns the result of MLIR's ceildiv operation on constants.
unsigned & getDenom(unsigned i)
unsigned getNumSymbolVars() const
ArrayRef< int64_t > getEquality(unsigned idx) const
unsigned getNumVars() const
void intersectRange(const IntegerPolyhedron &poly)
Intersect the given poly with the range in-place.
unsigned getNumConstraints() const
bool hasOnlyDivLocals() const
Check whether all local ids have a division representation.
void gcdTightenInequalities()
Tightens inequalities given that we are dealing with integer spaces.
static int64_t valueAt(ArrayRef< int64_t > expr, ArrayRef< int64_t > point)
Helper to evaluate an affine expression at a point.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt gcd(const MPInt &a, const MPInt &b)
static constexpr unsigned kExplosionFactor
A parameter that controls detection of an unrealistic number of constraints.
PresburgerSet subtract(const PresburgerSet &other) const
Return the set difference of this set and the given set, i.e., return this \ set. ...
Matrix equalities
Coefficients of affine equalities (in == 0 form).
MaybeOptimum< SmallVector< int64_t, 8 > > findIntegerLexMin() const
Same as above, but returns lexicographically minimal integer point.
bool isBoundedAlongConstraint(unsigned constraintIndex)
Returns whether the perpendicular of the specified constraint is a is a direction along which the pol...
unsigned appendExtraRow()
Add an extra row at the bottom of the matrix and return its position.
OptimumKind getKind() const
bool findConstraintWithNonZeroAt(unsigned colIdx, bool isEq, unsigned *rowIdx) const
Searches for a constraint with a non-zero coefficient at colIdx in equality (isEq=true) or inequality...
Optional< int64_t > getConstantBoundOnDimSize(unsigned pos, SmallVectorImpl< int64_t > *lb=nullptr, int64_t *boundFloorDivisor=nullptr, SmallVectorImpl< int64_t > *ub=nullptr, unsigned *minLbPos=nullptr, unsigned *minUbPos=nullptr) const
Returns the smallest known constant bound for the extent of the specified variable (pos^th)...
unsigned getNumEqs() const
static void getIndependentConstraints(const IntegerRelation &cst, unsigned pos, unsigned num, SmallVectorImpl< unsigned > &nbIneqIndices, SmallVectorImpl< unsigned > &nbEqIndices)
Find positions of inequalities and equalities that do not have a coefficient for [pos, pos + num) variables.
void removeVar(VarKind kind, unsigned pos)
Removes variables of the specified kind with the specified pos (or within the specified range) from t...
unsigned getNumDimAndSymbolVars() const
void negateRow(unsigned row)
Negate the specified row.
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of var starts.
IntegerRelation(unsigned numReservedInequalities, unsigned numReservedEqualities, unsigned numReservedCols, const PresburgerSpace &space)
Constructs a relation reserving memory for the specified number of constraints and variables...
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.
void removeTrivialRedundancy()
Removes duplicate constraints, trivially true constraints, and constraints that can be detected as re...
bool isSubsetOf(const PresburgerRelation &set) const
Return true if this set is a subset of the given set, and false otherwise.
unsigned getNumDimVars() const
void constantFoldVarRange(unsigned pos, unsigned num)
This method calls constantFoldVar for the specified range of variables, num variables starting at pos...
void resizeVertically(unsigned newNRows)
PresburgerSet getDomain() const
Return the domain of this piece-wise MultiAffineFunction.
void applyRange(const IntegerRelation &rel)
Given a relation rel, apply the relation to the range of this relation.
static Value min(ImplicitLocOpBuilder &builder, Value value, Value bound)
void detectRedundant(unsigned offset, unsigned count)
Finds a subset of constraints that is redundant, i.e., such that the set of solutions does not change...
bool isSubsetOf(const IntegerRelation &other) const
Return whether this is a subset of the given IntegerRelation.
static void removeConstraintsInvolvingVarRange(IntegerRelation &poly, unsigned begin, unsigned count)
void append(const IntegerRelation &other)
Appends constraints from other into this.
LogicalResult gaussianEliminateVar(unsigned position)
Eliminates a single variable at position from equality and inequality constraints.
void addBound(BoundType type, unsigned pos, int64_t value)
Adds a constant bound for the specified variable.
bool containsPoint(ArrayRef< int64_t > point) const
Returns true if the given point satisfies the constraints, or false otherwise.
Represents the result of a symbolic lexicographic minimization computation.
void normalizeConstraintsByGCD()
Normalized each constraints by the GCD of its coefficients.
MaybeOptimum< SmallVector< int64_t, 8 > > findIntegerLexMin()
Return the lexicographically minimum integer solution to the constraints.
std::pair< MaybeOptimum< int64_t >, MaybeOptimum< int64_t > > computeIntegerBounds(ArrayRef< int64_t > coeffs)
Returns a (min, max) pair denoting the minimum and maximum integer values of the given expression...
virtual void printSpace(raw_ostream &os) const
Prints the number of constraints, dimensions, symbols and locals in the IntegerRelation.
void getLowerAndUpperBoundIndices(unsigned pos, SmallVectorImpl< unsigned > *lbIndices, SmallVectorImpl< unsigned > *ubIndices, SmallVectorImpl< unsigned > *eqIndices=nullptr, unsigned offset=0, unsigned num=0) const
Gather positions of all lower and upper bounds of the variable at pos, and optionally any equalities ...
PresburgerRelation computeReprWithOnlyDivLocals() const
Compute an equivalent representation of the same set, such that all local vars in all disjuncts have ...
void intersectDomain(const IntegerPolyhedron &poly)
Intersect the given poly with the domain in-place.
virtual void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
void removeIndependentConstraints(unsigned pos, unsigned num)
Removes constraints that are independent of (i.e., do not have a coefficient) variables in the range ...
bool isEmpty() const
Checks for emptiness by performing variable elimination on all variables, running the GCD test on eac...
SymbolicLexMin findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation.
const PresburgerSpace & getSpace() const
int64_t atEq(unsigned i, unsigned j) const
Returns the value at the specified equality row and column.
unsigned getNumCols() const
Returns the number of columns in the constraint system.
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin()
Return the lexicographically minimum rational solution to the constraints.
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
std::unique_ptr< IntegerRelation > clone() const
PWMAFunction lexmin
This maps assignments of symbols to the corresponding lexmin.
MaybeLocalRepr computeSingleVarRepr(const IntegerRelation &cst, ArrayRef< bool > foundRepr, unsigned pos, MutableArrayRef< int64_t > dividend, unsigned &divisor)
Returns the MaybeLocalRepr struct which contains the indices of the constraints that can be expressed...
unsigned getNumLocalVars() const
virtual void clearAndCopyFrom(const IntegerRelation &other)
Replaces the contents of this IntegerRelation with other.
void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
Removes variables of the specified kind in the column range [varStart, varLimit). ...
IntegerPolyhedron getDomainSet() const
Return a set corresponding to all points in the domain of the relation.
unsigned getNumDomainVars() const
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables...
Matrix getBoundedDirections() const
Returns a matrix where each row is a vector along which the polytope is bounded.
CountsSnapshot getCounts() const
A class for lexicographic optimization without any symbols.
Optional< SmallVector< int64_t, 8 > > containsPointNoLocal(ArrayRef< int64_t > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists...
bool isEqual(const PresburgerSpace &other) const
Returns true if both the spaces are equal including local variables i.e.
static bool rangeIsZero(ArrayRef< int64_t > range)
void convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit, VarKind dstKind, unsigned pos)
Converts variables of kind srcKind in the range [varStart, varLimit) to variables of kind dstKind...
void removeRedundantConstraints()
Removes redundant constraints using Simplex.
void removeEqualityRange(unsigned start, unsigned end)
Remove the (in)equalities at positions [start, end).
static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)
IntegerPolyhedron intersect(const IntegerPolyhedron &other) const
Return the intersection of the two relations.
Optional< int64_t > getConstantBound(BoundType type, unsigned pos) const
Returns the constant bound for the pos^th variable if there is one; None otherwise.
void removeColumns(unsigned pos, unsigned count)
Remove the columns having positions pos, pos + 1, ...
void setSpaceExceptLocals(const PresburgerSpace &oSpace)
Set the space to oSpace, which should not have any local ids.
static PresburgerSpace getSetSpace(unsigned numDims=0, unsigned numSymbols=0, unsigned numLocals=0)
Optional< SmallVector< int64_t, 8 > > findIntegerSample() const
Find an integer sample point satisfying the constraints using a branch and bound algorithm with gener...
const PresburgerSpace & getSpace() const
Returns a reference to the underlying space.
static Value max(ImplicitLocOpBuilder &builder, Value value, Value bound)
Optional< SmallVector< int64_t, 8 > > findIntegerSample()
Returns an integer sample point if one exists, or None otherwise.