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