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