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