MLIR  17.0.0git
PresburgerRelation.cpp
Go to the documentation of this file.
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 
12 #include "llvm/ADT/STLExtras.h"
13 #include "llvm/ADT/ScopeExit.h"
14 #include "llvm/ADT/SmallBitVector.h"
15 #include <optional>
16 
17 using namespace mlir;
18 using namespace presburger;
19 
21  : space(disjunct.getSpaceWithoutLocals()) {
22  unionInPlace(disjunct);
23 }
24 
26  assert(space.getNumLocalVars() == 0 && "no locals should be present");
27  space = oSpace;
28  for (IntegerRelation &disjunct : disjuncts)
29  disjunct.setSpaceExceptLocals(space);
30 }
31 
33  return disjuncts.size();
34 }
35 
37  return disjuncts;
38 }
39 
40 const IntegerRelation &PresburgerRelation::getDisjunct(unsigned index) const {
41  assert(index < disjuncts.size() && "index out of bounds!");
42  return disjuncts[index];
43 }
44 
45 /// Mutate this set, turning it into the union of this set and the given
46 /// IntegerRelation.
48  assert(space.isCompatible(disjunct.getSpace()) && "Spaces should match");
49  disjuncts.push_back(disjunct);
50 }
51 
52 /// Mutate this set, turning it into the union of this set and the given set.
53 ///
54 /// This is accomplished by simply adding all the disjuncts of the given set
55 /// to this set.
57  assert(space.isCompatible(set.getSpace()) && "Spaces should match");
58  for (const IntegerRelation &disjunct : set.disjuncts)
59  unionInPlace(disjunct);
60 }
61 
62 /// Return the union of this set and the given set.
65  assert(space.isCompatible(set.getSpace()) && "Spaces should match");
66  PresburgerRelation result = *this;
67  result.unionInPlace(set);
68  return result;
69 }
70 
71 /// A point is contained in the union iff any of the parts contain the point.
73  return llvm::any_of(disjuncts, [&](const IntegerRelation &disjunct) {
74  return (disjunct.containsPointNoLocal(point));
75  });
76 }
77 
80  PresburgerRelation result(space);
82  return result;
83 }
84 
86  return PresburgerRelation(space);
87 }
88 
89 // Return the intersection of this set with the given set.
90 //
91 // We directly compute (S_1 or S_2 ...) and (T_1 or T_2 ...)
92 // as (S_1 and T_1) or (S_1 and T_2) or ...
93 //
94 // If S_i or T_j have local variables, then S_i and T_j contains the local
95 // variables of both.
98  assert(space.isCompatible(set.getSpace()) && "Spaces should match");
99 
100  PresburgerRelation result(getSpace());
101  for (const IntegerRelation &csA : disjuncts) {
102  for (const IntegerRelation &csB : set.disjuncts) {
103  IntegerRelation intersection = csA.intersect(csB);
104  if (!intersection.isEmpty())
105  result.unionInPlace(intersection);
106  }
107  }
108  return result;
109 }
110 
111 /// Return the coefficients of the ineq in `rel` specified by `idx`.
112 /// `idx` can refer not only to an actual inequality of `rel`, but also
113 /// to either of the inequalities that make up an equality in `rel`.
114 ///
115 /// When 0 <= idx < rel.getNumInequalities(), this returns the coeffs of the
116 /// idx-th inequality of `rel`.
117 ///
118 /// Otherwise, it is then considered to index into the ineqs corresponding to
119 /// eqs of `rel`, and it must hold that
120 ///
121 /// 0 <= idx - rel.getNumInequalities() < 2*getNumEqualities().
122 ///
123 /// For every eq `coeffs == 0` there are two possible ineqs to index into.
124 /// The first is coeffs >= 0 and the second is coeffs <= 0.
126  unsigned idx) {
127  assert(idx < rel.getNumInequalities() + 2 * rel.getNumEqualities() &&
128  "idx out of bounds!");
129  if (idx < rel.getNumInequalities())
130  return llvm::to_vector<8>(rel.getInequality(idx));
131 
132  idx -= rel.getNumInequalities();
133  ArrayRef<MPInt> eqCoeffs = rel.getEquality(idx / 2);
134 
135  if (idx % 2 == 0)
136  return llvm::to_vector<8>(eqCoeffs);
137  return getNegatedCoeffs(eqCoeffs);
138 }
139 
141  if (hasOnlyDivLocals())
142  return *this;
143 
144  // The result is just the union of the reprs of the disjuncts.
145  PresburgerRelation result(getSpace());
146  for (const IntegerRelation &disjunct : disjuncts)
147  result.unionInPlace(disjunct.computeReprWithOnlyDivLocals());
148  return result;
149 }
150 
151 /// Return the set difference b \ s.
152 ///
153 /// In the following, U denotes union, /\ denotes intersection, \ denotes set
154 /// difference and ~ denotes complement.
155 ///
156 /// Let s = (U_i s_i). We want b \ (U_i s_i).
157 ///
158 /// Let s_i = /\_j s_ij, where each s_ij is a single inequality. To compute
159 /// b \ s_i = b /\ ~s_i, we partition s_i based on the first violated
160 /// inequality: ~s_i = (~s_i1) U (s_i1 /\ ~s_i2) U (s_i1 /\ s_i2 /\ ~s_i3) U ...
161 /// And the required result is (b /\ ~s_i1) U (b /\ s_i1 /\ ~s_i2) U ...
162 /// We recurse by subtracting U_{j > i} S_j from each of these parts and
163 /// returning the union of the results. Each equality is handled as a
164 /// conjunction of two inequalities.
165 ///
166 /// Note that the same approach works even if an inequality involves a floor
167 /// division. For example, the complement of x <= 7*floor(x/7) is still
168 /// x > 7*floor(x/7). Since b \ s_i contains the inequalities of both b and s_i
169 /// (or the complements of those inequalities), b \ s_i may contain the
170 /// divisions present in both b and s_i. Therefore, we need to add the local
171 /// division variables of both b and s_i to each part in the result. This means
172 /// adding the local variables of both b and s_i, as well as the corresponding
173 /// division inequalities to each part. Since the division inequalities are
174 /// added to each part, we can skip the parts where the complement of any
175 /// division inequality is added, as these parts will become empty anyway.
176 ///
177 /// As a heuristic, we try adding all the constraints and check if simplex
178 /// says that the intersection is empty. If it is, then subtracting this
179 /// disjuncts is a no-op and we just skip it. Also, in the process we find out
180 /// that some constraints are redundant. These redundant constraints are
181 /// ignored.
182 ///
184  const PresburgerRelation &s) {
185  assert(b.getSpace().isCompatible(s.getSpace()) && "Spaces should match");
186  if (b.isEmptyByGCDTest())
188 
189  if (!s.hasOnlyDivLocals())
191 
192  // Remove duplicate divs up front here to avoid existing
193  // divs disappearing in the call to mergeLocalVars below.
195 
196  PresburgerRelation result =
198  Simplex simplex(b);
199 
200  // This algorithm is more naturally expressed recursively, but we implement
201  // it iteratively here to avoid issues with stack sizes.
202  //
203  // Each level of the recursion has five stack variables.
204  struct Frame {
205  // A snapshot of the simplex state to rollback to.
206  unsigned simplexSnapshot;
207  // A CountsSnapshot of `b` to rollback to.
209  // The IntegerRelation currently being operated on.
210  IntegerRelation sI;
211  // A list of indexes (see getIneqCoeffsFromIdx) of inequalities to be
212  // processed.
213  SmallVector<unsigned, 8> ineqsToProcess;
214  // The index of the last inequality that was processed at this level.
215  // This is empty when we are coming to this level for the first time.
216  std::optional<unsigned> lastIneqProcessed;
217  };
218  SmallVector<Frame, 2> frames;
219 
220  // When we "recurse", we ensure the current frame is stored in `frames` and
221  // increment `level`. When we return, we decrement `level`.
222  unsigned level = 1;
223  while (level > 0) {
224  if (level - 1 >= s.getNumDisjuncts()) {
225  // No more parts to subtract; add to the result and return.
226  result.unionInPlace(b);
227  level = frames.size();
228  continue;
229  }
230 
231  if (level > frames.size()) {
232  // No frame for this level yet, so we have just recursed into this level.
233  IntegerRelation sI = s.getDisjunct(level - 1);
234  // Remove the duplicate divs up front to avoid them possibly disappearing
235  // in the call to mergeLocalVars below.
236  sI.removeDuplicateDivs();
237 
238  // Below, we append some additional constraints and ids to b. We want to
239  // rollback b to its initial state before returning, which we will do by
240  // removing all constraints beyond the original number of inequalities
241  // and equalities, so we store these counts first.
242  IntegerRelation::CountsSnapshot initBCounts = b.getCounts();
243  // Similarly, we also want to rollback simplex to its original state.
244  unsigned initialSnapshot = simplex.getSnapshot();
245 
246  // Add sI's locals to b, after b's locals. Only those locals of sI which
247  // do not already exist in b will be added. (i.e., duplicate divisions
248  // will not be added.) Also add b's locals to sI, in such a way that both
249  // have the same locals in the same order in the end.
250  b.mergeLocalVars(sI);
251 
252  // Find out which inequalities of sI correspond to division inequalities
253  // for the local variables of sI.
254  //
255  // Careful! This has to be done after the merge above; otherwise, the
256  // dividends won't contain the new ids inserted during the merge.
257  std::vector<MaybeLocalRepr> repr(sI.getNumLocalVars());
258  DivisionRepr divs = sI.getLocalReprs(&repr);
259 
260  // Mark which inequalities of sI are division inequalities and add all
261  // such inequalities to b.
262  llvm::SmallBitVector canIgnoreIneq(sI.getNumInequalities() +
263  2 * sI.getNumEqualities());
264  for (unsigned i = initBCounts.getSpace().getNumLocalVars(),
265  e = sI.getNumLocalVars();
266  i < e; ++i) {
267  assert(
268  repr[i] &&
269  "Subtraction is not supported when a representation of the local "
270  "variables of the subtrahend cannot be found!");
271 
272  if (repr[i].kind == ReprKind::Inequality) {
273  unsigned lb = repr[i].repr.inequalityPair.lowerBoundIdx;
274  unsigned ub = repr[i].repr.inequalityPair.upperBoundIdx;
275 
276  b.addInequality(sI.getInequality(lb));
277  b.addInequality(sI.getInequality(ub));
278 
279  assert(lb != ub &&
280  "Upper and lower bounds must be different inequalities!");
281  canIgnoreIneq[lb] = true;
282  canIgnoreIneq[ub] = true;
283  } else {
284  assert(repr[i].kind == ReprKind::Equality &&
285  "ReprKind isn't inequality so should be equality");
286 
287  // Consider the case (x) : (x = 3e + 1), where e is a local.
288  // Its complement is (x) : (x = 3e) or (x = 3e + 2).
289  //
290  // This can be computed by considering the set to be
291  // (x) : (x = 3*(x floordiv 3) + 1).
292  //
293  // Now there are no equalities defining divisions; the division is
294  // defined by the standard division equalities for e = x floordiv 3,
295  // i.e., 0 <= x - 3*e <= 2.
296  // So now as before, we add these division inequalities to b. The
297  // equality is now just an ordinary constraint that must be considered
298  // in the remainder of the algorithm. The division inequalities must
299  // need not be considered, same as above, and they automatically will
300  // not be because they were never a part of sI; we just infer them
301  // from the equality and add them only to b.
302  b.addInequality(
303  getDivLowerBound(divs.getDividend(i), divs.getDenom(i),
305  b.addInequality(
306  getDivUpperBound(divs.getDividend(i), divs.getDenom(i),
308  }
309  }
310 
311  unsigned offset = simplex.getNumConstraints();
312  unsigned numLocalsAdded =
313  b.getNumLocalVars() - initBCounts.getSpace().getNumLocalVars();
314  simplex.appendVariable(numLocalsAdded);
315 
316  unsigned snapshotBeforeIntersect = simplex.getSnapshot();
317  simplex.intersectIntegerRelation(sI);
318 
319  if (simplex.isEmpty()) {
320  // b /\ s_i is empty, so b \ s_i = b. We move directly to i + 1.
321  // We are ignoring level i completely, so we restore the state
322  // *before* going to the next level.
323  b.truncate(initBCounts);
324  simplex.rollback(initialSnapshot);
325  // Recurse. We haven't processed any inequalities and
326  // we don't need to process anything when we return.
327  //
328  // TODO: consider supporting tail recursion directly if this becomes
329  // relevant for performance.
330  frames.push_back(Frame{initialSnapshot, initBCounts, sI,
331  /*ineqsToProcess=*/{},
332  /*lastIneqProcessed=*/{}});
333  ++level;
334  continue;
335  }
336 
337  // Equalities are added to simplex as a pair of inequalities.
338  unsigned totalNewSimplexInequalities =
339  2 * sI.getNumEqualities() + sI.getNumInequalities();
340  // Look for redundant constraints among the constraints of sI. We don't
341  // care about redundant constraints in `b` at this point.
342  //
343  // When there are two copies of a constraint in `simplex`, i.e., among the
344  // constraints of `b` and `sI`, only one of them can be marked redundant.
345  // (Assuming no other constraint makes these redundant.)
346  //
347  // In a case where there is one copy in `b` and one in `sI`, we want the
348  // one in `sI` to be marked, not the one in `b`. Therefore, it's not
349  // enough to ignore the constraints of `b` when checking which
350  // constraints `detectRedundant` has marked redundant; we explicitly tell
351  // `detectRedundant` to only mark constraints from `sI` as being
352  // redundant.
353  simplex.detectRedundant(offset, totalNewSimplexInequalities);
354  for (unsigned j = 0; j < totalNewSimplexInequalities; j++)
355  canIgnoreIneq[j] = simplex.isMarkedRedundant(offset + j);
356  simplex.rollback(snapshotBeforeIntersect);
357 
358  SmallVector<unsigned, 8> ineqsToProcess;
359  ineqsToProcess.reserve(totalNewSimplexInequalities);
360  for (unsigned i = 0; i < totalNewSimplexInequalities; ++i)
361  if (!canIgnoreIneq[i])
362  ineqsToProcess.push_back(i);
363 
364  if (ineqsToProcess.empty()) {
365  // Nothing to process; return. (we have no frame to pop.)
366  level = frames.size();
367  continue;
368  }
369 
370  unsigned simplexSnapshot = simplex.getSnapshot();
372  frames.push_back(Frame{simplexSnapshot, bCounts, sI, ineqsToProcess,
373  /*lastIneqProcessed=*/std::nullopt});
374  // We have completed the initial setup for this level.
375  // Fallthrough to the main recursive part below.
376  }
377 
378  // For each inequality ineq, we first recurse with the part where ineq
379  // is not satisfied, and then add ineq to b and simplex because
380  // ineq must be satisfied by all later parts.
381  if (level == frames.size()) {
382  Frame &frame = frames.back();
383  if (frame.lastIneqProcessed) {
384  // Let the current value of b be b' and
385  // let the initial value of b when we first came to this level be b.
386  //
387  // b' is equal to b /\ s_i1 /\ s_i2 /\ ... /\ s_i{j-1} /\ ~s_ij.
388  // We had previously recursed with the part where s_ij was not
389  // satisfied; all further parts satisfy s_ij, so we rollback to the
390  // state before adding this complement constraint, and add s_ij to b.
391  simplex.rollback(frame.simplexSnapshot);
392  b.truncate(frame.bCounts);
393  SmallVector<MPInt, 8> ineq =
394  getIneqCoeffsFromIdx(frame.sI, *frame.lastIneqProcessed);
395  b.addInequality(ineq);
396  simplex.addInequality(ineq);
397  }
398 
399  if (frame.ineqsToProcess.empty()) {
400  // No ineqs left to process; pop this level's frame and return.
401  frames.pop_back();
402  level = frames.size();
403  continue;
404  }
405 
406  // "Recurse" with the part where the ineq is not satisfied.
407  frame.bCounts = b.getCounts();
408  frame.simplexSnapshot = simplex.getSnapshot();
409 
410  unsigned idx = frame.ineqsToProcess.back();
411  SmallVector<MPInt, 8> ineq =
412  getComplementIneq(getIneqCoeffsFromIdx(frame.sI, idx));
413  b.addInequality(ineq);
414  simplex.addInequality(ineq);
415 
416  frame.ineqsToProcess.pop_back();
417  frame.lastIneqProcessed = idx;
418  ++level;
419  continue;
420  }
421  }
422 
423  return result;
424 }
425 
426 /// Return the complement of this set.
429 }
430 
431 /// Return the result of subtract the given set from this set, i.e.,
432 /// return `this \ set`.
435  assert(space.isCompatible(set.getSpace()) && "Spaces should match");
436  PresburgerRelation result(getSpace());
437  // We compute (U_i t_i) \ (U_i set_i) as U_i (t_i \ V_i set_i).
438  for (const IntegerRelation &disjunct : disjuncts)
439  result.unionInPlace(getSetDifference(disjunct, set));
440  return result;
441 }
442 
443 /// T is a subset of S iff T \ S is empty, since if T \ S contains a
444 /// point then this is a point that is contained in T but not S, and
445 /// if T contains a point that is not in S, this also lies in T \ S.
447  return this->subtract(set).isIntegerEmpty();
448 }
449 
450 /// Two sets are equal iff they are subsets of each other.
452  assert(space.isCompatible(set.getSpace()) && "Spaces should match");
453  return this->isSubsetOf(set) && set.isSubsetOf(*this);
454 }
455 
456 /// Return true if all the sets in the union are known to be integer empty,
457 /// false otherwise.
459  // The set is empty iff all of the disjuncts are empty.
460  return llvm::all_of(disjuncts, std::mem_fn(&IntegerRelation::isIntegerEmpty));
461 }
462 
464  // A sample exists iff any of the disjuncts contains a sample.
465  for (const IntegerRelation &disjunct : disjuncts) {
466  if (std::optional<SmallVector<MPInt, 8>> opt =
467  disjunct.findIntegerSample()) {
468  sample = std::move(*opt);
469  return true;
470  }
471  }
472  return false;
473 }
474 
475 std::optional<MPInt> PresburgerRelation::computeVolume() const {
476  assert(getNumSymbolVars() == 0 && "Symbols are not yet supported!");
477  // The sum of the volumes of the disjuncts is a valid overapproximation of the
478  // volume of their union, even if they overlap.
479  MPInt result(0);
480  for (const IntegerRelation &disjunct : disjuncts) {
481  std::optional<MPInt> volume = disjunct.computeVolume();
482  if (!volume)
483  return {};
484  result += *volume;
485  }
486  return result;
487 }
488 
489 /// The SetCoalescer class contains all functionality concerning the coalesce
490 /// heuristic. It is built from a `PresburgerRelation` and has the `coalesce()`
491 /// function as its main API. The coalesce heuristic simplifies the
492 /// representation of a PresburgerRelation. In particular, it removes all
493 /// disjuncts which are subsets of other disjuncts in the union and it combines
494 /// sets that overlap and can be combined in a convex way.
496 
497 public:
498  /// Simplifies the representation of a PresburgerSet.
499  PresburgerRelation coalesce();
500 
501  /// Construct a SetCoalescer from a PresburgerSet.
503 
504 private:
505  /// The space of the set the SetCoalescer is coalescing.
506  PresburgerSpace space;
507 
508  /// The current list of `IntegerRelation`s that the currently coalesced set is
509  /// the union of.
511  /// The list of `Simplex`s constructed from the elements of `disjuncts`.
512  SmallVector<Simplex, 2> simplices;
513 
514  /// The list of all inversed equalities during typing. This ensures that
515  /// the constraints exist even after the typing function has concluded.
517 
518  /// `redundantIneqsA` is the inequalities of `a` that are redundant for `b`
519  /// (similarly for `cuttingIneqsA`, `redundantIneqsB`, and `cuttingIneqsB`).
520  SmallVector<ArrayRef<MPInt>, 2> redundantIneqsA;
521  SmallVector<ArrayRef<MPInt>, 2> cuttingIneqsA;
522 
523  SmallVector<ArrayRef<MPInt>, 2> redundantIneqsB;
524  SmallVector<ArrayRef<MPInt>, 2> cuttingIneqsB;
525 
526  /// Given a Simplex `simp` and one of its inequalities `ineq`, check
527  /// that the facet of `simp` where `ineq` holds as an equality is contained
528  /// within `a`.
529  bool isFacetContained(ArrayRef<MPInt> ineq, Simplex &simp);
530 
531  /// Removes redundant constraints from `disjunct`, adds it to `disjuncts` and
532  /// removes the disjuncts at position `i` and `j`. Updates `simplices` to
533  /// reflect the changes. `i` and `j` cannot be equal.
534  void addCoalescedDisjunct(unsigned i, unsigned j,
535  const IntegerRelation &disjunct);
536 
537  /// Checks whether `a` and `b` can be combined in a convex sense, if there
538  /// exist cutting inequalities.
539  ///
540  /// An example of this case:
541  /// ___________ ___________
542  /// / / | / / /
543  /// \ \ | / ==> \ /
544  /// \ \ | / \ /
545  /// \___\|/ \_____/
546  ///
547  ///
548  LogicalResult coalescePairCutCase(unsigned i, unsigned j);
549 
550  /// Types the inequality `ineq` according to its `IneqType` for `simp` into
551  /// `redundantIneqsB` and `cuttingIneqsB`. Returns success, if no separate
552  /// inequalities were encountered. Otherwise, returns failure.
553  LogicalResult typeInequality(ArrayRef<MPInt> ineq, Simplex &simp);
554 
555  /// Types the equality `eq`, i.e. for `eq` == 0, types both `eq` >= 0 and
556  /// -`eq` >= 0 according to their `IneqType` for `simp` into
557  /// `redundantIneqsB` and `cuttingIneqsB`. Returns success, if no separate
558  /// inequalities were encountered. Otherwise, returns failure.
559  LogicalResult typeEquality(ArrayRef<MPInt> eq, Simplex &simp);
560 
561  /// Replaces the element at position `i` with the last element and erases
562  /// the last element for both `disjuncts` and `simplices`.
563  void eraseDisjunct(unsigned i);
564 
565  /// Attempts to coalesce the two IntegerRelations at position `i` and `j`
566  /// in `disjuncts` in-place. Returns whether the disjuncts were
567  /// successfully coalesced. The simplices in `simplices` need to be the ones
568  /// constructed from `disjuncts`. At this point, there are no empty
569  /// disjuncts in `disjuncts` left.
570  LogicalResult coalescePair(unsigned i, unsigned j);
571 };
572 
573 /// Constructs a `SetCoalescer` from a `PresburgerRelation`. Only adds non-empty
574 /// `IntegerRelation`s to the `disjuncts` vector.
575 SetCoalescer::SetCoalescer(const PresburgerRelation &s) : space(s.getSpace()) {
576 
577  disjuncts = s.disjuncts;
578 
579  simplices.reserve(s.getNumDisjuncts());
580  // Note that disjuncts.size() changes during the loop.
581  for (unsigned i = 0; i < disjuncts.size();) {
582  disjuncts[i].removeRedundantConstraints();
583  Simplex simp(disjuncts[i]);
584  if (simp.isEmpty()) {
585  disjuncts[i] = disjuncts[disjuncts.size() - 1];
586  disjuncts.pop_back();
587  continue;
588  }
589  ++i;
590  simplices.push_back(simp);
591  }
592 }
593 
594 /// Simplifies the representation of a PresburgerSet.
596  // For all tuples of IntegerRelations, check whether they can be
597  // coalesced. When coalescing is successful, the contained IntegerRelation
598  // is swapped with the last element of `disjuncts` and subsequently erased
599  // and similarly for simplices.
600  for (unsigned i = 0; i < disjuncts.size();) {
601 
602  // TODO: This does some comparisons two times (index 0 with 1 and index 1
603  // with 0).
604  bool broken = false;
605  for (unsigned j = 0, e = disjuncts.size(); j < e; ++j) {
606  negEqs.clear();
607  redundantIneqsA.clear();
608  redundantIneqsB.clear();
609  cuttingIneqsA.clear();
610  cuttingIneqsB.clear();
611  if (i == j)
612  continue;
613  if (coalescePair(i, j).succeeded()) {
614  broken = true;
615  break;
616  }
617  }
618 
619  // Only if the inner loop was not broken, i is incremented. This is
620  // required as otherwise, if a coalescing occurs, the IntegerRelation
621  // now at position i is not compared.
622  if (!broken)
623  ++i;
624  }
625 
626  PresburgerRelation newSet = PresburgerRelation::getEmpty(space);
627  for (unsigned i = 0, e = disjuncts.size(); i < e; ++i)
628  newSet.unionInPlace(disjuncts[i]);
629 
630  return newSet;
631 }
632 
633 /// Given a Simplex `simp` and one of its inequalities `ineq`, check
634 /// that all inequalities of `cuttingIneqsB` are redundant for the facet of
635 /// `simp` where `ineq` holds as an equality is contained within `a`.
636 bool SetCoalescer::isFacetContained(ArrayRef<MPInt> ineq, Simplex &simp) {
637  SimplexRollbackScopeExit scopeExit(simp);
638  simp.addEquality(ineq);
639  return llvm::all_of(cuttingIneqsB, [&simp](ArrayRef<MPInt> curr) {
640  return simp.isRedundantInequality(curr);
641  });
642 }
643 
644 void SetCoalescer::addCoalescedDisjunct(unsigned i, unsigned j,
645  const IntegerRelation &disjunct) {
646  assert(i != j && "The indices must refer to different disjuncts");
647  unsigned n = disjuncts.size();
648  if (j == n - 1) {
649  // This case needs special handling since position `n` - 1 is removed
650  // from the vector, hence the `IntegerRelation` at position `n` - 2 is
651  // lost otherwise.
652  disjuncts[i] = disjuncts[n - 2];
653  disjuncts.pop_back();
654  disjuncts[n - 2] = disjunct;
655  disjuncts[n - 2].removeRedundantConstraints();
656 
657  simplices[i] = simplices[n - 2];
658  simplices.pop_back();
659  simplices[n - 2] = Simplex(disjuncts[n - 2]);
660 
661  } else {
662  // Other possible edge cases are correct since for `j` or `i` == `n` -
663  // 2, the `IntegerRelation` at position `n` - 2 should be lost. The
664  // case `i` == `n` - 1 makes the first following statement a noop.
665  // Hence, in this case the same thing is done as above, but with `j`
666  // rather than `i`.
667  disjuncts[i] = disjuncts[n - 1];
668  disjuncts[j] = disjuncts[n - 2];
669  disjuncts.pop_back();
670  disjuncts[n - 2] = disjunct;
671  disjuncts[n - 2].removeRedundantConstraints();
672 
673  simplices[i] = simplices[n - 1];
674  simplices[j] = simplices[n - 2];
675  simplices.pop_back();
676  simplices[n - 2] = Simplex(disjuncts[n - 2]);
677  }
678 }
679 
680 /// Given two polyhedra `a` and `b` at positions `i` and `j` in
681 /// `disjuncts` and `redundantIneqsA` being the inequalities of `a` that
682 /// are redundant for `b` (similarly for `cuttingIneqsA`, `redundantIneqsB`,
683 /// and `cuttingIneqsB`), Checks whether the facets of all cutting
684 /// inequalites of `a` are contained in `b`. If so, a new polyhedron
685 /// consisting of all redundant inequalites of `a` and `b` and all
686 /// equalities of both is created.
687 ///
688 /// An example of this case:
689 /// ___________ ___________
690 /// / / | / / /
691 /// \ \ | / ==> \ /
692 /// \ \ | / \ /
693 /// \___\|/ \_____/
694 ///
695 ///
696 LogicalResult SetCoalescer::coalescePairCutCase(unsigned i, unsigned j) {
697  /// All inequalities of `b` need to be redundant. We already know that the
698  /// redundant ones are, so only the cutting ones remain to be checked.
699  Simplex &simp = simplices[i];
700  IntegerRelation &disjunct = disjuncts[i];
701  if (llvm::any_of(cuttingIneqsA, [this, &simp](ArrayRef<MPInt> curr) {
702  return !isFacetContained(curr, simp);
703  }))
704  return failure();
705  IntegerRelation newSet(disjunct.getSpace());
706 
707  for (ArrayRef<MPInt> curr : redundantIneqsA)
708  newSet.addInequality(curr);
709 
710  for (ArrayRef<MPInt> curr : redundantIneqsB)
711  newSet.addInequality(curr);
712 
713  addCoalescedDisjunct(i, j, newSet);
714  return success();
715 }
716 
717 LogicalResult SetCoalescer::typeInequality(ArrayRef<MPInt> ineq,
718  Simplex &simp) {
719  Simplex::IneqType type = simp.findIneqType(ineq);
720  if (type == Simplex::IneqType::Redundant)
721  redundantIneqsB.push_back(ineq);
722  else if (type == Simplex::IneqType::Cut)
723  cuttingIneqsB.push_back(ineq);
724  else
725  return failure();
726  return success();
727 }
728 
729 LogicalResult SetCoalescer::typeEquality(ArrayRef<MPInt> eq, Simplex &simp) {
730  if (typeInequality(eq, simp).failed())
731  return failure();
732  negEqs.push_back(getNegatedCoeffs(eq));
733  ArrayRef<MPInt> inv(negEqs.back());
734  if (typeInequality(inv, simp).failed())
735  return failure();
736  return success();
737 }
738 
739 void SetCoalescer::eraseDisjunct(unsigned i) {
740  assert(simplices.size() == disjuncts.size() &&
741  "simplices and disjuncts must be equally as long");
742  disjuncts[i] = disjuncts.back();
743  disjuncts.pop_back();
744  simplices[i] = simplices.back();
745  simplices.pop_back();
746 }
747 
748 LogicalResult SetCoalescer::coalescePair(unsigned i, unsigned j) {
749 
750  IntegerRelation &a = disjuncts[i];
751  IntegerRelation &b = disjuncts[j];
752  /// Handling of local ids is not yet implemented, so these cases are
753  /// skipped.
754  /// TODO: implement local id support.
755  if (a.getNumLocalVars() != 0 || b.getNumLocalVars() != 0)
756  return failure();
757  Simplex &simpA = simplices[i];
758  Simplex &simpB = simplices[j];
759 
760  // Organize all inequalities and equalities of `a` according to their type
761  // for `b` into `redundantIneqsA` and `cuttingIneqsA` (and vice versa for
762  // all inequalities of `b` according to their type in `a`). If a separate
763  // inequality is encountered during typing, the two IntegerRelations
764  // cannot be coalesced.
765  for (int k = 0, e = a.getNumInequalities(); k < e; ++k)
766  if (typeInequality(a.getInequality(k), simpB).failed())
767  return failure();
768 
769  for (int k = 0, e = a.getNumEqualities(); k < e; ++k)
770  if (typeEquality(a.getEquality(k), simpB).failed())
771  return failure();
772 
773  std::swap(redundantIneqsA, redundantIneqsB);
774  std::swap(cuttingIneqsA, cuttingIneqsB);
775 
776  for (int k = 0, e = b.getNumInequalities(); k < e; ++k)
777  if (typeInequality(b.getInequality(k), simpA).failed())
778  return failure();
779 
780  for (int k = 0, e = b.getNumEqualities(); k < e; ++k)
781  if (typeEquality(b.getEquality(k), simpA).failed())
782  return failure();
783 
784  // If there are no cutting inequalities of `a`, `b` is contained
785  // within `a`.
786  if (cuttingIneqsA.empty()) {
787  eraseDisjunct(j);
788  return success();
789  }
790 
791  // Try to apply the cut case
792  if (coalescePairCutCase(i, j).succeeded())
793  return success();
794 
795  // Swap the vectors to compare the pair (j,i) instead of (i,j).
796  std::swap(redundantIneqsA, redundantIneqsB);
797  std::swap(cuttingIneqsA, cuttingIneqsB);
798 
799  // If there are no cutting inequalities of `a`, `b` is contained
800  // within `a`.
801  if (cuttingIneqsA.empty()) {
802  eraseDisjunct(i);
803  return success();
804  }
805 
806  // Try to apply the cut case
807  if (coalescePairCutCase(j, i).succeeded())
808  return success();
809 
810  return failure();
811 }
812 
813 PresburgerRelation PresburgerRelation::coalesce() const {
814  return SetCoalescer(*this).coalesce();
815 }
816 
818  return llvm::all_of(disjuncts, [](const IntegerRelation &rel) {
819  return rel.hasOnlyDivLocals();
820  });
821 }
822 
823 void PresburgerRelation::print(raw_ostream &os) const {
824  os << "Number of Disjuncts: " << getNumDisjuncts() << "\n";
825  for (const IntegerRelation &disjunct : disjuncts) {
826  disjunct.print(os);
827  os << '\n';
828  }
829 }
830 
831 void PresburgerRelation::dump() const { print(llvm::errs()); }
832 
834  PresburgerSet result(space);
836  return result;
837 }
838 
840  return PresburgerSet(space);
841 }
842 
844  : PresburgerRelation(disjunct) {}
845 
847  : PresburgerRelation(set) {}
848 
851 }
852 
855 }
856 
859 }
860 
863 }
864 
867 }
static SmallVector< MPInt, 8 > getIneqCoeffsFromIdx(const IntegerRelation &rel, unsigned idx)
Return the coefficients of the ineq in rel specified by idx.
static PresburgerRelation getSetDifference(IntegerRelation b, const PresburgerRelation &s)
Return the set difference b \ s.
Class storing division representation of local variables of a constraint system.
Definition: Utils.h:118
MPInt & getDenom(unsigned i)
Definition: Utils.h:149
MutableArrayRef< MPInt > getDividend(unsigned i)
Definition: Utils.h:140
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
static IntegerPolyhedron getUniverse(const PresburgerSpace &space)
Return a system with no constraints, i.e., one which is satisfied by all points.
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
ArrayRef< MPInt > getEquality(unsigned idx) const
PresburgerSpace getSpaceWithoutLocals() const
Returns a copy of the space without locals.
void addInequality(ArrayRef< MPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
void truncate(const CountsSnapshot &counts)
bool isEmptyByGCDTest() const
Runs the GCD test on all equality constraints.
void print(raw_ostream &os) const
bool isIntegerEmpty() const
Returns true if the set of constraints is found to have no solution, false if a solution exists.
IntegerRelation intersect(IntegerRelation other) const
Return the intersection of the two relations.
ArrayRef< MPInt > getInequality(unsigned idx) const
std::optional< SmallVector< MPInt, 8 > > containsPointNoLocal(ArrayRef< MPInt > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists,...
static IntegerRelation getUniverse(const PresburgerSpace &space)
Return a system with no constraints, i.e., one which is satisfied by all points.
bool isEmpty() const
Checks for emptiness by performing variable elimination on all variables, running the GCD test on eac...
DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const
Returns a DivisonRepr representing the division representation of local variables in the constraint s...
bool hasOnlyDivLocals() const
Check whether all local ids have a division representation.
unsigned mergeLocalVars(IntegerRelation &other)
Adds additional local vars to the sets such that they both have the union of the local vars in each s...
const PresburgerSpace & getSpace() const
Returns a reference to the underlying space.
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of vars starts.
This class provides support for multi-precision arithmetic.
Definition: MPInt.h:87
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...
bool containsPoint(ArrayRef< MPInt > point) const
Return true if the set contains the given point, and false otherwise.
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace.
PresburgerRelation intersect(const PresburgerRelation &set) const
Return the intersection of this set and the given set.
bool hasOnlyDivLocals() const
Check whether all local ids in all disjuncts have a div representation.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
PresburgerRelation(const IntegerRelation &disjunct)
PresburgerRelation computeReprWithOnlyDivLocals() const
Compute an equivalent representation of the same relation, such that all local ids in all disjuncts h...
bool isSubsetOf(const PresburgerRelation &set) const
Return true if this set is a subset of the given set, and false otherwise.
bool isIntegerEmpty() const
Return true if all the sets in the union are known to be integer empty false otherwise.
void unionInPlace(const IntegerRelation &disjunct)
Mutate this set, turning it into the union of this set and the given disjunct.
std::optional< MPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the disjunct.
bool isEqual(const PresburgerRelation &set) const
Return true if this set is equal to the given set, and false otherwise.
static PresburgerRelation getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
unsigned getNumDisjuncts() const
Return the number of disjuncts in the union.
PresburgerRelation coalesce() const
Simplifies the representation of a PresburgerRelation.
static PresburgerRelation getUniverse(const PresburgerSpace &space)
Return a universe set of the specified type that contains all points.
const IntegerRelation & getDisjunct(unsigned index) const
Return the disjunct at the specified index.
ArrayRef< IntegerRelation > getAllDisjuncts() const
Return a reference to the list of disjuncts.
SmallVector< IntegerRelation, 2 > disjuncts
The list of disjuncts that this set is the union of.
const PresburgerSpace & getSpace() const
void print(raw_ostream &os) const
Print the set's internal state.
PresburgerRelation unionSet(const PresburgerRelation &set) const
Return the union of this set and the given set.
bool findIntegerSample(SmallVectorImpl< MPInt > &sample)
Find an integer sample from the given set.
PresburgerRelation complement() const
Return the complement of this set.
PresburgerSet intersect(const PresburgerRelation &set) const
PresburgerSet(const IntegerPolyhedron &disjunct)
Create a set from a relation.
PresburgerSet unionSet(const PresburgerRelation &set) const
These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...
PresburgerSet subtract(const PresburgerRelation &set) const
static PresburgerSet getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
static PresburgerSet getUniverse(const PresburgerSpace &space)
Return a universe set of the specified type that contains all points.
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
bool isEmpty() const
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
Definition: Simplex.cpp:1051
void appendVariable(unsigned count=1)
Add new variables to the end of the list of variables.
Definition: Simplex.cpp:1300
void intersectIntegerRelation(const IntegerRelation &rel)
Add all the constraints from the given IntegerRelation.
Definition: Simplex.cpp:1315
unsigned getSnapshot() const
Get a snapshot of the current state.
Definition: Simplex.cpp:1117
void addEquality(ArrayRef< MPInt > coeffs)
Add an equality to the tableau.
Definition: Simplex.cpp:1104
void rollback(unsigned snapshot)
Rollback to a snapshot. This invalidates all later snapshots.
Definition: Simplex.cpp:1270
unsigned getNumConstraints() const
Returns the number of constraints in the tableau.
Definition: Simplex.cpp:1113
Takes a snapshot of the simplex state on construction and rolls back to the snapshot on destruction.
Definition: Simplex.h:872
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...
Definition: Simplex.h:695
bool isMarkedRedundant(unsigned constraintIndex) const
Returns whether the specified constraint has been marked as redundant.
Definition: Simplex.cpp:1388
void addInequality(ArrayRef< MPInt > coeffs) final
Add an inequality to the tableau.
Definition: Simplex.cpp:1091
bool isRedundantInequality(ArrayRef< MPInt > coeffs)
Check if the specified inequality already holds in the polytope.
Definition: Simplex.cpp:2173
void detectRedundant(unsigned offset, unsigned count)
Finds a subset of constraints that is redundant, i.e., such that the set of solutions does not change...
Definition: Simplex.cpp:1408
IneqType findIneqType(ArrayRef< MPInt > coeffs)
Returns the type of the inequality with coefficients coeffs.
Definition: Simplex.cpp:2158
The SetCoalescer class contains all functionality concerning the coalesce heuristic.
SetCoalescer(const PresburgerRelation &s)
Construct a SetCoalescer from a PresburgerSet.
PresburgerRelation coalesce()
Simplifies the representation of a PresburgerSet.
SmallVector< MPInt, 8 > getDivLowerBound(ArrayRef< MPInt > dividend, const MPInt &divisor, unsigned localVarIdx)
Definition: Utils.cpp:323
SmallVector< MPInt, 8 > getDivUpperBound(ArrayRef< MPInt > dividend, const MPInt &divisor, unsigned localVarIdx)
If q is defined to be equal to expr floordiv d, this equivalent to saying that q is an integer and q ...
Definition: Utils.cpp:312
SmallVector< MPInt, 8 > getNegatedCoeffs(ArrayRef< MPInt > coeffs)
Return coeffs with all the elements negated.
Definition: Utils.cpp:364
SmallVector< MPInt, 8 > getComplementIneq(ArrayRef< MPInt > ineq)
Return the complement of the given inequality.
Definition: Utils.cpp:372
This header declares functions that assit transformations in the MemRef dialect.
LogicalResult failure(bool isFailure=true)
Utility function to generate a LogicalResult.
Definition: LogicalResult.h:62
bool succeeded(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a success value.
Definition: LogicalResult.h:68
LogicalResult success(bool isSuccess=true)
Utility function to generate a LogicalResult.
Definition: LogicalResult.h:56
bool failed(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a failure value.
Definition: LogicalResult.h:72
This class represents an efficient way to signal success or failure.
Definition: LogicalResult.h:26
bool failed() const
Returns true if the provided LogicalResult corresponds to a failure value.
Definition: LogicalResult.h:44
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type.
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.