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