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)
1504 const DynamicAPInt &divisor) {
1505 assert(dividend.size() ==
getNumCols() &&
"incorrect dividend size");
1506 assert(divisor > 0 &&
"positive divisor expected");
1511 dividendCopy.insert(dividendCopy.end() - 1, DynamicAPInt(0));
1519 assert(pos <
getNumVars() &&
"invalid position");
1521 DynamicAPInt v =
atEq(r, pos);
1527 for (c = 0; c < f; c++) {
1530 if (
atEq(r, c) != 0) {
1543 assert(pos <
getNumVars() &&
"invalid position");
1549 assert(
atEq(rowIdx, pos) *
atEq(rowIdx, pos) == 1);
1556 for (
unsigned s = pos, t = pos, e = pos + num; s < e; s++) {
1579 unsigned *minLbPos,
unsigned *minUbPos)
const {
1580 assert(pos <
getNumDimVars() &&
"Invalid variable position");
1592 [](
const DynamicAPInt &coeff) { return coeff == 0; }))
1593 return std::nullopt;
1602 DynamicAPInt v =
atEq(eqPos, pos);
1609 (*ub)[c] = (*lb)[c];
1611 assert(boundFloorDivisor &&
1612 "both lb and divisor or none should be provided");
1613 *boundFloorDivisor = 1;
1619 return DynamicAPInt(1);
1630 return std::nullopt;
1643 std::optional<DynamicAPInt> minDiff;
1644 unsigned minLbPosition = 0, minUbPosition = 0;
1645 for (
auto ubPos : ubIndices) {
1646 for (
auto lbPos : lbIndices) {
1664 diff = std::max<DynamicAPInt>(diff, DynamicAPInt(0));
1665 if (minDiff == std::nullopt || diff < minDiff) {
1667 minLbPosition = lbPos;
1668 minUbPosition = ubPos;
1672 if (lb && minDiff) {
1681 *boundFloorDivisor =
atIneq(minLbPosition, pos);
1682 assert(*boundFloorDivisor == -
atIneq(minUbPosition, pos));
1697 *minLbPos = minLbPosition;
1699 *minUbPos = minUbPosition;
1703 template <
bool isLower>
1704 std::optional<DynamicAPInt>
1706 assert(pos <
getNumVars() &&
"invalid position");
1724 return std::nullopt;
1726 std::optional<DynamicAPInt> minOrMaxConst;
1735 }
else if (
atIneq(r, 0) >= 0) {
1740 for (c = 0, f =
getNumCols() - 1; c < f; c++)
1741 if (c != 0 &&
atIneq(r, c) != 0)
1747 DynamicAPInt boundConst =
1751 if (minOrMaxConst == std::nullopt || boundConst > minOrMaxConst)
1752 minOrMaxConst = boundConst;
1754 if (minOrMaxConst == std::nullopt || boundConst < minOrMaxConst)
1755 minOrMaxConst = boundConst;
1758 return minOrMaxConst;
1761 std::optional<DynamicAPInt>
1765 .computeConstantLowerOrUpperBound<
true>(pos);
1768 .computeConstantLowerOrUpperBound<
false>(pos);
1771 std::optional<DynamicAPInt> lb =
1774 std::optional<DynamicAPInt> ub =
1776 .computeConstantLowerOrUpperBound<
false>(pos);
1777 return (lb && ub && *lb == *ub) ? std::optional<DynamicAPInt>(*ub)
1787 for (
unsigned c = pos; c < pos + num; c++) {
1796 for (
unsigned c = pos; c < pos + num; c++) {
1797 if (
atEq(r, c) != 0)
1819 SmallDenseMap<ArrayRef<DynamicAPInt>, std::pair<unsigned, DynamicAPInt>>
1820 rowsWithoutConstTerm;
1823 auto isTriviallyValid = [&](
unsigned r) ->
bool {
1824 for (
unsigned c = 0, e =
getNumCols() - 1; c < e; c++) {
1835 if (isTriviallyValid(r)) {
1836 redunIneq[r] =
true;
1845 auto rowWithoutConstTerm =
1848 rowsWithoutConstTerm.insert({rowWithoutConstTerm, {r, constTerm}});
1851 auto &val = ret.first->second;
1852 if (val.second > constTerm) {
1854 redunIneq[val.first] =
true;
1855 val = {r, constTerm};
1858 redunIneq[r] =
true;
1876 #define DEBUG_TYPE "fm"
1922 bool *isResultIntegerExact) {
1923 LLVM_DEBUG(llvm::dbgs() <<
"FM input (eliminate pos " << pos <<
"):\n");
1925 assert(pos <
getNumVars() &&
"invalid position");
1930 if (
atEq(r, pos) != 0) {
1934 assert(ret.succeeded() &&
"Gaussian elimination guaranteed to succeed");
1935 LLVM_DEBUG(llvm::dbgs() <<
"FM output (through Gaussian elimination):\n");
1949 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
1959 std::vector<unsigned> nbIndices;
1966 if (
atIneq(r, pos) == 0) {
1968 nbIndices.emplace_back(r);
1969 }
else if (
atIneq(r, pos) >= 1) {
1971 lbIndices.emplace_back(r);
1974 ubIndices.emplace_back(r);
1981 newSpace.
removeVarRange(idKindRemove, relativePos, relativePos + 1);
1984 IntegerRelation newRel(lbIndices.size() * ubIndices.size() + nbIndices.size(),
1988 bool allLCMsAreOne =
true;
2000 for (
auto ubPos : ubIndices) {
2001 for (
auto lbPos : lbIndices) {
2004 DynamicAPInt lbCoeff =
atIneq(lbPos, pos);
2008 DynamicAPInt ubCoeff = -
atIneq(ubPos, pos);
2010 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2013 assert(lbCoeff >= 1 && ubCoeff >= 1 &&
"bounds wrongly identified");
2014 DynamicAPInt lcm = llvm::lcm(lbCoeff, ubCoeff);
2015 ineq.emplace_back(
atIneq(ubPos, l) * (lcm / ubCoeff) +
2016 atIneq(lbPos, l) * (lcm / lbCoeff));
2017 assert(lcm > 0 &&
"lcm should be positive!");
2019 allLCMsAreOne =
false;
2024 ineq[ineq.size() - 1] += lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
2032 LLVM_DEBUG(llvm::dbgs() <<
"FM isResultIntegerExact: " << allLCMsAreOne
2034 if (allLCMsAreOne && isResultIntegerExact)
2035 *isResultIntegerExact =
true;
2038 for (
auto nbPos : nbIndices) {
2041 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2044 ineq.emplace_back(
atIneq(nbPos, l));
2050 lbIndices.size() * ubIndices.size() + nbIndices.size());
2056 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2059 eq.emplace_back(
atEq(r, l));
2070 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
2075 #define DEBUG_TYPE "presburger"
2083 assert(pos + num <
getNumCols() &&
"invalid range");
2086 unsigned currentPos = pos;
2087 unsigned numToEliminate = num;
2088 unsigned numGaussianEliminated = 0;
2091 unsigned curNumEliminated =
2094 numToEliminate -= curNumEliminated + 1;
2095 numGaussianEliminated += curNumEliminated;
2099 for (
unsigned i = 0; i < num - numGaussianEliminated; i++) {
2100 unsigned numToEliminate = num - numGaussianEliminated - i;
2114 enum BoundCmpResult { Greater, Less, Equal, Unknown };
2120 assert(a.size() == b.size());
2126 if (!std::equal(a.begin(), a.end() - 1, b.begin()))
2129 if (a.back() == b.back())
2132 return a.back() < b.back() ? Less : Greater;
2171 std::vector<SmallVector<DynamicAPInt, 8>> boundingLbs;
2172 std::vector<SmallVector<DynamicAPInt, 8>> boundingUbs;
2184 DynamicAPInt lbFloorDivisor, otherLbFloorDivisor;
2187 if (!extent.has_value())
2193 d, &otherLb, &otherLbFloorDivisor, &otherUb);
2194 if (!otherExtent.has_value() || lbFloorDivisor != otherLbFloorDivisor)
2198 assert(lbFloorDivisor > 0 &&
"divisor always expected to be positive");
2200 auto res = compareBounds(lb, otherLb);
2202 if (res == BoundCmpResult::Less || res == BoundCmpResult::Equal) {
2207 minLb.back() -= lbFloorDivisor - 1;
2208 }
else if (res == BoundCmpResult::Greater) {
2210 minLb.back() -= otherLbFloorDivisor - 1;
2215 if (!constLb.has_value() || !constOtherLb.has_value())
2217 std::fill(minLb.begin(), minLb.end(), 0);
2218 minLb.back() =
std::min(*constLb, *constOtherLb);
2222 auto uRes = compareBounds(ub, otherUb);
2223 if (uRes == BoundCmpResult::Greater || uRes == BoundCmpResult::Equal) {
2225 }
else if (uRes == BoundCmpResult::Less) {
2231 if (!constUb.has_value() || !constOtherUb.has_value())
2233 std::fill(maxUb.begin(), maxUb.end(), 0);
2234 maxUb.back() =
std::max(*constUb, *constOtherUb);
2237 std::fill(newLb.begin(), newLb.end(), 0);
2238 std::fill(newUb.begin(), newUb.end(), 0);
2242 newLb[d] = lbFloorDivisor;
2243 newUb[d] = -lbFloorDivisor;
2246 std::transform(newLb.begin() +
getNumDimVars(), newLb.end(),
2248 std::negate<DynamicAPInt>());
2251 boundingLbs.emplace_back(newLb);
2252 boundingUbs.emplace_back(newUb);
2284 assert(pos < cst.
getNumVars() &&
"invalid start position");
2285 assert(pos + num <= cst.
getNumVars() &&
"invalid limit");
2290 for (c = pos; c < pos + num; ++c) {
2291 if (cst.
atIneq(r, c) != 0)
2295 nbIneqIndices.emplace_back(r);
2301 for (c = pos; c < pos + num; ++c) {
2302 if (cst.
atEq(r, c) != 0)
2306 nbEqIndices.emplace_back(r);
2311 assert(pos + num <=
getNumVars() &&
"invalid range");
2320 for (
auto nbIndex : llvm::reverse(nbIneqIndices))
2322 for (
auto nbIndex : llvm::reverse(nbEqIndices))
2342 SmallDenseMap<ArrayRef<DynamicAPInt>,
unsigned> hashTable;
2350 hashTable.insert({row, 0});
2351 for (
unsigned k = 1; k < ineqs; ++k) {
2353 if (hashTable.try_emplace(row, k).second)
2357 unsigned l = hashTable[row];
2368 for (
unsigned k = 0; k < ineqs; ++k) {
2370 negIneq.assign(row.begin(), row.end());
2371 for (DynamicAPInt &ele : negIneq)
2373 if (!hashTable.contains(negIneq))
2378 unsigned l = hashTable[row];
2380 if (sum > 0 || l == k)
2416 "Domain set is not compatible with poly");
2432 "Range set is not compatible with poly");
2452 "Range of `this` should be compatible with Domain of `rel`");
2516 "Domain of this and range of other do not match");
2579 updatePrintMetrics<DynamicAPInt>(
atEq(i,
j), ptm);
2582 updatePrintMetrics<DynamicAPInt>(
atIneq(i,
j), ptm);
2584 constexpr
unsigned kMinSpacing = 1;
2587 printWithPrintMetrics<DynamicAPInt>(os,
atEq(i,
j), kMinSpacing, ptm);
2593 printWithPrintMetrics<DynamicAPInt>(os,
atIneq(i,
j), kMinSpacing, ptm);
2605 "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::@1215::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...
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.
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.
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.
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.