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
26using namespace mlir;
27using namespace presburger;
28
29PresburgerRelation::PresburgerRelation(const IntegerRelation &disjunct)
30 : space(disjunct.getSpaceWithoutLocals()) {
31 unionInPlace(disjunct);
32}
33
34void 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
41void 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
48void 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, varStart: srcPos, varLimit: srcPos + num, dstKind, pos: dstPos);
63}
64
65unsigned PresburgerRelation::getNumDisjuncts() const {
66 return disjuncts.size();
67}
68
69ArrayRef<IntegerRelation> PresburgerRelation::getAllDisjuncts() const {
70 return disjuncts;
71}
72
73const 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.
80void PresburgerRelation::unionInPlace(const IntegerRelation &disjunct) {
81 assert(space.isCompatible(disjunct.getSpace()) && "Spaces should match");
82 disjuncts.emplace_back(Args: 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.
89void 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.
114PresburgerRelation
115PresburgerRelation::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.
123bool PresburgerRelation::containsPoint(ArrayRef<DynamicAPInt> point) const {
124 return llvm::any_of(Range: disjuncts, P: [&point](const IntegerRelation &disjunct) {
125 return disjunct.containsPointNoLocal(point);
126 });
127}
128
129PresburgerRelation
130PresburgerRelation::getUniverse(const PresburgerSpace &space) {
131 PresburgerRelation result(space);
132 result.unionInPlace(disjunct: IntegerRelation::getUniverse(space));
133 return result;
134}
135
136PresburgerRelation 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.
147PresburgerRelation
148PresburgerRelation::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(other: csB);
163 if (!intersection.isEmpty())
164 result.unionInPlace(disjunct: intersection);
165 }
166 }
167 return result;
168}
169
170PresburgerRelation
171PresburgerRelation::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(kind: VarKind::Domain, pos: 0, num: getNumDomainVars());
177 return intersect(set: other);
178}
179
180PresburgerRelation
181PresburgerRelation::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(kind: VarKind::Domain, pos: 0, num: getNumRangeVars());
187 other.inverse();
188 return intersect(set: other);
189}
190
191PresburgerSet PresburgerRelation::getDomainSet() const {
192 PresburgerSet result = PresburgerSet::getEmpty(space: space.getDomainSpace());
193 for (const IntegerRelation &cs : disjuncts)
194 result.unionInPlace(disjunct: cs.getDomainSet());
195 return result;
196}
197
198PresburgerSet PresburgerRelation::getRangeSet() const {
199 PresburgerSet result = PresburgerSet::getEmpty(space: space.getRangeSpace());
200 for (const IntegerRelation &cs : disjuncts)
201 result.unionInPlace(disjunct: cs.getRangeSet());
202 return result;
203}
204
205void PresburgerRelation::inverse() {
206 for (IntegerRelation &cs : disjuncts)
207 cs.inverse();
208
209 if (getNumDisjuncts())
210 setSpace(getDisjunct(index: 0).getSpaceWithoutLocals());
211}
212
213void 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(space: PresburgerSpace::getRelationSpace(
220 numDomain: getNumDomainVars(), numRange: rel.getNumRangeVars(), numSymbols: getNumSymbolVars()));
221 for (const IntegerRelation &csA : disjuncts) {
222 for (const IntegerRelation &csB : rel.disjuncts) {
223 IntegerRelation composition = csA;
224 composition.compose(rel: csB);
225 if (!composition.isEmpty())
226 result.unionInPlace(disjunct: composition);
227 }
228 }
229 *this = result;
230}
231
232void 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
242void PresburgerRelation::applyRange(const PresburgerRelation &rel) {
243 compose(rel);
244}
245
246static 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(func: s.lexopt);
256 } else {
257 s = cs.findSymbolicIntegerLexMax();
258 lexopt = lexopt.unionLexMax(func: s.lexopt);
259 }
260 unboundedDomain = unboundedDomain.intersect(set: s.unboundedDomain);
261 }
262 return result;
263}
264
265SymbolicLexOpt PresburgerRelation::findSymbolicIntegerLexMin() const {
266 return findSymbolicIntegerLexOpt(rel: *this, isMin: true);
267}
268
269SymbolicLexOpt PresburgerRelation::findSymbolicIntegerLexMax() const {
270 return findSymbolicIntegerLexOpt(rel: *this, isMin: 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.
287static SmallVector<DynamicAPInt, 8>
288getIneqCoeffsFromIdx(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>(Range: rel.getInequality(idx));
293
294 idx -= rel.getNumInequalities();
295 ArrayRef<DynamicAPInt> eqCoeffs = rel.getEquality(idx: idx / 2);
296
297 if (idx % 2 == 0)
298 return llvm::to_vector<8>(Range&: eqCoeffs);
299 return getNegatedCoeffs(coeffs: eqCoeffs);
300}
301
302PresburgerRelation 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(set: 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///
345static 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(space: b.getSpaceWithoutLocals());
350
351 if (!s.hasOnlyDivLocals())
352 return getSetDifference(b, s: 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(space: 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(disjunct: 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(index: 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(other&: 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: &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(inEq: sI.getInequality(idx: lb));
448 b.addInequality(inEq: sI.getInequality(idx: 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 inEq: getDivLowerBound(dividend: divs.getDividend(i), divisor: divs.getDenom(i),
475 localVarIdx: sI.getVarKindOffset(kind: VarKind::Local) + i));
476 b.addInequality(
477 inEq: getDivUpperBound(dividend: divs.getDividend(i), divisor: divs.getDenom(i),
478 localVarIdx: sI.getVarKindOffset(kind: VarKind::Local) + i));
479 }
480 }
481
482 unsigned offset = simplex.getNumConstraints();
483 unsigned numLocalsAdded =
484 b.getNumLocalVars() - initBCounts.getSpace().getNumLocalVars();
485 simplex.appendVariable(count: numLocalsAdded);
486
487 unsigned snapshotBeforeIntersect = simplex.getSnapshot();
488 simplex.intersectIntegerRelation(rel: 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(counts: initBCounts);
495 simplex.rollback(snapshot: 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(Args: 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, count: totalNewSimplexInequalities);
523 for (unsigned j = 0; j < totalNewSimplexInequalities; j++)
524 canIgnoreIneq[j] = simplex.isMarkedRedundant(constraintIndex: offset + j);
525 simplex.rollback(snapshot: snapshotBeforeIntersect);
526
527 SmallVector<unsigned, 8> ineqsToProcess;
528 ineqsToProcess.reserve(N: totalNewSimplexInequalities);
529 for (unsigned i = 0; i < totalNewSimplexInequalities; ++i)
530 if (!canIgnoreIneq[i])
531 ineqsToProcess.emplace_back(Args&: 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(Args: 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(snapshot: frame.simplexSnapshot);
560 b.truncate(counts: frame.bCounts);
561 SmallVector<DynamicAPInt, 8> ineq =
562 getIneqCoeffsFromIdx(rel: frame.sI, idx: *frame.lastIneqProcessed);
563 b.addInequality(inEq: ineq);
564 simplex.addInequality(coeffs: 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(ineq: getIneqCoeffsFromIdx(rel: frame.sI, idx));
581 b.addInequality(inEq: ineq);
582 simplex.addInequality(coeffs: 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.
598PresburgerRelation PresburgerRelation::complement() const {
599 return getSetDifference(b: IntegerRelation::getUniverse(space: getSpace()), s: *this);
600}
601
602/// Return the result of subtract the given set from this set, i.e.,
603/// return `this \ set`.
604PresburgerRelation
605PresburgerRelation::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(set: getSetDifference(b: disjunct, s: 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.
623bool 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.
628bool PresburgerRelation::isEqual(const PresburgerRelation &set) const {
629 assert(space.isCompatible(set.getSpace()) && "Spaces should match");
630 return this->isSubsetOf(set) && set.isSubsetOf(set: *this);
631}
632
633bool PresburgerRelation::isObviouslyEqual(const PresburgerRelation &set) const {
634 if (!space.isCompatible(other: 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(index: i).isObviouslyEqual(other: set.getDisjunct(index: 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.
653bool PresburgerRelation::isObviouslyUniverse() const {
654 for (const IntegerRelation &disjunct : getAllDisjuncts()) {
655 if (disjunct.getNumConstraints() == 0)
656 return true;
657 }
658 return false;
659}
660
661bool PresburgerRelation::isConvexNoLocals() const {
662 return getNumDisjuncts() == 1 && getSpace().getNumLocalVars() == 0;
663}
664
665/// Return true if there is no disjunct, false otherwise.
666bool 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.
672bool PresburgerRelation::isIntegerEmpty() const {
673 // The set is empty iff all of the disjuncts are empty.
674 return llvm::all_of(Range: disjuncts, P: std::mem_fn(pm: &IntegerRelation::isIntegerEmpty));
675}
676
677bool 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
690std::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.
710class presburger::SetCoalescer {
711
712public:
713 /// Simplifies the representation of a PresburgerSet.
714 PresburgerRelation coalesce();
715
716 /// Construct a SetCoalescer from a PresburgerSet.
717 SetCoalescer(const PresburgerRelation &s);
718
719private:
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.
790SetCoalescer::SetCoalescer(const PresburgerRelation &s) : space(s.getSpace()) {
791
792 disjuncts = s.disjuncts;
793
794 simplices.reserve(N: 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(Args&: simp);
806 }
807}
808
809/// Simplifies the representation of a PresburgerSet.
810PresburgerRelation 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`.
851bool SetCoalescer::isFacetContained(ArrayRef<DynamicAPInt> ineq,
852 Simplex &simp) {
853 SimplexRollbackScopeExit scopeExit(simp);
854 simp.addEquality(coeffs: ineq);
855 return llvm::all_of(Range&: cuttingIneqsB, P: [&simp](ArrayRef<DynamicAPInt> curr) {
856 return simp.isRedundantInequality(coeffs: curr);
857 });
858}
859
860void 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///
912LogicalResult 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(Range&: cuttingIneqsA, P: [this, &simp](ArrayRef<DynamicAPInt> curr) {
918 return !isFacetContained(ineq: curr, simp);
919 }))
920 return failure();
921 IntegerRelation newSet(disjunct.getSpace());
922
923 for (ArrayRef<DynamicAPInt> curr : redundantIneqsA)
924 newSet.addInequality(inEq: curr);
925
926 for (ArrayRef<DynamicAPInt> curr : redundantIneqsB)
927 newSet.addInequality(inEq: curr);
928
929 addCoalescedDisjunct(i, j, disjunct: newSet);
930 return success();
931}
932
933LogicalResult SetCoalescer::typeInequality(ArrayRef<DynamicAPInt> ineq,
934 Simplex &simp) {
935 Simplex::IneqType type = simp.findIneqType(coeffs: ineq);
936 if (type == Simplex::IneqType::Redundant)
937 redundantIneqsB.emplace_back(Args&: ineq);
938 else if (type == Simplex::IneqType::Cut)
939 cuttingIneqsB.emplace_back(Args&: ineq);
940 else
941 return failure();
942 return success();
943}
944
945LogicalResult SetCoalescer::typeEquality(ArrayRef<DynamicAPInt> eq,
946 Simplex &simp) {
947 if (typeInequality(ineq: eq, simp).failed())
948 return failure();
949 negEqs.emplace_back(Args: getNegatedCoeffs(coeffs: eq));
950 ArrayRef<DynamicAPInt> inv(negEqs.back());
951 return typeInequality(ineq: inv, simp);
952}
953
954void 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
963LogicalResult 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(ineq: a.getInequality(idx: k), simp&: simpB).failed())
982 return failure();
983
984 for (int k = 0, e = a.getNumEqualities(); k < e; ++k)
985 if (typeEquality(eq: a.getEquality(idx: k), simp&: simpB).failed())
986 return failure();
987
988 std::swap(LHS&: redundantIneqsA, RHS&: redundantIneqsB);
989 std::swap(LHS&: cuttingIneqsA, RHS&: cuttingIneqsB);
990
991 for (int k = 0, e = b.getNumInequalities(); k < e; ++k)
992 if (typeInequality(ineq: b.getInequality(idx: k), simp&: simpA).failed())
993 return failure();
994
995 for (int k = 0, e = b.getNumEqualities(); k < e; ++k)
996 if (typeEquality(eq: b.getEquality(idx: k), simp&: 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(i: 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(LHS&: redundantIneqsA, RHS&: redundantIneqsB);
1012 std::swap(LHS&: cuttingIneqsA, RHS&: 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(i: j, j: i);
1023}
1024
1025PresburgerRelation PresburgerRelation::coalesce() const {
1026 return SetCoalescer(*this).coalesce();
1027}
1028
1029bool PresburgerRelation::hasOnlyDivLocals() const {
1030 return llvm::all_of(Range: disjuncts, P: [](const IntegerRelation &rel) {
1031 return rel.hasOnlyDivLocals();
1032 });
1033}
1034
1035PresburgerRelation 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
1046bool PresburgerRelation::isFullDim() const {
1047 return llvm::any_of(Range: getAllDisjuncts(), P: [](IntegerRelation disjunct) {
1048 return disjunct.isFullDim();
1049 });
1050}
1051
1052void 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
1060void PresburgerRelation::dump() const { print(os&: llvm::errs()); }
1061
1062PresburgerSet PresburgerSet::getUniverse(const PresburgerSpace &space) {
1063 PresburgerSet result(space);
1064 result.unionInPlace(disjunct: IntegerPolyhedron::getUniverse(space));
1065 return result;
1066}
1067
1068PresburgerSet PresburgerSet::getEmpty(const PresburgerSpace &space) {
1069 return PresburgerSet(space);
1070}
1071
1072PresburgerSet::PresburgerSet(const IntegerPolyhedron &disjunct)
1073 : PresburgerRelation(disjunct) {}
1074
1075PresburgerSet::PresburgerSet(const PresburgerRelation &set)
1076 : PresburgerRelation(set) {}
1077
1078PresburgerSet PresburgerSet::unionSet(const PresburgerRelation &set) const {
1079 return PresburgerSet(PresburgerRelation::unionSet(set));
1080}
1081
1082PresburgerSet PresburgerSet::intersect(const PresburgerRelation &set) const {
1083 return PresburgerSet(PresburgerRelation::intersect(set));
1084}
1085
1086PresburgerSet PresburgerSet::complement() const {
1087 return PresburgerSet(PresburgerRelation::complement());
1088}
1089
1090PresburgerSet PresburgerSet::subtract(const PresburgerRelation &set) const {
1091 return PresburgerSet(PresburgerRelation::subtract(set));
1092}
1093
1094PresburgerSet PresburgerSet::coalesce() const {
1095 return PresburgerSet(PresburgerRelation::coalesce());
1096}
1097

source code of mlir/lib/Analysis/Presburger/PresburgerRelation.cpp