21 #include "llvm/ADT/DenseMap.h"
22 #include "llvm/ADT/DenseSet.h"
23 #include "llvm/Support/Debug.h"
27 #define DEBUG_TYPE "presburger"
30 using namespace presburger;
32 using llvm::SmallDenseMap;
33 using llvm::SmallDenseSet;
36 return std::make_unique<IntegerRelation>(*
this);
40 return std::make_unique<IntegerPolyhedron>(*
this);
49 assert(oSpace.
getNumLocalVars() == 0 &&
"no locals should be present!");
103 "Incorrect number of vars in lexMin!");
122 "Incorrect number of vars in lexMin!");
128 return llvm::all_of(range, [](
const MPInt &x) {
return x == 0; });
132 unsigned begin,
unsigned count) {
151 assert(num <= curNum &&
"Can't truncate to more vars!");
180 copy.getLocalReprs(&reprs);
184 unsigned numNonDivLocals = 0;
186 for (
unsigned i = 0, e =
copy.getNumLocalVars(); i < e - numNonDivLocals;) {
191 copy.swapVar(offset + i, offset + e - numNonDivLocals - 1);
192 std::swap(reprs[i], reprs[e - numNonDivLocals - 1]);
200 if (numNonDivLocals == 0)
217 copy.getNumVars() - numNonDivLocals)))
234 llvm::SmallBitVector isSymbol(
getNumVars(),
false);
279 for (
unsigned i = 0, e = eq.size(); i < e; ++i)
286 for (
unsigned i = 0, e = inEq.size(); i < e; ++i)
300 if (varStart >= varLimit)
315 if (varStart >= varLimit)
321 auto removeVarKindInRange = [
this](
VarKind kind,
unsigned &start,
330 unsigned relativeStart =
331 start <= offset ? 0 :
std::min(num, start - offset);
332 unsigned relativeLimit =
333 limit <= offset ? 0 :
std::min(num, limit - offset);
341 limit -= relativeLimit - relativeStart;
371 assert(posA <
getNumVars() &&
"invalid position A");
372 assert(posB <
getNumVars() &&
"invalid position B");
392 unsigned offset,
unsigned num)
const {
393 assert(pos <
getNumVars() &&
"invalid position");
394 assert(offset + num <
getNumCols() &&
"invalid range");
398 auto containsConstraintDependentOnRange = [&](
unsigned r,
bool isEq) {
401 for (c = offset, f = offset + num; c < f; ++c) {
415 if (containsConstraintDependentOnRange(r,
false))
417 if (
atIneq(r, pos) >= 1) {
419 lbIndices->push_back(r);
420 }
else if (
atIneq(r, pos) <= -1) {
422 ubIndices->push_back(r);
432 if (
atEq(r, pos) == 0)
434 if (containsConstraintDependentOnRange(r,
true))
436 eqIndices->push_back(r);
452 "invalid position or too many values");
457 for (
unsigned i = 0, numVals = values.size(); i < numVals; ++i)
459 for (
unsigned i = 0, numVals = values.size(); i < numVals; ++i)
472 unsigned *rowIdx)
const {
473 assert(colIdx <
getNumCols() &&
"position out of bounds");
474 auto at = [&](
unsigned rowIdx) ->
MPInt {
475 return isEq ?
atEq(rowIdx, colIdx) :
atIneq(rowIdx, colIdx);
478 for (*rowIdx = 0; *rowIdx < e; ++(*rowIdx)) {
479 if (at(*rowIdx) != 0) {
495 auto check = [&](
bool isEq) ->
bool {
498 for (
unsigned i = 0, e = numRows; i < e; ++i) {
500 for (
j = 0;
j < numCols - 1; ++
j) {
506 if (
j < numCols - 1) {
512 if ((isEq && v != 0) || (!isEq && v < 0)) {
527 unsigned rowIdx,
unsigned pivotRow,
528 unsigned pivotCol,
unsigned elimColStart,
531 if (isEq && rowIdx == pivotRow)
533 auto at = [&](
unsigned i,
unsigned j) ->
MPInt {
534 return isEq ? constraints->
atEq(i,
j) : constraints->
atIneq(i,
j);
536 MPInt leadCoeff = at(rowIdx, pivotCol);
540 MPInt pivotCoeff = constraints->
atEq(pivotRow, pivotCol);
541 int sign = (leadCoeff * pivotCoeff > 0) ? -1 : 1;
543 MPInt pivotMultiplier = sign * (
lcm /
abs(pivotCoeff));
547 for (
unsigned j = 0;
j < numCols; ++
j) {
549 if (
j >= elimColStart &&
j < pivotCol)
551 MPInt v = pivotMultiplier * constraints->
atEq(pivotRow,
j) +
552 rowMultiplier * at(rowIdx,
j);
553 isEq ? constraints->
atEq(rowIdx,
j) = v
554 : constraints->
atIneq(rowIdx,
j) = v;
564 unsigned start,
unsigned end) {
567 auto getProductOfNumLowerUpperBounds = [&](
unsigned pos) {
571 if (cst.
atIneq(r, pos) > 0) {
573 }
else if (cst.
atIneq(r, pos) < 0) {
577 return numLb * numUb;
580 unsigned minLoc = start;
581 unsigned min = getProductOfNumLowerUpperBounds(start);
582 for (
unsigned c = start + 1; c < end; c++) {
583 unsigned numLbUbProduct = getProductOfNumLowerUpperBounds(c);
584 if (numLbUbProduct <
min) {
585 min = numLbUbProduct;
608 unsigned currentPos = 0;
621 for (
unsigned i = 0, e = tmpCst.
getNumVars(); i < e; i++) {
630 LLVM_DEBUG(llvm::dbgs() <<
"FM constraint explosion detected\n");
661 for (
unsigned j = 1;
j < numCols - 1; ++
j) {
665 if (
gcd > 0 && (v %
gcd != 0)) {
686 assert(!simplex.
isEmpty() &&
"It is not meaningful to ask whether a "
687 "direction is bounded in an empty set.");
694 boundedIneqs.push_back(i);
704 for (
unsigned i : boundedIneqs) {
705 for (
unsigned col = 0; col < dirsNumCols; ++col)
706 dirs(row, col) =
atIneq(i, col);
712 for (
unsigned col = 0; col < dirsNumCols; ++col)
713 dirs(row, col) =
atEq(i, col);
767 std::optional<SmallVector<MPInt, 8>>
791 std::pair<unsigned, LinearTransform> result =
800 unsigned numBoundedDims = result.first;
801 unsigned numUnboundedDims =
getNumVars() - numBoundedDims;
807 std::optional<SmallVector<MPInt, 8>> boundedSample =
812 "Simplex returned an invalid sample!");
856 Simplex shrunkenConeSimplex(cone);
857 assert(!shrunkenConeSimplex.
isEmpty() &&
"Shrunken cone cannot be empty!");
867 sample.append(coneSample.begin(), coneSample.end());
875 assert(expr.size() == 1 + point.size() &&
876 "Dimensionalities of point and expression don't match!");
877 MPInt value = expr.back();
878 for (
unsigned i = 0; i < point.size(); ++i)
879 value += expr[i] * point[i];
906 std::optional<SmallVector<MPInt, 8>>
909 "Point should contain all vars except locals!");
911 "This function depends on locals being stored last!");
913 copy.setAndEliminate(0, point);
914 return copy.findIntegerSample();
931 if (!foundRepr[i + localOffset]) {
941 foundRepr[localOffset + i] =
true;
978 if (posStart >= posLimit)
983 unsigned pivotCol = 0;
984 for (pivotCol = posStart; pivotCol < posLimit; ++pivotCol) {
1014 posLimit = pivotCol;
1017 return posLimit - posStart;
1066 for (
unsigned r = 0; r < numIneqs; r++) {
1110 bool hasUnboundedVar =
false;
1116 assert((!
min.isEmpty() && !
max.isEmpty()) &&
1117 "Polytope should be rationally non-empty!");
1121 if (
min.isUnbounded() ||
max.isUnbounded()) {
1122 hasUnboundedVar =
true;
1128 if (
min.getBoundedOptimum() >
max.getBoundedOptimum())
1131 count *= (*
max - *
min + 1);
1136 if (hasUnboundedVar)
1146 posA += localOffset;
1147 posB += localOffset;
1174 auto merge = [&relA, &relB, oldALocals](
unsigned i,
unsigned j) ->
bool {
1203 auto merge = [
this](
unsigned i,
unsigned j) ->
bool {
1223 unsigned i, e,
j, f;
1242 if (
atEq(k,
j) != 0) {
1259 unsigned varLimit,
VarKind dstKind,
1261 assert(varLimit <=
getNumVarKind(srcKind) &&
"Invalid id range");
1263 if (varStart >= varLimit)
1267 unsigned convertCount = varLimit - varStart;
1268 unsigned newVarsBegin =
insertVar(dstKind, pos, convertCount);
1278 for (
unsigned i = 0; i < convertCount; ++i)
1279 swapVar(offset + varStart + i, newVarsBegin + i);
1286 const MPInt &value) {
1301 const MPInt &value) {
1305 for (
unsigned i = 0, e = expr.size(); i < e; ++i)
1317 const MPInt &divisor) {
1318 assert(dividend.size() ==
getNumCols() &&
"incorrect dividend size");
1319 assert(divisor > 0 &&
"positive divisor expected");
1324 dividendCopy.insert(dividendCopy.end() - 1,
MPInt(0));
1337 bool symbolic =
false) {
1338 assert(pos < cst.
getNumVars() &&
"invalid position");
1346 for (c = 0; c < f; c++) {
1349 if (cst.
atEq(r, c) != 0) {
1362 assert(pos <
getNumVars() &&
"invalid position");
1368 assert(
atEq(rowIdx, pos) *
atEq(rowIdx, pos) == 1);
1375 for (
unsigned s = pos, t = pos, e = pos + num; s < e; s++) {
1398 assert(pos <
getNumDimVars() &&
"Invalid variable position");
1409 [](
const MPInt &coeff) { return coeff == 0; }))
1410 return std::nullopt;
1426 (*ub)[c] = (*lb)[c];
1428 assert(boundFloorDivisor &&
1429 "both lb and divisor or none should be provided");
1430 *boundFloorDivisor = 1;
1447 return std::nullopt;
1460 std::optional<MPInt> minDiff;
1461 unsigned minLbPosition = 0, minUbPosition = 0;
1462 for (
auto ubPos : ubIndices) {
1463 for (
auto lbPos : lbIndices) {
1481 diff = std::max<MPInt>(diff,
MPInt(0));
1482 if (minDiff == std::nullopt || diff < minDiff) {
1484 minLbPosition = lbPos;
1485 minUbPosition = ubPos;
1489 if (lb && minDiff) {
1498 *boundFloorDivisor =
atIneq(minLbPosition, pos);
1499 assert(*boundFloorDivisor == -
atIneq(minUbPosition, pos));
1514 *minLbPos = minLbPosition;
1516 *minUbPos = minUbPosition;
1520 template <
bool isLower>
1521 std::optional<MPInt>
1523 assert(pos <
getNumVars() &&
"invalid position");
1541 return std::nullopt;
1543 std::optional<MPInt> minOrMaxConst;
1552 }
else if (
atIneq(r, 0) >= 0) {
1557 for (c = 0, f =
getNumCols() - 1; c < f; c++)
1558 if (c != 0 &&
atIneq(r, c) != 0)
1568 if (minOrMaxConst == std::nullopt || boundConst > minOrMaxConst)
1569 minOrMaxConst = boundConst;
1571 if (minOrMaxConst == std::nullopt || boundConst < minOrMaxConst)
1572 minOrMaxConst = boundConst;
1575 return minOrMaxConst;
1579 unsigned pos)
const {
1582 .computeConstantLowerOrUpperBound<
true>(pos);
1585 .computeConstantLowerOrUpperBound<
false>(pos);
1588 std::optional<MPInt> lb =
1591 std::optional<MPInt> ub =
1593 .computeConstantLowerOrUpperBound<
false>(pos);
1594 return (lb && ub && *lb == *ub) ? std::optional<MPInt>(*ub) : std::nullopt;
1603 for (
unsigned c = pos; c < pos + num; c++) {
1612 for (
unsigned c = pos; c < pos + num; c++) {
1613 if (
atEq(r, c) != 0)
1635 SmallDenseMap<ArrayRef<MPInt>, std::pair<unsigned, MPInt>>
1636 rowsWithoutConstTerm;
1638 SmallDenseSet<ArrayRef<MPInt>, 8> rowSet;
1641 auto isTriviallyValid = [&](
unsigned r) ->
bool {
1642 for (
unsigned c = 0, e =
getNumCols() - 1; c < e; c++) {
1654 if (isTriviallyValid(r) || !rowSet.insert(row).second) {
1655 redunIneq[r] =
true;
1666 rowsWithoutConstTerm.insert({rowWithoutConstTerm, {r, constTerm}});
1669 auto &val = ret.first->second;
1670 if (val.second > constTerm) {
1672 redunIneq[val.first] =
true;
1673 val = {r, constTerm};
1676 redunIneq[r] =
true;
1694 #define DEBUG_TYPE "fm"
1740 bool *isResultIntegerExact) {
1741 LLVM_DEBUG(llvm::dbgs() <<
"FM input (eliminate pos " << pos <<
"):\n");
1743 assert(pos <
getNumVars() &&
"invalid position");
1748 if (
atEq(r, pos) != 0) {
1752 assert(
succeeded(ret) &&
"Gaussian elimination guaranteed to succeed");
1753 LLVM_DEBUG(llvm::dbgs() <<
"FM output (through Gaussian elimination):\n");
1767 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
1777 std::vector<unsigned> nbIndices;
1784 if (
atIneq(r, pos) == 0) {
1786 nbIndices.push_back(r);
1787 }
else if (
atIneq(r, pos) >= 1) {
1789 lbIndices.push_back(r);
1792 ubIndices.push_back(r);
1799 newSpace.
removeVarRange(idKindRemove, relativePos, relativePos + 1);
1802 IntegerRelation newRel(lbIndices.size() * ubIndices.size() + nbIndices.size(),
1806 bool allLCMsAreOne =
true;
1818 for (
auto ubPos : ubIndices) {
1819 for (
auto lbPos : lbIndices) {
1828 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
1831 assert(lbCoeff >= 1 && ubCoeff >= 1 &&
"bounds wrongly identified");
1833 ineq.push_back(
atIneq(ubPos, l) * (
lcm / ubCoeff) +
1835 assert(
lcm > 0 &&
"lcm should be positive!");
1837 allLCMsAreOne =
false;
1842 ineq[ineq.size() - 1] += lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
1850 LLVM_DEBUG(llvm::dbgs() <<
"FM isResultIntegerExact: " << allLCMsAreOne
1852 if (allLCMsAreOne && isResultIntegerExact)
1853 *isResultIntegerExact =
true;
1856 for (
auto nbPos : nbIndices) {
1859 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
1862 ineq.push_back(
atIneq(nbPos, l));
1868 lbIndices.size() * ubIndices.size() + nbIndices.size());
1874 for (
unsigned l = 0, e =
getNumCols(); l < e; l++) {
1877 eq.push_back(
atEq(r, l));
1888 LLVM_DEBUG(llvm::dbgs() <<
"FM output:\n");
1893 #define DEBUG_TYPE "presburger"
1901 assert(pos + num <
getNumCols() &&
"invalid range");
1904 unsigned currentPos = pos;
1905 unsigned numToEliminate = num;
1906 unsigned numGaussianEliminated = 0;
1909 unsigned curNumEliminated =
1912 numToEliminate -= curNumEliminated + 1;
1913 numGaussianEliminated += curNumEliminated;
1917 for (
unsigned i = 0; i < num - numGaussianEliminated; i++) {
1918 unsigned numToEliminate = num - numGaussianEliminated - i;
1932 enum BoundCmpResult { Greater, Less, Equal, Unknown };
1937 assert(a.size() == b.size());
1943 if (!std::equal(a.begin(), a.end() - 1, b.begin()))
1946 if (a.back() == b.back())
1949 return a.back() < b.back() ? Less : Greater;
1988 std::vector<SmallVector<MPInt, 8>> boundingLbs;
1989 std::vector<SmallVector<MPInt, 8>> boundingUbs;
2001 MPInt lbFloorDivisor, otherLbFloorDivisor;
2004 if (!extent.has_value())
2010 d, &otherLb, &otherLbFloorDivisor, &otherUb);
2011 if (!otherExtent.has_value() || lbFloorDivisor != otherLbFloorDivisor)
2015 assert(lbFloorDivisor > 0 &&
"divisor always expected to be positive");
2017 auto res = compareBounds(lb, otherLb);
2019 if (res == BoundCmpResult::Less || res == BoundCmpResult::Equal) {
2024 minLb.back() -= lbFloorDivisor - 1;
2025 }
else if (res == BoundCmpResult::Greater) {
2027 minLb.back() -= otherLbFloorDivisor - 1;
2032 if (!constLb.has_value() || !constOtherLb.has_value())
2034 std::fill(minLb.begin(), minLb.end(), 0);
2035 minLb.back() =
std::min(*constLb, *constOtherLb);
2039 auto uRes = compareBounds(ub, otherUb);
2040 if (uRes == BoundCmpResult::Greater || uRes == BoundCmpResult::Equal) {
2042 }
else if (uRes == BoundCmpResult::Less) {
2048 if (!constUb.has_value() || !constOtherUb.has_value())
2050 std::fill(maxUb.begin(), maxUb.end(), 0);
2051 maxUb.back() =
std::max(*constUb, *constOtherUb);
2054 std::fill(newLb.begin(), newLb.end(), 0);
2055 std::fill(newUb.begin(), newUb.end(), 0);
2059 newLb[d] = lbFloorDivisor;
2060 newUb[d] = -lbFloorDivisor;
2063 std::transform(newLb.begin() +
getNumDimVars(), newLb.end(),
2067 boundingLbs.push_back(newLb);
2068 boundingUbs.push_back(newUb);
2101 assert(pos < cst.
getNumVars() &&
"invalid start position");
2102 assert(pos + num <= cst.
getNumVars() &&
"invalid limit");
2107 for (c = pos; c < pos + num; ++c) {
2108 if (cst.
atIneq(r, c) != 0)
2112 nbIneqIndices.push_back(r);
2118 for (c = pos; c < pos + num; ++c) {
2119 if (cst.
atEq(r, c) != 0)
2123 nbEqIndices.push_back(r);
2128 assert(pos + num <=
getNumVars() &&
"invalid range");
2137 for (
auto nbIndex : llvm::reverse(nbIneqIndices))
2139 for (
auto nbIndex : llvm::reverse(nbEqIndices))
2172 "Domain set is not compatible with poly");
2188 "Range set is not compatible with poly");
2208 "Range of `this` should be compatible with Domain of `rel`");
2251 os <<
atEq(i,
j) <<
"\t";
2270 "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 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 ...
SymbolicLexMin findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation.
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.
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...
Matrix equalities
Coefficients of affine equalities (in == 0 form).
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)
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 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...
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.
Matrix getBoundedDirections() const
Returns a matrix where each row is a vector along which the polytope is bounded.
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 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.
unsigned getNumDimAndSymbolVars() const
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 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.
std::optional< MPInt > computeConstantLowerOrUpperBound(unsigned pos)
Returns the constant lower bound 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.
virtual bool hasConsistentState() const
Returns false if the fields corresponding to various variable counts, or equality/inequality buffer s...
Matrix inequalities
Coefficients of affine inequalities (in >= 0 form).
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,...
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.
This is a class to represent a resizable matrix.
bool hasConsistentState() const
Return whether the Matrix is in a consistent state with all its invariants satisfied.
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 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, ...
MPInt normalizeRow(unsigned row, unsigned nCols)
Divide the first nCols of the specified row by their GCD.
void removeRow(unsigned pos)
void resizeVertically(unsigned newNRows)
void fillRow(unsigned row, const MPInt &value)
unsigned getNumRows() const
void addToColumn(unsigned sourceColumn, unsigned targetColumn, const MPInt &scale)
Add scale multiples of the source column to the target column.
void reserveRows(unsigned rows)
Reserve enough space to resize to the specified number of rows without reallocations.
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
void removeOutputs(unsigned start, unsigned end)
Remove the specified range of outputs.
unsigned getNumOutputs() const
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.
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
bool isEqual(const PresburgerSpace &other) const
Returns true if both the spaces are equal including local variables i.e.
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.
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)
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)
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.
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...
SymbolicLexMin computeSymbolicIntegerLexMin()
The lexmin will be stored as a function lexmin 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 ...
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt abs(const MPInt &x)
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...
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)
This header declares functions that assit transformations in the MemRef dialect.
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 minimization computation.
PWMAFunction lexmin
This maps assignments of symbols to the corresponding lexmin.
PresburgerSet unboundedDomain
Contains all assignments to the symbols that made the lexmin unbounded.
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.