26 #include "llvm/ADT/DenseMap.h"
27 #include "llvm/ADT/DenseSet.h"
28 #include "llvm/ADT/STLExtras.h"
29 #include "llvm/ADT/Sequence.h"
30 #include "llvm/ADT/SmallBitVector.h"
31 #include "llvm/Support/Debug.h"
32 #include "llvm/Support/raw_ostream.h"
41 #define DEBUG_TYPE "presburger"
44 using namespace presburger;
46 using llvm::SmallDenseMap;
47 using llvm::SmallDenseSet;
50 return std::make_unique<IntegerRelation>(*
this);
54 return std::make_unique<IntegerPolyhedron>(*
this);
63 assert(oSpace.
getNumLocalVars() == 0 &&
"no locals should be present!");
72 "space must be using identifiers to set an identifier");
73 assert(kind !=
VarKind::Local &&
"local variables cannot have identifiers");
121 for (
unsigned j = 0;
j < cols; ++
j) {
127 for (
unsigned j = 0;
j < cols; ++
j) {
155 "Incorrect number of vars in lexMin!");
174 "Incorrect number of vars in lexMin!");
180 return llvm::all_of(range, [](
const MPInt &x) {
return x == 0; });
184 unsigned begin,
unsigned count) {
203 assert(num <= curNum &&
"Can't truncate to more vars!");
232 copy.getLocalReprs(&reprs);
236 unsigned numNonDivLocals = 0;
238 for (
unsigned i = 0, e =
copy.getNumLocalVars(); i < e - numNonDivLocals;) {
243 copy.swapVar(offset + i, offset + e - numNonDivLocals - 1);
244 std::swap(reprs[i], reprs[e - numNonDivLocals - 1]);
252 if (numNonDivLocals == 0)
269 copy.getNumVars() - numNonDivLocals)))
286 llvm::SmallBitVector isSymbol(
getNumVars(),
false);
330 symbolicIntegerLexMax(
333 for (
auto &flippedPiece :
335 IntMatrix mat = flippedPiece.output.getOutputMatrix();
336 for (
unsigned i = 0, e = mat.
getNumRows(); i < e; i++)
340 symbolicIntegerLexMax.lexopt.addPiece(piece);
342 symbolicIntegerLexMax.unboundedDomain =
344 return symbolicIntegerLexMax;
369 for (
unsigned i = 0, e = eq.size(); i < e; ++i)
376 for (
unsigned i = 0, e = inEq.size(); i < e; ++i)
390 if (varStart >= varLimit)
405 if (varStart >= varLimit)
411 auto removeVarKindInRange = [
this](
VarKind kind,
unsigned &start,
420 unsigned relativeStart =
421 start <= offset ? 0 :
std::min(num, start - offset);
422 unsigned relativeLimit =
423 limit <= offset ? 0 :
std::min(num, limit - offset);
431 limit -= relativeLimit - relativeStart;
461 assert(posA <
getNumVars() &&
"invalid position A");
462 assert(posB <
getNumVars() &&
"invalid position B");
471 space.
swapVar(kindA, kindB, relativePosA, relativePosB);
488 unsigned offset,
unsigned num)
const {
489 assert(pos <
getNumVars() &&
"invalid position");
490 assert(offset + num <
getNumCols() &&
"invalid range");
494 auto containsConstraintDependentOnRange = [&](
unsigned r,
bool isEq) {
497 for (c = offset, f = offset + num; c < f; ++c) {
511 if (containsConstraintDependentOnRange(r,
false))
513 if (
atIneq(r, pos) >= 1) {
515 lbIndices->push_back(r);
516 }
else if (
atIneq(r, pos) <= -1) {
518 ubIndices->push_back(r);
528 if (
atEq(r, pos) == 0)
530 if (containsConstraintDependentOnRange(r,
true))
532 eqIndices->push_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) ->
MPInt {
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) {
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) ->
MPInt {
630 return isEq ? constraints->
atEq(i,
j) : constraints->
atIneq(i,
j);
632 MPInt leadCoeff = at(rowIdx, pivotCol);
636 MPInt pivotCoeff = constraints->
atEq(pivotRow, pivotCol);
637 int sign = (leadCoeff * pivotCoeff > 0) ? -1 : 1;
639 MPInt pivotMultiplier = sign * (
lcm /
abs(pivotCoeff));
643 for (
unsigned j = 0;
j < numCols; ++
j) {
645 if (
j >= elimColStart &&
j < pivotCol)
647 MPInt 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");
761 for (
unsigned j = 1;
j < numCols - 1; ++
j) {
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.push_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<MPInt, 8>>
891 std::pair<unsigned, LinearTransform> result =
900 unsigned numBoundedDims = result.first;
901 unsigned numUnboundedDims =
getNumVars() - numBoundedDims;
907 std::optional<SmallVector<MPInt, 8>> boundedSample =
912 "Simplex returned an invalid sample!");
956 Simplex shrunkenConeSimplex(cone);
957 assert(!shrunkenConeSimplex.
isEmpty() &&
"Shrunken cone cannot be empty!");
967 sample.append(coneSample.begin(), coneSample.end());
975 assert(expr.size() == 1 + point.size() &&
976 "Dimensionalities of point and expression don't match!");
977 MPInt value = expr.back();
978 for (
unsigned i = 0; i < point.size(); ++i)
979 value += expr[i] * point[i];
1006 std::optional<SmallVector<MPInt, 8>>
1009 "Point should contain all vars except locals!");
1011 "This function depends on locals being stored last!");
1013 copy.setAndEliminate(0, point);
1014 return copy.findIntegerSample();
1021 foundRepr[i] =
true;
1031 if (!foundRepr[i + localOffset]) {
1041 foundRepr[localOffset + i] =
true;
1073 unsigned posLimit) {
1078 if (posStart >= posLimit)
1083 unsigned pivotCol = 0;
1084 for (pivotCol = posStart; pivotCol < posLimit; ++pivotCol) {
1114 posLimit = pivotCol;
1117 return posLimit - posStart;
1123 unsigned nowDone, eqs, pivotRow;
1126 for (; firstVar < vars; ++firstVar) {
1132 if (firstVar >= vars)
1136 if (pivotRow > nowDone) {
1142 for (
unsigned i = nowDone + 1; i < eqs; ++i) {
1159 for (
unsigned i = nowDone; i < eqs; ++i) {
1160 if (
atEq(i, vars) == 0)
1217 for (
unsigned r = 0; r < numIneqs; r++) {
1261 bool hasUnboundedVar =
false;
1267 assert((!
min.isEmpty() && !
max.isEmpty()) &&
1268 "Polytope should be rationally non-empty!");
1272 if (
min.isUnbounded() ||
max.isUnbounded()) {
1273 hasUnboundedVar =
true;
1279 if (
min.getBoundedOptimum() >
max.getBoundedOptimum())
1282 count *= (*
max - *
min + 1);
1287 if (hasUnboundedVar)
1297 posA += localOffset;
1298 posB += localOffset;
1311 "both relations need to have identifers to merge and align");
1320 const Identifier *itr = std::find(findBegin, findEnd, identifier);
1321 if (itr != findEnd) {
1324 std::distance(findBegin, itr));
1359 auto merge = [&relA, &relB, oldALocals](
unsigned i,
unsigned j) ->
bool {
1388 auto merge = [
this](
unsigned i,
unsigned j) ->
bool {
1396 bool changed =
true;
1422 unsigned i, e,
j, f;
1441 if (
atEq(k,
j) != 0) {
1458 unsigned varLimit,
VarKind dstKind,
1460 assert(varLimit <=
getNumVarKind(srcKind) &&
"invalid id range");
1462 if (varStart >= varLimit)
1467 unsigned convertCount = varLimit - varStart;
1468 int forwardMoveOffset = dstOffset > srcOffset ? -convertCount : 0;
1471 dstOffset + pos + forwardMoveOffset);
1473 dstOffset + pos + forwardMoveOffset);
1479 const MPInt &value) {
1494 const MPInt &value) {
1498 for (
unsigned i = 0, e = expr.size(); i < e; ++i)
1510 const MPInt &divisor) {
1511 assert(dividend.size() ==
getNumCols() &&
"incorrect dividend size");
1512 assert(divisor > 0 &&
"positive divisor expected");
1517 dividendCopy.insert(dividendCopy.end() - 1,
MPInt(0));
1530 bool symbolic =
false) {
1531 assert(pos < cst.
getNumVars() &&
"invalid position");
1539 for (c = 0; c < f; c++) {
1542 if (cst.
atEq(r, c) != 0) {
1555 assert(pos <
getNumVars() &&
"invalid position");
1561 assert(
atEq(rowIdx, pos) *
atEq(rowIdx, pos) == 1);
1568 for (
unsigned s = pos, t = pos, e = pos + num; s < e; s++) {
1591 assert(pos <
getNumDimVars() &&
"Invalid variable position");
1602 [](
const MPInt &coeff) { return coeff == 0; }))
1603 return std::nullopt;
1619 (*ub)[c] = (*lb)[c];
1621 assert(boundFloorDivisor &&
1622 "both lb and divisor or none should be provided");
1623 *boundFloorDivisor = 1;
1640 return std::nullopt;
1653 std::optional<MPInt> minDiff;
1654 unsigned minLbPosition = 0, minUbPosition = 0;
1655 for (
auto ubPos : ubIndices) {
1656 for (
auto lbPos : lbIndices) {
1674 diff = std::max<MPInt>(diff,
MPInt(0));
1675 if (minDiff == std::nullopt || diff < minDiff) {
1677 minLbPosition = lbPos;
1678 minUbPosition = ubPos;
1682 if (lb && minDiff) {
1691 *boundFloorDivisor =
atIneq(minLbPosition, pos);
1692 assert(*boundFloorDivisor == -
atIneq(minUbPosition, pos));
1707 *minLbPos = minLbPosition;
1709 *minUbPos = minUbPosition;
1713 template <
bool isLower>
1714 std::optional<MPInt>
1716 assert(pos <
getNumVars() &&
"invalid position");
1734 return std::nullopt;
1736 std::optional<MPInt> minOrMaxConst;
1745 }
else if (
atIneq(r, 0) >= 0) {
1750 for (c = 0, f =
getNumCols() - 1; c < f; c++)
1751 if (c != 0 &&
atIneq(r, c) != 0)
1761 if (minOrMaxConst == std::nullopt || boundConst > minOrMaxConst)
1762 minOrMaxConst = boundConst;
1764 if (minOrMaxConst == std::nullopt || boundConst < minOrMaxConst)
1765 minOrMaxConst = boundConst;
1768 return minOrMaxConst;
1772 unsigned pos)
const {
1775 .computeConstantLowerOrUpperBound<
true>(pos);
1778 .computeConstantLowerOrUpperBound<
false>(pos);
1781 std::optional<MPInt> lb =
1784 std::optional<MPInt> ub =
1786 .computeConstantLowerOrUpperBound<
false>(pos);
1787 return (lb && ub && *lb == *ub) ? std::optional<MPInt>(*ub) : std::nullopt;
1796 for (
unsigned c = pos; c < pos + num; c++) {
1805 for (
unsigned c = pos; c < pos + num; c++) {
1806 if (
atEq(r, c) != 0)
1828 SmallDenseMap<ArrayRef<MPInt>, std::pair<unsigned, MPInt>>
1829 rowsWithoutConstTerm;
1831 SmallDenseSet<ArrayRef<MPInt>, 8> rowSet;
1834 auto isTriviallyValid = [&](
unsigned r) ->
bool {
1835 for (
unsigned c = 0, e =
getNumCols() - 1; c < e; c++) {
1847 if (isTriviallyValid(r) || !rowSet.insert(row).second) {
1848 redunIneq[r] =
true;
1859 rowsWithoutConstTerm.insert({rowWithoutConstTerm, {r, constTerm}});
1862 auto &val = ret.first->second;
1863 if (val.second > constTerm) {
1865 redunIneq[val.first] =
true;
1866 val = {r, constTerm};
1869 redunIneq[r] =
true;
1887 #define DEBUG_TYPE "fm"
1933 bool *isResultIntegerExact) {
1934 LLVM_DEBUG(llvm::dbgs() <<
"FM input (eliminate pos " << pos <<
"):\n");
1936 assert(pos <
getNumVars() &&
"invalid position");
1941 if (
atEq(r, pos) != 0) {
1945 assert(
succeeded(ret) &&
"Gaussian elimination guaranteed to succeed");
1946 LLVM_DEBUG(llvm::dbgs() <<
"FM output (through Gaussian elimination):\n");
1960 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
1970 std::vector<unsigned> nbIndices;
1977 if (
atIneq(r, pos) == 0) {
1979 nbIndices.push_back(r);
1980 }
else if (
atIneq(r, pos) >= 1) {
1982 lbIndices.push_back(r);
1985 ubIndices.push_back(r);
1992 newSpace.
removeVarRange(idKindRemove, relativePos, relativePos + 1);
1995 IntegerRelation newRel(lbIndices.size() * ubIndices.size() + nbIndices.size(),
1999 bool allLCMsAreOne =
true;
2011 for (
auto ubPos : ubIndices) {
2012 for (
auto lbPos : lbIndices) {
2021 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2024 assert(lbCoeff >= 1 && ubCoeff >= 1 &&
"bounds wrongly identified");
2026 ineq.push_back(
atIneq(ubPos, l) * (
lcm / ubCoeff) +
2028 assert(
lcm > 0 &&
"lcm should be positive!");
2030 allLCMsAreOne =
false;
2035 ineq[ineq.size() - 1] += lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
2043 LLVM_DEBUG(llvm::dbgs() <<
"FM isResultIntegerExact: " << allLCMsAreOne
2045 if (allLCMsAreOne && isResultIntegerExact)
2046 *isResultIntegerExact =
true;
2049 for (
auto nbPos : nbIndices) {
2052 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2055 ineq.push_back(
atIneq(nbPos, l));
2061 lbIndices.size() * ubIndices.size() + nbIndices.size());
2067 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
2070 eq.push_back(
atEq(r, l));
2081 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
2086 #define DEBUG_TYPE "presburger"
2094 assert(pos + num <
getNumCols() &&
"invalid range");
2097 unsigned currentPos = pos;
2098 unsigned numToEliminate = num;
2099 unsigned numGaussianEliminated = 0;
2102 unsigned curNumEliminated =
2105 numToEliminate -= curNumEliminated + 1;
2106 numGaussianEliminated += curNumEliminated;
2110 for (
unsigned i = 0; i < num - numGaussianEliminated; i++) {
2111 unsigned numToEliminate = num - numGaussianEliminated - i;
2125 enum BoundCmpResult { Greater, Less, Equal, Unknown };
2130 assert(a.size() == b.size());
2136 if (!std::equal(a.begin(), a.end() - 1, b.begin()))
2139 if (a.back() == b.back())
2142 return a.back() < b.back() ? Less : Greater;
2181 std::vector<SmallVector<MPInt, 8>> boundingLbs;
2182 std::vector<SmallVector<MPInt, 8>> boundingUbs;
2194 MPInt lbFloorDivisor, otherLbFloorDivisor;
2197 if (!extent.has_value())
2203 d, &otherLb, &otherLbFloorDivisor, &otherUb);
2204 if (!otherExtent.has_value() || lbFloorDivisor != otherLbFloorDivisor)
2208 assert(lbFloorDivisor > 0 &&
"divisor always expected to be positive");
2210 auto res = compareBounds(lb, otherLb);
2212 if (res == BoundCmpResult::Less || res == BoundCmpResult::Equal) {
2217 minLb.back() -= lbFloorDivisor - 1;
2218 }
else if (res == BoundCmpResult::Greater) {
2220 minLb.back() -= otherLbFloorDivisor - 1;
2225 if (!constLb.has_value() || !constOtherLb.has_value())
2227 std::fill(minLb.begin(), minLb.end(), 0);
2228 minLb.back() =
std::min(*constLb, *constOtherLb);
2232 auto uRes = compareBounds(ub, otherUb);
2233 if (uRes == BoundCmpResult::Greater || uRes == BoundCmpResult::Equal) {
2235 }
else if (uRes == BoundCmpResult::Less) {
2241 if (!constUb.has_value() || !constOtherUb.has_value())
2243 std::fill(maxUb.begin(), maxUb.end(), 0);
2244 maxUb.back() =
std::max(*constUb, *constOtherUb);
2247 std::fill(newLb.begin(), newLb.end(), 0);
2248 std::fill(newUb.begin(), newUb.end(), 0);
2252 newLb[d] = lbFloorDivisor;
2253 newUb[d] = -lbFloorDivisor;
2256 std::transform(newLb.begin() +
getNumDimVars(), newLb.end(),
2260 boundingLbs.push_back(newLb);
2261 boundingUbs.push_back(newUb);
2294 assert(pos < cst.
getNumVars() &&
"invalid start position");
2295 assert(pos + num <= cst.
getNumVars() &&
"invalid limit");
2300 for (c = pos; c < pos + num; ++c) {
2301 if (cst.
atIneq(r, c) != 0)
2305 nbIneqIndices.push_back(r);
2311 for (c = pos; c < pos + num; ++c) {
2312 if (cst.
atEq(r, c) != 0)
2316 nbEqIndices.push_back(r);
2321 assert(pos + num <=
getNumVars() &&
"invalid range");
2330 for (
auto nbIndex : llvm::reverse(nbIneqIndices))
2332 for (
auto nbIndex : llvm::reverse(nbEqIndices))
2351 bool changed =
false;
2352 SmallDenseMap<ArrayRef<MPInt>,
unsigned> hashTable;
2360 hashTable.insert({row, 0});
2361 for (
unsigned k = 1; k < ineqs; ++k) {
2363 if (!hashTable.contains(row)) {
2364 hashTable.insert({row, k});
2369 unsigned l = hashTable[row];
2380 for (
unsigned k = 0; k < ineqs; ++k) {
2382 negIneq.assign(row.begin(), row.end());
2383 for (
MPInt &ele : negIneq)
2385 if (!hashTable.contains(negIneq))
2390 unsigned l = hashTable[row];
2392 if (sum > 0 || l == k)
2427 "Domain set is not compatible with poly");
2443 "Range set is not compatible with poly");
2463 "Range of `this` should be compatible with Domain of `rel`");
2527 "Domain of this and range of other do not match");
2590 os <<
atEq(i,
j) <<
"\t";
2609 "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 MPInt valueAt(ArrayRef< MPInt > expr, ArrayRef< MPInt > point)
Helper to evaluate an affine expression at a point.
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 bool rangeIsZero(ArrayRef< MPInt > range)
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 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.
MPInt & getDenom(unsigned i)
void clearRepr(unsigned i)
MutableArrayRef< MPInt > getDividend(unsigned i)
An Identifier stores a pointer to an object, such as a Value or an Operation.
MPInt 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 ...
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.
MPInt atEq(unsigned i, unsigned j) const
Returns the value at the specified equality row and column.
void removeIndependentConstraints(unsigned pos, unsigned num)
Removes constraints that are independent of (i.e., do not have a coefficient) variables in the range ...
ArrayRef< MPInt > getEquality(unsigned idx) const
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 addInequality(ArrayRef< MPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
std::optional< MPInt > getConstantBound(BoundType type, unsigned pos) const
Returns the constant bound for the pos^th variable if there is one; std::nullopt otherwise.
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 addEquality(ArrayRef< MPInt > eq)
Adds an equality from the coefficients specified in eq.
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
void removeEqualityRange(unsigned start, unsigned end)
Remove the (in)equalities at positions [start, end).
std::optional< MPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the relation.
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.
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()
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 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.
std::optional< SmallVector< MPInt, 8 > > findIntegerSample() const
Find an integer sample point satisfying the constraints using a branch and bound algorithm with gener...
MaybeOptimum< SmallVector< MPInt, 8 > > findIntegerLexMin() const
Same as above, but returns lexicographically minimal integer point.
virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
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.
IntegerRelation intersect(IntegerRelation other) const
Return the intersection of the two relations.
void addLocalFloorDiv(ArrayRef< MPInt > dividend, const MPInt &divisor)
Adds a new local variable as the floordiv of an affine function of other variables,...
ArrayRef< MPInt > getInequality(unsigned idx) const
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.
std::optional< SmallVector< MPInt, 8 > > containsPointNoLocal(ArrayRef< MPInt > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists,...
MPInt atIneq(unsigned i, unsigned j) const
Returns the value at the specified inequality row and column.
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.
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...
std::optional< MPInt > getConstantBoundOnDimSize(unsigned pos, SmallVectorImpl< MPInt > *lb=nullptr, MPInt *boundFloorDivisor=nullptr, SmallVectorImpl< MPInt > *ub=nullptr, unsigned *minLbPos=nullptr, unsigned *minUbPos=nullptr) const
Returns the smallest known constant bound for the extent of the specified variable (pos^th),...
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...
void addBound(BoundType type, unsigned pos, const MPInt &value)
Adds a constant bound for the specified variable.
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.
void setAndEliminate(unsigned pos, ArrayRef< MPInt > values)
Sets the values.size() variables starting at pos to the specified values and removes them.
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 mergeAndAlignSymbols(IntegerRelation &other)
Merge and align symbol variables of this and other with respect to identifiers.
std::optional< MPInt > computeConstantLowerOrUpperBound(unsigned pos)
Returns the constant lower bound if isLower is true, and the upper bound if isLower is false.
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...
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.
bool containsPoint(ArrayRef< MPInt > point) const
Returns true if the given point satisfies the constraints, or false otherwise.
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< MPInt, 8 > > findIntegerLexMin()
Return the lexicographically minimum integer solution to the constraints.
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin()
Return the lexicographically minimum rational solution to the constraints.
This class provides support for multi-precision arithmetic.
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...
bool isMarkedRedundant(unsigned constraintIndex) const
Returns whether the specified constraint has been marked as redundant.
std::optional< SmallVector< MPInt, 8 > > findIntegerSample()
Returns an integer sample point if one exists, or std::nullopt otherwise.
bool isFlatAlong(ArrayRef< MPInt > coeffs)
Check if the simplex takes only one rational value along the direction of coeffs.
std::pair< MaybeOptimum< MPInt >, MaybeOptimum< MPInt > > computeIntegerBounds(ArrayRef< MPInt > coeffs)
Returns a (min, max) pair denoting the minimum and maximum integer values of the given expression.
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.
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.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt gcd(const MPInt &a, const MPInt &b)
SmallVector< MPInt, 8 > getDivLowerBound(ArrayRef< MPInt > dividend, const MPInt &divisor, unsigned localVarIdx)
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt ceilDiv(const MPInt &lhs, const MPInt &rhs)
SmallVector< MPInt, 8 > getDivUpperBound(ArrayRef< MPInt > dividend, const MPInt &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 ...
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 ...
MaybeLocalRepr computeSingleVarRepr(const IntegerRelation &cst, ArrayRef< bool > foundRepr, unsigned pos, MutableArrayRef< MPInt > dividend, MPInt &divisor)
Returns the MaybeLocalRepr struct which contains the indices of the constraints that can be expressed...
Fraction abs(const Fraction &f)
MPInt ceil(const Fraction &f)
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt lcm(const MPInt &a, const MPInt &b)
Returns the least common multiple of 'a' and 'b'.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt floorDiv(const MPInt &lhs, const MPInt &rhs)
Include the generated interface declarations.
LogicalResult failure(bool isFailure=true)
Utility function to generate a LogicalResult.
bool succeeded(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a success value.
LogicalResult success(bool isSuccess=true)
Utility function to generate a LogicalResult.
bool failed(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a failure value.
This class represents an efficient way to signal success or failure.
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.