23 #include "llvm/ADT/DenseMap.h"
24 #include "llvm/ADT/STLExtras.h"
25 #include "llvm/ADT/Sequence.h"
26 #include "llvm/ADT/SmallBitVector.h"
27 #include "llvm/Support/Debug.h"
28 #include "llvm/Support/raw_ostream.h"
37 #define DEBUG_TYPE "presburger"
40 using namespace presburger;
42 using llvm::SmallDenseMap;
45 return std::make_unique<IntegerRelation>(*
this);
49 return std::make_unique<IntegerPolyhedron>(*
this);
58 assert(oSpace.
getNumLocalVars() == 0 &&
"no locals should be present!");
67 "space must be using identifiers to set an identifier");
116 for (
unsigned j = 0;
j <
cols; ++
j) {
122 for (
unsigned j = 0;
j <
cols; ++
j) {
150 "Incorrect number of vars in lexMin!");
170 "Incorrect number of vars in lexMin!");
176 return llvm::all_of(range, [](
const DynamicAPInt &x) {
return x == 0; });
180 unsigned begin,
unsigned count) {
199 assert(num <= curNum &&
"Can't truncate to more vars!");
228 copy.getLocalReprs(&reprs);
232 unsigned numNonDivLocals = 0;
234 for (
unsigned i = 0, e =
copy.getNumLocalVars(); i < e - numNonDivLocals;) {
239 copy.swapVar(offset + i, offset + e - numNonDivLocals - 1);
240 std::swap(reprs[i], reprs[e - numNonDivLocals - 1]);
248 if (numNonDivLocals == 0)
265 copy.getNumVars() - numNonDivLocals)))
282 llvm::SmallBitVector isSymbol(
getNumVars(),
false);
326 symbolicIntegerLexMax(
329 for (
auto &flippedPiece :
331 IntMatrix mat = flippedPiece.output.getOutputMatrix();
332 for (
unsigned i = 0, e = mat.
getNumRows(); i < e; i++)
336 symbolicIntegerLexMax.lexopt.addPiece(piece);
338 symbolicIntegerLexMax.unboundedDomain =
340 return symbolicIntegerLexMax;
365 for (
unsigned i = 0, e = eq.size(); i < e; ++i)
372 for (
unsigned i = 0, e = inEq.size(); i < e; ++i)
386 if (varStart >= varLimit)
401 if (varStart >= varLimit)
407 auto removeVarKindInRange = [
this](
VarKind kind,
unsigned &start,
416 unsigned relativeStart =
417 start <= offset ? 0 :
std::min(num, start - offset);
418 unsigned relativeLimit =
419 limit <= offset ? 0 :
std::min(num, limit - offset);
427 limit -= relativeLimit - relativeStart;
457 assert(posA <
getNumVars() &&
"invalid position A");
458 assert(posB <
getNumVars() &&
"invalid position B");
467 space.
swapVar(kindA, kindB, relativePosA, relativePosB);
484 unsigned offset,
unsigned num)
const {
485 assert(pos <
getNumVars() &&
"invalid position");
486 assert(offset + num <
getNumCols() &&
"invalid range");
490 auto containsConstraintDependentOnRange = [&](
unsigned r,
bool isEq) {
493 for (c = offset, f = offset + num; c < f; ++c) {
507 if (containsConstraintDependentOnRange(r,
false))
509 if (
atIneq(r, pos) >= 1) {
511 lbIndices->emplace_back(r);
512 }
else if (
atIneq(r, pos) <= -1) {
514 ubIndices->emplace_back(r);
524 if (
atEq(r, pos) == 0)
526 if (containsConstraintDependentOnRange(r,
true))
528 eqIndices->emplace_back(r);
545 "invalid position or too many values");
550 for (
unsigned i = 0, numVals = values.size(); i < numVals; ++i)
552 for (
unsigned i = 0, numVals = values.size(); i < numVals; ++i)
561 std::optional<unsigned>
563 assert(colIdx <
getNumCols() &&
"position out of bounds");
564 auto at = [&](
unsigned rowIdx) -> DynamicAPInt {
565 return isEq ?
atEq(rowIdx, colIdx) :
atIneq(rowIdx, colIdx);
568 for (
unsigned rowIdx = 0; rowIdx < e; ++rowIdx) {
584 auto check = [&](
bool isEq) ->
bool {
587 for (
unsigned i = 0, e = numRows; i < e; ++i) {
589 for (
j = 0;
j < numCols - 1; ++
j) {
595 if (
j < numCols - 1) {
600 DynamicAPInt v = isEq ?
atEq(i, numCols - 1) :
atIneq(i, numCols - 1);
601 if ((isEq && v != 0) || (!isEq && v < 0)) {
616 unsigned rowIdx,
unsigned pivotRow,
617 unsigned pivotCol,
unsigned elimColStart,
620 if (isEq && rowIdx == pivotRow)
622 auto at = [&](
unsigned i,
unsigned j) -> DynamicAPInt {
623 return isEq ? constraints->
atEq(i,
j) : constraints->
atIneq(i,
j);
625 DynamicAPInt leadCoeff = at(rowIdx, pivotCol);
629 DynamicAPInt pivotCoeff = constraints->
atEq(pivotRow, pivotCol);
630 int sign = (leadCoeff * pivotCoeff > 0) ? -1 : 1;
631 DynamicAPInt lcm = llvm::lcm(pivotCoeff, leadCoeff);
632 DynamicAPInt pivotMultiplier = sign * (lcm /
abs(pivotCoeff));
633 DynamicAPInt rowMultiplier = lcm /
abs(leadCoeff);
636 for (
unsigned j = 0;
j < numCols; ++
j) {
638 if (
j >= elimColStart &&
j < pivotCol)
640 DynamicAPInt v = pivotMultiplier * constraints->
atEq(pivotRow,
j) +
641 rowMultiplier * at(rowIdx,
j);
642 isEq ? constraints->
atEq(rowIdx,
j) = v
643 : constraints->
atIneq(rowIdx,
j) = v;
653 unsigned start,
unsigned end) {
656 auto getProductOfNumLowerUpperBounds = [&](
unsigned pos) {
660 if (cst.
atIneq(r, pos) > 0) {
662 }
else if (cst.
atIneq(r, pos) < 0) {
666 return numLb * numUb;
669 unsigned minLoc = start;
670 unsigned min = getProductOfNumLowerUpperBounds(start);
671 for (
unsigned c = start + 1; c < end; c++) {
672 unsigned numLbUbProduct = getProductOfNumLowerUpperBounds(c);
673 if (numLbUbProduct <
min) {
674 min = numLbUbProduct;
697 unsigned currentPos = 0;
710 for (
unsigned i = 0, e = tmpCst.
getNumVars(); i < e; i++) {
719 LLVM_DEBUG(llvm::dbgs() <<
"FM constraint explosion detected\n");
753 DynamicAPInt gcd =
abs(
atEq(i, 0));
754 for (
unsigned j = 1;
j < numCols - 1; ++
j) {
755 gcd = llvm::gcd(gcd,
abs(
atEq(i,
j)));
757 DynamicAPInt v =
abs(
atEq(i, numCols - 1));
758 if (gcd > 0 && (v % gcd != 0)) {
779 assert(!simplex.
isEmpty() &&
"It is not meaningful to ask whether a "
780 "direction is bounded in an empty set.");
787 boundedIneqs.emplace_back(i);
797 for (
unsigned i : boundedIneqs) {
798 for (
unsigned col = 0; col < dirsNumCols; ++col)
799 dirs(row, col) =
atIneq(i, col);
805 for (
unsigned col = 0; col < dirsNumCols; ++col)
806 dirs(row, col) =
atEq(i, col);
860 std::optional<SmallVector<DynamicAPInt, 8>>
884 std::pair<unsigned, LinearTransform> result =
893 unsigned numBoundedDims = result.first;
894 unsigned numUnboundedDims =
getNumVars() - numBoundedDims;
900 std::optional<SmallVector<DynamicAPInt, 8>> boundedSample =
905 "Simplex returned an invalid sample!");
939 DynamicAPInt coeff = cone.
atIneq(i,
j);
949 Simplex shrunkenConeSimplex(cone);
950 assert(!shrunkenConeSimplex.
isEmpty() &&
"Shrunken cone cannot be empty!");
957 llvm::map_range(shrunkenConeSample,
ceil));
961 sample.append(coneSample.begin(), coneSample.end());
970 assert(expr.size() == 1 + point.size() &&
971 "Dimensionalities of point and expression don't match!");
972 DynamicAPInt value = expr.back();
973 for (
unsigned i = 0; i < point.size(); ++i)
974 value += expr[i] * point[i];
1001 std::optional<SmallVector<DynamicAPInt, 8>>
1004 "Point should contain all vars except locals!");
1006 "This function depends on locals being stored last!");
1008 copy.setAndEliminate(0, point);
1009 return copy.findIntegerSample();
1016 foundRepr[i] =
true;
1026 if (!foundRepr[i + localOffset]) {
1036 foundRepr[localOffset + i] =
true;
1061 atIneq(i, numCols - 1) = floorDiv(
atIneq(i, numCols - 1), gcd);
1068 unsigned posLimit) {
1073 if (posStart >= posLimit)
1078 unsigned pivotCol = 0;
1079 for (pivotCol = posStart; pivotCol < posLimit; ++pivotCol) {
1081 std::optional<unsigned> pivotRow =
1108 posLimit = pivotCol;
1111 return posLimit - posStart;
1117 unsigned nowDone, eqs;
1118 std::optional<unsigned> pivotRow;
1121 for (; firstVar < vars; ++firstVar) {
1126 if (firstVar >= vars)
1130 if (*pivotRow > nowDone) {
1132 *pivotRow = nowDone;
1136 for (
unsigned i = nowDone + 1; i < eqs; ++i) {
1153 for (
unsigned i = nowDone; i < eqs; ++i) {
1154 if (
atEq(i, vars) == 0)
1211 for (
unsigned r = 0; r < numIneqs; r++) {
1237 return DynamicAPInt(0);
1253 DynamicAPInt count(1);
1255 bool hasUnboundedVar =
false;
1261 assert((!
min.isEmpty() && !
max.isEmpty()) &&
1262 "Polytope should be rationally non-empty!");
1266 if (
min.isUnbounded() ||
max.isUnbounded()) {
1267 hasUnboundedVar =
true;
1273 if (
min.getBoundedOptimum() >
max.getBoundedOptimum())
1274 return DynamicAPInt(0);
1276 count *= (*
max - *
min + 1);
1280 return DynamicAPInt(0);
1281 if (hasUnboundedVar)
1291 posA += localOffset;
1292 posB += localOffset;
1305 "both relations need to have identifers to merge and align");
1314 const Identifier *itr = std::find(findBegin, findEnd, identifier);
1315 if (itr != findEnd) {
1318 std::distance(findBegin, itr));
1353 auto merge = [&relA, &relB, oldALocals](
unsigned i,
unsigned j) ->
bool {
1382 auto merge = [
this](
unsigned i,
unsigned j) ->
bool {
1416 unsigned i, e,
j, f;
1435 if (
atEq(k,
j) != 0) {
1452 unsigned varLimit,
VarKind dstKind,
1454 assert(varLimit <=
getNumVarKind(srcKind) &&
"invalid id range");
1456 if (varStart >= varLimit)
1461 unsigned convertCount = varLimit - varStart;
1462 int forwardMoveOffset = dstOffset > srcOffset ? -convertCount : 0;
1465 dstOffset + pos + forwardMoveOffset);
1467 dstOffset + pos + forwardMoveOffset);
1473 const DynamicAPInt &value) {
1488 const DynamicAPInt &value) {
1492 for (
unsigned i = 0, e = expr.size(); i < e; ++i)
1505 const DynamicAPInt &divisor) {
1506 assert(dividend.size() ==
getNumCols() &&
"incorrect dividend size");
1507 assert(divisor > 0 &&
"positive divisor expected");
1512 dividendCopy.insert(dividendCopy.end() - 1, DynamicAPInt(0));
1521 const DynamicAPInt &modulus) {
1522 assert(exprs.size() ==
getNumCols() &&
"incorrect exprs size");
1523 assert(modulus > 0 &&
"positive modulus expected");
1535 exprsCopy.insert(exprsCopy.end() - 1,
1536 {DynamicAPInt(-modulus), DynamicAPInt(-1)});
1542 assert(pos <
getNumVars() &&
"invalid position");
1544 DynamicAPInt v =
atEq(r, pos);
1550 for (c = 0; c < f; c++) {
1553 if (
atEq(r, c) != 0) {
1566 assert(pos <
getNumVars() &&
"invalid position");
1572 assert(
atEq(rowIdx, pos) *
atEq(rowIdx, pos) == 1);
1579 for (
unsigned s = pos, t = pos, e = pos + num; s < e; s++) {
1602 unsigned *minLbPos,
unsigned *minUbPos)
const {
1603 assert(pos <
getNumDimVars() &&
"Invalid variable position");
1615 [](
const DynamicAPInt &coeff) { return coeff == 0; }))
1616 return std::nullopt;
1625 DynamicAPInt v =
atEq(eqPos, pos);
1632 (*ub)[c] = (*lb)[c];
1634 assert(boundFloorDivisor &&
1635 "both lb and divisor or none should be provided");
1636 *boundFloorDivisor = 1;
1642 return DynamicAPInt(1);
1653 return std::nullopt;
1666 std::optional<DynamicAPInt> minDiff;
1667 unsigned minLbPosition = 0, minUbPosition = 0;
1668 for (
auto ubPos : ubIndices) {
1669 for (
auto lbPos : lbIndices) {
1687 diff = std::max<DynamicAPInt>(diff, DynamicAPInt(0));
1688 if (minDiff == std::nullopt || diff < minDiff) {
1690 minLbPosition = lbPos;
1691 minUbPosition = ubPos;
1695 if (lb && minDiff) {
1704 *boundFloorDivisor =
atIneq(minLbPosition, pos);
1705 assert(*boundFloorDivisor == -
atIneq(minUbPosition, pos));
1720 *minLbPos = minLbPosition;
1722 *minUbPos = minUbPosition;
1726 template <
bool isLower>
1727 std::optional<DynamicAPInt>
1729 assert(pos <
getNumVars() &&
"invalid position");
1747 return std::nullopt;
1749 std::optional<DynamicAPInt> minOrMaxConst;
1758 }
else if (
atIneq(r, 0) >= 0) {
1763 for (c = 0, f =
getNumCols() - 1; c < f; c++)
1764 if (c != 0 &&
atIneq(r, c) != 0)
1770 DynamicAPInt boundConst =
1774 if (minOrMaxConst == std::nullopt || boundConst > minOrMaxConst)
1775 minOrMaxConst = boundConst;
1777 if (minOrMaxConst == std::nullopt || boundConst < minOrMaxConst)
1778 minOrMaxConst = boundConst;
1781 return minOrMaxConst;
1784 std::optional<DynamicAPInt>
1788 .computeConstantLowerOrUpperBound<
true>(pos);
1791 .computeConstantLowerOrUpperBound<
false>(pos);
1794 std::optional<DynamicAPInt> lb =
1797 std::optional<DynamicAPInt> ub =
1799 .computeConstantLowerOrUpperBound<
false>(pos);
1800 return (lb && ub && *lb == *ub) ? std::optional<DynamicAPInt>(*ub)
1810 for (
unsigned c = pos; c < pos + num; c++) {
1819 for (
unsigned c = pos; c < pos + num; c++) {
1820 if (
atEq(r, c) != 0)
1842 SmallDenseMap<ArrayRef<DynamicAPInt>, std::pair<unsigned, DynamicAPInt>>
1843 rowsWithoutConstTerm;
1846 auto isTriviallyValid = [&](
unsigned r) ->
bool {
1847 for (
unsigned c = 0, e =
getNumCols() - 1; c < e; c++) {
1858 if (isTriviallyValid(r)) {
1859 redunIneq[r] =
true;
1868 auto rowWithoutConstTerm =
1871 rowsWithoutConstTerm.insert({rowWithoutConstTerm, {r, constTerm}});
1874 auto &val = ret.first->second;
1875 if (val.second > constTerm) {
1877 redunIneq[val.first] =
true;
1878 val = {r, constTerm};
1881 redunIneq[r] =
true;
1899 #define DEBUG_TYPE "fm"
1945 bool *isResultIntegerExact) {
1946 LLVM_DEBUG(llvm::dbgs() <<
"FM input (eliminate pos " << pos <<
"):\n");
1948 assert(pos <
getNumVars() &&
"invalid position");
1953 if (
atEq(r, pos) != 0) {
1957 assert(ret.succeeded() &&
"Gaussian elimination guaranteed to succeed");
1958 LLVM_DEBUG(llvm::dbgs() <<
"FM output (through Gaussian elimination):\n");
1972 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
1982 std::vector<unsigned> nbIndices;
1989 if (
atIneq(r, pos) == 0) {
1991 nbIndices.emplace_back(r);
1992 }
else if (
atIneq(r, pos) >= 1) {
1994 lbIndices.emplace_back(r);
1997 ubIndices.emplace_back(r);
2004 newSpace.
removeVarRange(idKindRemove, relativePos, relativePos + 1);
2007 IntegerRelation newRel(lbIndices.size() * ubIndices.size() + nbIndices.size(),
2011 bool allLCMsAreOne =
true;
2023 for (
auto ubPos : ubIndices) {
2024 for (
auto lbPos : lbIndices) {
2027 DynamicAPInt lbCoeff =
atIneq(lbPos, pos);
2031 DynamicAPInt ubCoeff = -
atIneq(ubPos, pos);
2033 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2036 assert(lbCoeff >= 1 && ubCoeff >= 1 &&
"bounds wrongly identified");
2037 DynamicAPInt lcm = llvm::lcm(lbCoeff, ubCoeff);
2038 ineq.emplace_back(
atIneq(ubPos, l) * (lcm / ubCoeff) +
2039 atIneq(lbPos, l) * (lcm / lbCoeff));
2040 assert(lcm > 0 &&
"lcm should be positive!");
2042 allLCMsAreOne =
false;
2047 ineq[ineq.size() - 1] += lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
2055 LLVM_DEBUG(llvm::dbgs() <<
"FM isResultIntegerExact: " << allLCMsAreOne
2057 if (allLCMsAreOne && isResultIntegerExact)
2058 *isResultIntegerExact =
true;
2061 for (
auto nbPos : nbIndices) {
2064 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2067 ineq.emplace_back(
atIneq(nbPos, l));
2073 lbIndices.size() * ubIndices.size() + nbIndices.size());
2079 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2082 eq.emplace_back(
atEq(r, l));
2093 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
2098 #define DEBUG_TYPE "presburger"
2106 assert(pos + num <
getNumCols() &&
"invalid range");
2109 unsigned currentPos = pos;
2110 unsigned numToEliminate = num;
2111 unsigned numGaussianEliminated = 0;
2114 unsigned curNumEliminated =
2117 numToEliminate -= curNumEliminated + 1;
2118 numGaussianEliminated += curNumEliminated;
2122 for (
unsigned i = 0; i < num - numGaussianEliminated; i++) {
2123 unsigned numToEliminate = num - numGaussianEliminated - i;
2137 enum BoundCmpResult { Greater, Less, Equal, Unknown };
2143 assert(a.size() == b.size());
2149 if (!std::equal(a.begin(), a.end() - 1, b.begin()))
2152 if (a.back() == b.back())
2155 return a.back() < b.back() ? Less : Greater;
2194 std::vector<SmallVector<DynamicAPInt, 8>> boundingLbs;
2195 std::vector<SmallVector<DynamicAPInt, 8>> boundingUbs;
2207 DynamicAPInt lbFloorDivisor, otherLbFloorDivisor;
2210 if (!extent.has_value())
2216 d, &otherLb, &otherLbFloorDivisor, &otherUb);
2217 if (!otherExtent.has_value() || lbFloorDivisor != otherLbFloorDivisor)
2221 assert(lbFloorDivisor > 0 &&
"divisor always expected to be positive");
2223 auto res = compareBounds(lb, otherLb);
2225 if (res == BoundCmpResult::Less || res == BoundCmpResult::Equal) {
2230 minLb.back() -= lbFloorDivisor - 1;
2231 }
else if (res == BoundCmpResult::Greater) {
2233 minLb.back() -= otherLbFloorDivisor - 1;
2238 if (!constLb.has_value() || !constOtherLb.has_value())
2240 llvm::fill(minLb, 0);
2241 minLb.back() =
std::min(*constLb, *constOtherLb);
2245 auto uRes = compareBounds(ub, otherUb);
2246 if (uRes == BoundCmpResult::Greater || uRes == BoundCmpResult::Equal) {
2248 }
else if (uRes == BoundCmpResult::Less) {
2254 if (!constUb.has_value() || !constOtherUb.has_value())
2256 llvm::fill(maxUb, 0);
2257 maxUb.back() =
std::max(*constUb, *constOtherUb);
2260 llvm::fill(newLb, 0);
2261 llvm::fill(newUb, 0);
2265 newLb[d] = lbFloorDivisor;
2266 newUb[d] = -lbFloorDivisor;
2269 std::transform(newLb.begin() +
getNumDimVars(), newLb.end(),
2271 std::negate<DynamicAPInt>());
2274 boundingLbs.emplace_back(newLb);
2275 boundingUbs.emplace_back(newUb);
2307 assert(pos < cst.
getNumVars() &&
"invalid start position");
2308 assert(pos + num <= cst.
getNumVars() &&
"invalid limit");
2313 for (c = pos; c < pos + num; ++c) {
2314 if (cst.
atIneq(r, c) != 0)
2318 nbIneqIndices.emplace_back(r);
2324 for (c = pos; c < pos + num; ++c) {
2325 if (cst.
atEq(r, c) != 0)
2329 nbEqIndices.emplace_back(r);
2334 assert(pos + num <=
getNumVars() &&
"invalid range");
2343 for (
auto nbIndex : llvm::reverse(nbIneqIndices))
2345 for (
auto nbIndex : llvm::reverse(nbEqIndices))
2365 SmallDenseMap<ArrayRef<DynamicAPInt>,
unsigned> hashTable;
2373 hashTable.insert({row, 0});
2374 for (
unsigned k = 1; k < ineqs; ++k) {
2376 if (hashTable.try_emplace(row, k).second)
2380 unsigned l = hashTable[row];
2391 for (
unsigned k = 0; k < ineqs; ++k) {
2393 negIneq.assign(row.begin(), row.end());
2394 for (DynamicAPInt &ele : negIneq)
2396 if (!hashTable.contains(negIneq))
2401 unsigned l = hashTable[row];
2403 if (sum > 0 || l == k)
2439 "Domain set is not compatible with poly");
2455 "Range set is not compatible with poly");
2475 "Range of `this` should be compatible with Domain of `rel`");
2512 "Range product is only defined for relations with equal domains");
2529 copy.insert(
copy.begin() + relRangeVarStart,
2530 numThisRangeVars + numNewSymbolVars, DynamicAPInt(0));
2537 copy.insert(
copy.begin() + relRangeVarStart,
2538 numThisRangeVars + numNewSymbolVars, DynamicAPInt(0));
2577 "Domain of this and range of other do not match");
2640 updatePrintMetrics<DynamicAPInt>(
atEq(i,
j), ptm);
2643 updatePrintMetrics<DynamicAPInt>(
atIneq(i,
j), ptm);
2645 constexpr
unsigned kMinSpacing = 1;
2648 printWithPrintMetrics<DynamicAPInt>(os,
atEq(i,
j), kMinSpacing, ptm);
2654 printWithPrintMetrics<DynamicAPInt>(os,
atIneq(i,
j), kMinSpacing, ptm);
2666 "Domain has to be zero in a set");
static void copy(Location loc, Value dst, Value src, Value size, OpBuilder &builder)
Copies the given number of bytes from src to dst pointers.
static bool rangeIsZero(ArrayRef< DynamicAPInt > range)
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,...
static void removeConstraintsInvolvingVarRange(IntegerRelation &poly, unsigned begin, unsigned count)
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 <number of u...
static void getCommonConstraints(const IntegerRelation &a, const IntegerRelation &b, IntegerRelation &c)
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.
static DynamicAPInt valueAt(ArrayRef< DynamicAPInt > expr, ArrayRef< DynamicAPInt > point)
Helper to evaluate an affine expression at a point.
union mlir::linalg::@1244::ArityGroupAndKind::Kind kind
static Value max(ImplicitLocOpBuilder &builder, Value value, Value bound)
static Value min(ImplicitLocOpBuilder &builder, Value value, Value bound)
Class storing division representation of local variables of a constraint system.
void removeDuplicateDivs(llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Removes duplicate divisions.
void clearRepr(unsigned i)
DynamicAPInt & getDenom(unsigned i)
MutableArrayRef< DynamicAPInt > getDividend(unsigned i)
An Identifier stores a pointer to an object, such as a Value or an Operation.
DynamicAPInt normalizeRow(unsigned row, unsigned nCols)
Divide the first nCols of the specified row by their GCD.
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
IntegerPolyhedron intersect(const IntegerPolyhedron &other) const
Return the intersection of the two relations.
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1) override
Insert num variables of the specified kind at position pos.
PresburgerSet subtract(const PresburgerSet &other) const
Return the set difference of this set and the given set, i.e., return this \ set.
IntegerPolyhedron(unsigned numReservedInequalities, unsigned numReservedEqualities, unsigned numReservedCols, const PresburgerSpace &space)
Constructs a set reserving memory for the specified number of constraints and variables.
std::unique_ptr< IntegerPolyhedron > clone() const
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
std::optional< DynamicAPInt > getConstantBoundOnDimSize(unsigned pos, SmallVectorImpl< DynamicAPInt > *lb=nullptr, DynamicAPInt *boundFloorDivisor=nullptr, SmallVectorImpl< DynamicAPInt > *ub=nullptr, unsigned *minLbPos=nullptr, unsigned *minUbPos=nullptr) const
Returns the smallest known constant bound for the extent of the specified variable (pos^th),...
void setId(VarKind kind, unsigned i, Identifier id)
Set the identifier for the ith variable of the specified kind of the IntegerRelation's PresburgerSpac...
virtual void swapVar(unsigned posA, unsigned posB)
Swap the posA^th variable with the posB^th variable.
void removeIndependentConstraints(unsigned pos, unsigned num)
Removes constraints that are independent of (i.e., do not have a coefficient) variables in the range ...
void compose(const IntegerRelation &rel)
Let the relation this be R1, and the relation rel be R2.
void applyRange(const IntegerRelation &rel)
Given a relation rel, apply the relation to the range of this relation.
unsigned getVarKindEnd(VarKind kind) const
Return the index at Which the specified kind of vars ends.
ArrayRef< Identifier > getIds(VarKind kind)
Get the identifiers for the variables of specified varKind.
void removeTrivialRedundancy()
Removes duplicate constraints, trivially true constraints, and constraints that can be detected as re...
unsigned addLocalModulo(ArrayRef< DynamicAPInt > exprs, const DynamicAPInt &modulus)
Adds a new local variable as the modulus of an affine function of other variables,...
static IntegerRelation getEmpty(const PresburgerSpace &space)
Return an empty system containing an invalid equation 0 = 1.
std::optional< unsigned > findConstraintWithNonZeroAt(unsigned colIdx, bool isEq) const
Finds a constraint with a non-zero coefficient at colIdx in equality (isEq=true) or inequality (isEq=...
void removeInequalityRange(unsigned start, unsigned end)
void normalizeConstraintsByGCD()
Normalized each constraints by the GCD of its coefficients.
void truncate(const CountsSnapshot &counts)
virtual void eliminateRedundantLocalVar(unsigned posA, unsigned posB)
Eliminate the posB^th local variable, replacing every instance of it with the posA^th local variable.
CountsSnapshot getCounts() const
std::optional< DynamicAPInt > computeConstantLowerOrUpperBound(unsigned pos)
Returns the constant lower bound if isLower is true, and the upper bound if isLower is false.
void removeEqualityRange(unsigned start, unsigned end)
Remove the (in)equalities at positions [start, end).
LogicalResult constantFoldVar(unsigned pos)
Tries to fold the specified variable to a constant using a trivial equality detection; if successful,...
unsigned getNumSymbolVars() const
void removeEquality(unsigned pos)
bool isObviouslyEqual(const IntegerRelation &other) const
Perform a quick equality check on this and other.
IntegerPolyhedron getRangeSet() const
Return a set corresponding to all points in the range of the relation.
std::optional< SmallVector< DynamicAPInt, 8 > > containsPointNoLocal(ArrayRef< DynamicAPInt > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists,...
ArrayRef< DynamicAPInt > getInequality(unsigned idx) const
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
bool isEmptyByGCDTest() const
Runs the GCD test on all equality constraints.
void simplify()
Simplify the constraint system by removing canonicalizing constraints and removing redundant constrai...
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 removeDuplicateDivs()
void addBound(BoundType type, unsigned pos, const DynamicAPInt &value)
Adds a constant bound for the specified variable.
unsigned appendVar(VarKind kind, unsigned num=1)
Append num variables of the specified kind after the last variable of that kind.
void intersectRange(const IntegerPolyhedron &poly)
Intersect the given poly with the range in-place.
IntegerRelation rangeProduct(const IntegerRelation &rel)
Let the relation this be R1, and the relation rel be R2.
void print(raw_ostream &os) const
bool isIntegerEmpty() const
Returns true if the set of constraints is found to have no solution, false if a solution exists.
DynamicAPInt atIneq(unsigned i, unsigned j) const
Returns the value at the specified inequality row and column.
virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
bool containsPoint(ArrayRef< DynamicAPInt > point) const
Returns true if the given point satisfies the constraints, or false otherwise.
std::optional< SmallVector< DynamicAPInt, 8 > > findIntegerSample() const
Find an integer sample point satisfying the constraints using a branch and bound algorithm with gener...
bool hasInvalidConstraint() const
Checks all rows of equality/inequality constraints for trivial contradictions (for example: 1 == 0,...
LogicalResult unionBoundingBox(const IntegerRelation &other)
Updates the constraints to be the smallest bounding (enclosing) box that contains the points of this ...
IntegerRelation(unsigned numReservedInequalities, unsigned numReservedEqualities, unsigned numReservedCols, const PresburgerSpace &space)
Constructs a relation reserving memory for the specified number of constraints and variables.
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 convertToLocal(VarKind kind, unsigned varStart, unsigned varLimit)
IntMatrix getBoundedDirections() const
Returns a matrix where each row is a vector along which the polytope is bounded.
unsigned getNumDomainVars() const
LogicalResult gaussianEliminateVar(unsigned position)
Eliminates a single variable at position from equality and inequality constraints.
void clearConstraints()
Removes all equalities and inequalities.
DynamicAPInt atEq(unsigned i, unsigned j) const
Returns the value at the specified equality row and column.
IntegerRelation intersect(IntegerRelation other) const
Return the intersection of the two relations.
std::optional< DynamicAPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the relation.
MaybeOptimum< SmallVector< DynamicAPInt, 8 > > findIntegerLexMin() const
Same as above, but returns lexicographically minimal integer point.
void removeTrivialEqualities()
SymbolicLexOpt findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation.
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace, which should have the same number of ids as the current space.
int findEqualityToConstant(unsigned pos, bool symbolic=false) const
Finds an equality that equates the specified variable to a constant.
unsigned getNumVars() const
void inverse()
Invert the relation i.e., swap its domain and range.
void append(const IntegerRelation &other)
Appends constraints from other into this.
void applyDomain(const IntegerRelation &rel)
Given a relation rel, apply the relation to the domain of this relation.
void intersectDomain(const IntegerPolyhedron &poly)
Intersect the given poly with the domain in-place.
unsigned addLocalFloorDiv(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
Adds a new local variable as the floordiv of an affine function of other variables,...
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
bool isEqual(const IntegerRelation &other) const
Return whether this and other are equal.
virtual void printSpace(raw_ostream &os) const
Prints the number of constraints, dimensions, symbols and locals in the IntegerRelation.
void addEquality(ArrayRef< DynamicAPInt > eq)
Adds an equality from the coefficients specified in eq.
unsigned getNumRangeVars() const
unsigned getNumLocalVars() const
void removeRedundantConstraints()
Removes redundant constraints using Simplex.
PresburgerRelation computeReprWithOnlyDivLocals() const
Compute an equivalent representation of the same set, such that all local vars in all disjuncts have ...
void removeRedundantInequalities()
A more expensive check than removeTrivialRedundancy to detect redundant inequalities.
bool isObviouslyEmpty() const
Performs GCD checks and invalid constraint checks.
IntMatrix equalities
Coefficients of affine equalities (in == 0 form).
SymbolicLexOpt findSymbolicIntegerLexMax() const
Same as findSymbolicIntegerLexMin but produces lexmax instead of lexmin.
unsigned getNumDimAndSymbolVars() const
bool gaussianEliminate()
Perform a Gaussian elimination operation to reduce all equations to standard form.
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 constantFoldVarRange(unsigned pos, unsigned num)
This method calls constantFoldVar for the specified range of variables, num variables starting at pos...
bool isEmpty() const
Checks for emptiness by performing variable elimination on all variables, running the GCD test on eac...
unsigned getNumCols() const
Returns the number of columns in the constraint system.
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 ...
void gcdTightenInequalities()
Tightens inequalities given that we are dealing with integer spaces.
void removeVar(VarKind kind, unsigned pos)
Removes variables of the specified kind with the specified pos (or within the specified range) from t...
void setSpaceExceptLocals(const PresburgerSpace &oSpace)
Set the space to oSpace, which should not have any local ids.
unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit)
Eliminates variables from equality and inequality constraints in column range [posStart,...
void removeInequality(unsigned pos)
void mergeAndCompose(const IntegerRelation &other)
Given a relation other: (A -> B), this operation merges the symbol and local variables and then takes...
IntegerPolyhedron getDomainSet() const
Return a set corresponding to all points in the domain of the relation.
DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const
Returns a DivisonRepr representing the division representation of local variables in the constraint s...
bool hasOnlyDivLocals() const
Check whether all local ids have a division representation.
constexpr static unsigned kExplosionFactor
A parameter that controls detection of an unrealistic number of constraints.
std::optional< DynamicAPInt > getConstantBound(BoundType type, unsigned pos) const
Returns the constant bound for the pos^th variable if there is one; std::nullopt otherwise.
virtual void clearAndCopyFrom(const IntegerRelation &other)
Replaces the contents of this IntegerRelation with other.
void projectOut(unsigned pos, unsigned num)
Projects out (aka eliminates) num variables starting at position pos.
void addInequality(ArrayRef< DynamicAPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
void mergeAndAlignSymbols(IntegerRelation &other)
Merge and align symbol variables of this and other with respect to identifiers.
void removeRedundantLocalVars()
Removes local variables using equalities.
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...
unsigned getNumConstraints() const
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin() const
Get the lexicographically minimum rational point satisfying the constraints.
IntMatrix inequalities
Coefficients of affine inequalities (in >= 0 form).
virtual bool hasConsistentState() const
Returns false if the fields corresponding to various variable counts, or equality/inequality buffer s...
ArrayRef< DynamicAPInt > getEquality(unsigned idx) const
unsigned getNumInequalities() const
bool isSubsetOf(const IntegerRelation &other) const
Return whether this is a subset of the given IntegerRelation.
std::unique_ptr< IntegerRelation > clone() const
const PresburgerSpace & getSpace() const
Returns a reference to the underlying space.
void setAndEliminate(unsigned pos, ArrayRef< DynamicAPInt > values)
Sets the values.size() variables starting at pos to the specified values and removes them.
unsigned getNumEqualities() const
bool isColZero(unsigned pos) const
Returns true if the pos^th column is all zero for both inequalities and equalities.
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of vars starts.
unsigned getNumDimVars() const
virtual void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
virtual void fourierMotzkinEliminate(unsigned pos, bool darkShadow=false, bool *isResultIntegerExact=nullptr)
Eliminates the variable at the specified position using Fourier-Motzkin variable elimination,...
bool removeDuplicateConstraints()
Checks for identical inequalities and eliminates redundant inequalities.
A class for lexicographic optimization without any symbols.
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin()
Return the lexicographically minimum rational solution to the constraints.
MaybeOptimum< SmallVector< DynamicAPInt, 8 > > findIntegerLexMin()
Return the lexicographically minimum integer solution to the constraints.
void moveColumns(unsigned srcPos, unsigned num, unsigned dstPos)
Move the columns in the source range [srcPos, srcPos + num) to the specified destination [dstPos,...
bool hasConsistentState() const
Return whether the Matrix is in a consistent state with all its invariants satisfied.
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.
void addToColumn(unsigned sourceColumn, unsigned targetColumn, const T &scale)
Add scale multiples of the source column to the target column.
void copyRow(unsigned sourceRow, unsigned targetRow)
void removeColumns(unsigned pos, unsigned count)
Remove the columns having positions pos, pos + 1, ...
void insertColumns(unsigned pos, unsigned count)
Insert columns having positions pos, pos + 1, ...
void removeRow(unsigned pos)
void resizeVertically(unsigned newNRows)
void swapRows(unsigned row, unsigned otherRow)
Swap the given rows.
void reserveRows(unsigned rows)
Reserve enough space to resize to the specified number of rows without reallocations.
void fillRow(unsigned row, const T &value)
void negateRow(unsigned row)
Negate the specified row.
void removeRows(unsigned pos, unsigned count)
Remove the rows having positions pos, pos + 1, ...
OptimumKind getKind() const
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 removeOutputs(unsigned start, unsigned end)
Remove the specified range of outputs.
unsigned getNumOutputs() const
ArrayRef< Piece > getAllPieces() const
Return all the pieces of this piece-wise function.
PresburgerSet getDomain() const
Return the domain of this piece-wise MultiAffineFunction.
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
bool isSubsetOf(const PresburgerRelation &set) const
Return true if this set is a subset of the given set, and false otherwise.
bool isEqual(const PresburgerRelation &set) const
Return true if this set is equal to the given set, and false otherwise.
PresburgerSet unionSet(const PresburgerRelation &set) const
These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
void setId(VarKind kind, unsigned pos, Identifier id)
Set the identifier of pos^th variable of the specified kind.
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
void resetIds()
Reset the stored identifiers in the space.
bool isEqual(const PresburgerSpace &other) const
Returns true if both the spaces are equal including local variables i.e.
bool isUsingIds() const
Returns if identifiers are being used.
void convertVarKind(VarKind srcKind, unsigned srcPos, unsigned num, VarKind dstKind, unsigned dstPos)
Converts variables of the specified kind in the column range [srcPos, srcPos + num) to variables of t...
void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
Removes variables of the specified kind in the column range [varStart, varLimit).
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of var starts.
Identifier getId(VarKind kind, unsigned pos) const
Get the identifier of pos^th variable of the specified kind.
unsigned getNumVars() const
unsigned getNumLocalVars() const
VarKind getVarKindAt(unsigned pos) const
Return the VarKind of the var at the specified position.
static PresburgerSpace getSetSpace(unsigned numDims=0, unsigned numSymbols=0, unsigned numLocals=0)
ArrayRef< Identifier > getIds(VarKind kind) const
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
void print(llvm::raw_ostream &os) const
static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)
void swapVar(VarKind kindA, VarKind kindB, unsigned posA, unsigned posB)
Swaps the posA^th variable of kindA and posB^th variable of kindB.
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
bool isEmpty() const
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
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.
bool isFlatAlong(ArrayRef< DynamicAPInt > coeffs)
Check if the simplex takes only one rational value along the direction of coeffs.
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.
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...
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.
A class to perform symbolic lexicographic optimization, i.e., to find, for every assignment to the sy...
SymbolicLexOpt computeSymbolicIntegerLexMin()
The lexmin will be stored as a function lexopt from symbols to non-symbols in the result.
BoundType
The type of bound: equal, lower bound or upper bound.
MaybeLocalRepr computeSingleVarRepr(const IntegerRelation &cst, ArrayRef< bool > foundRepr, unsigned pos, MutableArrayRef< DynamicAPInt > dividend, DynamicAPInt &divisor)
Returns the MaybeLocalRepr struct which contains the indices of the constraints that can be expressed...
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 ...
DynamicAPInt ceil(const Fraction &f)
Fraction abs(const Fraction &f)
SmallVector< DynamicAPInt, 8 > getDivUpperBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &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 ...
SmallVector< DynamicAPInt, 8 > getDivLowerBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor, unsigned localVarIdx)
Include the generated interface declarations.
const FrozenRewritePatternSet GreedyRewriteConfig bool * changed
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type.
const PresburgerSpace & getSpace() const
unsigned getNumIneqs() const
unsigned getNumEqs() const
MaybeLocalRepr contains the indices of the constraints that can be expressed as a floordiv of an affi...
Example usage: Print .12, 3.4, 56.7 preAlign = ".", minSpacing = 1, .12 .12 3.4 3....
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.