MLIR  17.0.0git
IntegerRelation.cpp
Go to the documentation of this file.
1 //===- IntegerRelation.cpp - MLIR IntegerRelation 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 //
9 // A class to represent an relation over integer tuples. A relation is
10 // represented as a constraint system over a space of tuples of integer valued
11 // variables supporting symbolic variables and existential quantification.
12 //
13 //===----------------------------------------------------------------------===//
14 
21 #include "llvm/ADT/DenseMap.h"
22 #include "llvm/ADT/DenseSet.h"
23 #include "llvm/Support/Debug.h"
24 #include <numeric>
25 #include <optional>
26 
27 #define DEBUG_TYPE "presburger"
28 
29 using namespace mlir;
30 using namespace presburger;
31 
32 using llvm::SmallDenseMap;
33 using llvm::SmallDenseSet;
34 
35 std::unique_ptr<IntegerRelation> IntegerRelation::clone() const {
36  return std::make_unique<IntegerRelation>(*this);
37 }
38 
39 std::unique_ptr<IntegerPolyhedron> IntegerPolyhedron::clone() const {
40  return std::make_unique<IntegerPolyhedron>(*this);
41 }
42 
44  assert(space.getNumVars() == oSpace.getNumVars() && "invalid space!");
45  space = oSpace;
46 }
47 
49  assert(oSpace.getNumLocalVars() == 0 && "no locals should be present!");
50  assert(oSpace.getNumVars() <= getNumVars() && "invalid space!");
51  unsigned newNumLocals = getNumVars() - oSpace.getNumVars();
52  space = oSpace;
53  space.insertVar(VarKind::Local, 0, newNumLocals);
54 }
55 
57  assert(space.isEqual(other.getSpace()) && "Spaces must be equal.");
58 
60  other.getNumInequalities());
62 
63  for (unsigned r = 0, e = other.getNumInequalities(); r < e; r++) {
64  addInequality(other.getInequality(r));
65  }
66  for (unsigned r = 0, e = other.getNumEqualities(); r < e; r++) {
67  addEquality(other.getEquality(r));
68  }
69 }
70 
72  IntegerRelation result = *this;
73  result.mergeLocalVars(other);
74  result.append(other);
75  return result;
76 }
77 
78 bool IntegerRelation::isEqual(const IntegerRelation &other) const {
79  assert(space.isCompatible(other.getSpace()) && "Spaces must be compatible.");
80  return PresburgerRelation(*this).isEqual(PresburgerRelation(other));
81 }
82 
83 bool IntegerRelation::isSubsetOf(const IntegerRelation &other) const {
84  assert(space.isCompatible(other.getSpace()) && "Spaces must be compatible.");
85  return PresburgerRelation(*this).isSubsetOf(PresburgerRelation(other));
86 }
87 
90  assert(getNumSymbolVars() == 0 && "Symbols are not supported!");
93 
94  if (!maybeLexMin.isBounded())
95  return maybeLexMin;
96 
97  // The Simplex returns the lexmin over all the variables including locals. But
98  // locals are not actually part of the space and should not be returned in the
99  // result. Since the locals are placed last in the list of variables, they
100  // will be minimized last in the lexmin. So simply truncating out the locals
101  // from the end of the answer gives the desired lexmin over the dimensions.
102  assert(maybeLexMin->size() == getNumVars() &&
103  "Incorrect number of vars in lexMin!");
104  maybeLexMin->resize(getNumDimAndSymbolVars());
105  return maybeLexMin;
106 }
107 
109  assert(getNumSymbolVars() == 0 && "Symbols are not supported!");
111  LexSimplex(*this).findIntegerLexMin();
112 
113  if (!maybeLexMin.isBounded())
114  return maybeLexMin.getKind();
115 
116  // The Simplex returns the lexmin over all the variables including locals. But
117  // locals are not actually part of the space and should not be returned in the
118  // result. Since the locals are placed last in the list of variables, they
119  // will be minimized last in the lexmin. So simply truncating out the locals
120  // from the end of the answer gives the desired lexmin over the dimensions.
121  assert(maybeLexMin->size() == getNumVars() &&
122  "Incorrect number of vars in lexMin!");
123  maybeLexMin->resize(getNumDimAndSymbolVars());
124  return maybeLexMin;
125 }
126 
127 static bool rangeIsZero(ArrayRef<MPInt> range) {
128  return llvm::all_of(range, [](const MPInt &x) { return x == 0; });
129 }
130 
132  unsigned begin, unsigned count) {
133  // We loop until i > 0 and index into i - 1 to avoid sign issues.
134  //
135  // We iterate backwards so that whether we remove constraint i - 1 or not, the
136  // next constraint to be tested is always i - 2.
137  for (unsigned i = poly.getNumEqualities(); i > 0; i--)
138  if (!rangeIsZero(poly.getEquality(i - 1).slice(begin, count)))
139  poly.removeEquality(i - 1);
140  for (unsigned i = poly.getNumInequalities(); i > 0; i--)
141  if (!rangeIsZero(poly.getInequality(i - 1).slice(begin, count)))
142  poly.removeInequality(i - 1);
143 }
144 
147 }
148 
149 void IntegerRelation::truncateVarKind(VarKind kind, unsigned num) {
150  unsigned curNum = getNumVarKind(kind);
151  assert(num <= curNum && "Can't truncate to more vars!");
152  removeVarRange(kind, num, curNum);
153 }
154 
156  const CountsSnapshot &counts) {
157  truncateVarKind(kind, counts.getSpace().getNumVarKind(kind));
158 }
159 
167 }
168 
170  // If there are no locals, we're done.
171  if (getNumLocalVars() == 0)
172  return PresburgerRelation(*this);
173 
174  // Move all the non-div locals to the end, as the current API to
175  // SymbolicLexMin requires these to form a contiguous range.
176  //
177  // Take a copy so we can perform mutations.
178  IntegerRelation copy = *this;
179  std::vector<MaybeLocalRepr> reprs(getNumLocalVars());
180  copy.getLocalReprs(&reprs);
181 
182  // Iterate through all the locals. The last `numNonDivLocals` are the locals
183  // that have been scanned already and do not have division representations.
184  unsigned numNonDivLocals = 0;
185  unsigned offset = copy.getVarKindOffset(VarKind::Local);
186  for (unsigned i = 0, e = copy.getNumLocalVars(); i < e - numNonDivLocals;) {
187  if (!reprs[i]) {
188  // Whenever we come across a local that does not have a division
189  // representation, we swap it to the `numNonDivLocals`-th last position
190  // and increment `numNonDivLocal`s. `reprs` also needs to be swapped.
191  copy.swapVar(offset + i, offset + e - numNonDivLocals - 1);
192  std::swap(reprs[i], reprs[e - numNonDivLocals - 1]);
193  ++numNonDivLocals;
194  continue;
195  }
196  ++i;
197  }
198 
199  // If there are no non-div locals, we're done.
200  if (numNonDivLocals == 0)
201  return PresburgerRelation(*this);
202 
203  // We computeSymbolicIntegerLexMin by considering the non-div locals as
204  // "non-symbols" and considering everything else as "symbols". This will
205  // compute a function mapping assignments to "symbols" to the
206  // lexicographically minimal valid assignment of "non-symbols", when a
207  // satisfying assignment exists. It separately returns the set of assignments
208  // to the "symbols" such that a satisfying assignment to the "non-symbols"
209  // exists but the lexmin is unbounded. We basically want to find the set of
210  // values of the "symbols" such that an assignment to the "non-symbols"
211  // exists, which is the union of the domain of the returned lexmin function
212  // and the returned set of assignments to the "symbols" that makes the lexmin
213  // unbounded.
214  SymbolicLexMin lexminResult =
215  SymbolicLexSimplex(copy, /*symbolOffset*/ 0,
217  /*numDims=*/copy.getNumVars() - numNonDivLocals)))
219  PresburgerRelation result =
220  lexminResult.lexmin.getDomain().unionSet(lexminResult.unboundedDomain);
221 
222  // The result set might lie in the wrong space -- all its ids are dims.
223  // Set it to the desired space and return.
226  result.setSpace(space);
227  return result;
228 }
229 
231  // Symbol and Domain vars will be used as symbols for symbolic lexmin.
232  // In other words, for every value of the symbols and domain, return the
233  // lexmin value of the (range, locals).
234  llvm::SmallBitVector isSymbol(getNumVars(), false);
235  isSymbol.set(getVarKindOffset(VarKind::Symbol),
237  isSymbol.set(getVarKindOffset(VarKind::Domain),
239  // Compute the symbolic lexmin of the dims and locals, with the symbols being
240  // the actual symbols of this set.
241  // The resultant space of lexmin is the space of the relation itself.
242  SymbolicLexMin result =
243  SymbolicLexSimplex(*this,
245  /*numDims=*/getNumDomainVars(),
246  /*numSymbols=*/getNumSymbolVars())),
247  isSymbol)
249 
250  // We want to return only the lexmin over the dims, so strip the locals from
251  // the computed lexmin.
253  result.lexmin.getNumOutputs());
254  return result;
255 }
256 
259  return PresburgerRelation(*this).subtract(set);
260 }
261 
262 unsigned IntegerRelation::insertVar(VarKind kind, unsigned pos, unsigned num) {
263  assert(pos <= getNumVarKind(kind));
264 
265  unsigned insertPos = space.insertVar(kind, pos, num);
266  inequalities.insertColumns(insertPos, num);
267  equalities.insertColumns(insertPos, num);
268  return insertPos;
269 }
270 
271 unsigned IntegerRelation::appendVar(VarKind kind, unsigned num) {
272  unsigned pos = getNumVarKind(kind);
273  return insertVar(kind, pos, num);
274 }
275 
277  assert(eq.size() == getNumCols());
278  unsigned row = equalities.appendExtraRow();
279  for (unsigned i = 0, e = eq.size(); i < e; ++i)
280  equalities(row, i) = eq[i];
281 }
282 
284  assert(inEq.size() == getNumCols());
285  unsigned row = inequalities.appendExtraRow();
286  for (unsigned i = 0, e = inEq.size(); i < e; ++i)
287  inequalities(row, i) = inEq[i];
288 }
289 
290 void IntegerRelation::removeVar(VarKind kind, unsigned pos) {
291  removeVarRange(kind, pos, pos + 1);
292 }
293 
294 void IntegerRelation::removeVar(unsigned pos) { removeVarRange(pos, pos + 1); }
295 
296 void IntegerRelation::removeVarRange(VarKind kind, unsigned varStart,
297  unsigned varLimit) {
298  assert(varLimit <= getNumVarKind(kind));
299 
300  if (varStart >= varLimit)
301  return;
302 
303  // Remove eliminated variables from the constraints.
304  unsigned offset = getVarKindOffset(kind);
305  equalities.removeColumns(offset + varStart, varLimit - varStart);
306  inequalities.removeColumns(offset + varStart, varLimit - varStart);
307 
308  // Remove eliminated variables from the space.
309  space.removeVarRange(kind, varStart, varLimit);
310 }
311 
312 void IntegerRelation::removeVarRange(unsigned varStart, unsigned varLimit) {
313  assert(varLimit <= getNumVars());
314 
315  if (varStart >= varLimit)
316  return;
317 
318  // Helper function to remove vars of the specified kind in the given range
319  // [start, limit), The range is absolute (i.e. it is not relative to the kind
320  // of variable). Also updates `limit` to reflect the deleted variables.
321  auto removeVarKindInRange = [this](VarKind kind, unsigned &start,
322  unsigned &limit) {
323  if (start >= limit)
324  return;
325 
326  unsigned offset = getVarKindOffset(kind);
327  unsigned num = getNumVarKind(kind);
328 
329  // Get `start`, `limit` relative to the specified kind.
330  unsigned relativeStart =
331  start <= offset ? 0 : std::min(num, start - offset);
332  unsigned relativeLimit =
333  limit <= offset ? 0 : std::min(num, limit - offset);
334 
335  // Remove vars of the specified kind in the relative range.
336  removeVarRange(kind, relativeStart, relativeLimit);
337 
338  // Update `limit` to reflect deleted variables.
339  // `start` does not need to be updated because any variables that are
340  // deleted are after position `start`.
341  limit -= relativeLimit - relativeStart;
342  };
343 
344  removeVarKindInRange(VarKind::Domain, varStart, varLimit);
345  removeVarKindInRange(VarKind::Range, varStart, varLimit);
346  removeVarKindInRange(VarKind::Symbol, varStart, varLimit);
347  removeVarKindInRange(VarKind::Local, varStart, varLimit);
348 }
349 
351  equalities.removeRow(pos);
352 }
353 
355  inequalities.removeRow(pos);
356 }
357 
358 void IntegerRelation::removeEqualityRange(unsigned start, unsigned end) {
359  if (start >= end)
360  return;
361  equalities.removeRows(start, end - start);
362 }
363 
364 void IntegerRelation::removeInequalityRange(unsigned start, unsigned end) {
365  if (start >= end)
366  return;
367  inequalities.removeRows(start, end - start);
368 }
369 
370 void IntegerRelation::swapVar(unsigned posA, unsigned posB) {
371  assert(posA < getNumVars() && "invalid position A");
372  assert(posB < getNumVars() && "invalid position B");
373 
374  if (posA == posB)
375  return;
376 
377  inequalities.swapColumns(posA, posB);
378  equalities.swapColumns(posA, posB);
379 }
380 
384 }
385 
386 /// Gather all lower and upper bounds of the variable at `pos`, and
387 /// optionally any equalities on it. In addition, the bounds are to be
388 /// independent of variables in position range [`offset`, `offset` + `num`).
390  unsigned pos, SmallVectorImpl<unsigned> *lbIndices,
392  unsigned offset, unsigned num) const {
393  assert(pos < getNumVars() && "invalid position");
394  assert(offset + num < getNumCols() && "invalid range");
395 
396  // Checks for a constraint that has a non-zero coeff for the variables in
397  // the position range [offset, offset + num) while ignoring `pos`.
398  auto containsConstraintDependentOnRange = [&](unsigned r, bool isEq) {
399  unsigned c, f;
400  auto cst = isEq ? getEquality(r) : getInequality(r);
401  for (c = offset, f = offset + num; c < f; ++c) {
402  if (c == pos)
403  continue;
404  if (cst[c] != 0)
405  break;
406  }
407  return c < f;
408  };
409 
410  // Gather all lower bounds and upper bounds of the variable. Since the
411  // canonical form c_1*x_1 + c_2*x_2 + ... + c_0 >= 0, a constraint is a lower
412  // bound for x_i if c_i >= 1, and an upper bound if c_i <= -1.
413  for (unsigned r = 0, e = getNumInequalities(); r < e; r++) {
414  // The bounds are to be independent of [offset, offset + num) columns.
415  if (containsConstraintDependentOnRange(r, /*isEq=*/false))
416  continue;
417  if (atIneq(r, pos) >= 1) {
418  // Lower bound.
419  lbIndices->push_back(r);
420  } else if (atIneq(r, pos) <= -1) {
421  // Upper bound.
422  ubIndices->push_back(r);
423  }
424  }
425 
426  // An equality is both a lower and upper bound. Record any equalities
427  // involving the pos^th variable.
428  if (!eqIndices)
429  return;
430 
431  for (unsigned r = 0, e = getNumEqualities(); r < e; r++) {
432  if (atEq(r, pos) == 0)
433  continue;
434  if (containsConstraintDependentOnRange(r, /*isEq=*/true))
435  continue;
436  eqIndices->push_back(r);
437  }
438 }
439 
442  return false;
444  return false;
445  return true;
446 }
447 
449  if (values.empty())
450  return;
451  assert(pos + values.size() <= getNumVars() &&
452  "invalid position or too many values");
453  // Setting x_j = p in sum_i a_i x_i + c is equivalent to adding p*a_j to the
454  // constant term and removing the var x_j. We do this for all the vars
455  // pos, pos + 1, ... pos + values.size() - 1.
456  unsigned constantColPos = getNumCols() - 1;
457  for (unsigned i = 0, numVals = values.size(); i < numVals; ++i)
458  inequalities.addToColumn(i + pos, constantColPos, values[i]);
459  for (unsigned i = 0, numVals = values.size(); i < numVals; ++i)
460  equalities.addToColumn(i + pos, constantColPos, values[i]);
461  removeVarRange(pos, pos + values.size());
462 }
463 
465  *this = other;
466 }
467 
468 // Searches for a constraint with a non-zero coefficient at `colIdx` in
469 // equality (isEq=true) or inequality (isEq=false) constraints.
470 // Returns true and sets row found in search in `rowIdx`, false otherwise.
471 bool IntegerRelation::findConstraintWithNonZeroAt(unsigned colIdx, bool isEq,
472  unsigned *rowIdx) const {
473  assert(colIdx < getNumCols() && "position out of bounds");
474  auto at = [&](unsigned rowIdx) -> MPInt {
475  return isEq ? atEq(rowIdx, colIdx) : atIneq(rowIdx, colIdx);
476  };
477  unsigned e = isEq ? getNumEqualities() : getNumInequalities();
478  for (*rowIdx = 0; *rowIdx < e; ++(*rowIdx)) {
479  if (at(*rowIdx) != 0) {
480  return true;
481  }
482  }
483  return false;
484 }
485 
487  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i)
489  for (unsigned i = 0, e = getNumInequalities(); i < e; ++i)
491 }
492 
494  assert(hasConsistentState());
495  auto check = [&](bool isEq) -> bool {
496  unsigned numCols = getNumCols();
497  unsigned numRows = isEq ? getNumEqualities() : getNumInequalities();
498  for (unsigned i = 0, e = numRows; i < e; ++i) {
499  unsigned j;
500  for (j = 0; j < numCols - 1; ++j) {
501  MPInt v = isEq ? atEq(i, j) : atIneq(i, j);
502  // Skip rows with non-zero variable coefficients.
503  if (v != 0)
504  break;
505  }
506  if (j < numCols - 1) {
507  continue;
508  }
509  // Check validity of constant term at 'numCols - 1' w.r.t 'isEq'.
510  // Example invalid constraints include: '1 == 0' or '-1 >= 0'
511  MPInt v = isEq ? atEq(i, numCols - 1) : atIneq(i, numCols - 1);
512  if ((isEq && v != 0) || (!isEq && v < 0)) {
513  return true;
514  }
515  }
516  return false;
517  };
518  if (check(/*isEq=*/true))
519  return true;
520  return check(/*isEq=*/false);
521 }
522 
523 /// Eliminate variable from constraint at `rowIdx` based on coefficient at
524 /// pivotRow, pivotCol. Columns in range [elimColStart, pivotCol) will not be
525 /// updated as they have already been eliminated.
526 static void eliminateFromConstraint(IntegerRelation *constraints,
527  unsigned rowIdx, unsigned pivotRow,
528  unsigned pivotCol, unsigned elimColStart,
529  bool isEq) {
530  // Skip if equality 'rowIdx' if same as 'pivotRow'.
531  if (isEq && rowIdx == pivotRow)
532  return;
533  auto at = [&](unsigned i, unsigned j) -> MPInt {
534  return isEq ? constraints->atEq(i, j) : constraints->atIneq(i, j);
535  };
536  MPInt leadCoeff = at(rowIdx, pivotCol);
537  // Skip if leading coefficient at 'rowIdx' is already zero.
538  if (leadCoeff == 0)
539  return;
540  MPInt pivotCoeff = constraints->atEq(pivotRow, pivotCol);
541  int sign = (leadCoeff * pivotCoeff > 0) ? -1 : 1;
542  MPInt lcm = presburger::lcm(pivotCoeff, leadCoeff);
543  MPInt pivotMultiplier = sign * (lcm / abs(pivotCoeff));
544  MPInt rowMultiplier = lcm / abs(leadCoeff);
545 
546  unsigned numCols = constraints->getNumCols();
547  for (unsigned j = 0; j < numCols; ++j) {
548  // Skip updating column 'j' if it was just eliminated.
549  if (j >= elimColStart && j < pivotCol)
550  continue;
551  MPInt v = pivotMultiplier * constraints->atEq(pivotRow, j) +
552  rowMultiplier * at(rowIdx, j);
553  isEq ? constraints->atEq(rowIdx, j) = v
554  : constraints->atIneq(rowIdx, j) = v;
555  }
556 }
557 
558 /// Returns the position of the variable that has the minimum <number of lower
559 /// bounds> times <number of upper bounds> from the specified range of
560 /// variables [start, end). It is often best to eliminate in the increasing
561 /// order of these counts when doing Fourier-Motzkin elimination since FM adds
562 /// that many new constraints.
563 static unsigned getBestVarToEliminate(const IntegerRelation &cst,
564  unsigned start, unsigned end) {
565  assert(start < cst.getNumVars() && end < cst.getNumVars() + 1);
566 
567  auto getProductOfNumLowerUpperBounds = [&](unsigned pos) {
568  unsigned numLb = 0;
569  unsigned numUb = 0;
570  for (unsigned r = 0, e = cst.getNumInequalities(); r < e; r++) {
571  if (cst.atIneq(r, pos) > 0) {
572  ++numLb;
573  } else if (cst.atIneq(r, pos) < 0) {
574  ++numUb;
575  }
576  }
577  return numLb * numUb;
578  };
579 
580  unsigned minLoc = start;
581  unsigned min = getProductOfNumLowerUpperBounds(start);
582  for (unsigned c = start + 1; c < end; c++) {
583  unsigned numLbUbProduct = getProductOfNumLowerUpperBounds(c);
584  if (numLbUbProduct < min) {
585  min = numLbUbProduct;
586  minLoc = c;
587  }
588  }
589  return minLoc;
590 }
591 
592 // Checks for emptiness of the set by eliminating variables successively and
593 // using the GCD test (on all equality constraints) and checking for trivially
594 // invalid constraints. Returns 'true' if the constraint system is found to be
595 // empty; false otherwise.
598  return true;
599 
600  IntegerRelation tmpCst(*this);
601 
602  // First, eliminate as many local variables as possible using equalities.
603  tmpCst.removeRedundantLocalVars();
604  if (tmpCst.isEmptyByGCDTest() || tmpCst.hasInvalidConstraint())
605  return true;
606 
607  // Eliminate as many variables as possible using Gaussian elimination.
608  unsigned currentPos = 0;
609  while (currentPos < tmpCst.getNumVars()) {
610  tmpCst.gaussianEliminateVars(currentPos, tmpCst.getNumVars());
611  ++currentPos;
612  // We check emptiness through trivial checks after eliminating each ID to
613  // detect emptiness early. Since the checks isEmptyByGCDTest() and
614  // hasInvalidConstraint() are linear time and single sweep on the constraint
615  // buffer, this appears reasonable - but can optimize in the future.
616  if (tmpCst.hasInvalidConstraint() || tmpCst.isEmptyByGCDTest())
617  return true;
618  }
619 
620  // Eliminate the remaining using FM.
621  for (unsigned i = 0, e = tmpCst.getNumVars(); i < e; i++) {
623  getBestVarToEliminate(tmpCst, 0, tmpCst.getNumVars()));
624  // Check for a constraint explosion. This rarely happens in practice, but
625  // this check exists as a safeguard against improperly constructed
626  // constraint systems or artificially created arbitrarily complex systems
627  // that aren't the intended use case for IntegerRelation. This is
628  // needed since FM has a worst case exponential complexity in theory.
629  if (tmpCst.getNumConstraints() >= kExplosionFactor * getNumVars()) {
630  LLVM_DEBUG(llvm::dbgs() << "FM constraint explosion detected\n");
631  return false;
632  }
633 
634  // FM wouldn't have modified the equalities in any way. So no need to again
635  // run GCD test. Check for trivial invalid constraints.
636  if (tmpCst.hasInvalidConstraint())
637  return true;
638  }
639  return false;
640 }
641 
642 // Runs the GCD test on all equality constraints. Returns 'true' if this test
643 // fails on any equality. Returns 'false' otherwise.
644 // This test can be used to disprove the existence of a solution. If it returns
645 // true, no integer solution to the equality constraints can exist.
646 //
647 // GCD test definition:
648 //
649 // The equality constraint:
650 //
651 // c_1*x_1 + c_2*x_2 + ... + c_n*x_n = c_0
652 //
653 // has an integer solution iff:
654 //
655 // GCD of c_1, c_2, ..., c_n divides c_0.
657  assert(hasConsistentState());
658  unsigned numCols = getNumCols();
659  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i) {
660  MPInt gcd = abs(atEq(i, 0));
661  for (unsigned j = 1; j < numCols - 1; ++j) {
662  gcd = presburger::gcd(gcd, abs(atEq(i, j)));
663  }
664  MPInt v = abs(atEq(i, numCols - 1));
665  if (gcd > 0 && (v % gcd != 0)) {
666  return true;
667  }
668  }
669  return false;
670 }
671 
672 // Returns a matrix where each row is a vector along which the polytope is
673 // bounded. The span of the returned vectors is guaranteed to contain all
674 // such vectors. The returned vectors are NOT guaranteed to be linearly
675 // independent. This function should not be called on empty sets.
676 //
677 // It is sufficient to check the perpendiculars of the constraints, as the set
678 // of perpendiculars which are bounded must span all bounded directions.
680  // Note that it is necessary to add the equalities too (which the constructor
681  // does) even though we don't need to check if they are bounded; whether an
682  // inequality is bounded or not depends on what other constraints, including
683  // equalities, are present.
684  Simplex simplex(*this);
685 
686  assert(!simplex.isEmpty() && "It is not meaningful to ask whether a "
687  "direction is bounded in an empty set.");
688 
689  SmallVector<unsigned, 8> boundedIneqs;
690  // The constructor adds the inequalities to the simplex first, so this
691  // processes all the inequalities.
692  for (unsigned i = 0, e = getNumInequalities(); i < e; ++i) {
693  if (simplex.isBoundedAlongConstraint(i))
694  boundedIneqs.push_back(i);
695  }
696 
697  // The direction vector is given by the coefficients and does not include the
698  // constant term, so the matrix has one fewer column.
699  unsigned dirsNumCols = getNumCols() - 1;
700  Matrix dirs(boundedIneqs.size() + getNumEqualities(), dirsNumCols);
701 
702  // Copy the bounded inequalities.
703  unsigned row = 0;
704  for (unsigned i : boundedIneqs) {
705  for (unsigned col = 0; col < dirsNumCols; ++col)
706  dirs(row, col) = atIneq(i, col);
707  ++row;
708  }
709 
710  // Copy the equalities. All the equalities' perpendiculars are bounded.
711  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i) {
712  for (unsigned col = 0; col < dirsNumCols; ++col)
713  dirs(row, col) = atEq(i, col);
714  ++row;
715  }
716 
717  return dirs;
718 }
719 
721 
722 /// Let this set be S. If S is bounded then we directly call into the GBR
723 /// sampling algorithm. Otherwise, there are some unbounded directions, i.e.,
724 /// vectors v such that S extends to infinity along v or -v. In this case we
725 /// use an algorithm described in the integer set library (isl) manual and used
726 /// by the isl_set_sample function in that library. The algorithm is:
727 ///
728 /// 1) Apply a unimodular transform T to S to obtain S*T, such that all
729 /// dimensions in which S*T is bounded lie in the linear span of a prefix of the
730 /// dimensions.
731 ///
732 /// 2) Construct a set B by removing all constraints that involve
733 /// the unbounded dimensions and then deleting the unbounded dimensions. Note
734 /// that B is a Bounded set.
735 ///
736 /// 3) Try to obtain a sample from B using the GBR sampling
737 /// algorithm. If no sample is found, return that S is empty.
738 ///
739 /// 4) Otherwise, substitute the obtained sample into S*T to obtain a set
740 /// C. C is a full-dimensional Cone and always contains a sample.
741 ///
742 /// 5) Obtain an integer sample from C.
743 ///
744 /// 6) Return T*v, where v is the concatenation of the samples from B and C.
745 ///
746 /// The following is a sketch of a proof that
747 /// a) If the algorithm returns empty, then S is empty.
748 /// b) If the algorithm returns a sample, it is a valid sample in S.
749 ///
750 /// The algorithm returns empty only if B is empty, in which case S*T is
751 /// certainly empty since B was obtained by removing constraints and then
752 /// deleting unconstrained dimensions from S*T. Since T is unimodular, a vector
753 /// v is in S*T iff T*v is in S. So in this case, since
754 /// S*T is empty, S is empty too.
755 ///
756 /// Otherwise, the algorithm substitutes the sample from B into S*T. All the
757 /// constraints of S*T that did not involve unbounded dimensions are satisfied
758 /// by this substitution. All dimensions in the linear span of the dimensions
759 /// outside the prefix are unbounded in S*T (step 1). Substituting values for
760 /// the bounded dimensions cannot make these dimensions bounded, and these are
761 /// the only remaining dimensions in C, so C is unbounded along every vector (in
762 /// the positive or negative direction, or both). C is hence a full-dimensional
763 /// cone and therefore always contains an integer point.
764 ///
765 /// Concatenating the samples from B and C gives a sample v in S*T, so the
766 /// returned sample T*v is a sample in S.
767 std::optional<SmallVector<MPInt, 8>>
769  // First, try the GCD test heuristic.
770  if (isEmptyByGCDTest())
771  return {};
772 
773  Simplex simplex(*this);
774  if (simplex.isEmpty())
775  return {};
776 
777  // For a bounded set, we directly call into the GBR sampling algorithm.
778  if (!simplex.isUnbounded())
779  return simplex.findIntegerSample();
780 
781  // The set is unbounded. We cannot directly use the GBR algorithm.
782  //
783  // m is a matrix containing, in each row, a vector in which S is
784  // bounded, such that the linear span of all these dimensions contains all
785  // bounded dimensions in S.
787  // In column echelon form, each row of m occupies only the first rank(m)
788  // columns and has zeros on the other columns. The transform T that brings S
789  // to column echelon form is unimodular as well, so this is a suitable
790  // transform to use in step 1 of the algorithm.
791  std::pair<unsigned, LinearTransform> result =
793  const LinearTransform &transform = result.second;
794  // 1) Apply T to S to obtain S*T.
795  IntegerRelation transformedSet = transform.applyTo(*this);
796 
797  // 2) Remove the unbounded dimensions and constraints involving them to
798  // obtain a bounded set.
799  IntegerRelation boundedSet(transformedSet);
800  unsigned numBoundedDims = result.first;
801  unsigned numUnboundedDims = getNumVars() - numBoundedDims;
802  removeConstraintsInvolvingVarRange(boundedSet, numBoundedDims,
803  numUnboundedDims);
804  boundedSet.removeVarRange(numBoundedDims, boundedSet.getNumVars());
805 
806  // 3) Try to obtain a sample from the bounded set.
807  std::optional<SmallVector<MPInt, 8>> boundedSample =
808  Simplex(boundedSet).findIntegerSample();
809  if (!boundedSample)
810  return {};
811  assert(boundedSet.containsPoint(*boundedSample) &&
812  "Simplex returned an invalid sample!");
813 
814  // 4) Substitute the values of the bounded dimensions into S*T to obtain a
815  // full-dimensional cone, which necessarily contains an integer sample.
816  transformedSet.setAndEliminate(0, *boundedSample);
817  IntegerRelation &cone = transformedSet;
818 
819  // 5) Obtain an integer sample from the cone.
820  //
821  // We shrink the cone such that for any rational point in the shrunken cone,
822  // rounding up each of the point's coordinates produces a point that still
823  // lies in the original cone.
824  //
825  // Rounding up a point x adds a number e_i in [0, 1) to each coordinate x_i.
826  // For each inequality sum_i a_i x_i + c >= 0 in the original cone, the
827  // shrunken cone will have the inequality tightened by some amount s, such
828  // that if x satisfies the shrunken cone's tightened inequality, then x + e
829  // satisfies the original inequality, i.e.,
830  //
831  // sum_i a_i x_i + c + s >= 0 implies sum_i a_i (x_i + e_i) + c >= 0
832  //
833  // for any e_i values in [0, 1). In fact, we will handle the slightly more
834  // general case where e_i can be in [0, 1]. For example, consider the
835  // inequality 2x_1 - 3x_2 - 7x_3 - 6 >= 0, and let x = (3, 0, 0). How low
836  // could the LHS go if we added a number in [0, 1] to each coordinate? The LHS
837  // is minimized when we add 1 to the x_i with negative coefficient a_i and
838  // keep the other x_i the same. In the example, we would get x = (3, 1, 1),
839  // changing the value of the LHS by -3 + -7 = -10.
840  //
841  // In general, the value of the LHS can change by at most the sum of the
842  // negative a_i, so we accomodate this by shifting the inequality by this
843  // amount for the shrunken cone.
844  for (unsigned i = 0, e = cone.getNumInequalities(); i < e; ++i) {
845  for (unsigned j = 0; j < cone.getNumVars(); ++j) {
846  MPInt coeff = cone.atIneq(i, j);
847  if (coeff < 0)
848  cone.atIneq(i, cone.getNumVars()) += coeff;
849  }
850  }
851 
852  // Obtain an integer sample in the cone by rounding up a rational point from
853  // the shrunken cone. Shrinking the cone amounts to shifting its apex
854  // "inwards" without changing its "shape"; the shrunken cone is still a
855  // full-dimensional cone and is hence non-empty.
856  Simplex shrunkenConeSimplex(cone);
857  assert(!shrunkenConeSimplex.isEmpty() && "Shrunken cone cannot be empty!");
858 
859  // The sample will always exist since the shrunken cone is non-empty.
860  SmallVector<Fraction, 8> shrunkenConeSample =
861  *shrunkenConeSimplex.getRationalSample();
862 
863  SmallVector<MPInt, 8> coneSample(llvm::map_range(shrunkenConeSample, ceil));
864 
865  // 6) Return transform * concat(boundedSample, coneSample).
866  SmallVector<MPInt, 8> &sample = *boundedSample;
867  sample.append(coneSample.begin(), coneSample.end());
868  return transform.postMultiplyWithColumn(sample);
869 }
870 
871 /// Helper to evaluate an affine expression at a point.
872 /// The expression is a list of coefficients for the dimensions followed by the
873 /// constant term.
875  assert(expr.size() == 1 + point.size() &&
876  "Dimensionalities of point and expression don't match!");
877  MPInt value = expr.back();
878  for (unsigned i = 0; i < point.size(); ++i)
879  value += expr[i] * point[i];
880  return value;
881 }
882 
883 /// A point satisfies an equality iff the value of the equality at the
884 /// expression is zero, and it satisfies an inequality iff the value of the
885 /// inequality at that point is non-negative.
887  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i) {
888  if (valueAt(getEquality(i), point) != 0)
889  return false;
890  }
891  for (unsigned i = 0, e = getNumInequalities(); i < e; ++i) {
892  if (valueAt(getInequality(i), point) < 0)
893  return false;
894  }
895  return true;
896 }
897 
898 /// Just substitute the values given and check if an integer sample exists for
899 /// the local vars.
900 ///
901 /// TODO: this could be made more efficient by handling divisions separately.
902 /// Instead of finding an integer sample over all the locals, we can first
903 /// compute the values of the locals that have division representations and
904 /// only use the integer emptiness check for the locals that don't have this.
905 /// Handling this correctly requires ordering the divs, though.
906 std::optional<SmallVector<MPInt, 8>>
908  assert(point.size() == getNumVars() - getNumLocalVars() &&
909  "Point should contain all vars except locals!");
911  "This function depends on locals being stored last!");
912  IntegerRelation copy = *this;
913  copy.setAndEliminate(0, point);
914  return copy.findIntegerSample();
915 }
916 
918 IntegerRelation::getLocalReprs(std::vector<MaybeLocalRepr> *repr) const {
919  SmallVector<bool, 8> foundRepr(getNumVars(), false);
920  for (unsigned i = 0, e = getNumDimAndSymbolVars(); i < e; ++i)
921  foundRepr[i] = true;
922 
923  unsigned localOffset = getVarKindOffset(VarKind::Local);
925  bool changed;
926  do {
927  // Each time changed is true, at end of this iteration, one or more local
928  // vars have been detected as floor divs.
929  changed = false;
930  for (unsigned i = 0, e = getNumLocalVars(); i < e; ++i) {
931  if (!foundRepr[i + localOffset]) {
932  MaybeLocalRepr res =
933  computeSingleVarRepr(*this, foundRepr, localOffset + i,
934  divs.getDividend(i), divs.getDenom(i));
935  if (!res) {
936  // No representation was found, so clear the representation and
937  // continue.
938  divs.clearRepr(i);
939  continue;
940  }
941  foundRepr[localOffset + i] = true;
942  if (repr)
943  (*repr)[i] = res;
944  changed = true;
945  }
946  }
947  } while (changed);
948 
949  return divs;
950 }
951 
952 /// Tightens inequalities given that we are dealing with integer spaces. This is
953 /// analogous to the GCD test but applied to inequalities. The constant term can
954 /// be reduced to the preceding multiple of the GCD of the coefficients, i.e.,
955 /// 64*i - 100 >= 0 => 64*i - 128 >= 0 (since 'i' is an integer). This is a
956 /// fast method - linear in the number of coefficients.
957 // Example on how this affects practical cases: consider the scenario:
958 // 64*i >= 100, j = 64*i; without a tightening, elimination of i would yield
959 // j >= 100 instead of the tighter (exact) j >= 128.
961  unsigned numCols = getNumCols();
962  for (unsigned i = 0, e = getNumInequalities(); i < e; ++i) {
963  // Normalize the constraint and tighten the constant term by the GCD.
965  if (gcd > 1)
966  atIneq(i, numCols - 1) = floorDiv(atIneq(i, numCols - 1), gcd);
967  }
968 }
969 
970 // Eliminates all variable variables in column range [posStart, posLimit).
971 // Returns the number of variables eliminated.
972 unsigned IntegerRelation::gaussianEliminateVars(unsigned posStart,
973  unsigned posLimit) {
974  // Return if variable positions to eliminate are out of range.
975  assert(posLimit <= getNumVars());
976  assert(hasConsistentState());
977 
978  if (posStart >= posLimit)
979  return 0;
980 
982 
983  unsigned pivotCol = 0;
984  for (pivotCol = posStart; pivotCol < posLimit; ++pivotCol) {
985  // Find a row which has a non-zero coefficient in column 'j'.
986  unsigned pivotRow;
987  if (!findConstraintWithNonZeroAt(pivotCol, /*isEq=*/true, &pivotRow)) {
988  // No pivot row in equalities with non-zero at 'pivotCol'.
989  if (!findConstraintWithNonZeroAt(pivotCol, /*isEq=*/false, &pivotRow)) {
990  // If inequalities are also non-zero in 'pivotCol', it can be
991  // eliminated.
992  continue;
993  }
994  break;
995  }
996 
997  // Eliminate variable at 'pivotCol' from each equality row.
998  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i) {
999  eliminateFromConstraint(this, i, pivotRow, pivotCol, posStart,
1000  /*isEq=*/true);
1002  }
1003 
1004  // Eliminate variable at 'pivotCol' from each inequality row.
1005  for (unsigned i = 0, e = getNumInequalities(); i < e; ++i) {
1006  eliminateFromConstraint(this, i, pivotRow, pivotCol, posStart,
1007  /*isEq=*/false);
1009  }
1010  removeEquality(pivotRow);
1012  }
1013  // Update position limit based on number eliminated.
1014  posLimit = pivotCol;
1015  // Remove eliminated columns from all constraints.
1016  removeVarRange(posStart, posLimit);
1017  return posLimit - posStart;
1018 }
1019 
1020 // A more complex check to eliminate redundant inequalities. Uses FourierMotzkin
1021 // to check if a constraint is redundant.
1023  SmallVector<bool, 32> redun(getNumInequalities(), false);
1024  // To check if an inequality is redundant, we replace the inequality by its
1025  // complement (for eg., i - 1 >= 0 by i <= 0), and check if the resulting
1026  // system is empty. If it is, the inequality is redundant.
1027  IntegerRelation tmpCst(*this);
1028  for (unsigned r = 0, e = getNumInequalities(); r < e; r++) {
1029  // Change the inequality to its complement.
1030  tmpCst.inequalities.negateRow(r);
1031  --tmpCst.atIneq(r, tmpCst.getNumCols() - 1);
1032  if (tmpCst.isEmpty()) {
1033  redun[r] = true;
1034  // Zero fill the redundant inequality.
1035  inequalities.fillRow(r, /*value=*/0);
1036  tmpCst.inequalities.fillRow(r, /*value=*/0);
1037  } else {
1038  // Reverse the change (to avoid recreating tmpCst each time).
1039  ++tmpCst.atIneq(r, tmpCst.getNumCols() - 1);
1040  tmpCst.inequalities.negateRow(r);
1041  }
1042  }
1043 
1044  unsigned pos = 0;
1045  for (unsigned r = 0, e = getNumInequalities(); r < e; ++r) {
1046  if (!redun[r])
1047  inequalities.copyRow(r, pos++);
1048  }
1050 }
1051 
1052 // A more complex check to eliminate redundant inequalities and equalities. Uses
1053 // Simplex to check if a constraint is redundant.
1055  // First, we run gcdTightenInequalities. This allows us to catch some
1056  // constraints which are not redundant when considering rational solutions
1057  // but are redundant in terms of integer solutions.
1059  Simplex simplex(*this);
1060  simplex.detectRedundant();
1061 
1062  unsigned pos = 0;
1063  unsigned numIneqs = getNumInequalities();
1064  // Scan to get rid of all inequalities marked redundant, in-place. In Simplex,
1065  // the first constraints added are the inequalities.
1066  for (unsigned r = 0; r < numIneqs; r++) {
1067  if (!simplex.isMarkedRedundant(r))
1068  inequalities.copyRow(r, pos++);
1069  }
1071 
1072  // Scan to get rid of all equalities marked redundant, in-place. In Simplex,
1073  // after the inequalities, a pair of constraints for each equality is added.
1074  // An equality is redundant if both the inequalities in its pair are
1075  // redundant.
1076  pos = 0;
1077  for (unsigned r = 0, e = getNumEqualities(); r < e; r++) {
1078  if (!(simplex.isMarkedRedundant(numIneqs + 2 * r) &&
1079  simplex.isMarkedRedundant(numIneqs + 2 * r + 1)))
1080  equalities.copyRow(r, pos++);
1081  }
1083 }
1084 
1085 std::optional<MPInt> IntegerRelation::computeVolume() const {
1086  assert(getNumSymbolVars() == 0 && "Symbols are not yet supported!");
1087 
1088  Simplex simplex(*this);
1089  // If the polytope is rationally empty, there are certainly no integer
1090  // points.
1091  if (simplex.isEmpty())
1092  return MPInt(0);
1093 
1094  // Just find the maximum and minimum integer value of each non-local var
1095  // separately, thus finding the number of integer values each such var can
1096  // take. Multiplying these together gives a valid overapproximation of the
1097  // number of integer points in the relation. The result this gives is
1098  // equivalent to projecting (rationally) the relation onto its non-local vars
1099  // and returning the number of integer points in a minimal axis-parallel
1100  // hyperrectangular overapproximation of that.
1101  //
1102  // We also handle the special case where one dimension is unbounded and
1103  // another dimension can take no integer values. In this case, the volume is
1104  // zero.
1105  //
1106  // If there is no such empty dimension, if any dimension is unbounded we
1107  // just return the result as unbounded.
1108  MPInt count(1);
1109  SmallVector<MPInt, 8> dim(getNumVars() + 1);
1110  bool hasUnboundedVar = false;
1111  for (unsigned i = 0, e = getNumDimAndSymbolVars(); i < e; ++i) {
1112  dim[i] = 1;
1113  auto [min, max] = simplex.computeIntegerBounds(dim);
1114  dim[i] = 0;
1115 
1116  assert((!min.isEmpty() && !max.isEmpty()) &&
1117  "Polytope should be rationally non-empty!");
1118 
1119  // One of the dimensions is unbounded. Note this fact. We will return
1120  // unbounded if none of the other dimensions makes the volume zero.
1121  if (min.isUnbounded() || max.isUnbounded()) {
1122  hasUnboundedVar = true;
1123  continue;
1124  }
1125 
1126  // In this case there are no valid integer points and the volume is
1127  // definitely zero.
1128  if (min.getBoundedOptimum() > max.getBoundedOptimum())
1129  return MPInt(0);
1130 
1131  count *= (*max - *min + 1);
1132  }
1133 
1134  if (count == 0)
1135  return MPInt(0);
1136  if (hasUnboundedVar)
1137  return {};
1138  return count;
1139 }
1140 
1141 void IntegerRelation::eliminateRedundantLocalVar(unsigned posA, unsigned posB) {
1142  assert(posA < getNumLocalVars() && "Invalid local var position");
1143  assert(posB < getNumLocalVars() && "Invalid local var position");
1144 
1145  unsigned localOffset = getVarKindOffset(VarKind::Local);
1146  posA += localOffset;
1147  posB += localOffset;
1148  inequalities.addToColumn(posB, posA, 1);
1149  equalities.addToColumn(posB, posA, 1);
1150  removeVar(posB);
1151 }
1152 
1153 /// Adds additional local ids to the sets such that they both have the union
1154 /// of the local ids in each set, without changing the set of points that
1155 /// lie in `this` and `other`.
1156 ///
1157 /// To detect local ids that always take the same value, each local id is
1158 /// represented as a floordiv with constant denominator in terms of other ids.
1159 /// After extracting these divisions, local ids in `other` with the same
1160 /// division representation as some other local id in any set are considered
1161 /// duplicate and are merged.
1162 ///
1163 /// It is possible that division representation for some local id cannot be
1164 /// obtained, and thus these local ids are not considered for detecting
1165 /// duplicates.
1167  IntegerRelation &relA = *this;
1168  IntegerRelation &relB = other;
1169 
1170  unsigned oldALocals = relA.getNumLocalVars();
1171 
1172  // Merge function that merges the local variables in both sets by treating
1173  // them as the same variable.
1174  auto merge = [&relA, &relB, oldALocals](unsigned i, unsigned j) -> bool {
1175  // We only merge from local at pos j to local at pos i, where j > i.
1176  if (i >= j)
1177  return false;
1178 
1179  // If i < oldALocals, we are trying to merge duplicate divs. Since we do not
1180  // want to merge duplicates in A, we ignore this call.
1181  if (j < oldALocals)
1182  return false;
1183 
1184  // Merge local at pos j into local at position i.
1185  relA.eliminateRedundantLocalVar(i, j);
1186  relB.eliminateRedundantLocalVar(i, j);
1187  return true;
1188  };
1189 
1190  presburger::mergeLocalVars(*this, other, merge);
1191 
1192  // Since we do not remove duplicate divisions in relA, this is guranteed to be
1193  // non-negative.
1194  return relA.getNumLocalVars() - oldALocals;
1195 }
1196 
1198  return getLocalReprs().hasAllReprs();
1199 }
1200 
1202  DivisionRepr divs = getLocalReprs();
1203  auto merge = [this](unsigned i, unsigned j) -> bool {
1205  return true;
1206  };
1207  divs.removeDuplicateDivs(merge);
1208 }
1209 
1210 /// Removes local variables using equalities. Each equality is checked if it
1211 /// can be reduced to the form: `e = affine-expr`, where `e` is a local
1212 /// variable and `affine-expr` is an affine expression not containing `e`.
1213 /// If an equality satisfies this form, the local variable is replaced in
1214 /// each constraint and then removed. The equality used to replace this local
1215 /// variable is also removed.
1217  // Normalize the equality constraints to reduce coefficients of local
1218  // variables to 1 wherever possible.
1219  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i)
1221 
1222  while (true) {
1223  unsigned i, e, j, f;
1224  for (i = 0, e = getNumEqualities(); i < e; ++i) {
1225  // Find a local variable to eliminate using ith equality.
1226  for (j = getNumDimAndSymbolVars(), f = getNumVars(); j < f; ++j)
1227  if (abs(atEq(i, j)) == 1)
1228  break;
1229 
1230  // Local variable can be eliminated using ith equality.
1231  if (j < f)
1232  break;
1233  }
1234 
1235  // No equality can be used to eliminate a local variable.
1236  if (i == e)
1237  break;
1238 
1239  // Use the ith equality to simplify other equalities. If any changes
1240  // are made to an equality constraint, it is normalized by GCD.
1241  for (unsigned k = 0, t = getNumEqualities(); k < t; ++k) {
1242  if (atEq(k, j) != 0) {
1243  eliminateFromConstraint(this, k, i, j, j, /*isEq=*/true);
1245  }
1246  }
1247 
1248  // Use the ith equality to simplify inequalities.
1249  for (unsigned k = 0, t = getNumInequalities(); k < t; ++k)
1250  eliminateFromConstraint(this, k, i, j, j, /*isEq=*/false);
1251 
1252  // Remove the ith equality and the found local variable.
1253  removeVar(j);
1254  removeEquality(i);
1255  }
1256 }
1257 
1258 void IntegerRelation::convertVarKind(VarKind srcKind, unsigned varStart,
1259  unsigned varLimit, VarKind dstKind,
1260  unsigned pos) {
1261  assert(varLimit <= getNumVarKind(srcKind) && "Invalid id range");
1262 
1263  if (varStart >= varLimit)
1264  return;
1265 
1266  // Append new local variables corresponding to the dimensions to be converted.
1267  unsigned convertCount = varLimit - varStart;
1268  unsigned newVarsBegin = insertVar(dstKind, pos, convertCount);
1269 
1270  // Swap the new local variables with dimensions.
1271  //
1272  // Essentially, this moves the information corresponding to the specified ids
1273  // of kind `srcKind` to the `convertCount` newly created ids of kind
1274  // `dstKind`. In particular, this moves the columns in the constraint
1275  // matrices, and zeros out the initially occupied columns (because the newly
1276  // created ids we're swapping with were zero-initialized).
1277  unsigned offset = getVarKindOffset(srcKind);
1278  for (unsigned i = 0; i < convertCount; ++i)
1279  swapVar(offset + varStart + i, newVarsBegin + i);
1280 
1281  // Complete the move by deleting the initially occupied columns.
1282  removeVarRange(srcKind, varStart, varLimit);
1283 }
1284 
1285 void IntegerRelation::addBound(BoundType type, unsigned pos,
1286  const MPInt &value) {
1287  assert(pos < getNumCols());
1288  if (type == BoundType::EQ) {
1289  unsigned row = equalities.appendExtraRow();
1290  equalities(row, pos) = 1;
1291  equalities(row, getNumCols() - 1) = -value;
1292  } else {
1293  unsigned row = inequalities.appendExtraRow();
1294  inequalities(row, pos) = type == BoundType::LB ? 1 : -1;
1295  inequalities(row, getNumCols() - 1) =
1296  type == BoundType::LB ? -value : value;
1297  }
1298 }
1299 
1301  const MPInt &value) {
1302  assert(type != BoundType::EQ && "EQ not implemented");
1303  assert(expr.size() == getNumCols());
1304  unsigned row = inequalities.appendExtraRow();
1305  for (unsigned i = 0, e = expr.size(); i < e; ++i)
1306  inequalities(row, i) = type == BoundType::LB ? expr[i] : -expr[i];
1308  type == BoundType::LB ? -value : value;
1309 }
1310 
1311 /// Adds a new local variable as the floordiv of an affine function of other
1312 /// variables, the coefficients of which are provided in 'dividend' and with
1313 /// respect to a positive constant 'divisor'. Two constraints are added to the
1314 /// system to capture equivalence with the floordiv.
1315 /// q = expr floordiv c <=> c*q <= expr <= c*q + c - 1.
1317  const MPInt &divisor) {
1318  assert(dividend.size() == getNumCols() && "incorrect dividend size");
1319  assert(divisor > 0 && "positive divisor expected");
1320 
1322 
1323  SmallVector<MPInt, 8> dividendCopy(dividend.begin(), dividend.end());
1324  dividendCopy.insert(dividendCopy.end() - 1, MPInt(0));
1325  addInequality(
1326  getDivLowerBound(dividendCopy, divisor, dividendCopy.size() - 2));
1327  addInequality(
1328  getDivUpperBound(dividendCopy, divisor, dividendCopy.size() - 2));
1329 }
1330 
1331 /// Finds an equality that equates the specified variable to a constant.
1332 /// Returns the position of the equality row. If 'symbolic' is set to true,
1333 /// symbols are also treated like a constant, i.e., an affine function of the
1334 /// symbols is also treated like a constant. Returns -1 if such an equality
1335 /// could not be found.
1336 static int findEqualityToConstant(const IntegerRelation &cst, unsigned pos,
1337  bool symbolic = false) {
1338  assert(pos < cst.getNumVars() && "invalid position");
1339  for (unsigned r = 0, e = cst.getNumEqualities(); r < e; r++) {
1340  MPInt v = cst.atEq(r, pos);
1341  if (v * v != 1)
1342  continue;
1343  unsigned c;
1344  unsigned f = symbolic ? cst.getNumDimVars() : cst.getNumVars();
1345  // This checks for zeros in all positions other than 'pos' in [0, f)
1346  for (c = 0; c < f; c++) {
1347  if (c == pos)
1348  continue;
1349  if (cst.atEq(r, c) != 0) {
1350  // Dependent on another variable.
1351  break;
1352  }
1353  }
1354  if (c == f)
1355  // Equality is free of other variables.
1356  return r;
1357  }
1358  return -1;
1359 }
1360 
1362  assert(pos < getNumVars() && "invalid position");
1363  int rowIdx;
1364  if ((rowIdx = findEqualityToConstant(*this, pos)) == -1)
1365  return failure();
1366 
1367  // atEq(rowIdx, pos) is either -1 or 1.
1368  assert(atEq(rowIdx, pos) * atEq(rowIdx, pos) == 1);
1369  MPInt constVal = -atEq(rowIdx, getNumCols() - 1) / atEq(rowIdx, pos);
1370  setAndEliminate(pos, constVal);
1371  return success();
1372 }
1373 
1374 void IntegerRelation::constantFoldVarRange(unsigned pos, unsigned num) {
1375  for (unsigned s = pos, t = pos, e = pos + num; s < e; s++) {
1376  if (failed(constantFoldVar(t)))
1377  t++;
1378  }
1379 }
1380 
1381 /// Returns a non-negative constant bound on the extent (upper bound - lower
1382 /// bound) of the specified variable if it is found to be a constant; returns
1383 /// std::nullopt if it's not a constant. This methods treats symbolic variables
1384 /// specially, i.e., it looks for constant differences between affine
1385 /// expressions involving only the symbolic variables. See comments at function
1386 /// definition for example. 'lb', if provided, is set to the lower bound
1387 /// associated with the constant difference. Note that 'lb' is purely symbolic
1388 /// and thus will contain the coefficients of the symbolic variables and the
1389 /// constant coefficient.
1390 // Egs: 0 <= i <= 15, return 16.
1391 // s0 + 2 <= i <= s0 + 17, returns 16. (s0 has to be a symbol)
1392 // s0 + s1 + 16 <= d0 <= s0 + s1 + 31, returns 16.
1393 // s0 - 7 <= 8*j <= s0 returns 1 with lb = s0, lbDivisor = 8 (since lb =
1394 // ceil(s0 - 7 / 8) = floor(s0 / 8)).
1396  unsigned pos, SmallVectorImpl<MPInt> *lb, MPInt *boundFloorDivisor,
1397  SmallVectorImpl<MPInt> *ub, unsigned *minLbPos, unsigned *minUbPos) const {
1398  assert(pos < getNumDimVars() && "Invalid variable position");
1399 
1400  // Find an equality for 'pos'^th variable that equates it to some function
1401  // of the symbolic variables (+ constant).
1402  int eqPos = findEqualityToConstant(*this, pos, /*symbolic=*/true);
1403  if (eqPos != -1) {
1404  auto eq = getEquality(eqPos);
1405  // If the equality involves a local var, punt for now.
1406  // TODO: this can be handled in the future by using the explicit
1407  // representation of the local vars.
1408  if (!std::all_of(eq.begin() + getNumDimAndSymbolVars(), eq.end() - 1,
1409  [](const MPInt &coeff) { return coeff == 0; }))
1410  return std::nullopt;
1411 
1412  // This variable can only take a single value.
1413  if (lb) {
1414  // Set lb to that symbolic value.
1415  lb->resize(getNumSymbolVars() + 1);
1416  if (ub)
1417  ub->resize(getNumSymbolVars() + 1);
1418  for (unsigned c = 0, f = getNumSymbolVars() + 1; c < f; c++) {
1419  MPInt v = atEq(eqPos, pos);
1420  // atEq(eqRow, pos) is either -1 or 1.
1421  assert(v * v == 1);
1422  (*lb)[c] = v < 0 ? atEq(eqPos, getNumDimVars() + c) / -v
1423  : -atEq(eqPos, getNumDimVars() + c) / v;
1424  // Since this is an equality, ub = lb.
1425  if (ub)
1426  (*ub)[c] = (*lb)[c];
1427  }
1428  assert(boundFloorDivisor &&
1429  "both lb and divisor or none should be provided");
1430  *boundFloorDivisor = 1;
1431  }
1432  if (minLbPos)
1433  *minLbPos = eqPos;
1434  if (minUbPos)
1435  *minUbPos = eqPos;
1436  return MPInt(1);
1437  }
1438 
1439  // Check if the variable appears at all in any of the inequalities.
1440  unsigned r, e;
1441  for (r = 0, e = getNumInequalities(); r < e; r++) {
1442  if (atIneq(r, pos) != 0)
1443  break;
1444  }
1445  if (r == e)
1446  // If it doesn't, there isn't a bound on it.
1447  return std::nullopt;
1448 
1449  // Positions of constraints that are lower/upper bounds on the variable.
1450  SmallVector<unsigned, 4> lbIndices, ubIndices;
1451 
1452  // Gather all symbolic lower bounds and upper bounds of the variable, i.e.,
1453  // the bounds can only involve symbolic (and local) variables. Since the
1454  // canonical form c_1*x_1 + c_2*x_2 + ... + c_0 >= 0, a constraint is a lower
1455  // bound for x_i if c_i >= 1, and an upper bound if c_i <= -1.
1456  getLowerAndUpperBoundIndices(pos, &lbIndices, &ubIndices,
1457  /*eqIndices=*/nullptr, /*offset=*/0,
1458  /*num=*/getNumDimVars());
1459 
1460  std::optional<MPInt> minDiff;
1461  unsigned minLbPosition = 0, minUbPosition = 0;
1462  for (auto ubPos : ubIndices) {
1463  for (auto lbPos : lbIndices) {
1464  // Look for a lower bound and an upper bound that only differ by a
1465  // constant, i.e., pairs of the form 0 <= c_pos - f(c_i's) <= diffConst.
1466  // For example, if ii is the pos^th variable, we are looking for
1467  // constraints like ii >= i, ii <= ii + 50, 50 being the difference. The
1468  // minimum among all such constant differences is kept since that's the
1469  // constant bounding the extent of the pos^th variable.
1470  unsigned j, e;
1471  for (j = 0, e = getNumCols() - 1; j < e; j++)
1472  if (atIneq(ubPos, j) != -atIneq(lbPos, j)) {
1473  break;
1474  }
1475  if (j < getNumCols() - 1)
1476  continue;
1477  MPInt diff = ceilDiv(atIneq(ubPos, getNumCols() - 1) +
1478  atIneq(lbPos, getNumCols() - 1) + 1,
1479  atIneq(lbPos, pos));
1480  // This bound is non-negative by definition.
1481  diff = std::max<MPInt>(diff, MPInt(0));
1482  if (minDiff == std::nullopt || diff < minDiff) {
1483  minDiff = diff;
1484  minLbPosition = lbPos;
1485  minUbPosition = ubPos;
1486  }
1487  }
1488  }
1489  if (lb && minDiff) {
1490  // Set lb to the symbolic lower bound.
1491  lb->resize(getNumSymbolVars() + 1);
1492  if (ub)
1493  ub->resize(getNumSymbolVars() + 1);
1494  // The lower bound is the ceildiv of the lb constraint over the coefficient
1495  // of the variable at 'pos'. We express the ceildiv equivalently as a floor
1496  // for uniformity. For eg., if the lower bound constraint was: 32*d0 - N +
1497  // 31 >= 0, the lower bound for d0 is ceil(N - 31, 32), i.e., floor(N, 32).
1498  *boundFloorDivisor = atIneq(minLbPosition, pos);
1499  assert(*boundFloorDivisor == -atIneq(minUbPosition, pos));
1500  for (unsigned c = 0, e = getNumSymbolVars() + 1; c < e; c++) {
1501  (*lb)[c] = -atIneq(minLbPosition, getNumDimVars() + c);
1502  }
1503  if (ub) {
1504  for (unsigned c = 0, e = getNumSymbolVars() + 1; c < e; c++)
1505  (*ub)[c] = atIneq(minUbPosition, getNumDimVars() + c);
1506  }
1507  // The lower bound leads to a ceildiv while the upper bound is a floordiv
1508  // whenever the coefficient at pos != 1. ceildiv (val / d) = floordiv (val +
1509  // d - 1 / d); hence, the addition of 'atIneq(minLbPosition, pos) - 1' to
1510  // the constant term for the lower bound.
1511  (*lb)[getNumSymbolVars()] += atIneq(minLbPosition, pos) - 1;
1512  }
1513  if (minLbPos)
1514  *minLbPos = minLbPosition;
1515  if (minUbPos)
1516  *minUbPos = minUbPosition;
1517  return minDiff;
1518 }
1519 
1520 template <bool isLower>
1521 std::optional<MPInt>
1523  assert(pos < getNumVars() && "invalid position");
1524  // Project to 'pos'.
1525  projectOut(0, pos);
1526  projectOut(1, getNumVars() - 1);
1527  // Check if there's an equality equating the '0'^th variable to a constant.
1528  int eqRowIdx = findEqualityToConstant(*this, 0, /*symbolic=*/false);
1529  if (eqRowIdx != -1)
1530  // atEq(rowIdx, 0) is either -1 or 1.
1531  return -atEq(eqRowIdx, getNumCols() - 1) / atEq(eqRowIdx, 0);
1532 
1533  // Check if the variable appears at all in any of the inequalities.
1534  unsigned r, e;
1535  for (r = 0, e = getNumInequalities(); r < e; r++) {
1536  if (atIneq(r, 0) != 0)
1537  break;
1538  }
1539  if (r == e)
1540  // If it doesn't, there isn't a bound on it.
1541  return std::nullopt;
1542 
1543  std::optional<MPInt> minOrMaxConst;
1544 
1545  // Take the max across all const lower bounds (or min across all constant
1546  // upper bounds).
1547  for (unsigned r = 0, e = getNumInequalities(); r < e; r++) {
1548  if (isLower) {
1549  if (atIneq(r, 0) <= 0)
1550  // Not a lower bound.
1551  continue;
1552  } else if (atIneq(r, 0) >= 0) {
1553  // Not an upper bound.
1554  continue;
1555  }
1556  unsigned c, f;
1557  for (c = 0, f = getNumCols() - 1; c < f; c++)
1558  if (c != 0 && atIneq(r, c) != 0)
1559  break;
1560  if (c < getNumCols() - 1)
1561  // Not a constant bound.
1562  continue;
1563 
1564  MPInt boundConst =
1565  isLower ? ceilDiv(-atIneq(r, getNumCols() - 1), atIneq(r, 0))
1566  : floorDiv(atIneq(r, getNumCols() - 1), -atIneq(r, 0));
1567  if (isLower) {
1568  if (minOrMaxConst == std::nullopt || boundConst > minOrMaxConst)
1569  minOrMaxConst = boundConst;
1570  } else {
1571  if (minOrMaxConst == std::nullopt || boundConst < minOrMaxConst)
1572  minOrMaxConst = boundConst;
1573  }
1574  }
1575  return minOrMaxConst;
1576 }
1577 
1579  unsigned pos) const {
1580  if (type == BoundType::LB)
1581  return IntegerRelation(*this)
1582  .computeConstantLowerOrUpperBound</*isLower=*/true>(pos);
1583  if (type == BoundType::UB)
1584  return IntegerRelation(*this)
1585  .computeConstantLowerOrUpperBound</*isLower=*/false>(pos);
1586 
1587  assert(type == BoundType::EQ && "expected EQ");
1588  std::optional<MPInt> lb =
1589  IntegerRelation(*this).computeConstantLowerOrUpperBound</*isLower=*/true>(
1590  pos);
1591  std::optional<MPInt> ub =
1592  IntegerRelation(*this)
1593  .computeConstantLowerOrUpperBound</*isLower=*/false>(pos);
1594  return (lb && ub && *lb == *ub) ? std::optional<MPInt>(*ub) : std::nullopt;
1595 }
1596 
1597 // A simple (naive and conservative) check for hyper-rectangularity.
1598 bool IntegerRelation::isHyperRectangular(unsigned pos, unsigned num) const {
1599  assert(pos < getNumCols() - 1);
1600  // Check for two non-zero coefficients in the range [pos, pos + sum).
1601  for (unsigned r = 0, e = getNumInequalities(); r < e; r++) {
1602  unsigned sum = 0;
1603  for (unsigned c = pos; c < pos + num; c++) {
1604  if (atIneq(r, c) != 0)
1605  sum++;
1606  }
1607  if (sum > 1)
1608  return false;
1609  }
1610  for (unsigned r = 0, e = getNumEqualities(); r < e; r++) {
1611  unsigned sum = 0;
1612  for (unsigned c = pos; c < pos + num; c++) {
1613  if (atEq(r, c) != 0)
1614  sum++;
1615  }
1616  if (sum > 1)
1617  return false;
1618  }
1619  return true;
1620 }
1621 
1622 /// Removes duplicate constraints, trivially true constraints, and constraints
1623 /// that can be detected as redundant as a result of differing only in their
1624 /// constant term part. A constraint of the form <non-negative constant> >= 0 is
1625 /// considered trivially true.
1626 // Uses a DenseSet to hash and detect duplicates followed by a linear scan to
1627 // remove duplicates in place.
1631 
1632  // A map used to detect redundancy stemming from constraints that only differ
1633  // in their constant term. The value stored is <row position, const term>
1634  // for a given row.
1635  SmallDenseMap<ArrayRef<MPInt>, std::pair<unsigned, MPInt>>
1636  rowsWithoutConstTerm;
1637  // To unique rows.
1638  SmallDenseSet<ArrayRef<MPInt>, 8> rowSet;
1639 
1640  // Check if constraint is of the form <non-negative-constant> >= 0.
1641  auto isTriviallyValid = [&](unsigned r) -> bool {
1642  for (unsigned c = 0, e = getNumCols() - 1; c < e; c++) {
1643  if (atIneq(r, c) != 0)
1644  return false;
1645  }
1646  return atIneq(r, getNumCols() - 1) >= 0;
1647  };
1648 
1649  // Detect and mark redundant constraints.
1650  SmallVector<bool, 256> redunIneq(getNumInequalities(), false);
1651  for (unsigned r = 0, e = getNumInequalities(); r < e; r++) {
1652  MPInt *rowStart = &inequalities(r, 0);
1653  auto row = ArrayRef<MPInt>(rowStart, getNumCols());
1654  if (isTriviallyValid(r) || !rowSet.insert(row).second) {
1655  redunIneq[r] = true;
1656  continue;
1657  }
1658 
1659  // Among constraints that only differ in the constant term part, mark
1660  // everything other than the one with the smallest constant term redundant.
1661  // (eg: among i - 16j - 5 >= 0, i - 16j - 1 >=0, i - 16j - 7 >= 0, the
1662  // former two are redundant).
1663  MPInt constTerm = atIneq(r, getNumCols() - 1);
1664  auto rowWithoutConstTerm = ArrayRef<MPInt>(rowStart, getNumCols() - 1);
1665  const auto &ret =
1666  rowsWithoutConstTerm.insert({rowWithoutConstTerm, {r, constTerm}});
1667  if (!ret.second) {
1668  // Check if the other constraint has a higher constant term.
1669  auto &val = ret.first->second;
1670  if (val.second > constTerm) {
1671  // The stored row is redundant. Mark it so, and update with this one.
1672  redunIneq[val.first] = true;
1673  val = {r, constTerm};
1674  } else {
1675  // The one stored makes this one redundant.
1676  redunIneq[r] = true;
1677  }
1678  }
1679  }
1680 
1681  // Scan to get rid of all rows marked redundant, in-place.
1682  unsigned pos = 0;
1683  for (unsigned r = 0, e = getNumInequalities(); r < e; r++)
1684  if (!redunIneq[r])
1685  inequalities.copyRow(r, pos++);
1686 
1688 
1689  // TODO: consider doing this for equalities as well, but probably not worth
1690  // the savings.
1691 }
1692 
1693 #undef DEBUG_TYPE
1694 #define DEBUG_TYPE "fm"
1695 
1696 /// Eliminates variable at the specified position using Fourier-Motzkin
1697 /// variable elimination. This technique is exact for rational spaces but
1698 /// conservative (in "rare" cases) for integer spaces. The operation corresponds
1699 /// to a projection operation yielding the (convex) set of integer points
1700 /// contained in the rational shadow of the set. An emptiness test that relies
1701 /// on this method will guarantee emptiness, i.e., it disproves the existence of
1702 /// a solution if it says it's empty.
1703 /// If a non-null isResultIntegerExact is passed, it is set to true if the
1704 /// result is also integer exact. If it's set to false, the obtained solution
1705 /// *may* not be exact, i.e., it may contain integer points that do not have an
1706 /// integer pre-image in the original set.
1707 ///
1708 /// Eg:
1709 /// j >= 0, j <= i + 1
1710 /// i >= 0, i <= N + 1
1711 /// Eliminating i yields,
1712 /// j >= 0, 0 <= N + 1, j - 1 <= N + 1
1713 ///
1714 /// If darkShadow = true, this method computes the dark shadow on elimination;
1715 /// the dark shadow is a convex integer subset of the exact integer shadow. A
1716 /// non-empty dark shadow proves the existence of an integer solution. The
1717 /// elimination in such a case could however be an under-approximation, and thus
1718 /// should not be used for scanning sets or used by itself for dependence
1719 /// checking.
1720 ///
1721 /// Eg: 2-d set, * represents grid points, 'o' represents a point in the set.
1722 /// ^
1723 /// |
1724 /// | * * * * o o
1725 /// i | * * o o o o
1726 /// | o * * * * *
1727 /// --------------->
1728 /// j ->
1729 ///
1730 /// Eliminating i from this system (projecting on the j dimension):
1731 /// rational shadow / integer light shadow: 1 <= j <= 6
1732 /// dark shadow: 3 <= j <= 6
1733 /// exact integer shadow: j = 1 \union 3 <= j <= 6
1734 /// holes/splinters: j = 2
1735 ///
1736 /// darkShadow = false, isResultIntegerExact = nullptr are default values.
1737 // TODO: a slight modification to yield dark shadow version of FM (tightened),
1738 // which can prove the existence of a solution if there is one.
1739 void IntegerRelation::fourierMotzkinEliminate(unsigned pos, bool darkShadow,
1740  bool *isResultIntegerExact) {
1741  LLVM_DEBUG(llvm::dbgs() << "FM input (eliminate pos " << pos << "):\n");
1742  LLVM_DEBUG(dump());
1743  assert(pos < getNumVars() && "invalid position");
1744  assert(hasConsistentState());
1745 
1746  // Check if this variable can be eliminated through a substitution.
1747  for (unsigned r = 0, e = getNumEqualities(); r < e; r++) {
1748  if (atEq(r, pos) != 0) {
1749  // Use Gaussian elimination here (since we have an equality).
1751  (void)ret;
1752  assert(succeeded(ret) && "Gaussian elimination guaranteed to succeed");
1753  LLVM_DEBUG(llvm::dbgs() << "FM output (through Gaussian elimination):\n");
1754  LLVM_DEBUG(dump());
1755  return;
1756  }
1757  }
1758 
1759  // A fast linear time tightening.
1761 
1762  // Check if the variable appears at all in any of the inequalities.
1763  if (isColZero(pos)) {
1764  // If it doesn't appear, just remove the column and return.
1765  // TODO: refactor removeColumns to use it from here.
1766  removeVar(pos);
1767  LLVM_DEBUG(llvm::dbgs() << "FM output:\n");
1768  LLVM_DEBUG(dump());
1769  return;
1770  }
1771 
1772  // Positions of constraints that are lower bounds on the variable.
1773  SmallVector<unsigned, 4> lbIndices;
1774  // Positions of constraints that are lower bounds on the variable.
1775  SmallVector<unsigned, 4> ubIndices;
1776  // Positions of constraints that do not involve the variable.
1777  std::vector<unsigned> nbIndices;
1778  nbIndices.reserve(getNumInequalities());
1779 
1780  // Gather all lower bounds and upper bounds of the variable. Since the
1781  // canonical form c_1*x_1 + c_2*x_2 + ... + c_0 >= 0, a constraint is a lower
1782  // bound for x_i if c_i >= 1, and an upper bound if c_i <= -1.
1783  for (unsigned r = 0, e = getNumInequalities(); r < e; r++) {
1784  if (atIneq(r, pos) == 0) {
1785  // Var does not appear in bound.
1786  nbIndices.push_back(r);
1787  } else if (atIneq(r, pos) >= 1) {
1788  // Lower bound.
1789  lbIndices.push_back(r);
1790  } else {
1791  // Upper bound.
1792  ubIndices.push_back(r);
1793  }
1794  }
1795 
1796  PresburgerSpace newSpace = getSpace();
1797  VarKind idKindRemove = newSpace.getVarKindAt(pos);
1798  unsigned relativePos = pos - newSpace.getVarKindOffset(idKindRemove);
1799  newSpace.removeVarRange(idKindRemove, relativePos, relativePos + 1);
1800 
1801  /// Create the new system which has one variable less.
1802  IntegerRelation newRel(lbIndices.size() * ubIndices.size() + nbIndices.size(),
1803  getNumEqualities(), getNumCols() - 1, newSpace);
1804 
1805  // This will be used to check if the elimination was integer exact.
1806  bool allLCMsAreOne = true;
1807 
1808  // Let x be the variable we are eliminating.
1809  // For each lower bound, lb <= c_l*x, and each upper bound c_u*x <= ub, (note
1810  // that c_l, c_u >= 1) we have:
1811  // lb*lcm(c_l, c_u)/c_l <= lcm(c_l, c_u)*x <= ub*lcm(c_l, c_u)/c_u
1812  // We thus generate a constraint:
1813  // lcm(c_l, c_u)/c_l*lb <= lcm(c_l, c_u)/c_u*ub.
1814  // Note if c_l = c_u = 1, all integer points captured by the resulting
1815  // constraint correspond to integer points in the original system (i.e., they
1816  // have integer pre-images). Hence, if the lcm's are all 1, the elimination is
1817  // integer exact.
1818  for (auto ubPos : ubIndices) {
1819  for (auto lbPos : lbIndices) {
1820  SmallVector<MPInt, 4> ineq;
1821  ineq.reserve(newRel.getNumCols());
1822  MPInt lbCoeff = atIneq(lbPos, pos);
1823  // Note that in the comments above, ubCoeff is the negation of the
1824  // coefficient in the canonical form as the view taken here is that of the
1825  // term being moved to the other size of '>='.
1826  MPInt ubCoeff = -atIneq(ubPos, pos);
1827  // TODO: refactor this loop to avoid all branches inside.
1828  for (unsigned l = 0, e = getNumCols(); l < e; l++) {
1829  if (l == pos)
1830  continue;
1831  assert(lbCoeff >= 1 && ubCoeff >= 1 && "bounds wrongly identified");
1832  MPInt lcm = presburger::lcm(lbCoeff, ubCoeff);
1833  ineq.push_back(atIneq(ubPos, l) * (lcm / ubCoeff) +
1834  atIneq(lbPos, l) * (lcm / lbCoeff));
1835  assert(lcm > 0 && "lcm should be positive!");
1836  if (lcm != 1)
1837  allLCMsAreOne = false;
1838  }
1839  if (darkShadow) {
1840  // The dark shadow is a convex subset of the exact integer shadow. If
1841  // there is a point here, it proves the existence of a solution.
1842  ineq[ineq.size() - 1] += lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
1843  }
1844  // TODO: we need to have a way to add inequalities in-place in
1845  // IntegerRelation instead of creating and copying over.
1846  newRel.addInequality(ineq);
1847  }
1848  }
1849 
1850  LLVM_DEBUG(llvm::dbgs() << "FM isResultIntegerExact: " << allLCMsAreOne
1851  << "\n");
1852  if (allLCMsAreOne && isResultIntegerExact)
1853  *isResultIntegerExact = true;
1854 
1855  // Copy over the constraints not involving this variable.
1856  for (auto nbPos : nbIndices) {
1857  SmallVector<MPInt, 4> ineq;
1858  ineq.reserve(getNumCols() - 1);
1859  for (unsigned l = 0, e = getNumCols(); l < e; l++) {
1860  if (l == pos)
1861  continue;
1862  ineq.push_back(atIneq(nbPos, l));
1863  }
1864  newRel.addInequality(ineq);
1865  }
1866 
1867  assert(newRel.getNumConstraints() ==
1868  lbIndices.size() * ubIndices.size() + nbIndices.size());
1869 
1870  // Copy over the equalities.
1871  for (unsigned r = 0, e = getNumEqualities(); r < e; r++) {
1873  eq.reserve(newRel.getNumCols());
1874  for (unsigned l = 0, e = getNumCols(); l < e; l++) {
1875  if (l == pos)
1876  continue;
1877  eq.push_back(atEq(r, l));
1878  }
1879  newRel.addEquality(eq);
1880  }
1881 
1882  // GCD tightening and normalization allows detection of more trivially
1883  // redundant constraints.
1884  newRel.gcdTightenInequalities();
1885  newRel.normalizeConstraintsByGCD();
1886  newRel.removeTrivialRedundancy();
1887  clearAndCopyFrom(newRel);
1888  LLVM_DEBUG(llvm::dbgs() << "FM output:\n");
1889  LLVM_DEBUG(dump());
1890 }
1891 
1892 #undef DEBUG_TYPE
1893 #define DEBUG_TYPE "presburger"
1894 
1895 void IntegerRelation::projectOut(unsigned pos, unsigned num) {
1896  if (num == 0)
1897  return;
1898 
1899  // 'pos' can be at most getNumCols() - 2 if num > 0.
1900  assert((getNumCols() < 2 || pos <= getNumCols() - 2) && "invalid position");
1901  assert(pos + num < getNumCols() && "invalid range");
1902 
1903  // Eliminate as many variables as possible using Gaussian elimination.
1904  unsigned currentPos = pos;
1905  unsigned numToEliminate = num;
1906  unsigned numGaussianEliminated = 0;
1907 
1908  while (currentPos < getNumVars()) {
1909  unsigned curNumEliminated =
1910  gaussianEliminateVars(currentPos, currentPos + numToEliminate);
1911  ++currentPos;
1912  numToEliminate -= curNumEliminated + 1;
1913  numGaussianEliminated += curNumEliminated;
1914  }
1915 
1916  // Eliminate the remaining using Fourier-Motzkin.
1917  for (unsigned i = 0; i < num - numGaussianEliminated; i++) {
1918  unsigned numToEliminate = num - numGaussianEliminated - i;
1920  getBestVarToEliminate(*this, pos, pos + numToEliminate));
1921  }
1922 
1923  // Fast/trivial simplifications.
1925  // Normalize constraints after tightening since the latter impacts this, but
1926  // not the other way round.
1928 }
1929 
1930 namespace {
1931 
1932 enum BoundCmpResult { Greater, Less, Equal, Unknown };
1933 
1934 /// Compares two affine bounds whose coefficients are provided in 'first' and
1935 /// 'second'. The last coefficient is the constant term.
1936 static BoundCmpResult compareBounds(ArrayRef<MPInt> a, ArrayRef<MPInt> b) {
1937  assert(a.size() == b.size());
1938 
1939  // For the bounds to be comparable, their corresponding variable
1940  // coefficients should be equal; the constant terms are then compared to
1941  // determine less/greater/equal.
1942 
1943  if (!std::equal(a.begin(), a.end() - 1, b.begin()))
1944  return Unknown;
1945 
1946  if (a.back() == b.back())
1947  return Equal;
1948 
1949  return a.back() < b.back() ? Less : Greater;
1950 }
1951 } // namespace
1952 
1953 // Returns constraints that are common to both A & B.
1955  const IntegerRelation &b, IntegerRelation &c) {
1956  c = IntegerRelation(a.getSpace());
1957  // a naive O(n^2) check should be enough here given the input sizes.
1958  for (unsigned r = 0, e = a.getNumInequalities(); r < e; ++r) {
1959  for (unsigned s = 0, f = b.getNumInequalities(); s < f; ++s) {
1960  if (a.getInequality(r) == b.getInequality(s)) {
1961  c.addInequality(a.getInequality(r));
1962  break;
1963  }
1964  }
1965  }
1966  for (unsigned r = 0, e = a.getNumEqualities(); r < e; ++r) {
1967  for (unsigned s = 0, f = b.getNumEqualities(); s < f; ++s) {
1968  if (a.getEquality(r) == b.getEquality(s)) {
1969  c.addEquality(a.getEquality(r));
1970  break;
1971  }
1972  }
1973  }
1974 }
1975 
1976 // Computes the bounding box with respect to 'other' by finding the min of the
1977 // lower bounds and the max of the upper bounds along each of the dimensions.
1980  assert(space.isEqual(otherCst.getSpace()) && "Spaces should match.");
1981  assert(getNumLocalVars() == 0 && "local ids not supported yet here");
1982 
1983  // Get the constraints common to both systems; these will be added as is to
1984  // the union.
1986  getCommonConstraints(*this, otherCst, commonCst);
1987 
1988  std::vector<SmallVector<MPInt, 8>> boundingLbs;
1989  std::vector<SmallVector<MPInt, 8>> boundingUbs;
1990  boundingLbs.reserve(2 * getNumDimVars());
1991  boundingUbs.reserve(2 * getNumDimVars());
1992 
1993  // To hold lower and upper bounds for each dimension.
1994  SmallVector<MPInt, 4> lb, otherLb, ub, otherUb;
1995  // To compute min of lower bounds and max of upper bounds for each dimension.
1998  // To compute final new lower and upper bounds for the union.
1999  SmallVector<MPInt, 8> newLb(getNumCols()), newUb(getNumCols());
2000 
2001  MPInt lbFloorDivisor, otherLbFloorDivisor;
2002  for (unsigned d = 0, e = getNumDimVars(); d < e; ++d) {
2003  auto extent = getConstantBoundOnDimSize(d, &lb, &lbFloorDivisor, &ub);
2004  if (!extent.has_value())
2005  // TODO: symbolic extents when necessary.
2006  // TODO: handle union if a dimension is unbounded.
2007  return failure();
2008 
2009  auto otherExtent = otherCst.getConstantBoundOnDimSize(
2010  d, &otherLb, &otherLbFloorDivisor, &otherUb);
2011  if (!otherExtent.has_value() || lbFloorDivisor != otherLbFloorDivisor)
2012  // TODO: symbolic extents when necessary.
2013  return failure();
2014 
2015  assert(lbFloorDivisor > 0 && "divisor always expected to be positive");
2016 
2017  auto res = compareBounds(lb, otherLb);
2018  // Identify min.
2019  if (res == BoundCmpResult::Less || res == BoundCmpResult::Equal) {
2020  minLb = lb;
2021  // Since the divisor is for a floordiv, we need to convert to ceildiv,
2022  // i.e., i >= expr floordiv div <=> i >= (expr - div + 1) ceildiv div <=>
2023  // div * i >= expr - div + 1.
2024  minLb.back() -= lbFloorDivisor - 1;
2025  } else if (res == BoundCmpResult::Greater) {
2026  minLb = otherLb;
2027  minLb.back() -= otherLbFloorDivisor - 1;
2028  } else {
2029  // Uncomparable - check for constant lower/upper bounds.
2030  auto constLb = getConstantBound(BoundType::LB, d);
2031  auto constOtherLb = otherCst.getConstantBound(BoundType::LB, d);
2032  if (!constLb.has_value() || !constOtherLb.has_value())
2033  return failure();
2034  std::fill(minLb.begin(), minLb.end(), 0);
2035  minLb.back() = std::min(*constLb, *constOtherLb);
2036  }
2037 
2038  // Do the same for ub's but max of upper bounds. Identify max.
2039  auto uRes = compareBounds(ub, otherUb);
2040  if (uRes == BoundCmpResult::Greater || uRes == BoundCmpResult::Equal) {
2041  maxUb = ub;
2042  } else if (uRes == BoundCmpResult::Less) {
2043  maxUb = otherUb;
2044  } else {
2045  // Uncomparable - check for constant lower/upper bounds.
2046  auto constUb = getConstantBound(BoundType::UB, d);
2047  auto constOtherUb = otherCst.getConstantBound(BoundType::UB, d);
2048  if (!constUb.has_value() || !constOtherUb.has_value())
2049  return failure();
2050  std::fill(maxUb.begin(), maxUb.end(), 0);
2051  maxUb.back() = std::max(*constUb, *constOtherUb);
2052  }
2053 
2054  std::fill(newLb.begin(), newLb.end(), 0);
2055  std::fill(newUb.begin(), newUb.end(), 0);
2056 
2057  // The divisor for lb, ub, otherLb, otherUb at this point is lbDivisor,
2058  // and so it's the divisor for newLb and newUb as well.
2059  newLb[d] = lbFloorDivisor;
2060  newUb[d] = -lbFloorDivisor;
2061  // Copy over the symbolic part + constant term.
2062  std::copy(minLb.begin(), minLb.end(), newLb.begin() + getNumDimVars());
2063  std::transform(newLb.begin() + getNumDimVars(), newLb.end(),
2064  newLb.begin() + getNumDimVars(), std::negate<MPInt>());
2065  std::copy(maxUb.begin(), maxUb.end(), newUb.begin() + getNumDimVars());
2066 
2067  boundingLbs.push_back(newLb);
2068  boundingUbs.push_back(newUb);
2069  }
2070 
2071  // Clear all constraints and add the lower/upper bounds for the bounding box.
2072  clearConstraints();
2073  for (unsigned d = 0, e = getNumDimVars(); d < e; ++d) {
2074  addInequality(boundingLbs[d]);
2075  addInequality(boundingUbs[d]);
2076  }
2077 
2078  // Add the constraints that were common to both systems.
2079  append(commonCst);
2081 
2082  // TODO: copy over pure symbolic constraints from this and 'other' over to the
2083  // union (since the above are just the union along dimensions); we shouldn't
2084  // be discarding any other constraints on the symbols.
2085 
2086  return success();
2087 }
2088 
2089 bool IntegerRelation::isColZero(unsigned pos) const {
2090  unsigned rowPos;
2091  return !findConstraintWithNonZeroAt(pos, /*isEq=*/false, &rowPos) &&
2092  !findConstraintWithNonZeroAt(pos, /*isEq=*/true, &rowPos);
2093 }
2094 
2095 /// Find positions of inequalities and equalities that do not have a coefficient
2096 /// for [pos, pos + num) variables.
2097 static void getIndependentConstraints(const IntegerRelation &cst, unsigned pos,
2098  unsigned num,
2099  SmallVectorImpl<unsigned> &nbIneqIndices,
2100  SmallVectorImpl<unsigned> &nbEqIndices) {
2101  assert(pos < cst.getNumVars() && "invalid start position");
2102  assert(pos + num <= cst.getNumVars() && "invalid limit");
2103 
2104  for (unsigned r = 0, e = cst.getNumInequalities(); r < e; r++) {
2105  // The bounds are to be independent of [offset, offset + num) columns.
2106  unsigned c;
2107  for (c = pos; c < pos + num; ++c) {
2108  if (cst.atIneq(r, c) != 0)
2109  break;
2110  }
2111  if (c == pos + num)
2112  nbIneqIndices.push_back(r);
2113  }
2114 
2115  for (unsigned r = 0, e = cst.getNumEqualities(); r < e; r++) {
2116  // The bounds are to be independent of [offset, offset + num) columns.
2117  unsigned c;
2118  for (c = pos; c < pos + num; ++c) {
2119  if (cst.atEq(r, c) != 0)
2120  break;
2121  }
2122  if (c == pos + num)
2123  nbEqIndices.push_back(r);
2124  }
2125 }
2126 
2127 void IntegerRelation::removeIndependentConstraints(unsigned pos, unsigned num) {
2128  assert(pos + num <= getNumVars() && "invalid range");
2129 
2130  // Remove constraints that are independent of these variables.
2131  SmallVector<unsigned, 4> nbIneqIndices, nbEqIndices;
2132  getIndependentConstraints(*this, /*pos=*/0, num, nbIneqIndices, nbEqIndices);
2133 
2134  // Iterate in reverse so that indices don't have to be updated.
2135  // TODO: This method can be made more efficient (because removal of each
2136  // inequality leads to much shifting/copying in the underlying buffer).
2137  for (auto nbIndex : llvm::reverse(nbIneqIndices))
2138  removeInequality(nbIndex);
2139  for (auto nbIndex : llvm::reverse(nbEqIndices))
2140  removeEquality(nbIndex);
2141 }
2142 
2144  IntegerRelation copyRel = *this;
2145 
2146  // Convert Range variables to Local variables.
2148  VarKind::Local);
2149 
2150  // Convert Domain variables to SetDim(Range) variables.
2152  VarKind::SetDim);
2153 
2154  return IntegerPolyhedron(std::move(copyRel));
2155 }
2156 
2158  IntegerRelation copyRel = *this;
2159 
2160  // Convert Domain variables to Local variables.
2162  VarKind::Local);
2163 
2164  // We do not need to do anything to Range variables since they are already in
2165  // SetDim position.
2166 
2167  return IntegerPolyhedron(std::move(copyRel));
2168 }
2169 
2171  assert(getDomainSet().getSpace().isCompatible(poly.getSpace()) &&
2172  "Domain set is not compatible with poly");
2173 
2174  // Treating the poly as a relation, convert it from `0 -> R` to `R -> 0`.
2175  IntegerRelation rel = poly;
2176  rel.inverse();
2177 
2178  // Append dummy range variables to make the spaces compatible.
2180 
2181  // Intersect in place.
2182  mergeLocalVars(rel);
2183  append(rel);
2184 }
2185 
2187  assert(getRangeSet().getSpace().isCompatible(poly.getSpace()) &&
2188  "Range set is not compatible with poly");
2189 
2190  IntegerRelation rel = poly;
2191 
2192  // Append dummy domain variables to make the spaces compatible.
2194 
2195  mergeLocalVars(rel);
2196  append(rel);
2197 }
2198 
2200  unsigned numRangeVars = getNumVarKind(VarKind::Range);
2202  VarKind::Range);
2203  convertVarKind(VarKind::Range, 0, numRangeVars, VarKind::Domain);
2204 }
2205 
2207  assert(getRangeSet().getSpace().isCompatible(rel.getDomainSet().getSpace()) &&
2208  "Range of `this` should be compatible with Domain of `rel`");
2209 
2210  IntegerRelation copyRel = rel;
2211 
2212  // Let relation `this` be R1: A -> B, and `rel` be R2: B -> C.
2213  // We convert R1 to A -> (B X C), and R2 to B X C then intersect the range of
2214  // R1 with R2. After this, we get R1: A -> C, by projecting out B.
2215  // TODO: Using nested spaces here would help, since we could directly
2216  // intersect the range with another relation.
2217  unsigned numBVars = getNumRangeVars();
2218 
2219  // Convert R1 from A -> B to A -> (B X C).
2221 
2222  // Convert R2 to B X C.
2223  copyRel.convertVarKind(VarKind::Domain, 0, numBVars, VarKind::Range, 0);
2224 
2225  // Intersect R2 to range of R1.
2227 
2228  // Project out B in R1.
2230 }
2231 
2233  inverse();
2234  compose(rel);
2235  inverse();
2236 }
2237 
2239 
2240 void IntegerRelation::printSpace(raw_ostream &os) const {
2241  space.print(os);
2242  os << getNumConstraints() << " constraints\n";
2243 }
2244 
2245 void IntegerRelation::print(raw_ostream &os) const {
2246  assert(hasConsistentState());
2247  printSpace(os);
2248  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i) {
2249  os << " ";
2250  for (unsigned j = 0, f = getNumCols(); j < f; ++j) {
2251  os << atEq(i, j) << "\t";
2252  }
2253  os << "= 0\n";
2254  }
2255  for (unsigned i = 0, e = getNumInequalities(); i < e; ++i) {
2256  os << " ";
2257  for (unsigned j = 0, f = getNumCols(); j < f; ++j) {
2258  os << atIneq(i, j) << "\t";
2259  }
2260  os << ">= 0\n";
2261  }
2262  os << '\n';
2263 }
2264 
2265 void IntegerRelation::dump() const { print(llvm::errs()); }
2266 
2267 unsigned IntegerPolyhedron::insertVar(VarKind kind, unsigned pos,
2268  unsigned num) {
2269  assert((kind != VarKind::Domain || num == 0) &&
2270  "Domain has to be zero in a set");
2271  return IntegerRelation::insertVar(kind, pos, num);
2272 }
2276 }
2277 
2280 }
static void copy(Location loc, Value dst, Value src, Value size, OpBuilder &builder)
Copies the given number of bytes from src to dst pointers.
static MPInt valueAt(ArrayRef< MPInt > expr, ArrayRef< MPInt > point)
Helper to evaluate an affine expression at a point.
static void getIndependentConstraints(const IntegerRelation &cst, unsigned pos, unsigned num, SmallVectorImpl< unsigned > &nbIneqIndices, SmallVectorImpl< unsigned > &nbEqIndices)
Find positions of inequalities and equalities that do not have a coefficient for [pos,...
static bool rangeIsZero(ArrayRef< MPInt > range)
static void removeConstraintsInvolvingVarRange(IntegerRelation &poly, unsigned begin, unsigned count)
static int findEqualityToConstant(const IntegerRelation &cst, unsigned pos, bool symbolic=false)
Finds an equality that equates the specified variable to a constant.
static unsigned getBestVarToEliminate(const IntegerRelation &cst, unsigned start, unsigned end)
Returns the position of the variable that has the minimum <number of lower bounds> times <number of u...
static void getCommonConstraints(const IntegerRelation &a, const IntegerRelation &b, IntegerRelation &c)
static void eliminateFromConstraint(IntegerRelation *constraints, unsigned rowIdx, unsigned pivotRow, unsigned pivotCol, unsigned elimColStart, bool isEq)
Eliminate variable from constraint at rowIdx based on coefficient at pivotRow, pivotCol.
static Value max(ImplicitLocOpBuilder &builder, Value value, Value bound)
static Value min(ImplicitLocOpBuilder &builder, Value value, Value bound)
Class storing division representation of local variables of a constraint system.
Definition: Utils.h:118
void removeDuplicateDivs(llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Removes duplicate divisions.
Definition: Utils.cpp:430
MPInt & getDenom(unsigned i)
Definition: Utils.h:149
bool hasAllReprs() const
Definition: Utils.h:134
void clearRepr(unsigned i)
Definition: Utils.h:137
MutableArrayRef< MPInt > getDividend(unsigned i)
Definition: Utils.h:140
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
IntegerPolyhedron intersect(const IntegerPolyhedron &other) const
Return the intersection of the two relations.
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1) override
Insert num variables of the specified kind at position pos.
PresburgerSet subtract(const PresburgerSet &other) const
Return the set difference of this set and the given set, i.e., return this \ set.
IntegerPolyhedron(unsigned numReservedInequalities, unsigned numReservedEqualities, unsigned numReservedCols, const PresburgerSpace &space)
Constructs a set reserving memory for the specified number of constraints and variables.
std::unique_ptr< IntegerPolyhedron > clone() const
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
SymbolicLexMin findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation.
virtual void swapVar(unsigned posA, unsigned posB)
Swap the posA^th variable with the posB^th variable.
MPInt atEq(unsigned i, unsigned j) const
Returns the value at the specified equality row and column.
void removeIndependentConstraints(unsigned pos, unsigned num)
Removes constraints that are independent of (i.e., do not have a coefficient) variables in the range ...
ArrayRef< MPInt > getEquality(unsigned idx) const
void compose(const IntegerRelation &rel)
Let the relation this be R1, and the relation rel be R2.
void applyRange(const IntegerRelation &rel)
Given a relation rel, apply the relation to the range of this relation.
unsigned getVarKindEnd(VarKind kind) const
Return the index at Which the specified kind of vars ends.
void addInequality(ArrayRef< MPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
std::optional< MPInt > getConstantBound(BoundType type, unsigned pos) const
Returns the constant bound for the pos^th variable if there is one; std::nullopt otherwise.
void removeTrivialRedundancy()
Removes duplicate constraints, trivially true constraints, and constraints that can be detected as re...
Matrix equalities
Coefficients of affine equalities (in == 0 form).
void addEquality(ArrayRef< MPInt > eq)
Adds an equality from the coefficients specified in eq.
void removeInequalityRange(unsigned start, unsigned end)
void normalizeConstraintsByGCD()
Normalized each constraints by the GCD of its coefficients.
void truncate(const CountsSnapshot &counts)
virtual void eliminateRedundantLocalVar(unsigned posA, unsigned posB)
Eliminate the posB^th local variable, replacing every instance of it with the posA^th local variable.
void removeEqualityRange(unsigned start, unsigned end)
Remove the (in)equalities at positions [start, end).
std::optional< MPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the relation.
LogicalResult constantFoldVar(unsigned pos)
Tries to fold the specified variable to a constant using a trivial equality detection; if successful,...
IntegerPolyhedron getRangeSet() const
Return a set corresponding to all points in the range of the relation.
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
bool isEmptyByGCDTest() const
Runs the GCD test on all equality constraints.
void convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit, VarKind dstKind, unsigned pos)
Converts variables of kind srcKind in the range [varStart, varLimit) to variables of kind dstKind.
unsigned appendVar(VarKind kind, unsigned num=1)
Append num variables of the specified kind after the last variable of that kind.
void intersectRange(const IntegerPolyhedron &poly)
Intersect the given poly with the range in-place.
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.
std::optional< SmallVector< MPInt, 8 > > findIntegerSample() const
Find an integer sample point satisfying the constraints using a branch and bound algorithm with gener...
MaybeOptimum< SmallVector< MPInt, 8 > > findIntegerLexMin() const
Same as above, but returns lexicographically minimal integer point.
virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
bool hasInvalidConstraint() const
Checks all rows of equality/inequality constraints for trivial contradictions (for example: 1 == 0,...
LogicalResult unionBoundingBox(const IntegerRelation &other)
Updates the constraints to be the smallest bounding (enclosing) box that contains the points of this ...
IntegerRelation(unsigned numReservedInequalities, unsigned numReservedEqualities, unsigned numReservedCols, const PresburgerSpace &space)
Constructs a relation reserving memory for the specified number of constraints and variables.
bool isHyperRectangular(unsigned pos, unsigned num) const
Returns true if the set can be trivially detected as being hyper-rectangular on the specified contigu...
LogicalResult gaussianEliminateVar(unsigned position)
Eliminates a single variable at position from equality and inequality constraints.
void clearConstraints()
Removes all equalities and inequalities.
Matrix getBoundedDirections() const
Returns a matrix where each row is a vector along which the polytope is bounded.
IntegerRelation intersect(IntegerRelation other) const
Return the intersection of the two relations.
void addLocalFloorDiv(ArrayRef< MPInt > dividend, const MPInt &divisor)
Adds a new local variable as the floordiv of an affine function of other variables,...
ArrayRef< MPInt > getInequality(unsigned idx) const
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace, which should have the same number of ids as the current space.
std::optional< SmallVector< MPInt, 8 > > containsPointNoLocal(ArrayRef< MPInt > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists,...
MPInt atIneq(unsigned i, unsigned j) const
Returns the value at the specified inequality row and column.
void inverse()
Invert the relation i.e., swap its domain and range.
void append(const IntegerRelation &other)
Appends constraints from other into this.
void applyDomain(const IntegerRelation &rel)
Given a relation rel, apply the relation to the domain of this relation.
void intersectDomain(const IntegerPolyhedron &poly)
Intersect the given poly with the domain in-place.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
bool isEqual(const IntegerRelation &other) const
Return whether this and other are equal.
virtual void printSpace(raw_ostream &os) const
Prints the number of constraints, dimensions, symbols and locals in the IntegerRelation.
void removeRedundantConstraints()
Removes redundant constraints using Simplex.
PresburgerRelation computeReprWithOnlyDivLocals() const
Compute an equivalent representation of the same set, such that all local vars in all disjuncts have ...
void removeRedundantInequalities()
A more expensive check than removeTrivialRedundancy to detect redundant inequalities.
void truncateVarKind(VarKind kind, unsigned num)
Truncate the vars of the specified kind to the specified number by dropping some vars at the end.
void constantFoldVarRange(unsigned pos, unsigned num)
This method calls constantFoldVar for the specified range of variables, num variables starting at pos...
std::optional< MPInt > getConstantBoundOnDimSize(unsigned pos, SmallVectorImpl< MPInt > *lb=nullptr, MPInt *boundFloorDivisor=nullptr, SmallVectorImpl< MPInt > *ub=nullptr, unsigned *minLbPos=nullptr, unsigned *minUbPos=nullptr) const
Returns the smallest known constant bound for the extent of the specified variable (pos^th),...
bool isEmpty() const
Checks for emptiness by performing variable elimination on all variables, running the GCD test on eac...
unsigned getNumCols() const
Returns the number of columns in the constraint system.
void getLowerAndUpperBoundIndices(unsigned pos, SmallVectorImpl< unsigned > *lbIndices, SmallVectorImpl< unsigned > *ubIndices, SmallVectorImpl< unsigned > *eqIndices=nullptr, unsigned offset=0, unsigned num=0) const
Gather positions of all lower and upper bounds of the variable at pos, and optionally any equalities ...
void gcdTightenInequalities()
Tightens inequalities given that we are dealing with integer spaces.
void removeVar(VarKind kind, unsigned pos)
Removes variables of the specified kind with the specified pos (or within the specified range) from t...
void setSpaceExceptLocals(const PresburgerSpace &oSpace)
Set the space to oSpace, which should not have any local ids.
unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit)
Eliminates variables from equality and inequality constraints in column range [posStart,...
void addBound(BoundType type, unsigned pos, const MPInt &value)
Adds a constant bound for the specified variable.
IntegerPolyhedron getDomainSet() const
Return a set corresponding to all points in the domain of the relation.
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.
constexpr static unsigned kExplosionFactor
A parameter that controls detection of an unrealistic number of constraints.
void setAndEliminate(unsigned pos, ArrayRef< MPInt > values)
Sets the values.size() variables starting at pos to the specified values and removes them.
virtual void clearAndCopyFrom(const IntegerRelation &other)
Replaces the contents of this IntegerRelation with other.
void projectOut(unsigned pos, unsigned num)
Projects out (aka eliminates) num variables starting at position pos.
std::optional< MPInt > computeConstantLowerOrUpperBound(unsigned pos)
Returns the constant lower bound bound if isLower is true, and the upper bound if isLower is false.
void removeRedundantLocalVars()
Removes local variables using equalities.
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...
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin() const
Get the lexicographically minimum rational point satisfying the constraints.
virtual bool hasConsistentState() const
Returns false if the fields corresponding to various variable counts, or equality/inequality buffer s...
Matrix inequalities
Coefficients of affine inequalities (in >= 0 form).
bool findConstraintWithNonZeroAt(unsigned colIdx, bool isEq, unsigned *rowIdx) const
Searches for a constraint with a non-zero coefficient at colIdx in equality (isEq=true) or inequality...
bool isSubsetOf(const IntegerRelation &other) const
Return whether this is a subset of the given IntegerRelation.
std::unique_ptr< IntegerRelation > clone() const
const PresburgerSpace & getSpace() const
Returns a reference to the underlying space.
bool containsPoint(ArrayRef< MPInt > point) const
Returns true if the given point satisfies the constraints, or false otherwise.
bool isColZero(unsigned pos) const
Returns true if the pos^th column is all zero for both inequalities and equalities.
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of vars starts.
virtual void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
virtual void fourierMotzkinEliminate(unsigned pos, bool darkShadow=false, bool *isResultIntegerExact=nullptr)
Eliminates the variable at the specified position using Fourier-Motzkin variable elimination,...
A class for lexicographic optimization without any symbols.
Definition: Simplex.h:482
MaybeOptimum< SmallVector< MPInt, 8 > > findIntegerLexMin()
Return the lexicographically minimum integer solution to the constraints.
Definition: Simplex.cpp:288
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin()
Return the lexicographically minimum rational solution to the constraints.
Definition: Simplex.cpp:217
static std::pair< unsigned, LinearTransform > makeTransformToColumnEchelon(const Matrix &m)
SmallVector< MPInt, 8 > postMultiplyWithColumn(ArrayRef< MPInt > colVec) const
IntegerRelation applyTo(const IntegerRelation &rel) const
This class provides support for multi-precision arithmetic.
Definition: MPInt.h:87
This is a class to represent a resizable matrix.
Definition: Matrix.h:35
bool hasConsistentState() const
Return whether the Matrix is in a consistent state with all its invariants satisfied.
Definition: Matrix.cpp:365
void swapColumns(unsigned column, unsigned otherColumn)
Swap the given columns.
Definition: Matrix.cpp:78
unsigned appendExtraRow()
Add an extra row at the bottom of the matrix and return its position.
Definition: Matrix.cpp:39
void copyRow(unsigned sourceRow, unsigned targetRow)
Definition: Matrix.cpp:182
void removeColumns(unsigned pos, unsigned count)
Remove the columns having positions pos, pos + 1, ...
Definition: Matrix.cpp:145
void insertColumns(unsigned pos, unsigned count)
Insert columns having positions pos, pos + 1, ...
Definition: Matrix.cpp:103
MPInt normalizeRow(unsigned row, unsigned nCols)
Divide the first nCols of the specified row by their GCD.
Definition: Matrix.cpp:225
void removeRow(unsigned pos)
Definition: Matrix.cpp:172
void resizeVertically(unsigned newNRows)
Definition: Matrix.cpp:64
void fillRow(unsigned row, const MPInt &value)
Definition: Matrix.cpp:189
unsigned getNumRows() const
Definition: Matrix.h:76
void addToColumn(unsigned sourceColumn, unsigned targetColumn, const MPInt &scale)
Add scale multiples of the source column to the target column.
Definition: Matrix.cpp:207
void reserveRows(unsigned rows)
Reserve enough space to resize to the specified number of rows without reallocations.
Definition: Matrix.cpp:35
void negateRow(unsigned row)
Negate the specified row.
Definition: Matrix.cpp:220
void removeRows(unsigned pos, unsigned count)
Remove the rows having positions pos, pos + 1, ...
Definition: Matrix.cpp:173
bool isBounded() const
Definition: Utils.h:52
OptimumKind getKind() const
Definition: Utils.h:51
void removeOutputs(unsigned start, unsigned end)
Remove the specified range of outputs.
unsigned getNumOutputs() const
Definition: PWMAFunction.h:178
PresburgerSet getDomain() const
Return the domain of this piece-wise MultiAffineFunction.
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 subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
bool isSubsetOf(const PresburgerRelation &set) const
Return true if this set is a subset of the given set, and false otherwise.
bool isEqual(const PresburgerRelation &set) const
Return true if this set is equal to the given set, and false otherwise.
PresburgerSet unionSet(const PresburgerRelation &set) const
These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
bool isEqual(const PresburgerSpace &other) const
Returns true if both the spaces are equal including local variables i.e.
void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
Removes variables of the specified kind in the column range [varStart, varLimit).
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of var starts.
VarKind getVarKindAt(unsigned pos) const
Return the VarKind of the var at the specified position.
static PresburgerSpace getSetSpace(unsigned numDims=0, unsigned numSymbols=0, unsigned numLocals=0)
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
void print(llvm::raw_ostream &os) const
static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
bool isEmpty() const
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
Definition: Simplex.cpp:1051
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...
Definition: Simplex.h:695
bool isMarkedRedundant(unsigned constraintIndex) const
Returns whether the specified constraint has been marked as redundant.
Definition: Simplex.cpp:1388
std::optional< SmallVector< MPInt, 8 > > findIntegerSample()
Returns an integer sample point if one exists, or std::nullopt otherwise.
Definition: Simplex.cpp:1973
std::pair< MaybeOptimum< MPInt >, MaybeOptimum< MPInt > > computeIntegerBounds(ArrayRef< MPInt > coeffs)
Returns a (min, max) pair denoting the minimum and maximum integer values of the given expression.
Definition: Simplex.cpp:2084
bool isBoundedAlongConstraint(unsigned constraintIndex)
Returns whether the perpendicular of the specified constraint is a is a direction along which the pol...
Definition: Simplex.cpp:1378
bool isUnbounded()
Returns true if the polytope is unbounded, i.e., extends to infinity in some direction.
Definition: Simplex.cpp:1450
void detectRedundant(unsigned offset, unsigned count)
Finds a subset of constraints that is redundant, i.e., such that the set of solutions does not change...
Definition: Simplex.cpp:1408
std::optional< SmallVector< Fraction, 8 > > getRationalSample() const
Returns the current sample point, which may contain non-integer (rational) coordinates.
Definition: Simplex.cpp:1550
A class to perform symbolic lexicographic optimization, i.e., to find, for every assignment to the sy...
Definition: Simplex.h:576
SymbolicLexMin computeSymbolicIntegerLexMin()
The lexmin will be stored as a function lexmin from symbols to non-symbols in the result.
Definition: Simplex.cpp:518
BoundType
The type of bound: equal, lower bound or upper bound.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt gcd(const MPInt &a, const MPInt &b)
Definition: MPInt.h:399
VarKind
Kind of variable.
SmallVector< MPInt, 8 > getDivLowerBound(ArrayRef< MPInt > dividend, const MPInt &divisor, unsigned localVarIdx)
Definition: Utils.cpp:323
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt ceilDiv(const MPInt &lhs, const MPInt &rhs)
Definition: MPInt.h:374
SmallVector< MPInt, 8 > getDivUpperBound(ArrayRef< MPInt > dividend, const MPInt &divisor, unsigned localVarIdx)
If q is defined to be equal to expr floordiv d, this equivalent to saying that q is an integer and q ...
Definition: Utils.cpp:312
void mergeLocalVars(IntegerRelation &relA, IntegerRelation &relB, llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Given two relations, A and B, add additional local vars to the sets such that both have the union of ...
Definition: Utils.cpp:286
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt abs(const MPInt &x)
Definition: MPInt.h:370
MaybeLocalRepr computeSingleVarRepr(const IntegerRelation &cst, ArrayRef< bool > foundRepr, unsigned pos, MutableArrayRef< MPInt > dividend, MPInt &divisor)
Returns the MaybeLocalRepr struct which contains the indices of the constraints that can be expressed...
Definition: Utils.cpp:223
MPInt ceil(const Fraction &f)
Definition: Fraction.h:70
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt lcm(const MPInt &a, const MPInt &b)
Returns the least common multiple of 'a' and 'b'.
Definition: MPInt.h:407
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt floorDiv(const MPInt &lhs, const MPInt &rhs)
Definition: MPInt.h:382
This header declares functions that assit transformations in the MemRef dialect.
LogicalResult failure(bool isFailure=true)
Utility function to generate a LogicalResult.
Definition: LogicalResult.h:62
bool succeeded(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a success value.
Definition: LogicalResult.h:68
LogicalResult success(bool isSuccess=true)
Utility function to generate a LogicalResult.
Definition: LogicalResult.h:56
bool failed(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a failure value.
Definition: LogicalResult.h:72
This class represents an efficient way to signal success or failure.
Definition: LogicalResult.h:26
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type.
MaybeLocalRepr contains the indices of the constraints that can be expressed as a floordiv of an affi...
Definition: Utils.h:98
Represents the result of a symbolic lexicographic minimization computation.
Definition: Simplex.h:533
PWMAFunction lexmin
This maps assignments of symbols to the corresponding lexmin.
Definition: Simplex.h:541
PresburgerSet unboundedDomain
Contains all assignments to the symbols that made the lexmin unbounded.
Definition: Simplex.h:545
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.