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