23 #include "llvm/ADT/DenseMap.h"
24 #include "llvm/ADT/DenseSet.h"
25 #include "llvm/ADT/STLExtras.h"
26 #include "llvm/ADT/Sequence.h"
27 #include "llvm/ADT/SmallBitVector.h"
28 #include "llvm/Support/Debug.h"
29 #include "llvm/Support/LogicalResult.h"
30 #include "llvm/Support/raw_ostream.h"
39 #define DEBUG_TYPE "presburger"
42 using namespace presburger;
44 using llvm::SmallDenseMap;
45 using llvm::SmallDenseSet;
48 return std::make_unique<IntegerRelation>(*
this);
52 return std::make_unique<IntegerPolyhedron>(*
this);
61 assert(oSpace.
getNumLocalVars() == 0 &&
"no locals should be present!");
70 "space must be using identifiers to set an identifier");
71 assert(kind !=
VarKind::Local &&
"local variables cannot have identifiers");
119 for (
unsigned j = 0;
j <
cols; ++
j) {
125 for (
unsigned j = 0;
j <
cols; ++
j) {
153 "Incorrect number of vars in lexMin!");
173 "Incorrect number of vars in lexMin!");
179 return llvm::all_of(range, [](
const DynamicAPInt &x) {
return x == 0; });
183 unsigned begin,
unsigned count) {
202 assert(num <= curNum &&
"Can't truncate to more vars!");
231 copy.getLocalReprs(&reprs);
235 unsigned numNonDivLocals = 0;
237 for (
unsigned i = 0, e =
copy.getNumLocalVars(); i < e - numNonDivLocals;) {
242 copy.swapVar(offset + i, offset + e - numNonDivLocals - 1);
243 std::swap(reprs[i], reprs[e - numNonDivLocals - 1]);
251 if (numNonDivLocals == 0)
268 copy.getNumVars() - numNonDivLocals)))
285 llvm::SmallBitVector isSymbol(
getNumVars(),
false);
329 symbolicIntegerLexMax(
332 for (
auto &flippedPiece :
334 IntMatrix mat = flippedPiece.output.getOutputMatrix();
335 for (
unsigned i = 0, e = mat.
getNumRows(); i < e; i++)
339 symbolicIntegerLexMax.lexopt.addPiece(piece);
341 symbolicIntegerLexMax.unboundedDomain =
343 return symbolicIntegerLexMax;
368 for (
unsigned i = 0, e = eq.size(); i < e; ++i)
375 for (
unsigned i = 0, e = inEq.size(); i < e; ++i)
389 if (varStart >= varLimit)
404 if (varStart >= varLimit)
410 auto removeVarKindInRange = [
this](
VarKind kind,
unsigned &start,
419 unsigned relativeStart =
420 start <= offset ? 0 :
std::min(num, start - offset);
421 unsigned relativeLimit =
422 limit <= offset ? 0 :
std::min(num, limit - offset);
430 limit -= relativeLimit - relativeStart;
460 assert(posA <
getNumVars() &&
"invalid position A");
461 assert(posB <
getNumVars() &&
"invalid position B");
470 space.
swapVar(kindA, kindB, relativePosA, relativePosB);
487 unsigned offset,
unsigned num)
const {
488 assert(pos <
getNumVars() &&
"invalid position");
489 assert(offset + num <
getNumCols() &&
"invalid range");
493 auto containsConstraintDependentOnRange = [&](
unsigned r,
bool isEq) {
496 for (c = offset, f = offset + num; c < f; ++c) {
510 if (containsConstraintDependentOnRange(r,
false))
512 if (
atIneq(r, pos) >= 1) {
514 lbIndices->emplace_back(r);
515 }
else if (
atIneq(r, pos) <= -1) {
517 ubIndices->emplace_back(r);
527 if (
atEq(r, pos) == 0)
529 if (containsConstraintDependentOnRange(r,
true))
531 eqIndices->emplace_back(r);
548 "invalid position or too many values");
553 for (
unsigned i = 0, numVals = values.size(); i < numVals; ++i)
555 for (
unsigned i = 0, numVals = values.size(); i < numVals; ++i)
568 unsigned *rowIdx)
const {
569 assert(colIdx <
getNumCols() &&
"position out of bounds");
570 auto at = [&](
unsigned rowIdx) -> DynamicAPInt {
571 return isEq ?
atEq(rowIdx, colIdx) :
atIneq(rowIdx, colIdx);
574 for (*rowIdx = 0; *rowIdx < e; ++(*rowIdx)) {
575 if (at(*rowIdx) != 0) {
591 auto check = [&](
bool isEq) ->
bool {
594 for (
unsigned i = 0, e = numRows; i < e; ++i) {
596 for (
j = 0;
j < numCols - 1; ++
j) {
602 if (
j < numCols - 1) {
607 DynamicAPInt v = isEq ?
atEq(i, numCols - 1) :
atIneq(i, numCols - 1);
608 if ((isEq && v != 0) || (!isEq && v < 0)) {
623 unsigned rowIdx,
unsigned pivotRow,
624 unsigned pivotCol,
unsigned elimColStart,
627 if (isEq && rowIdx == pivotRow)
629 auto at = [&](
unsigned i,
unsigned j) -> DynamicAPInt {
630 return isEq ? constraints->
atEq(i,
j) : constraints->
atIneq(i,
j);
632 DynamicAPInt leadCoeff = at(rowIdx, pivotCol);
636 DynamicAPInt pivotCoeff = constraints->
atEq(pivotRow, pivotCol);
637 int sign = (leadCoeff * pivotCoeff > 0) ? -1 : 1;
638 DynamicAPInt lcm = llvm::lcm(pivotCoeff, leadCoeff);
639 DynamicAPInt pivotMultiplier = sign * (lcm /
abs(pivotCoeff));
640 DynamicAPInt rowMultiplier = lcm /
abs(leadCoeff);
643 for (
unsigned j = 0;
j < numCols; ++
j) {
645 if (
j >= elimColStart &&
j < pivotCol)
647 DynamicAPInt v = pivotMultiplier * constraints->
atEq(pivotRow,
j) +
648 rowMultiplier * at(rowIdx,
j);
649 isEq ? constraints->
atEq(rowIdx,
j) = v
650 : constraints->
atIneq(rowIdx,
j) = v;
660 unsigned start,
unsigned end) {
663 auto getProductOfNumLowerUpperBounds = [&](
unsigned pos) {
667 if (cst.
atIneq(r, pos) > 0) {
669 }
else if (cst.
atIneq(r, pos) < 0) {
673 return numLb * numUb;
676 unsigned minLoc = start;
677 unsigned min = getProductOfNumLowerUpperBounds(start);
678 for (
unsigned c = start + 1; c < end; c++) {
679 unsigned numLbUbProduct = getProductOfNumLowerUpperBounds(c);
680 if (numLbUbProduct <
min) {
681 min = numLbUbProduct;
704 unsigned currentPos = 0;
717 for (
unsigned i = 0, e = tmpCst.
getNumVars(); i < e; i++) {
726 LLVM_DEBUG(llvm::dbgs() <<
"FM constraint explosion detected\n");
760 DynamicAPInt gcd =
abs(
atEq(i, 0));
761 for (
unsigned j = 1;
j < numCols - 1; ++
j) {
762 gcd = llvm::gcd(gcd,
abs(
atEq(i,
j)));
764 DynamicAPInt v =
abs(
atEq(i, numCols - 1));
765 if (gcd > 0 && (v % gcd != 0)) {
786 assert(!simplex.
isEmpty() &&
"It is not meaningful to ask whether a "
787 "direction is bounded in an empty set.");
794 boundedIneqs.emplace_back(i);
804 for (
unsigned i : boundedIneqs) {
805 for (
unsigned col = 0; col < dirsNumCols; ++col)
806 dirs(row, col) =
atIneq(i, col);
812 for (
unsigned col = 0; col < dirsNumCols; ++col)
813 dirs(row, col) =
atEq(i, col);
867 std::optional<SmallVector<DynamicAPInt, 8>>
891 std::pair<unsigned, LinearTransform> result =
900 unsigned numBoundedDims = result.first;
901 unsigned numUnboundedDims =
getNumVars() - numBoundedDims;
907 std::optional<SmallVector<DynamicAPInt, 8>> boundedSample =
912 "Simplex returned an invalid sample!");
946 DynamicAPInt coeff = cone.
atIneq(i,
j);
956 Simplex shrunkenConeSimplex(cone);
957 assert(!shrunkenConeSimplex.
isEmpty() &&
"Shrunken cone cannot be empty!");
964 llvm::map_range(shrunkenConeSample,
ceil));
968 sample.append(coneSample.begin(), coneSample.end());
977 assert(expr.size() == 1 + point.size() &&
978 "Dimensionalities of point and expression don't match!");
979 DynamicAPInt value = expr.back();
980 for (
unsigned i = 0; i < point.size(); ++i)
981 value += expr[i] * point[i];
1008 std::optional<SmallVector<DynamicAPInt, 8>>
1011 "Point should contain all vars except locals!");
1013 "This function depends on locals being stored last!");
1015 copy.setAndEliminate(0, point);
1016 return copy.findIntegerSample();
1023 foundRepr[i] =
true;
1033 if (!foundRepr[i + localOffset]) {
1043 foundRepr[localOffset + i] =
true;
1068 atIneq(i, numCols - 1) = floorDiv(
atIneq(i, numCols - 1), gcd);
1075 unsigned posLimit) {
1080 if (posStart >= posLimit)
1085 unsigned pivotCol = 0;
1086 for (pivotCol = posStart; pivotCol < posLimit; ++pivotCol) {
1116 posLimit = pivotCol;
1119 return posLimit - posStart;
1125 unsigned nowDone, eqs, pivotRow;
1128 for (; firstVar < vars; ++firstVar) {
1134 if (firstVar >= vars)
1138 if (pivotRow > nowDone) {
1144 for (
unsigned i = nowDone + 1; i < eqs; ++i) {
1161 for (
unsigned i = nowDone; i < eqs; ++i) {
1162 if (
atEq(i, vars) == 0)
1219 for (
unsigned r = 0; r < numIneqs; r++) {
1245 return DynamicAPInt(0);
1261 DynamicAPInt count(1);
1263 bool hasUnboundedVar =
false;
1269 assert((!
min.isEmpty() && !
max.isEmpty()) &&
1270 "Polytope should be rationally non-empty!");
1274 if (
min.isUnbounded() ||
max.isUnbounded()) {
1275 hasUnboundedVar =
true;
1281 if (
min.getBoundedOptimum() >
max.getBoundedOptimum())
1282 return DynamicAPInt(0);
1284 count *= (*
max - *
min + 1);
1288 return DynamicAPInt(0);
1289 if (hasUnboundedVar)
1299 posA += localOffset;
1300 posB += localOffset;
1313 "both relations need to have identifers to merge and align");
1322 const Identifier *itr = std::find(findBegin, findEnd, identifier);
1323 if (itr != findEnd) {
1326 std::distance(findBegin, itr));
1361 auto merge = [&relA, &relB, oldALocals](
unsigned i,
unsigned j) ->
bool {
1390 auto merge = [
this](
unsigned i,
unsigned j) ->
bool {
1398 bool changed =
true;
1424 unsigned i, e,
j, f;
1443 if (
atEq(k,
j) != 0) {
1460 unsigned varLimit,
VarKind dstKind,
1462 assert(varLimit <=
getNumVarKind(srcKind) &&
"invalid id range");
1464 if (varStart >= varLimit)
1469 unsigned convertCount = varLimit - varStart;
1470 int forwardMoveOffset = dstOffset > srcOffset ? -convertCount : 0;
1473 dstOffset + pos + forwardMoveOffset);
1475 dstOffset + pos + forwardMoveOffset);
1481 const DynamicAPInt &value) {
1496 const DynamicAPInt &value) {
1500 for (
unsigned i = 0, e = expr.size(); i < e; ++i)
1512 const DynamicAPInt &divisor) {
1513 assert(dividend.size() ==
getNumCols() &&
"incorrect dividend size");
1514 assert(divisor > 0 &&
"positive divisor expected");
1519 dividendCopy.insert(dividendCopy.end() - 1, DynamicAPInt(0));
1532 bool symbolic =
false) {
1533 assert(pos < cst.
getNumVars() &&
"invalid position");
1535 DynamicAPInt v = cst.
atEq(r, pos);
1541 for (c = 0; c < f; c++) {
1544 if (cst.
atEq(r, c) != 0) {
1557 assert(pos <
getNumVars() &&
"invalid position");
1563 assert(
atEq(rowIdx, pos) *
atEq(rowIdx, pos) == 1);
1570 for (
unsigned s = pos, t = pos, e = pos + num; s < e; s++) {
1593 unsigned *minLbPos,
unsigned *minUbPos)
const {
1594 assert(pos <
getNumDimVars() &&
"Invalid variable position");
1605 [](
const DynamicAPInt &coeff) { return coeff == 0; }))
1606 return std::nullopt;
1615 DynamicAPInt v =
atEq(eqPos, pos);
1622 (*ub)[c] = (*lb)[c];
1624 assert(boundFloorDivisor &&
1625 "both lb and divisor or none should be provided");
1626 *boundFloorDivisor = 1;
1632 return DynamicAPInt(1);
1643 return std::nullopt;
1656 std::optional<DynamicAPInt> minDiff;
1657 unsigned minLbPosition = 0, minUbPosition = 0;
1658 for (
auto ubPos : ubIndices) {
1659 for (
auto lbPos : lbIndices) {
1677 diff = std::max<DynamicAPInt>(diff, DynamicAPInt(0));
1678 if (minDiff == std::nullopt || diff < minDiff) {
1680 minLbPosition = lbPos;
1681 minUbPosition = ubPos;
1685 if (lb && minDiff) {
1694 *boundFloorDivisor =
atIneq(minLbPosition, pos);
1695 assert(*boundFloorDivisor == -
atIneq(minUbPosition, pos));
1710 *minLbPos = minLbPosition;
1712 *minUbPos = minUbPosition;
1716 template <
bool isLower>
1717 std::optional<DynamicAPInt>
1719 assert(pos <
getNumVars() &&
"invalid position");
1737 return std::nullopt;
1739 std::optional<DynamicAPInt> minOrMaxConst;
1748 }
else if (
atIneq(r, 0) >= 0) {
1753 for (c = 0, f =
getNumCols() - 1; c < f; c++)
1754 if (c != 0 &&
atIneq(r, c) != 0)
1760 DynamicAPInt boundConst =
1764 if (minOrMaxConst == std::nullopt || boundConst > minOrMaxConst)
1765 minOrMaxConst = boundConst;
1767 if (minOrMaxConst == std::nullopt || boundConst < minOrMaxConst)
1768 minOrMaxConst = boundConst;
1771 return minOrMaxConst;
1774 std::optional<DynamicAPInt>
1778 .computeConstantLowerOrUpperBound<
true>(pos);
1781 .computeConstantLowerOrUpperBound<
false>(pos);
1784 std::optional<DynamicAPInt> lb =
1787 std::optional<DynamicAPInt> ub =
1789 .computeConstantLowerOrUpperBound<
false>(pos);
1790 return (lb && ub && *lb == *ub) ? std::optional<DynamicAPInt>(*ub)
1800 for (
unsigned c = pos; c < pos + num; c++) {
1809 for (
unsigned c = pos; c < pos + num; c++) {
1810 if (
atEq(r, c) != 0)
1832 SmallDenseMap<ArrayRef<DynamicAPInt>, std::pair<unsigned, DynamicAPInt>>
1833 rowsWithoutConstTerm;
1835 SmallDenseSet<ArrayRef<DynamicAPInt>, 8> rowSet;
1838 auto isTriviallyValid = [&](
unsigned r) ->
bool {
1839 for (
unsigned c = 0, e =
getNumCols() - 1; c < e; c++) {
1851 if (isTriviallyValid(r) || !rowSet.insert(row).second) {
1852 redunIneq[r] =
true;
1861 auto rowWithoutConstTerm =
1864 rowsWithoutConstTerm.insert({rowWithoutConstTerm, {r, constTerm}});
1867 auto &val = ret.first->second;
1868 if (val.second > constTerm) {
1870 redunIneq[val.first] =
true;
1871 val = {r, constTerm};
1874 redunIneq[r] =
true;
1892 #define DEBUG_TYPE "fm"
1938 bool *isResultIntegerExact) {
1939 LLVM_DEBUG(llvm::dbgs() <<
"FM input (eliminate pos " << pos <<
"):\n");
1941 assert(pos <
getNumVars() &&
"invalid position");
1946 if (
atEq(r, pos) != 0) {
1950 assert(ret.succeeded() &&
"Gaussian elimination guaranteed to succeed");
1951 LLVM_DEBUG(llvm::dbgs() <<
"FM output (through Gaussian elimination):\n");
1965 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
1975 std::vector<unsigned> nbIndices;
1982 if (
atIneq(r, pos) == 0) {
1984 nbIndices.emplace_back(r);
1985 }
else if (
atIneq(r, pos) >= 1) {
1987 lbIndices.emplace_back(r);
1990 ubIndices.emplace_back(r);
1997 newSpace.
removeVarRange(idKindRemove, relativePos, relativePos + 1);
2000 IntegerRelation newRel(lbIndices.size() * ubIndices.size() + nbIndices.size(),
2004 bool allLCMsAreOne =
true;
2016 for (
auto ubPos : ubIndices) {
2017 for (
auto lbPos : lbIndices) {
2020 DynamicAPInt lbCoeff =
atIneq(lbPos, pos);
2024 DynamicAPInt ubCoeff = -
atIneq(ubPos, pos);
2026 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2029 assert(lbCoeff >= 1 && ubCoeff >= 1 &&
"bounds wrongly identified");
2030 DynamicAPInt lcm = llvm::lcm(lbCoeff, ubCoeff);
2031 ineq.emplace_back(
atIneq(ubPos, l) * (lcm / ubCoeff) +
2032 atIneq(lbPos, l) * (lcm / lbCoeff));
2033 assert(lcm > 0 &&
"lcm should be positive!");
2035 allLCMsAreOne =
false;
2040 ineq[ineq.size() - 1] += lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
2048 LLVM_DEBUG(llvm::dbgs() <<
"FM isResultIntegerExact: " << allLCMsAreOne
2050 if (allLCMsAreOne && isResultIntegerExact)
2051 *isResultIntegerExact =
true;
2054 for (
auto nbPos : nbIndices) {
2057 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2060 ineq.emplace_back(
atIneq(nbPos, l));
2066 lbIndices.size() * ubIndices.size() + nbIndices.size());
2072 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2075 eq.emplace_back(
atEq(r, l));
2086 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
2091 #define DEBUG_TYPE "presburger"
2099 assert(pos + num <
getNumCols() &&
"invalid range");
2102 unsigned currentPos = pos;
2103 unsigned numToEliminate = num;
2104 unsigned numGaussianEliminated = 0;
2107 unsigned curNumEliminated =
2110 numToEliminate -= curNumEliminated + 1;
2111 numGaussianEliminated += curNumEliminated;
2115 for (
unsigned i = 0; i < num - numGaussianEliminated; i++) {
2116 unsigned numToEliminate = num - numGaussianEliminated - i;
2130 enum BoundCmpResult { Greater, Less, Equal, Unknown };
2136 assert(a.size() == b.size());
2142 if (!std::equal(a.begin(), a.end() - 1, b.begin()))
2145 if (a.back() == b.back())
2148 return a.back() < b.back() ? Less : Greater;
2187 std::vector<SmallVector<DynamicAPInt, 8>> boundingLbs;
2188 std::vector<SmallVector<DynamicAPInt, 8>> boundingUbs;
2200 DynamicAPInt lbFloorDivisor, otherLbFloorDivisor;
2203 if (!extent.has_value())
2209 d, &otherLb, &otherLbFloorDivisor, &otherUb);
2210 if (!otherExtent.has_value() || lbFloorDivisor != otherLbFloorDivisor)
2214 assert(lbFloorDivisor > 0 &&
"divisor always expected to be positive");
2216 auto res = compareBounds(lb, otherLb);
2218 if (res == BoundCmpResult::Less || res == BoundCmpResult::Equal) {
2223 minLb.back() -= lbFloorDivisor - 1;
2224 }
else if (res == BoundCmpResult::Greater) {
2226 minLb.back() -= otherLbFloorDivisor - 1;
2231 if (!constLb.has_value() || !constOtherLb.has_value())
2233 std::fill(minLb.begin(), minLb.end(), 0);
2234 minLb.back() =
std::min(*constLb, *constOtherLb);
2238 auto uRes = compareBounds(ub, otherUb);
2239 if (uRes == BoundCmpResult::Greater || uRes == BoundCmpResult::Equal) {
2241 }
else if (uRes == BoundCmpResult::Less) {
2247 if (!constUb.has_value() || !constOtherUb.has_value())
2249 std::fill(maxUb.begin(), maxUb.end(), 0);
2250 maxUb.back() =
std::max(*constUb, *constOtherUb);
2253 std::fill(newLb.begin(), newLb.end(), 0);
2254 std::fill(newUb.begin(), newUb.end(), 0);
2258 newLb[d] = lbFloorDivisor;
2259 newUb[d] = -lbFloorDivisor;
2262 std::transform(newLb.begin() +
getNumDimVars(), newLb.end(),
2264 std::negate<DynamicAPInt>());
2267 boundingLbs.emplace_back(newLb);
2268 boundingUbs.emplace_back(newUb);
2301 assert(pos < cst.
getNumVars() &&
"invalid start position");
2302 assert(pos + num <= cst.
getNumVars() &&
"invalid limit");
2307 for (c = pos; c < pos + num; ++c) {
2308 if (cst.
atIneq(r, c) != 0)
2312 nbIneqIndices.emplace_back(r);
2318 for (c = pos; c < pos + num; ++c) {
2319 if (cst.
atEq(r, c) != 0)
2323 nbEqIndices.emplace_back(r);
2328 assert(pos + num <=
getNumVars() &&
"invalid range");
2337 for (
auto nbIndex : llvm::reverse(nbIneqIndices))
2339 for (
auto nbIndex : llvm::reverse(nbEqIndices))
2358 bool changed =
false;
2359 SmallDenseMap<ArrayRef<DynamicAPInt>,
unsigned> hashTable;
2367 hashTable.insert({row, 0});
2368 for (
unsigned k = 1; k < ineqs; ++k) {
2370 if (!hashTable.contains(row)) {
2371 hashTable.insert({row, k});
2376 unsigned l = hashTable[row];
2387 for (
unsigned k = 0; k < ineqs; ++k) {
2389 negIneq.assign(row.begin(), row.end());
2390 for (DynamicAPInt &ele : negIneq)
2392 if (!hashTable.contains(negIneq))
2397 unsigned l = hashTable[row];
2399 if (sum > 0 || l == k)
2434 "Domain set is not compatible with poly");
2450 "Range set is not compatible with poly");
2470 "Range of `this` should be compatible with Domain of `rel`");
2534 "Domain of this and range of other do not match");
2597 os <<
atEq(i,
j) <<
"\t";
2616 "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 int findEqualityToConstant(const IntegerRelation &cst, unsigned pos, bool symbolic=false)
Finds an equality that equates the specified variable to a constant.
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.
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...
static IntegerRelation getEmpty(const PresburgerSpace &space)
Return an empty system containing an invalid equation 0 = 1.
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.
void addLocalFloorDiv(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
Adds a new local variable as the floordiv of an affine function of other variables,...
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.
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.
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 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...
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.
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...
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.