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, varStart: srcPos, varLimit: srcPos + num, dstKind, pos: 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(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. |
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(Range: disjuncts, P: [&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(disjunct: 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(other: csB); |
163 | if (!intersection.isEmpty()) |
164 | result.unionInPlace(disjunct: 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(kind: VarKind::Domain, pos: 0, num: getNumDomainVars()); |
177 | return intersect(set: 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(kind: VarKind::Domain, pos: 0, num: getNumRangeVars()); |
187 | other.inverse(); |
188 | return intersect(set: other); |
189 | } |
190 | |
191 | PresburgerSet 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 | |
198 | PresburgerSet 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 | |
205 | void PresburgerRelation::inverse() { |
206 | for (IntegerRelation &cs : disjuncts) |
207 | cs.inverse(); |
208 | |
209 | if (getNumDisjuncts()) |
210 | setSpace(getDisjunct(index: 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(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 | |
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(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 | |
265 | SymbolicLexOpt PresburgerRelation::findSymbolicIntegerLexMin() const { |
266 | return findSymbolicIntegerLexOpt(rel: *this, isMin: true); |
267 | } |
268 | |
269 | SymbolicLexOpt 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. |
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>(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 | |
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(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 | /// |
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(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. |
598 | PresburgerRelation 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`. |
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(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. |
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(set: *this); |
631 | } |
632 | |
633 | bool 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. |
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(Range: disjuncts, P: std::mem_fn(pm: &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(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. |
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(coeffs: ineq); |
855 | return llvm::all_of(Range&: cuttingIneqsB, P: [&simp](ArrayRef<DynamicAPInt> curr) { |
856 | return simp.isRedundantInequality(coeffs: 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(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 | |
933 | LogicalResult 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 | |
945 | LogicalResult 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 | |
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(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 | |
1025 | PresburgerRelation PresburgerRelation::coalesce() const { |
1026 | return SetCoalescer(*this).coalesce(); |
1027 | } |
1028 | |
1029 | bool PresburgerRelation::hasOnlyDivLocals() const { |
1030 | return llvm::all_of(Range: disjuncts, P: [](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(Range: getAllDisjuncts(), P: [](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(os&: llvm::errs()); } |
1061 | |
1062 | PresburgerSet PresburgerSet::getUniverse(const PresburgerSpace &space) { |
1063 | PresburgerSet result(space); |
1064 | result.unionInPlace(disjunct: 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 |
Definitions
- PresburgerRelation
- setSpace
- insertVarInPlace
- convertVarKind
- getNumDisjuncts
- getAllDisjuncts
- getDisjunct
- unionInPlace
- unionInPlace
- unionSet
- containsPoint
- getUniverse
- getEmpty
- intersect
- intersectRange
- intersectDomain
- getDomainSet
- getRangeSet
- inverse
- compose
- applyDomain
- applyRange
- findSymbolicIntegerLexOpt
- findSymbolicIntegerLexMin
- findSymbolicIntegerLexMax
- getIneqCoeffsFromIdx
- computeReprWithOnlyDivLocals
- getSetDifference
- complement
- subtract
- isSubsetOf
- isEqual
- isObviouslyEqual
- isObviouslyUniverse
- isConvexNoLocals
- isObviouslyEmpty
- isIntegerEmpty
- findIntegerSample
- computeVolume
- SetCoalescer
- SetCoalescer
- coalesce
- isFacetContained
- addCoalescedDisjunct
- coalescePairCutCase
- typeInequality
- typeEquality
- eraseDisjunct
- coalescePair
- coalesce
- hasOnlyDivLocals
- simplify
- isFullDim
- dump
- getUniverse
- getEmpty
- PresburgerSet
- PresburgerSet
- unionSet
- intersect
- complement
- subtract
Update your C++ knowledge – Modern C++11/14/17 Training
Find out more