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