1096 lines · cpp
1//===- PresburgerRelation.cpp - MLIR PresburgerRelation Class -------------===//2//3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.4// See https://llvm.org/LICENSE.txt for license information.5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception6//7//===----------------------------------------------------------------------===//8 9#include "mlir/Analysis/Presburger/PresburgerRelation.h"10#include "mlir/Analysis/Presburger/IntegerRelation.h"11#include "mlir/Analysis/Presburger/PWMAFunction.h"12#include "mlir/Analysis/Presburger/PresburgerSpace.h"13#include "mlir/Analysis/Presburger/Simplex.h"14#include "mlir/Analysis/Presburger/Utils.h"15#include "llvm/ADT/STLExtras.h"16#include "llvm/ADT/SmallBitVector.h"17#include "llvm/ADT/SmallVector.h"18#include "llvm/Support/raw_ostream.h"19#include <cassert>20#include <functional>21#include <optional>22#include <utility>23#include <vector>24 25using namespace mlir;26using namespace presburger;27 28PresburgerRelation::PresburgerRelation(const IntegerRelation &disjunct)29 : space(disjunct.getSpaceWithoutLocals()) {30 unionInPlace(disjunct);31}32 33void PresburgerRelation::setSpace(const PresburgerSpace &oSpace) {34 assert(space.getNumLocalVars() == 0 && "no locals should be present");35 space = oSpace;36 for (IntegerRelation &disjunct : disjuncts)37 disjunct.setSpaceExceptLocals(space);38}39 40void PresburgerRelation::insertVarInPlace(VarKind kind, unsigned pos,41 unsigned num) {42 for (IntegerRelation &cs : disjuncts)43 cs.insertVar(kind, pos, num);44 space.insertVar(kind, pos, num);45}46 47void PresburgerRelation::convertVarKind(VarKind srcKind, unsigned srcPos,48 unsigned num, VarKind dstKind,49 unsigned dstPos) {50 assert(srcKind != VarKind::Local && dstKind != VarKind::Local &&51 "srcKind/dstKind cannot be local");52 assert(srcKind != dstKind && "cannot convert variables to the same kind");53 assert(srcPos + num <= space.getNumVarKind(srcKind) &&54 "invalid range for source variables");55 assert(dstPos <= space.getNumVarKind(dstKind) &&56 "invalid position for destination variables");57 58 space.convertVarKind(srcKind, srcPos, num, dstKind, dstPos);59 60 for (IntegerRelation &disjunct : disjuncts)61 disjunct.convertVarKind(srcKind, srcPos, srcPos + num, dstKind, dstPos);62}63 64unsigned PresburgerRelation::getNumDisjuncts() const {65 return disjuncts.size();66}67 68ArrayRef<IntegerRelation> PresburgerRelation::getAllDisjuncts() const {69 return disjuncts;70}71 72const IntegerRelation &PresburgerRelation::getDisjunct(unsigned index) const {73 assert(index < disjuncts.size() && "index out of bounds!");74 return disjuncts[index];75}76 77/// Mutate this set, turning it into the union of this set and the given78/// IntegerRelation.79void PresburgerRelation::unionInPlace(const IntegerRelation &disjunct) {80 assert(space.isCompatible(disjunct.getSpace()) && "Spaces should match");81 disjuncts.emplace_back(disjunct);82}83 84/// Mutate this set, turning it into the union of this set and the given set.85///86/// This is accomplished by simply adding all the disjuncts of the given set87/// to this set.88void PresburgerRelation::unionInPlace(const PresburgerRelation &set) {89 assert(space.isCompatible(set.getSpace()) && "Spaces should match");90 91 if (isObviouslyEqual(set))92 return;93 94 if (isObviouslyEmpty()) {95 disjuncts = set.disjuncts;96 return;97 }98 if (set.isObviouslyEmpty())99 return;100 101 if (isObviouslyUniverse())102 return;103 if (set.isObviouslyUniverse()) {104 disjuncts = set.disjuncts;105 return;106 }107 108 for (const IntegerRelation &disjunct : set.disjuncts)109 unionInPlace(disjunct);110}111 112/// Return the union of this set and the given set.113PresburgerRelation114PresburgerRelation::unionSet(const PresburgerRelation &set) const {115 assert(space.isCompatible(set.getSpace()) && "Spaces should match");116 PresburgerRelation result = *this;117 result.unionInPlace(set);118 return result;119}120 121/// A point is contained in the union iff any of the parts contain the point.122bool PresburgerRelation::containsPoint(ArrayRef<DynamicAPInt> point) const {123 return llvm::any_of(disjuncts, [&point](const IntegerRelation &disjunct) {124 return disjunct.containsPointNoLocal(point);125 });126}127 128PresburgerRelation129PresburgerRelation::getUniverse(const PresburgerSpace &space) {130 PresburgerRelation result(space);131 result.unionInPlace(IntegerRelation::getUniverse(space));132 return result;133}134 135PresburgerRelation PresburgerRelation::getEmpty(const PresburgerSpace &space) {136 return PresburgerRelation(space);137}138 139// Return the intersection of this set with the given set.140//141// We directly compute (S_1 or S_2 ...) and (T_1 or T_2 ...)142// as (S_1 and T_1) or (S_1 and T_2) or ...143//144// If S_i or T_j have local variables, then S_i and T_j contains the local145// variables of both.146PresburgerRelation147PresburgerRelation::intersect(const PresburgerRelation &set) const {148 assert(space.isCompatible(set.getSpace()) && "Spaces should match");149 150 // If the set is empty or the other set is universe,151 // directly return the set152 if (isObviouslyEmpty() || set.isObviouslyUniverse())153 return *this;154 155 if (set.isObviouslyEmpty() || isObviouslyUniverse())156 return set;157 158 PresburgerRelation result(getSpace());159 for (const IntegerRelation &csA : disjuncts) {160 for (const IntegerRelation &csB : set.disjuncts) {161 IntegerRelation intersection = csA.intersect(csB);162 if (!intersection.isEmpty())163 result.unionInPlace(intersection);164 }165 }166 return result;167}168 169PresburgerRelation170PresburgerRelation::intersectRange(const PresburgerSet &set) const {171 assert(space.getRangeSpace().isCompatible(set.getSpace()) &&172 "Range of `this` must be compatible with range of `set`");173 174 PresburgerRelation other = set;175 other.insertVarInPlace(VarKind::Domain, 0, getNumDomainVars());176 return intersect(other);177}178 179PresburgerRelation180PresburgerRelation::intersectDomain(const PresburgerSet &set) const {181 assert(space.getDomainSpace().isCompatible(set.getSpace()) &&182 "Domain of `this` must be compatible with range of `set`");183 184 PresburgerRelation other = set;185 other.insertVarInPlace(VarKind::Domain, 0, getNumRangeVars());186 other.inverse();187 return intersect(other);188}189 190PresburgerSet PresburgerRelation::getDomainSet() const {191 PresburgerSet result = PresburgerSet::getEmpty(space.getDomainSpace());192 for (const IntegerRelation &cs : disjuncts)193 result.unionInPlace(cs.getDomainSet());194 return result;195}196 197PresburgerSet PresburgerRelation::getRangeSet() const {198 PresburgerSet result = PresburgerSet::getEmpty(space.getRangeSpace());199 for (const IntegerRelation &cs : disjuncts)200 result.unionInPlace(cs.getRangeSet());201 return result;202}203 204void PresburgerRelation::inverse() {205 for (IntegerRelation &cs : disjuncts)206 cs.inverse();207 208 if (getNumDisjuncts())209 setSpace(getDisjunct(0).getSpaceWithoutLocals());210}211 212void PresburgerRelation::compose(const PresburgerRelation &rel) {213 assert(getSpace().getRangeSpace().isCompatible(214 rel.getSpace().getDomainSpace()) &&215 "Range of `this` should be compatible with domain of `rel`");216 217 PresburgerRelation result =218 PresburgerRelation::getEmpty(PresburgerSpace::getRelationSpace(219 getNumDomainVars(), rel.getNumRangeVars(), getNumSymbolVars()));220 for (const IntegerRelation &csA : disjuncts) {221 for (const IntegerRelation &csB : rel.disjuncts) {222 IntegerRelation composition = csA;223 composition.compose(csB);224 if (!composition.isEmpty())225 result.unionInPlace(composition);226 }227 }228 *this = result;229}230 231void PresburgerRelation::applyDomain(const PresburgerRelation &rel) {232 assert(getSpace().getDomainSpace().isCompatible(233 rel.getSpace().getDomainSpace()) &&234 "Domain of `this` should be compatible with domain of `rel`");235 236 inverse();237 compose(rel);238 inverse();239}240 241void PresburgerRelation::applyRange(const PresburgerRelation &rel) {242 compose(rel);243}244 245static SymbolicLexOpt findSymbolicIntegerLexOpt(const PresburgerRelation &rel,246 bool isMin) {247 SymbolicLexOpt result(rel.getSpace());248 PWMAFunction &lexopt = result.lexopt;249 PresburgerSet &unboundedDomain = result.unboundedDomain;250 for (const IntegerRelation &cs : rel.getAllDisjuncts()) {251 SymbolicLexOpt s(rel.getSpace());252 if (isMin) {253 s = cs.findSymbolicIntegerLexMin();254 lexopt = lexopt.unionLexMin(s.lexopt);255 } else {256 s = cs.findSymbolicIntegerLexMax();257 lexopt = lexopt.unionLexMax(s.lexopt);258 }259 unboundedDomain = unboundedDomain.intersect(s.unboundedDomain);260 }261 return result;262}263 264SymbolicLexOpt PresburgerRelation::findSymbolicIntegerLexMin() const {265 return findSymbolicIntegerLexOpt(*this, true);266}267 268SymbolicLexOpt PresburgerRelation::findSymbolicIntegerLexMax() const {269 return findSymbolicIntegerLexOpt(*this, false);270}271 272/// Return the coefficients of the ineq in `rel` specified by `idx`.273/// `idx` can refer not only to an actual inequality of `rel`, but also274/// to either of the inequalities that make up an equality in `rel`.275///276/// When 0 <= idx < rel.getNumInequalities(), this returns the coeffs of the277/// idx-th inequality of `rel`.278///279/// Otherwise, it is then considered to index into the ineqs corresponding to280/// eqs of `rel`, and it must hold that281///282/// 0 <= idx - rel.getNumInequalities() < 2*getNumEqualities().283///284/// For every eq `coeffs == 0` there are two possible ineqs to index into.285/// The first is coeffs >= 0 and the second is coeffs <= 0.286static SmallVector<DynamicAPInt, 8>287getIneqCoeffsFromIdx(const IntegerRelation &rel, unsigned idx) {288 assert(idx < rel.getNumInequalities() + 2 * rel.getNumEqualities() &&289 "idx out of bounds!");290 if (idx < rel.getNumInequalities())291 return llvm::to_vector<8>(rel.getInequality(idx));292 293 idx -= rel.getNumInequalities();294 ArrayRef<DynamicAPInt> eqCoeffs = rel.getEquality(idx / 2);295 296 if (idx % 2 == 0)297 return llvm::to_vector<8>(eqCoeffs);298 return getNegatedCoeffs(eqCoeffs);299}300 301PresburgerRelation PresburgerRelation::computeReprWithOnlyDivLocals() const {302 if (hasOnlyDivLocals())303 return *this;304 305 // The result is just the union of the reprs of the disjuncts.306 PresburgerRelation result(getSpace());307 for (const IntegerRelation &disjunct : disjuncts)308 result.unionInPlace(disjunct.computeReprWithOnlyDivLocals());309 return result;310}311 312/// Return the set difference b \ s.313///314/// In the following, U denotes union, /\ denotes intersection, \ denotes set315/// difference and ~ denotes complement.316///317/// Let s = (U_i s_i). We want b \ (U_i s_i).318///319/// Let s_i = /\_j s_ij, where each s_ij is a single inequality. To compute320/// b \ s_i = b /\ ~s_i, we partition s_i based on the first violated321/// inequality: ~s_i = (~s_i1) U (s_i1 /\ ~s_i2) U (s_i1 /\ s_i2 /\ ~s_i3) U ...322/// And the required result is (b /\ ~s_i1) U (b /\ s_i1 /\ ~s_i2) U ...323/// We recurse by subtracting U_{j > i} S_j from each of these parts and324/// returning the union of the results. Each equality is handled as a325/// conjunction of two inequalities.326///327/// Note that the same approach works even if an inequality involves a floor328/// division. For example, the complement of x <= 7*floor(x/7) is still329/// x > 7*floor(x/7). Since b \ s_i contains the inequalities of both b and s_i330/// (or the complements of those inequalities), b \ s_i may contain the331/// divisions present in both b and s_i. Therefore, we need to add the local332/// division variables of both b and s_i to each part in the result. This means333/// adding the local variables of both b and s_i, as well as the corresponding334/// division inequalities to each part. Since the division inequalities are335/// added to each part, we can skip the parts where the complement of any336/// division inequality is added, as these parts will become empty anyway.337///338/// As a heuristic, we try adding all the constraints and check if simplex339/// says that the intersection is empty. If it is, then subtracting this340/// disjuncts is a no-op and we just skip it. Also, in the process we find out341/// that some constraints are redundant. These redundant constraints are342/// ignored.343///344static PresburgerRelation getSetDifference(IntegerRelation b,345 const PresburgerRelation &s) {346 assert(b.getSpace().isCompatible(s.getSpace()) && "Spaces should match");347 if (b.isEmptyByGCDTest())348 return PresburgerRelation::getEmpty(b.getSpaceWithoutLocals());349 350 if (!s.hasOnlyDivLocals())351 return getSetDifference(b, s.computeReprWithOnlyDivLocals());352 353 // Remove duplicate divs up front here to avoid existing354 // divs disappearing in the call to mergeLocalVars below.355 b.removeDuplicateDivs();356 357 PresburgerRelation result =358 PresburgerRelation::getEmpty(b.getSpaceWithoutLocals());359 Simplex simplex(b);360 361 // This algorithm is more naturally expressed recursively, but we implement362 // it iteratively here to avoid issues with stack sizes.363 //364 // Each level of the recursion has five stack variables.365 struct Frame {366 // A snapshot of the simplex state to rollback to.367 unsigned simplexSnapshot;368 // A CountsSnapshot of `b` to rollback to.369 IntegerRelation::CountsSnapshot bCounts;370 // The IntegerRelation currently being operated on.371 IntegerRelation sI;372 // A list of indexes (see getIneqCoeffsFromIdx) of inequalities to be373 // processed.374 SmallVector<unsigned, 8> ineqsToProcess;375 // The index of the last inequality that was processed at this level.376 // This is empty when we are coming to this level for the first time.377 std::optional<unsigned> lastIneqProcessed;378 379 // Convenience constructor.380 Frame(unsigned simplexSnapshot,381 const IntegerRelation::CountsSnapshot &bCounts,382 const IntegerRelation &sI, ArrayRef<unsigned> ineqsToProcess = {},383 std::optional<unsigned> lastIneqProcessed = std::nullopt)384 : simplexSnapshot(simplexSnapshot), bCounts(bCounts), sI(sI),385 ineqsToProcess(ineqsToProcess), lastIneqProcessed(lastIneqProcessed) {386 }387 };388 SmallVector<Frame, 2> frames;389 390 // When we "recurse", we ensure the current frame is stored in `frames` and391 // increment `level`. When we return, we decrement `level`.392 unsigned level = 1;393 while (level > 0) {394 if (level - 1 >= s.getNumDisjuncts()) {395 // No more parts to subtract; add to the result and return.396 result.unionInPlace(b);397 level = frames.size();398 continue;399 }400 401 if (level > frames.size()) {402 // No frame for this level yet, so we have just recursed into this level.403 IntegerRelation sI = s.getDisjunct(level - 1);404 // Remove the duplicate divs up front to avoid them possibly disappearing405 // in the call to mergeLocalVars below.406 sI.removeDuplicateDivs();407 408 // Below, we append some additional constraints and ids to b. We want to409 // rollback b to its initial state before returning, which we will do by410 // removing all constraints beyond the original number of inequalities411 // and equalities, so we store these counts first.412 IntegerRelation::CountsSnapshot initBCounts = b.getCounts();413 // Similarly, we also want to rollback simplex to its original state.414 unsigned initialSnapshot = simplex.getSnapshot();415 416 // Add sI's locals to b, after b's locals. Only those locals of sI which417 // do not already exist in b will be added. (i.e., duplicate divisions418 // will not be added.) Also add b's locals to sI, in such a way that both419 // have the same locals in the same order in the end.420 b.mergeLocalVars(sI);421 422 // Find out which inequalities of sI correspond to division inequalities423 // for the local variables of sI.424 //425 // Careful! This has to be done after the merge above; otherwise, the426 // dividends won't contain the new ids inserted during the merge.427 std::vector<MaybeLocalRepr> repr(sI.getNumLocalVars());428 DivisionRepr divs = sI.getLocalReprs(&repr);429 430 // Mark which inequalities of sI are division inequalities and add all431 // such inequalities to b.432 llvm::SmallBitVector canIgnoreIneq(sI.getNumInequalities() +433 2 * sI.getNumEqualities());434 for (unsigned i = initBCounts.getSpace().getNumLocalVars(),435 e = sI.getNumLocalVars();436 i < e; ++i) {437 assert(438 repr[i] &&439 "Subtraction is not supported when a representation of the local "440 "variables of the subtrahend cannot be found!");441 442 if (repr[i].kind == ReprKind::Inequality) {443 unsigned lb = repr[i].repr.inequalityPair.lowerBoundIdx;444 unsigned ub = repr[i].repr.inequalityPair.upperBoundIdx;445 446 b.addInequality(sI.getInequality(lb));447 b.addInequality(sI.getInequality(ub));448 449 assert(lb != ub &&450 "Upper and lower bounds must be different inequalities!");451 canIgnoreIneq[lb] = true;452 canIgnoreIneq[ub] = true;453 } else {454 assert(repr[i].kind == ReprKind::Equality &&455 "ReprKind isn't inequality so should be equality");456 457 // Consider the case (x) : (x = 3e + 1), where e is a local.458 // Its complement is (x) : (x = 3e) or (x = 3e + 2).459 //460 // This can be computed by considering the set to be461 // (x) : (x = 3*(x floordiv 3) + 1).462 //463 // Now there are no equalities defining divisions; the division is464 // defined by the standard division equalities for e = x floordiv 3,465 // i.e., 0 <= x - 3*e <= 2.466 // So now as before, we add these division inequalities to b. The467 // equality is now just an ordinary constraint that must be considered468 // in the remainder of the algorithm. The division inequalities must469 // need not be considered, same as above, and they automatically will470 // not be because they were never a part of sI; we just infer them471 // from the equality and add them only to b.472 b.addInequality(473 getDivLowerBound(divs.getDividend(i), divs.getDenom(i),474 sI.getVarKindOffset(VarKind::Local) + i));475 b.addInequality(476 getDivUpperBound(divs.getDividend(i), divs.getDenom(i),477 sI.getVarKindOffset(VarKind::Local) + i));478 }479 }480 481 unsigned offset = simplex.getNumConstraints();482 unsigned numLocalsAdded =483 b.getNumLocalVars() - initBCounts.getSpace().getNumLocalVars();484 simplex.appendVariable(numLocalsAdded);485 486 unsigned snapshotBeforeIntersect = simplex.getSnapshot();487 simplex.intersectIntegerRelation(sI);488 489 if (simplex.isEmpty()) {490 // b /\ s_i is empty, so b \ s_i = b. We move directly to i + 1.491 // We are ignoring level i completely, so we restore the state492 // *before* going to the next level.493 b.truncate(initBCounts);494 simplex.rollback(initialSnapshot);495 // Recurse. We haven't processed any inequalities and496 // we don't need to process anything when we return.497 //498 // TODO: consider supporting tail recursion directly if this becomes499 // relevant for performance.500 frames.emplace_back(Frame{initialSnapshot, initBCounts, sI});501 ++level;502 continue;503 }504 505 // Equalities are added to simplex as a pair of inequalities.506 unsigned totalNewSimplexInequalities =507 2 * sI.getNumEqualities() + sI.getNumInequalities();508 // Look for redundant constraints among the constraints of sI. We don't509 // care about redundant constraints in `b` at this point.510 //511 // When there are two copies of a constraint in `simplex`, i.e., among the512 // constraints of `b` and `sI`, only one of them can be marked redundant.513 // (Assuming no other constraint makes these redundant.)514 //515 // In a case where there is one copy in `b` and one in `sI`, we want the516 // one in `sI` to be marked, not the one in `b`. Therefore, it's not517 // enough to ignore the constraints of `b` when checking which518 // constraints `detectRedundant` has marked redundant; we explicitly tell519 // `detectRedundant` to only mark constraints from `sI` as being520 // redundant.521 simplex.detectRedundant(offset, totalNewSimplexInequalities);522 for (unsigned j = 0; j < totalNewSimplexInequalities; j++)523 canIgnoreIneq[j] = simplex.isMarkedRedundant(offset + j);524 simplex.rollback(snapshotBeforeIntersect);525 526 SmallVector<unsigned, 8> ineqsToProcess;527 ineqsToProcess.reserve(totalNewSimplexInequalities);528 for (unsigned i = 0; i < totalNewSimplexInequalities; ++i)529 if (!canIgnoreIneq[i])530 ineqsToProcess.emplace_back(i);531 532 if (ineqsToProcess.empty()) {533 // Nothing to process; return. (we have no frame to pop.)534 level = frames.size();535 continue;536 }537 538 unsigned simplexSnapshot = simplex.getSnapshot();539 IntegerRelation::CountsSnapshot bCounts = b.getCounts();540 frames.emplace_back(Frame{simplexSnapshot, bCounts, sI, ineqsToProcess});541 // We have completed the initial setup for this level.542 // Fallthrough to the main recursive part below.543 }544 545 // For each inequality ineq, we first recurse with the part where ineq546 // is not satisfied, and then add ineq to b and simplex because547 // ineq must be satisfied by all later parts.548 if (level == frames.size()) {549 Frame &frame = frames.back();550 if (frame.lastIneqProcessed) {551 // Let the current value of b be b' and552 // let the initial value of b when we first came to this level be b.553 //554 // b' is equal to b /\ s_i1 /\ s_i2 /\ ... /\ s_i{j-1} /\ ~s_ij.555 // We had previously recursed with the part where s_ij was not556 // satisfied; all further parts satisfy s_ij, so we rollback to the557 // state before adding this complement constraint, and add s_ij to b.558 simplex.rollback(frame.simplexSnapshot);559 b.truncate(frame.bCounts);560 SmallVector<DynamicAPInt, 8> ineq =561 getIneqCoeffsFromIdx(frame.sI, *frame.lastIneqProcessed);562 b.addInequality(ineq);563 simplex.addInequality(ineq);564 }565 566 if (frame.ineqsToProcess.empty()) {567 // No ineqs left to process; pop this level's frame and return.568 frames.pop_back();569 level = frames.size();570 continue;571 }572 573 // "Recurse" with the part where the ineq is not satisfied.574 frame.bCounts = b.getCounts();575 frame.simplexSnapshot = simplex.getSnapshot();576 577 unsigned idx = frame.ineqsToProcess.back();578 SmallVector<DynamicAPInt, 8> ineq =579 getComplementIneq(getIneqCoeffsFromIdx(frame.sI, idx));580 b.addInequality(ineq);581 simplex.addInequality(ineq);582 583 frame.ineqsToProcess.pop_back();584 frame.lastIneqProcessed = idx;585 ++level;586 continue;587 }588 }589 590 // Try to simplify the results.591 result = result.simplify();592 593 return result;594}595 596/// Return the complement of this set.597PresburgerRelation PresburgerRelation::complement() const {598 return getSetDifference(IntegerRelation::getUniverse(getSpace()), *this);599}600 601/// Return the result of subtract the given set from this set, i.e.,602/// return `this \ set`.603PresburgerRelation604PresburgerRelation::subtract(const PresburgerRelation &set) const {605 assert(space.isCompatible(set.getSpace()) && "Spaces should match");606 PresburgerRelation result(getSpace());607 608 // If we know that the two sets are clearly equal, we can simply return the609 // empty set.610 if (isObviouslyEqual(set))611 return result;612 613 // We compute (U_i t_i) \ (U_i set_i) as U_i (t_i \ V_i set_i).614 for (const IntegerRelation &disjunct : disjuncts)615 result.unionInPlace(getSetDifference(disjunct, set));616 return result;617}618 619/// T is a subset of S iff T \ S is empty, since if T \ S contains a620/// point then this is a point that is contained in T but not S, and621/// if T contains a point that is not in S, this also lies in T \ S.622bool PresburgerRelation::isSubsetOf(const PresburgerRelation &set) const {623 return this->subtract(set).isIntegerEmpty();624}625 626/// Two sets are equal iff they are subsets of each other.627bool PresburgerRelation::isEqual(const PresburgerRelation &set) const {628 assert(space.isCompatible(set.getSpace()) && "Spaces should match");629 return this->isSubsetOf(set) && set.isSubsetOf(*this);630}631 632bool PresburgerRelation::isObviouslyEqual(const PresburgerRelation &set) const {633 if (!space.isCompatible(set.getSpace()))634 return false;635 636 if (getNumDisjuncts() != set.getNumDisjuncts())637 return false;638 639 // Compare each disjunct in this PresburgerRelation with the corresponding640 // disjunct in the other PresburgerRelation.641 for (unsigned int i = 0, n = getNumDisjuncts(); i < n; ++i) {642 if (!getDisjunct(i).isObviouslyEqual(set.getDisjunct(i)))643 return false;644 }645 return true;646}647 648/// Return true if the Presburger relation represents the universe set, false649/// otherwise. It is a simple check that only check if the relation has at least650/// one unconstrained disjunct, indicating the absence of constraints or651/// conditions.652bool PresburgerRelation::isObviouslyUniverse() const {653 for (const IntegerRelation &disjunct : getAllDisjuncts()) {654 if (disjunct.getNumConstraints() == 0)655 return true;656 }657 return false;658}659 660bool PresburgerRelation::isConvexNoLocals() const {661 return getNumDisjuncts() == 1 && getSpace().getNumLocalVars() == 0;662}663 664/// Return true if there is no disjunct, false otherwise.665bool PresburgerRelation::isObviouslyEmpty() const {666 return getNumDisjuncts() == 0;667}668 669/// Return true if all the sets in the union are known to be integer empty,670/// false otherwise.671bool PresburgerRelation::isIntegerEmpty() const {672 // The set is empty iff all of the disjuncts are empty.673 return llvm::all_of(disjuncts, std::mem_fn(&IntegerRelation::isIntegerEmpty));674}675 676bool PresburgerRelation::findIntegerSample(677 SmallVectorImpl<DynamicAPInt> &sample) {678 // A sample exists iff any of the disjuncts contains a sample.679 for (const IntegerRelation &disjunct : disjuncts) {680 if (std::optional<SmallVector<DynamicAPInt, 8>> opt =681 disjunct.findIntegerSample()) {682 sample = std::move(*opt);683 return true;684 }685 }686 return false;687}688 689std::optional<DynamicAPInt> PresburgerRelation::computeVolume() const {690 assert(getNumSymbolVars() == 0 && "Symbols are not yet supported!");691 // The sum of the volumes of the disjuncts is a valid overapproximation of the692 // volume of their union, even if they overlap.693 DynamicAPInt result(0);694 for (const IntegerRelation &disjunct : disjuncts) {695 std::optional<DynamicAPInt> volume = disjunct.computeVolume();696 if (!volume)697 return {};698 result += *volume;699 }700 return result;701}702 703/// The SetCoalescer class contains all functionality concerning the coalesce704/// heuristic. It is built from a `PresburgerRelation` and has the `coalesce()`705/// function as its main API. The coalesce heuristic simplifies the706/// representation of a PresburgerRelation. In particular, it removes all707/// disjuncts which are subsets of other disjuncts in the union and it combines708/// sets that overlap and can be combined in a convex way.709class presburger::SetCoalescer {710 711public:712 /// Simplifies the representation of a PresburgerSet.713 PresburgerRelation coalesce();714 715 /// Construct a SetCoalescer from a PresburgerSet.716 SetCoalescer(const PresburgerRelation &s);717 718private:719 /// The space of the set the SetCoalescer is coalescing.720 PresburgerSpace space;721 722 /// The current list of `IntegerRelation`s that the currently coalesced set is723 /// the union of.724 SmallVector<IntegerRelation, 2> disjuncts;725 /// The list of `Simplex`s constructed from the elements of `disjuncts`.726 SmallVector<Simplex, 2> simplices;727 728 /// The list of all inversed equalities during typing. This ensures that729 /// the constraints exist even after the typing function has concluded.730 SmallVector<SmallVector<DynamicAPInt, 2>, 2> negEqs;731 732 /// `redundantIneqsA` is the inequalities of `a` that are redundant for `b`733 /// (similarly for `cuttingIneqsA`, `redundantIneqsB`, and `cuttingIneqsB`).734 SmallVector<ArrayRef<DynamicAPInt>, 2> redundantIneqsA;735 SmallVector<ArrayRef<DynamicAPInt>, 2> cuttingIneqsA;736 737 SmallVector<ArrayRef<DynamicAPInt>, 2> redundantIneqsB;738 SmallVector<ArrayRef<DynamicAPInt>, 2> cuttingIneqsB;739 740 /// Given a Simplex `simp` and one of its inequalities `ineq`, check741 /// that the facet of `simp` where `ineq` holds as an equality is contained742 /// within `a`.743 bool isFacetContained(ArrayRef<DynamicAPInt> ineq, Simplex &simp);744 745 /// Removes redundant constraints from `disjunct`, adds it to `disjuncts` and746 /// removes the disjuncts at position `i` and `j`. Updates `simplices` to747 /// reflect the changes. `i` and `j` cannot be equal.748 void addCoalescedDisjunct(unsigned i, unsigned j,749 const IntegerRelation &disjunct);750 751 /// Checks whether `a` and `b` can be combined in a convex sense, if there752 /// exist cutting inequalities.753 ///754 /// An example of this case:755 /// ___________ ___________756 /// / / | / / /757 /// \ \ | / ==> \ /758 /// \ \ | / \ /759 /// \___\|/ \_____/760 ///761 ///762 LogicalResult coalescePairCutCase(unsigned i, unsigned j);763 764 /// Types the inequality `ineq` according to its `IneqType` for `simp` into765 /// `redundantIneqsB` and `cuttingIneqsB`. Returns success, if no separate766 /// inequalities were encountered. Otherwise, returns failure.767 LogicalResult typeInequality(ArrayRef<DynamicAPInt> ineq, Simplex &simp);768 769 /// Types the equality `eq`, i.e. for `eq` == 0, types both `eq` >= 0 and770 /// -`eq` >= 0 according to their `IneqType` for `simp` into771 /// `redundantIneqsB` and `cuttingIneqsB`. Returns success, if no separate772 /// inequalities were encountered. Otherwise, returns failure.773 LogicalResult typeEquality(ArrayRef<DynamicAPInt> eq, Simplex &simp);774 775 /// Replaces the element at position `i` with the last element and erases776 /// the last element for both `disjuncts` and `simplices`.777 void eraseDisjunct(unsigned i);778 779 /// Attempts to coalesce the two IntegerRelations at position `i` and `j`780 /// in `disjuncts` in-place. Returns whether the disjuncts were781 /// successfully coalesced. The simplices in `simplices` need to be the ones782 /// constructed from `disjuncts`. At this point, there are no empty783 /// disjuncts in `disjuncts` left.784 LogicalResult coalescePair(unsigned i, unsigned j);785};786 787/// Constructs a `SetCoalescer` from a `PresburgerRelation`. Only adds non-empty788/// `IntegerRelation`s to the `disjuncts` vector.789SetCoalescer::SetCoalescer(const PresburgerRelation &s) : space(s.getSpace()) {790 791 disjuncts = s.disjuncts;792 793 simplices.reserve(s.getNumDisjuncts());794 // Note that disjuncts.size() changes during the loop.795 for (unsigned i = 0; i < disjuncts.size();) {796 disjuncts[i].removeRedundantConstraints();797 Simplex simp(disjuncts[i]);798 if (simp.isEmpty()) {799 disjuncts[i] = disjuncts[disjuncts.size() - 1];800 disjuncts.pop_back();801 continue;802 }803 ++i;804 simplices.emplace_back(simp);805 }806}807 808/// Simplifies the representation of a PresburgerSet.809PresburgerRelation SetCoalescer::coalesce() {810 // For all tuples of IntegerRelations, check whether they can be811 // coalesced. When coalescing is successful, the contained IntegerRelation812 // is swapped with the last element of `disjuncts` and subsequently erased813 // and similarly for simplices.814 for (unsigned i = 0; i < disjuncts.size();) {815 816 // TODO: This does some comparisons two times (index 0 with 1 and index 1817 // with 0).818 bool broken = false;819 for (unsigned j = 0, e = disjuncts.size(); j < e; ++j) {820 negEqs.clear();821 redundantIneqsA.clear();822 redundantIneqsB.clear();823 cuttingIneqsA.clear();824 cuttingIneqsB.clear();825 if (i == j)826 continue;827 if (coalescePair(i, j).succeeded()) {828 broken = true;829 break;830 }831 }832 833 // Only if the inner loop was not broken, i is incremented. This is834 // required as otherwise, if a coalescing occurs, the IntegerRelation835 // now at position i is not compared.836 if (!broken)837 ++i;838 }839 840 PresburgerRelation newSet = PresburgerRelation::getEmpty(space);841 for (const IntegerRelation &disjunct : disjuncts)842 newSet.unionInPlace(disjunct);843 844 return newSet;845}846 847/// Given a Simplex `simp` and one of its inequalities `ineq`, check848/// that all inequalities of `cuttingIneqsB` are redundant for the facet of849/// `simp` where `ineq` holds as an equality is contained within `a`.850bool SetCoalescer::isFacetContained(ArrayRef<DynamicAPInt> ineq,851 Simplex &simp) {852 SimplexRollbackScopeExit scopeExit(simp);853 simp.addEquality(ineq);854 return llvm::all_of(cuttingIneqsB, [&simp](ArrayRef<DynamicAPInt> curr) {855 return simp.isRedundantInequality(curr);856 });857}858 859void SetCoalescer::addCoalescedDisjunct(unsigned i, unsigned j,860 const IntegerRelation &disjunct) {861 assert(i != j && "The indices must refer to different disjuncts");862 unsigned n = disjuncts.size();863 if (j == n - 1) {864 // This case needs special handling since position `n` - 1 is removed865 // from the vector, hence the `IntegerRelation` at position `n` - 2 is866 // lost otherwise.867 disjuncts[i] = disjuncts[n - 2];868 disjuncts.pop_back();869 disjuncts[n - 2] = disjunct;870 disjuncts[n - 2].removeRedundantConstraints();871 872 simplices[i] = simplices[n - 2];873 simplices.pop_back();874 simplices[n - 2] = Simplex(disjuncts[n - 2]);875 876 } else {877 // Other possible edge cases are correct since for `j` or `i` == `n` -878 // 2, the `IntegerRelation` at position `n` - 2 should be lost. The879 // case `i` == `n` - 1 makes the first following statement a noop.880 // Hence, in this case the same thing is done as above, but with `j`881 // rather than `i`.882 disjuncts[i] = disjuncts[n - 1];883 disjuncts[j] = disjuncts[n - 2];884 disjuncts.pop_back();885 disjuncts[n - 2] = disjunct;886 disjuncts[n - 2].removeRedundantConstraints();887 888 simplices[i] = simplices[n - 1];889 simplices[j] = simplices[n - 2];890 simplices.pop_back();891 simplices[n - 2] = Simplex(disjuncts[n - 2]);892 }893}894 895/// Given two polyhedra `a` and `b` at positions `i` and `j` in896/// `disjuncts` and `redundantIneqsA` being the inequalities of `a` that897/// are redundant for `b` (similarly for `cuttingIneqsA`, `redundantIneqsB`,898/// and `cuttingIneqsB`), Checks whether the facets of all cutting899/// inequalites of `a` are contained in `b`. If so, a new polyhedron900/// consisting of all redundant inequalites of `a` and `b` and all901/// equalities of both is created.902///903/// An example of this case:904/// ___________ ___________905/// / / | / / /906/// \ \ | / ==> \ /907/// \ \ | / \ /908/// \___\|/ \_____/909///910///911LogicalResult SetCoalescer::coalescePairCutCase(unsigned i, unsigned j) {912 /// All inequalities of `b` need to be redundant. We already know that the913 /// redundant ones are, so only the cutting ones remain to be checked.914 Simplex &simp = simplices[i];915 IntegerRelation &disjunct = disjuncts[i];916 if (llvm::any_of(cuttingIneqsA, [this, &simp](ArrayRef<DynamicAPInt> curr) {917 return !isFacetContained(curr, simp);918 }))919 return failure();920 IntegerRelation newSet(disjunct.getSpace());921 922 for (ArrayRef<DynamicAPInt> curr : redundantIneqsA)923 newSet.addInequality(curr);924 925 for (ArrayRef<DynamicAPInt> curr : redundantIneqsB)926 newSet.addInequality(curr);927 928 addCoalescedDisjunct(i, j, newSet);929 return success();930}931 932LogicalResult SetCoalescer::typeInequality(ArrayRef<DynamicAPInt> ineq,933 Simplex &simp) {934 Simplex::IneqType type = simp.findIneqType(ineq);935 if (type == Simplex::IneqType::Redundant)936 redundantIneqsB.emplace_back(ineq);937 else if (type == Simplex::IneqType::Cut)938 cuttingIneqsB.emplace_back(ineq);939 else940 return failure();941 return success();942}943 944LogicalResult SetCoalescer::typeEquality(ArrayRef<DynamicAPInt> eq,945 Simplex &simp) {946 if (typeInequality(eq, simp).failed())947 return failure();948 negEqs.emplace_back(getNegatedCoeffs(eq));949 ArrayRef<DynamicAPInt> inv(negEqs.back());950 return typeInequality(inv, simp);951}952 953void SetCoalescer::eraseDisjunct(unsigned i) {954 assert(simplices.size() == disjuncts.size() &&955 "simplices and disjuncts must be equally as long");956 disjuncts[i] = disjuncts.back();957 disjuncts.pop_back();958 simplices[i] = simplices.back();959 simplices.pop_back();960}961 962LogicalResult SetCoalescer::coalescePair(unsigned i, unsigned j) {963 964 IntegerRelation &a = disjuncts[i];965 IntegerRelation &b = disjuncts[j];966 /// Handling of local ids is not yet implemented, so these cases are967 /// skipped.968 /// TODO: implement local id support.969 if (a.getNumLocalVars() != 0 || b.getNumLocalVars() != 0)970 return failure();971 Simplex &simpA = simplices[i];972 Simplex &simpB = simplices[j];973 974 // Organize all inequalities and equalities of `a` according to their type975 // for `b` into `redundantIneqsA` and `cuttingIneqsA` (and vice versa for976 // all inequalities of `b` according to their type in `a`). If a separate977 // inequality is encountered during typing, the two IntegerRelations978 // cannot be coalesced.979 for (int k = 0, e = a.getNumInequalities(); k < e; ++k)980 if (typeInequality(a.getInequality(k), simpB).failed())981 return failure();982 983 for (int k = 0, e = a.getNumEqualities(); k < e; ++k)984 if (typeEquality(a.getEquality(k), simpB).failed())985 return failure();986 987 std::swap(redundantIneqsA, redundantIneqsB);988 std::swap(cuttingIneqsA, cuttingIneqsB);989 990 for (int k = 0, e = b.getNumInequalities(); k < e; ++k)991 if (typeInequality(b.getInequality(k), simpA).failed())992 return failure();993 994 for (int k = 0, e = b.getNumEqualities(); k < e; ++k)995 if (typeEquality(b.getEquality(k), simpA).failed())996 return failure();997 998 // If there are no cutting inequalities of `a`, `b` is contained999 // within `a`.1000 if (cuttingIneqsA.empty()) {1001 eraseDisjunct(j);1002 return success();1003 }1004 1005 // Try to apply the cut case1006 if (coalescePairCutCase(i, j).succeeded())1007 return success();1008 1009 // Swap the vectors to compare the pair (j,i) instead of (i,j).1010 std::swap(redundantIneqsA, redundantIneqsB);1011 std::swap(cuttingIneqsA, cuttingIneqsB);1012 1013 // If there are no cutting inequalities of `a`, `b` is contained1014 // within `a`.1015 if (cuttingIneqsA.empty()) {1016 eraseDisjunct(i);1017 return success();1018 }1019 1020 // Try to apply the cut case1021 return coalescePairCutCase(j, i);1022}1023 1024PresburgerRelation PresburgerRelation::coalesce() const {1025 return SetCoalescer(*this).coalesce();1026}1027 1028bool PresburgerRelation::hasOnlyDivLocals() const {1029 return llvm::all_of(disjuncts, [](const IntegerRelation &rel) {1030 return rel.hasOnlyDivLocals();1031 });1032}1033 1034PresburgerRelation PresburgerRelation::simplify() const {1035 PresburgerRelation origin = *this;1036 PresburgerRelation result = PresburgerRelation(getSpace());1037 for (IntegerRelation &disjunct : origin.disjuncts) {1038 disjunct.simplify();1039 if (!disjunct.isObviouslyEmpty())1040 result.unionInPlace(disjunct);1041 }1042 return result;1043}1044 1045bool PresburgerRelation::isFullDim() const {1046 return llvm::any_of(getAllDisjuncts(), [](IntegerRelation disjunct) {1047 return disjunct.isFullDim();1048 });1049}1050 1051void PresburgerRelation::print(raw_ostream &os) const {1052 os << "Number of Disjuncts: " << getNumDisjuncts() << "\n";1053 for (const IntegerRelation &disjunct : disjuncts) {1054 disjunct.print(os);1055 os << '\n';1056 }1057}1058 1059void PresburgerRelation::dump() const { print(llvm::errs()); }1060 1061PresburgerSet PresburgerSet::getUniverse(const PresburgerSpace &space) {1062 PresburgerSet result(space);1063 result.unionInPlace(IntegerPolyhedron::getUniverse(space));1064 return result;1065}1066 1067PresburgerSet PresburgerSet::getEmpty(const PresburgerSpace &space) {1068 return PresburgerSet(space);1069}1070 1071PresburgerSet::PresburgerSet(const IntegerPolyhedron &disjunct)1072 : PresburgerRelation(disjunct) {}1073 1074PresburgerSet::PresburgerSet(const PresburgerRelation &set)1075 : PresburgerRelation(set) {}1076 1077PresburgerSet PresburgerSet::unionSet(const PresburgerRelation &set) const {1078 return PresburgerSet(PresburgerRelation::unionSet(set));1079}1080 1081PresburgerSet PresburgerSet::intersect(const PresburgerRelation &set) const {1082 return PresburgerSet(PresburgerRelation::intersect(set));1083}1084 1085PresburgerSet PresburgerSet::complement() const {1086 return PresburgerSet(PresburgerRelation::complement());1087}1088 1089PresburgerSet PresburgerSet::subtract(const PresburgerRelation &set) const {1090 return PresburgerSet(PresburgerRelation::subtract(set));1091}1092 1093PresburgerSet PresburgerSet::coalesce() const {1094 return PresburgerSet(PresburgerRelation::coalesce());1095}1096