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 
25 #define DEBUG_TYPE "presburger"
26 
27 using namespace mlir;
28 using namespace presburger;
29 
30 using llvm::SmallDenseMap;
31 using llvm::SmallDenseSet;
32 
33 std::unique_ptr<IntegerRelation> IntegerRelation::clone() const {
34  return std::make_unique<IntegerRelation>(*this);
35 }
36 
37 std::unique_ptr<IntegerPolyhedron> IntegerPolyhedron::clone() const {
38  return std::make_unique<IntegerPolyhedron>(*this);
39 }
40 
42  assert(space.getNumVars() == oSpace.getNumVars() && "invalid space!");
43  space = oSpace;
44 }
45 
47  assert(oSpace.getNumLocalVars() == 0 && "no locals should be present!");
48  assert(oSpace.getNumVars() <= getNumVars() && "invalid space!");
49  unsigned newNumLocals = getNumVars() - oSpace.getNumVars();
50  space = oSpace;
51  space.insertVar(VarKind::Local, 0, newNumLocals);
52 }
53 
55  assert(space.isEqual(other.getSpace()) && "Spaces must be equal.");
56 
58  other.getNumInequalities());
60 
61  for (unsigned r = 0, e = other.getNumInequalities(); r < e; r++) {
62  addInequality(other.getInequality(r));
63  }
64  for (unsigned r = 0, e = other.getNumEqualities(); r < e; r++) {
65  addEquality(other.getEquality(r));
66  }
67 }
68 
70  IntegerRelation result = *this;
71  result.mergeLocalVars(other);
72  result.append(other);
73  return result;
74 }
75 
76 bool IntegerRelation::isEqual(const IntegerRelation &other) const {
77  assert(space.isCompatible(other.getSpace()) && "Spaces must be compatible.");
78  return PresburgerRelation(*this).isEqual(PresburgerRelation(other));
79 }
80 
81 bool IntegerRelation::isSubsetOf(const IntegerRelation &other) const {
82  assert(space.isCompatible(other.getSpace()) && "Spaces must be compatible.");
83  return PresburgerRelation(*this).isSubsetOf(PresburgerRelation(other));
84 }
85 
88  assert(getNumSymbolVars() == 0 && "Symbols are not supported!");
91 
92  if (!maybeLexMin.isBounded())
93  return maybeLexMin;
94 
95  // The Simplex returns the lexmin over all the variables including locals. But
96  // locals are not actually part of the space and should not be returned in the
97  // result. Since the locals are placed last in the list of variables, they
98  // will be minimized last in the lexmin. So simply truncating out the locals
99  // from the end of the answer gives the desired lexmin over the dimensions.
100  assert(maybeLexMin->size() == getNumVars() &&
101  "Incorrect number of vars in lexMin!");
102  maybeLexMin->resize(getNumDimAndSymbolVars());
103  return maybeLexMin;
104 }
105 
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<int64_t> range) {
127  return llvm::all_of(range, [](int64_t 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)))
217  .computeSymbolicIntegerLexMin();
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  SymbolicLexMin result =
241  SymbolicLexSimplex(*this,
243  /*numDims=*/getNumDomainVars(),
244  /*numSymbols=*/getNumSymbolVars())),
245  isSymbol)
247 
248  // We want to return only the lexmin over the dims, so strip the locals from
249  // the computed lexmin.
250  result.lexmin.truncateOutput(result.lexmin.getNumOutputs() -
251  getNumLocalVars());
252  return result;
253 }
254 
257  return PresburgerRelation(*this).subtract(set);
258 }
259 
260 unsigned IntegerRelation::insertVar(VarKind kind, unsigned pos, unsigned num) {
261  assert(pos <= getNumVarKind(kind));
262 
263  unsigned insertPos = space.insertVar(kind, pos, num);
264  inequalities.insertColumns(insertPos, num);
265  equalities.insertColumns(insertPos, num);
266  return insertPos;
267 }
268 
269 unsigned IntegerRelation::appendVar(VarKind kind, unsigned num) {
270  unsigned pos = getNumVarKind(kind);
271  return insertVar(kind, pos, num);
272 }
273 
275  assert(eq.size() == getNumCols());
276  unsigned row = equalities.appendExtraRow();
277  for (unsigned i = 0, e = eq.size(); i < e; ++i)
278  equalities(row, i) = eq[i];
279 }
280 
282  assert(inEq.size() == getNumCols());
283  unsigned row = inequalities.appendExtraRow();
284  for (unsigned i = 0, e = inEq.size(); i < e; ++i)
285  inequalities(row, i) = inEq[i];
286 }
287 
288 void IntegerRelation::removeVar(VarKind kind, unsigned pos) {
289  removeVarRange(kind, pos, pos + 1);
290 }
291 
292 void IntegerRelation::removeVar(unsigned pos) { removeVarRange(pos, pos + 1); }
293 
294 void IntegerRelation::removeVarRange(VarKind kind, unsigned varStart,
295  unsigned varLimit) {
296  assert(varLimit <= getNumVarKind(kind));
297 
298  if (varStart >= varLimit)
299  return;
300 
301  // Remove eliminated variables from the constraints.
302  unsigned offset = getVarKindOffset(kind);
303  equalities.removeColumns(offset + varStart, varLimit - varStart);
304  inequalities.removeColumns(offset + varStart, varLimit - varStart);
305 
306  // Remove eliminated variables from the space.
307  space.removeVarRange(kind, varStart, varLimit);
308 }
309 
310 void IntegerRelation::removeVarRange(unsigned varStart, unsigned varLimit) {
311  assert(varLimit <= getNumVars());
312 
313  if (varStart >= varLimit)
314  return;
315 
316  // Helper function to remove vars of the specified kind in the given range
317  // [start, limit), The range is absolute (i.e. it is not relative to the kind
318  // of variable). Also updates `limit` to reflect the deleted variables.
319  auto removeVarKindInRange = [this](VarKind kind, unsigned &start,
320  unsigned &limit) {
321  if (start >= limit)
322  return;
323 
324  unsigned offset = getVarKindOffset(kind);
325  unsigned num = getNumVarKind(kind);
326 
327  // Get `start`, `limit` relative to the specified kind.
328  unsigned relativeStart =
329  start <= offset ? 0 : std::min(num, start - offset);
330  unsigned relativeLimit =
331  limit <= offset ? 0 : std::min(num, limit - offset);
332 
333  // Remove vars of the specified kind in the relative range.
334  removeVarRange(kind, relativeStart, relativeLimit);
335 
336  // Update `limit` to reflect deleted variables.
337  // `start` does not need to be updated because any variables that are
338  // deleted are after position `start`.
339  limit -= relativeLimit - relativeStart;
340  };
341 
342  removeVarKindInRange(VarKind::Domain, varStart, varLimit);
343  removeVarKindInRange(VarKind::Range, varStart, varLimit);
344  removeVarKindInRange(VarKind::Symbol, varStart, varLimit);
345  removeVarKindInRange(VarKind::Local, varStart, varLimit);
346 }
347 
349  equalities.removeRow(pos);
350 }
351 
353  inequalities.removeRow(pos);
354 }
355 
356 void IntegerRelation::removeEqualityRange(unsigned start, unsigned end) {
357  if (start >= end)
358  return;
359  equalities.removeRows(start, end - start);
360 }
361 
362 void IntegerRelation::removeInequalityRange(unsigned start, unsigned end) {
363  if (start >= end)
364  return;
365  inequalities.removeRows(start, end - start);
366 }
367 
368 void IntegerRelation::swapVar(unsigned posA, unsigned posB) {
369  assert(posA < getNumVars() && "invalid position A");
370  assert(posB < getNumVars() && "invalid position B");
371 
372  if (posA == posB)
373  return;
374 
375  inequalities.swapColumns(posA, posB);
376  equalities.swapColumns(posA, posB);
377 }
378 
382 }
383 
384 /// Gather all lower and upper bounds of the variable at `pos`, and
385 /// optionally any equalities on it. In addition, the bounds are to be
386 /// independent of variables in position range [`offset`, `offset` + `num`).
388  unsigned pos, SmallVectorImpl<unsigned> *lbIndices,
390  unsigned offset, unsigned num) const {
391  assert(pos < getNumVars() && "invalid position");
392  assert(offset + num < getNumCols() && "invalid range");
393 
394  // Checks for a constraint that has a non-zero coeff for the variables in
395  // the position range [offset, offset + num) while ignoring `pos`.
396  auto containsConstraintDependentOnRange = [&](unsigned r, bool isEq) {
397  unsigned c, f;
398  auto cst = isEq ? getEquality(r) : getInequality(r);
399  for (c = offset, f = offset + num; c < f; ++c) {
400  if (c == pos)
401  continue;
402  if (cst[c] != 0)
403  break;
404  }
405  return c < f;
406  };
407 
408  // Gather all lower bounds and upper bounds of the variable. Since the
409  // canonical form c_1*x_1 + c_2*x_2 + ... + c_0 >= 0, a constraint is a lower
410  // bound for x_i if c_i >= 1, and an upper bound if c_i <= -1.
411  for (unsigned r = 0, e = getNumInequalities(); r < e; r++) {
412  // The bounds are to be independent of [offset, offset + num) columns.
413  if (containsConstraintDependentOnRange(r, /*isEq=*/false))
414  continue;
415  if (atIneq(r, pos) >= 1) {
416  // Lower bound.
417  lbIndices->push_back(r);
418  } else if (atIneq(r, pos) <= -1) {
419  // Upper bound.
420  ubIndices->push_back(r);
421  }
422  }
423 
424  // An equality is both a lower and upper bound. Record any equalities
425  // involving the pos^th variable.
426  if (!eqIndices)
427  return;
428 
429  for (unsigned r = 0, e = getNumEqualities(); r < e; r++) {
430  if (atEq(r, pos) == 0)
431  continue;
432  if (containsConstraintDependentOnRange(r, /*isEq=*/true))
433  continue;
434  eqIndices->push_back(r);
435  }
436 }
437 
440  return false;
442  return false;
443  return true;
444 }
445 
447  if (values.empty())
448  return;
449  assert(pos + values.size() <= getNumVars() &&
450  "invalid position or too many values");
451  // Setting x_j = p in sum_i a_i x_i + c is equivalent to adding p*a_j to the
452  // constant term and removing the var x_j. We do this for all the vars
453  // pos, pos + 1, ... pos + values.size() - 1.
454  unsigned constantColPos = getNumCols() - 1;
455  for (unsigned i = 0, numVals = values.size(); i < numVals; ++i)
456  inequalities.addToColumn(i + pos, constantColPos, values[i]);
457  for (unsigned i = 0, numVals = values.size(); i < numVals; ++i)
458  equalities.addToColumn(i + pos, constantColPos, values[i]);
459  removeVarRange(pos, pos + values.size());
460 }
461 
463  *this = other;
464 }
465 
466 // Searches for a constraint with a non-zero coefficient at `colIdx` in
467 // equality (isEq=true) or inequality (isEq=false) constraints.
468 // Returns true and sets row found in search in `rowIdx`, false otherwise.
469 bool IntegerRelation::findConstraintWithNonZeroAt(unsigned colIdx, bool isEq,
470  unsigned *rowIdx) const {
471  assert(colIdx < getNumCols() && "position out of bounds");
472  auto at = [&](unsigned rowIdx) -> int64_t {
473  return isEq ? atEq(rowIdx, colIdx) : atIneq(rowIdx, colIdx);
474  };
475  unsigned e = isEq ? getNumEqualities() : getNumInequalities();
476  for (*rowIdx = 0; *rowIdx < e; ++(*rowIdx)) {
477  if (at(*rowIdx) != 0) {
478  return true;
479  }
480  }
481  return false;
482 }
483 
485  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i)
487  for (unsigned i = 0, e = getNumInequalities(); i < e; ++i)
489 }
490 
492  assert(hasConsistentState());
493  auto check = [&](bool isEq) -> bool {
494  unsigned numCols = getNumCols();
495  unsigned numRows = isEq ? getNumEqualities() : getNumInequalities();
496  for (unsigned i = 0, e = numRows; i < e; ++i) {
497  unsigned j;
498  for (j = 0; j < numCols - 1; ++j) {
499  int64_t v = isEq ? atEq(i, j) : atIneq(i, j);
500  // Skip rows with non-zero variable coefficients.
501  if (v != 0)
502  break;
503  }
504  if (j < numCols - 1) {
505  continue;
506  }
507  // Check validity of constant term at 'numCols - 1' w.r.t 'isEq'.
508  // Example invalid constraints include: '1 == 0' or '-1 >= 0'
509  int64_t v = isEq ? atEq(i, numCols - 1) : atIneq(i, numCols - 1);
510  if ((isEq && v != 0) || (!isEq && v < 0)) {
511  return true;
512  }
513  }
514  return false;
515  };
516  if (check(/*isEq=*/true))
517  return true;
518  return check(/*isEq=*/false);
519 }
520 
521 /// Eliminate variable from constraint at `rowIdx` based on coefficient at
522 /// pivotRow, pivotCol. Columns in range [elimColStart, pivotCol) will not be
523 /// updated as they have already been eliminated.
524 static void eliminateFromConstraint(IntegerRelation *constraints,
525  unsigned rowIdx, unsigned pivotRow,
526  unsigned pivotCol, unsigned elimColStart,
527  bool isEq) {
528  // Skip if equality 'rowIdx' if same as 'pivotRow'.
529  if (isEq && rowIdx == pivotRow)
530  return;
531  auto at = [&](unsigned i, unsigned j) -> int64_t {
532  return isEq ? constraints->atEq(i, j) : constraints->atIneq(i, j);
533  };
534  int64_t leadCoeff = at(rowIdx, pivotCol);
535  // Skip if leading coefficient at 'rowIdx' is already zero.
536  if (leadCoeff == 0)
537  return;
538  int64_t pivotCoeff = constraints->atEq(pivotRow, pivotCol);
539  int64_t sign = (leadCoeff * pivotCoeff > 0) ? -1 : 1;
540  int64_t lcm = mlir::lcm(pivotCoeff, leadCoeff);
541  int64_t pivotMultiplier = sign * (lcm / std::abs(pivotCoeff));
542  int64_t rowMultiplier = lcm / std::abs(leadCoeff);
543 
544  unsigned numCols = constraints->getNumCols();
545  for (unsigned j = 0; j < numCols; ++j) {
546  // Skip updating column 'j' if it was just eliminated.
547  if (j >= elimColStart && j < pivotCol)
548  continue;
549  int64_t v = pivotMultiplier * constraints->atEq(pivotRow, j) +
550  rowMultiplier * at(rowIdx, j);
551  isEq ? constraints->atEq(rowIdx, j) = v
552  : constraints->atIneq(rowIdx, j) = v;
553  }
554 }
555 
556 /// Returns the position of the variable that has the minimum <number of lower
557 /// bounds> times <number of upper bounds> from the specified range of
558 /// variables [start, end). It is often best to eliminate in the increasing
559 /// order of these counts when doing Fourier-Motzkin elimination since FM adds
560 /// that many new constraints.
561 static unsigned getBestVarToEliminate(const IntegerRelation &cst,
562  unsigned start, unsigned end) {
563  assert(start < cst.getNumVars() && end < cst.getNumVars() + 1);
564 
565  auto getProductOfNumLowerUpperBounds = [&](unsigned pos) {
566  unsigned numLb = 0;
567  unsigned numUb = 0;
568  for (unsigned r = 0, e = cst.getNumInequalities(); r < e; r++) {
569  if (cst.atIneq(r, pos) > 0) {
570  ++numLb;
571  } else if (cst.atIneq(r, pos) < 0) {
572  ++numUb;
573  }
574  }
575  return numLb * numUb;
576  };
577 
578  unsigned minLoc = start;
579  unsigned min = getProductOfNumLowerUpperBounds(start);
580  for (unsigned c = start + 1; c < end; c++) {
581  unsigned numLbUbProduct = getProductOfNumLowerUpperBounds(c);
582  if (numLbUbProduct < min) {
583  min = numLbUbProduct;
584  minLoc = c;
585  }
586  }
587  return minLoc;
588 }
589 
590 // Checks for emptiness of the set by eliminating variables successively and
591 // using the GCD test (on all equality constraints) and checking for trivially
592 // invalid constraints. Returns 'true' if the constraint system is found to be
593 // empty; false otherwise.
596  return true;
597 
598  IntegerRelation tmpCst(*this);
599 
600  // First, eliminate as many local variables as possible using equalities.
601  tmpCst.removeRedundantLocalVars();
602  if (tmpCst.isEmptyByGCDTest() || tmpCst.hasInvalidConstraint())
603  return true;
604 
605  // Eliminate as many variables as possible using Gaussian elimination.
606  unsigned currentPos = 0;
607  while (currentPos < tmpCst.getNumVars()) {
608  tmpCst.gaussianEliminateVars(currentPos, tmpCst.getNumVars());
609  ++currentPos;
610  // We check emptiness through trivial checks after eliminating each ID to
611  // detect emptiness early. Since the checks isEmptyByGCDTest() and
612  // hasInvalidConstraint() are linear time and single sweep on the constraint
613  // buffer, this appears reasonable - but can optimize in the future.
614  if (tmpCst.hasInvalidConstraint() || tmpCst.isEmptyByGCDTest())
615  return true;
616  }
617 
618  // Eliminate the remaining using FM.
619  for (unsigned i = 0, e = tmpCst.getNumVars(); i < e; i++) {
621  getBestVarToEliminate(tmpCst, 0, tmpCst.getNumVars()));
622  // Check for a constraint explosion. This rarely happens in practice, but
623  // this check exists as a safeguard against improperly constructed
624  // constraint systems or artificially created arbitrarily complex systems
625  // that aren't the intended use case for IntegerRelation. This is
626  // needed since FM has a worst case exponential complexity in theory.
627  if (tmpCst.getNumConstraints() >= kExplosionFactor * getNumVars()) {
628  LLVM_DEBUG(llvm::dbgs() << "FM constraint explosion detected\n");
629  return false;
630  }
631 
632  // FM wouldn't have modified the equalities in any way. So no need to again
633  // run GCD test. Check for trivial invalid constraints.
634  if (tmpCst.hasInvalidConstraint())
635  return true;
636  }
637  return false;
638 }
639 
640 // Runs the GCD test on all equality constraints. Returns 'true' if this test
641 // fails on any equality. Returns 'false' otherwise.
642 // This test can be used to disprove the existence of a solution. If it returns
643 // true, no integer solution to the equality constraints can exist.
644 //
645 // GCD test definition:
646 //
647 // The equality constraint:
648 //
649 // c_1*x_1 + c_2*x_2 + ... + c_n*x_n = c_0
650 //
651 // has an integer solution iff:
652 //
653 // GCD of c_1, c_2, ..., c_n divides c_0.
654 //
656  assert(hasConsistentState());
657  unsigned numCols = getNumCols();
658  for (unsigned i = 0, e = getNumEqualities(); i < e; ++i) {
659  uint64_t gcd = std::abs(atEq(i, 0));
660  for (unsigned j = 1; j < numCols - 1; ++j) {
661  gcd = llvm::GreatestCommonDivisor64(gcd, std::abs(atEq(i, j)));
662  }
663  int64_t v = std::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<int64_t, 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  int64_t 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<int64_t, 8> coneSample(llvm::map_range(shrunkenConeSample, ceil));
862 
863  // 6) Return transform * concat(boundedSample, coneSample).
864  SmallVector<int64_t, 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.
872 static int64_t valueAt(ArrayRef<int64_t> expr, ArrayRef<int64_t> point) {
873  assert(expr.size() == 1 + point.size() &&
874  "Dimensionalities of point and expression don't match!");
875  int64_t 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.
962  int64_t gcd = inequalities.normalizeRow(i, getNumCols() - 1);
963  if (gcd > 1)
964  atIneq(i, numCols - 1) = mlir::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 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  uint64_t count = 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 0;
1128 
1129  count *= (*max - *min + 1);
1130  }
1131 
1132  if (count == 0)
1133  return 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 (std::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, int64_t value) {
1284  assert(pos < getNumCols());
1285  if (type == BoundType::EQ) {
1286  unsigned row = equalities.appendExtraRow();
1287  equalities(row, pos) = 1;
1288  equalities(row, getNumCols() - 1) = -value;
1289  } else {
1290  unsigned row = inequalities.appendExtraRow();
1291  inequalities(row, pos) = type == BoundType::LB ? 1 : -1;
1292  inequalities(row, getNumCols() - 1) =
1293  type == BoundType::LB ? -value : value;
1294  }
1295 }
1296 
1298  int64_t value) {
1299  assert(type != BoundType::EQ && "EQ not implemented");
1300  assert(expr.size() == getNumCols());
1301  unsigned row = inequalities.appendExtraRow();
1302  for (unsigned i = 0, e = expr.size(); i < e; ++i)
1303  inequalities(row, i) = type == BoundType::LB ? expr[i] : -expr[i];
1305  type == BoundType::LB ? -value : value;
1306 }
1307 
1308 /// Adds a new local variable as the floordiv of an affine function of other
1309 /// variables, the coefficients of which are provided in 'dividend' and with
1310 /// respect to a positive constant 'divisor'. Two constraints are added to the
1311 /// system to capture equivalence with the floordiv.
1312 /// q = expr floordiv c <=> c*q <= expr <= c*q + c - 1.
1314  int64_t divisor) {
1315  assert(dividend.size() == getNumCols() && "incorrect dividend size");
1316  assert(divisor > 0 && "positive divisor expected");
1317 
1319 
1320  SmallVector<int64_t, 8> dividendCopy(dividend.begin(), dividend.end());
1321  dividendCopy.insert(dividendCopy.end() - 1, 0);
1322  addInequality(
1323  getDivLowerBound(dividendCopy, divisor, dividendCopy.size() - 2));
1324  addInequality(
1325  getDivUpperBound(dividendCopy, divisor, dividendCopy.size() - 2));
1326 }
1327 
1328 /// Finds an equality that equates the specified variable to a constant.
1329 /// Returns the position of the equality row. If 'symbolic' is set to true,
1330 /// symbols are also treated like a constant, i.e., an affine function of the
1331 /// symbols is also treated like a constant. Returns -1 if such an equality
1332 /// could not be found.
1333 static int findEqualityToConstant(const IntegerRelation &cst, unsigned pos,
1334  bool symbolic = false) {
1335  assert(pos < cst.getNumVars() && "invalid position");
1336  for (unsigned r = 0, e = cst.getNumEqualities(); r < e; r++) {
1337  int64_t v = cst.atEq(r, pos);
1338  if (v * v != 1)
1339  continue;
1340  unsigned c;
1341  unsigned f = symbolic ? cst.getNumDimVars() : cst.getNumVars();
1342  // This checks for zeros in all positions other than 'pos' in [0, f)
1343  for (c = 0; c < f; c++) {
1344  if (c == pos)
1345  continue;
1346  if (cst.atEq(r, c) != 0) {
1347  // Dependent on another variable.
1348  break;
1349  }
1350  }
1351  if (c == f)
1352  // Equality is free of other variables.
1353  return r;
1354  }
1355  return -1;
1356 }
1357 
1359  assert(pos < getNumVars() && "invalid position");
1360  int rowIdx;
1361  if ((rowIdx = findEqualityToConstant(*this, pos)) == -1)
1362  return failure();
1363 
1364  // atEq(rowIdx, pos) is either -1 or 1.
1365  assert(atEq(rowIdx, pos) * atEq(rowIdx, pos) == 1);
1366  int64_t constVal = -atEq(rowIdx, getNumCols() - 1) / atEq(rowIdx, pos);
1367  setAndEliminate(pos, constVal);
1368  return success();
1369 }
1370 
1371 void IntegerRelation::constantFoldVarRange(unsigned pos, unsigned num) {
1372  for (unsigned s = pos, t = pos, e = pos + num; s < e; s++) {
1373  if (failed(constantFoldVar(t)))
1374  t++;
1375  }
1376 }
1377 
1378 /// Returns a non-negative constant bound on the extent (upper bound - lower
1379 /// bound) of the specified variable if it is found to be a constant; returns
1380 /// None if it's not a constant. This methods treats symbolic variables
1381 /// specially, i.e., it looks for constant differences between affine
1382 /// expressions involving only the symbolic variables. See comments at
1383 /// function definition for example. 'lb', if provided, is set to the lower
1384 /// bound associated with the constant difference. Note that 'lb' is purely
1385 /// symbolic and thus will contain the coefficients of the symbolic variables
1386 /// and the constant coefficient.
1387 // Egs: 0 <= i <= 15, return 16.
1388 // s0 + 2 <= i <= s0 + 17, returns 16. (s0 has to be a symbol)
1389 // s0 + s1 + 16 <= d0 <= s0 + s1 + 31, returns 16.
1390 // s0 - 7 <= 8*j <= s0 returns 1 with lb = s0, lbDivisor = 8 (since lb =
1391 // ceil(s0 - 7 / 8) = floor(s0 / 8)).
1393  unsigned pos, SmallVectorImpl<int64_t> *lb, int64_t *boundFloorDivisor,
1394  SmallVectorImpl<int64_t> *ub, unsigned *minLbPos,
1395  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  [](int64_t coeff) { return coeff == 0; }))
1408  return None;
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  int64_t 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 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 None;
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<int64_t> minDiff = None;
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  int64_t 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<int64_t>(diff, 0);
1480  if (minDiff == None || 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 None;
1540 
1541  Optional<int64_t> minOrMaxConst = None;
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  int64_t boundConst =
1563  isLower ? mlir::ceilDiv(-atIneq(r, getNumCols() - 1), atIneq(r, 0))
1564  : mlir::floorDiv(atIneq(r, getNumCols() - 1), -atIneq(r, 0));
1565  if (isLower) {
1566  if (minOrMaxConst == None || boundConst > minOrMaxConst)
1567  minOrMaxConst = boundConst;
1568  } else {
1569  if (minOrMaxConst == None || 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<int64_t> lb =
1587  IntegerRelation(*this).computeConstantLowerOrUpperBound</*isLower=*/true>(
1588  pos);
1589  Optional<int64_t> ub =
1590  IntegerRelation(*this)
1591  .computeConstantLowerOrUpperBound</*isLower=*/false>(pos);
1592  return (lb && ub && *lb == *ub) ? Optional<int64_t>(*ub) : None;
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<int64_t>, std::pair<unsigned, int64_t>>
1634  rowsWithoutConstTerm;
1635  // To unique rows.
1636  SmallDenseSet<ArrayRef<int64_t>, 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  int64_t *rowStart = &inequalities(r, 0);
1651  auto row = ArrayRef<int64_t>(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  int64_t constTerm = atIneq(r, getNumCols() - 1);
1662  auto rowWithoutConstTerm = ArrayRef<int64_t>(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) {
1819  ineq.reserve(newRel.getNumCols());
1820  int64_t 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  int64_t 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  int64_t lcm = mlir::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) {
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<int64_t> a, ArrayRef<int64_t> 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<int64_t, 8>> boundingLbs;
1987  std::vector<SmallVector<int64_t, 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<int64_t, 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<int64_t, 8> newLb(getNumCols()), newUb(getNumCols());
1998 
1999  int64_t 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<int64_t>());
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 }
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt lcm(const MPInt &a, const MPInt &b)
Returns the least common multiple of &#39;a&#39; and &#39;b&#39;.
Definition: MPInt.h:406
int64_t normalizeRow(unsigned row, unsigned nCols)
Divide the first nCols of the specified row by their GCD.
Definition: Matrix.cpp:219
Include the generated interface declarations.
virtual bool hasConsistentState() const
Returns false if the fields corresponding to various variable counts, or equality/inequality buffer s...
void addLocalFloorDiv(ArrayRef< int64_t > dividend, int64_t divisor)
Adds a new local variable as the floordiv of an affine function of other variables, the coefficients of which are provided in dividend and with respect to a positive constant divisor.
int64_t lcm(int64_t a, int64_t b)
Returns the least common multiple of &#39;a&#39; and &#39;b&#39;.
Definition: MathExtras.h:51
Matrix inequalities
Coefficients of affine inequalities (in >= 0 form).
void removeInequalityRange(unsigned start, unsigned end)
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt ceilDiv(const MPInt &lhs, const MPInt &rhs)
Definition: MPInt.h:373
LogicalResult constantFoldVar(unsigned pos)
Tries to fold the specified variable to a constant using a trivial equality detection; if successful...
Class storing division representation of local variables of a constraint system.
Definition: Utils.h:116
Optional< uint64_t > computeVolume() const
Compute an overapproximation of the number of integer points in the relation.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt abs(const MPInt &x)
Definition: MPInt.h:369
SymbolicLexMin computeSymbolicIntegerLexMin()
The lexmin will be stored as a function lexmin from symbols to non-symbols in the result...
Definition: Simplex.cpp:509
void removeDuplicateDivs(llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Removes duplicate divisions.
Definition: Utils.cpp:360
bool isEmpty() const
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
Definition: Simplex.cpp:1039
unsigned appendVar(VarKind kind, unsigned num=1)
Append num variables of the specified kind after the last variable.
bool hasConsistentState() const
Return whether the Matrix is in a consistent state with all its invariants satisfied.
Definition: Matrix.cpp:260
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...
Definition: Simplex.h:693
void print(llvm::raw_ostream &os) const
Optional< int64_t > computeConstantLowerOrUpperBound(unsigned pos)
Returns the constant lower bound bound if isLower is true, and the upper bound if isLower is false...
virtual void swapVar(unsigned posA, unsigned posB)
Swap the posA^th variable with the posB^th variable.
virtual void eliminateRedundantLocalVar(unsigned posA, unsigned posB)
Eliminate the posB^th local variable, replacing every instance of it with the posA^th local variable...
unsigned getNumOutputs() const
Definition: PWMAFunction.h:152
void removeRows(unsigned pos, unsigned count)
Remove the rows having positions pos, pos + 1, ...
Definition: Matrix.cpp:173
bool isEqual(const PresburgerRelation &set) const
Return true if this set is equal to the given set, and false otherwise.
unsigned getNumRows() const
Definition: Matrix.h:75
bool isHyperRectangular(unsigned pos, unsigned num) const
Returns true if the set can be trivially detected as being hyper-rectangular on the specified contigu...
void compose(const IntegerRelation &rel)
Let the relation this be R1, and the relation rel be R2.
A class to perform symbolic lexicographic optimization, i.e., to find, for every assignment to the sy...
Definition: Simplex.h:574
void addEquality(ArrayRef< int64_t > eq)
Adds an equality from the coefficients specified in eq.
SmallVector< int64_t, 8 > getDivUpperBound(ArrayRef< int64_t > dividend, int64_t 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:293
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1) override
Insert num variables of the specified kind at position pos.
MaybeLocalRepr contains the indices of the constraints that can be expressed as a floordiv of an affi...
Definition: Utils.h:97
std::unique_ptr< IntegerPolyhedron > clone() const
void fillRow(unsigned row, int64_t value)
Definition: Matrix.cpp:189
IntegerPolyhedron getRangeSet() const
Return a set corresponding to all points in the range of the relation.
void clearConstraints()
Removes all equalities and inequalities.
static void copy(Location loc, Value dst, Value src, Value size, OpBuilder &builder)
Copies the given number of bytes from src to dst pointers.
bool failed(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a failure value...
Definition: LogicalResult.h:72
bool isMarkedRedundant(unsigned constraintIndex) const
Returns whether the specified constraint has been marked as redundant.
Definition: Simplex.cpp:1374
void addToColumn(unsigned sourceColumn, unsigned targetColumn, int64_t scale)
Add scale multiples of the source column to the target column.
Definition: Matrix.cpp:201
VarKind getVarKindAt(unsigned pos) const
Return the VarKind of the var at the specified position.
ArrayRef< int64_t > getInequality(unsigned idx) const
DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const
Returns a DivisonRepr representing the division representation of local variables in the constraint s...
bool isIntegerEmpty() const
Returns true if the set of constraints is found to have no solution, false if a solution exists...
This is a class to represent a resizable matrix.
Definition: Matrix.h:34
void truncate(const CountsSnapshot &counts)
void applyDomain(const IntegerRelation &rel)
Given a relation rel, apply the relation to the domain of this relation.
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin() const
Get the lexicographically minimum rational point satisfying the constraints.
PresburgerSet unboundedDomain
Contains all assignments to the symbols that made the lexmin unbounded.
Definition: Simplex.h:543
static void getCommonConstraints(const IntegerRelation &a, const IntegerRelation &b, IntegerRelation &c)
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of vars starts.
void clearRepr(unsigned i)
Definition: Utils.h:137
Optional< SmallVector< Fraction, 8 > > getRationalSample() const
Returns the current sample point, which may contain non-integer (rational) coordinates.
Definition: Simplex.cpp:1535
bool succeeded(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a success value...
Definition: LogicalResult.h:68
void reserveRows(unsigned rows)
Reserve enough space to resize to the specified number of rows without reallocations.
Definition: Matrix.cpp:35
void setAndEliminate(unsigned pos, ArrayRef< int64_t > values)
Sets the values.size() variables starting at pos to the specified values and removes them...
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:265
static int findEqualityToConstant(const IntegerRelation &cst, unsigned pos, bool symbolic=false)
Finds an equality that equates the specified variable to a constant.
bool hasAllReprs() const
Definition: Utils.h:132
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace.
int64_t atIneq(unsigned i, unsigned j) const
Returns the value at the specified inequality row and column.
SmallVector< int64_t, 8 > getDivLowerBound(ArrayRef< int64_t > dividend, int64_t divisor, unsigned localVarIdx)
Definition: Utils.cpp:303
LogicalResult unionBoundingBox(const IntegerRelation &other)
Updates the constraints to be the smallest bounding (enclosing) box that contains the points of this ...
virtual void fourierMotzkinEliminate(unsigned pos, bool darkShadow=false, bool *isResultIntegerExact=nullptr)
Eliminates the variable at the specified position using Fourier-Motzkin variable elimination, but uses Gaussian elimination if there is an equality involving that variable.
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
BoundType
The type of bound: equal, lower bound or upper bound.
void removeRedundantInequalities()
A more expensive check than removeTrivialRedundancy to detect redundant inequalities.
static constexpr const bool value
void swapColumns(unsigned column, unsigned otherColumn)
Swap the given columns.
Definition: Matrix.cpp:78
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
void print(raw_ostream &os) const
void copyRow(unsigned sourceRow, unsigned targetRow)
Definition: Matrix.cpp:182
bool isUnbounded()
Returns true if the polytope is unbounded, i.e., extends to infinity in some direction.
Definition: Simplex.cpp:1435
void removeRedundantLocalVars()
Removes local variables using equalities.
PresburgerSet unionSet(const PresburgerRelation &set) const
These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...
unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit)
Eliminates variables from equality and inequality constraints in column range [posStart, posLimit).
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 addInequality(ArrayRef< int64_t > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
unsigned getVarKindEnd(VarKind kind) const
Return the index at Which the specified kind of vars ends.
IntegerRelation intersect(IntegerRelation other) const
Return the intersection of the two relations.
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 <n...
bool isEmptyByGCDTest() const
Runs the GCD test on all equality constraints.
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
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.
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...
LogicalResult success(bool isSuccess=true)
Utility function to generate a LogicalResult.
Definition: LogicalResult.h:56
static std::pair< unsigned, LinearTransform > makeTransformToColumnEchelon(Matrix m)
This class represents an efficient way to signal success or failure.
Definition: LogicalResult.h:26
LogicalResult failure(bool isFailure=true)
Utility function to generate a LogicalResult.
Definition: LogicalResult.h:62
void projectOut(unsigned pos, unsigned num)
Projects out (aka eliminates) num variables starting at position pos.
MutableArrayRef< int64_t > getDividend(unsigned i)
Definition: Utils.h:140
int64_t floorDiv(int64_t lhs, int64_t rhs)
Returns the result of MLIR&#39;s floordiv operation on constants.
Definition: MathExtras.h:33
bool isColZero(unsigned pos) const
Returns true if the pos^th column is all zero for both inequalities and equalities.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set. ...
BoundCmpResult
void inverse()
Invert the relation i.e., swap its domain and range.
bool hasInvalidConstraint() const
Checks all rows of equality/inequality constraints for trivial contradictions (for example: 1 == 0...
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type...
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace, which should have the same number of ids as the current space.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set. ...
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
void insertColumns(unsigned pos, unsigned count)
Insert columns having positions pos, pos + 1, ...
Definition: Matrix.cpp:103
void removeRow(unsigned pos)
Definition: Matrix.cpp:172
void truncateOutput(unsigned count)
Truncate the output dimensions to the first count dimensions.
bool isEqual(const IntegerRelation &other) const
Return whether this and other are equal.
int64_t ceilDiv(int64_t lhs, int64_t rhs)
Returns the result of MLIR&#39;s ceildiv operation on constants.
Definition: MathExtras.h:23
unsigned & getDenom(unsigned i)
Definition: Utils.h:148
ArrayRef< int64_t > getEquality(unsigned idx) const
void intersectRange(const IntegerPolyhedron &poly)
Intersect the given poly with the range in-place.
bool hasOnlyDivLocals() const
Check whether all local ids have a division representation.
void gcdTightenInequalities()
Tightens inequalities given that we are dealing with integer spaces.
static int64_t valueAt(ArrayRef< int64_t > expr, ArrayRef< int64_t > point)
Helper to evaluate an affine expression at a point.
LLVM_ATTRIBUTE_ALWAYS_INLINE MPInt gcd(const MPInt &a, const MPInt &b)
Definition: MPInt.h:398
static constexpr unsigned kExplosionFactor
A parameter that controls detection of an unrealistic number of constraints.
VarKind
Kind of variable.
PresburgerSet subtract(const PresburgerSet &other) const
Return the set difference of this set and the given set, i.e., return this \ set. ...
Matrix equalities
Coefficients of affine equalities (in == 0 form).
MaybeOptimum< SmallVector< int64_t, 8 > > findIntegerLexMin() const
Same as above, but returns lexicographically minimal integer point.
bool isBoundedAlongConstraint(unsigned constraintIndex)
Returns whether the perpendicular of the specified constraint is a is a direction along which the pol...
Definition: Simplex.cpp:1364
unsigned appendExtraRow()
Add an extra row at the bottom of the matrix and return its position.
Definition: Matrix.cpp:39
OptimumKind getKind() const
Definition: Utils.h:50
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...
Optional< int64_t > getConstantBoundOnDimSize(unsigned pos, SmallVectorImpl< int64_t > *lb=nullptr, int64_t *boundFloorDivisor=nullptr, SmallVectorImpl< int64_t > *ub=nullptr, unsigned *minLbPos=nullptr, unsigned *minUbPos=nullptr) const
Returns the smallest known constant bound for the extent of the specified variable (pos^th)...
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, pos + num) variables.
void removeVar(VarKind kind, unsigned pos)
Removes variables of the specified kind with the specified pos (or within the specified range) from t...
void negateRow(unsigned row)
Negate the specified row.
Definition: Matrix.cpp:214
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of var starts.
IntegerRelation(unsigned numReservedInequalities, unsigned numReservedEqualities, unsigned numReservedCols, const PresburgerSpace &space)
Constructs a relation reserving memory for the specified number of constraints and variables...
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.
void removeTrivialRedundancy()
Removes duplicate constraints, trivially true constraints, and constraints that can be detected as re...
bool isSubsetOf(const PresburgerRelation &set) const
Return true if this set is a subset of the given set, and false otherwise.
void constantFoldVarRange(unsigned pos, unsigned num)
This method calls constantFoldVar for the specified range of variables, num variables starting at pos...
void resizeVertically(unsigned newNRows)
Definition: Matrix.cpp:64
PresburgerSet getDomain() const
Return the domain of this piece-wise MultiAffineFunction.
void applyRange(const IntegerRelation &rel)
Given a relation rel, apply the relation to the range of this relation.
static Value min(ImplicitLocOpBuilder &builder, Value value, Value bound)
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:1394
bool isSubsetOf(const IntegerRelation &other) const
Return whether this is a subset of the given IntegerRelation.
static void removeConstraintsInvolvingVarRange(IntegerRelation &poly, unsigned begin, unsigned count)
void append(const IntegerRelation &other)
Appends constraints from other into this.
LogicalResult gaussianEliminateVar(unsigned position)
Eliminates a single variable at position from equality and inequality constraints.
void addBound(BoundType type, unsigned pos, int64_t value)
Adds a constant bound for the specified variable.
bool containsPoint(ArrayRef< int64_t > point) const
Returns true if the given point satisfies the constraints, or false otherwise.
Represents the result of a symbolic lexicographic minimization computation.
Definition: Simplex.h:531
void normalizeConstraintsByGCD()
Normalized each constraints by the GCD of its coefficients.
MaybeOptimum< SmallVector< int64_t, 8 > > findIntegerLexMin()
Return the lexicographically minimum integer solution to the constraints.
Definition: Simplex.cpp:287
int64_t ceil(Fraction f)
Definition: Fraction.h:65
std::pair< MaybeOptimum< int64_t >, MaybeOptimum< int64_t > > computeIntegerBounds(ArrayRef< int64_t > coeffs)
Returns a (min, max) pair denoting the minimum and maximum integer values of the given expression...
Definition: Simplex.cpp:2067
virtual void printSpace(raw_ostream &os) const
Prints the number of constraints, dimensions, symbols and locals in the IntegerRelation.
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 ...
PresburgerRelation computeReprWithOnlyDivLocals() const
Compute an equivalent representation of the same set, such that all local vars in all disjuncts have ...
void intersectDomain(const IntegerPolyhedron &poly)
Intersect the given poly with the domain in-place.
virtual void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
void removeIndependentConstraints(unsigned pos, unsigned num)
Removes constraints that are independent of (i.e., do not have a coefficient) variables in the range ...
bool isEmpty() const
Checks for emptiness by performing variable elimination on all variables, running the GCD test on eac...
SymbolicLexMin findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation.
SmallVector< int64_t, 8 > postMultiplyWithColumn(ArrayRef< int64_t > colVec) const
int64_t atEq(unsigned i, unsigned j) const
Returns the value at the specified equality row and column.
unsigned getNumCols() const
Returns the number of columns in the constraint system.
MaybeOptimum< SmallVector< Fraction, 8 > > findRationalLexMin()
Return the lexicographically minimum rational solution to the constraints.
Definition: Simplex.cpp:216
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
std::unique_ptr< IntegerRelation > clone() const
PWMAFunction lexmin
This maps assignments of symbols to the corresponding lexmin.
Definition: Simplex.h:539
MaybeLocalRepr computeSingleVarRepr(const IntegerRelation &cst, ArrayRef< bool > foundRepr, unsigned pos, MutableArrayRef< int64_t > dividend, unsigned &divisor)
Returns the MaybeLocalRepr struct which contains the indices of the constraints that can be expressed...
Definition: Utils.cpp:216
virtual void clearAndCopyFrom(const IntegerRelation &other)
Replaces the contents of this IntegerRelation with other.
void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
Removes variables of the specified kind in the column range [varStart, varLimit). ...
IntegerPolyhedron getDomainSet() const
Return a set corresponding to all points in the domain of the relation.
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables...
Matrix getBoundedDirections() const
Returns a matrix where each row is a vector along which the polytope is bounded.
A class for lexicographic optimization without any symbols.
Definition: Simplex.h:480
Optional< SmallVector< int64_t, 8 > > containsPointNoLocal(ArrayRef< int64_t > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists...
bool isEqual(const PresburgerSpace &other) const
Returns true if both the spaces are equal including local variables i.e.
IntegerRelation applyTo(const IntegerRelation &rel) const
static bool rangeIsZero(ArrayRef< int64_t > range)
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...
void removeRedundantConstraints()
Removes redundant constraints using Simplex.
void removeEqualityRange(unsigned start, unsigned end)
Remove the (in)equalities at positions [start, end).
static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)
IntegerPolyhedron intersect(const IntegerPolyhedron &other) const
Return the intersection of the two relations.
Optional< int64_t > getConstantBound(BoundType type, unsigned pos) const
Returns the constant bound for the pos^th variable if there is one; None otherwise.
void removeColumns(unsigned pos, unsigned count)
Remove the columns having positions pos, pos + 1, ...
Definition: Matrix.cpp:145
void setSpaceExceptLocals(const PresburgerSpace &oSpace)
Set the space to oSpace, which should not have any local ids.
bool isBounded() const
Definition: Utils.h:51
static PresburgerSpace getSetSpace(unsigned numDims=0, unsigned numSymbols=0, unsigned numLocals=0)
Optional< SmallVector< int64_t, 8 > > findIntegerSample() const
Find an integer sample point satisfying the constraints using a branch and bound algorithm with gener...
const PresburgerSpace & getSpace() const
Returns a reference to the underlying space.
static Value max(ImplicitLocOpBuilder &builder, Value value, Value bound)
Optional< SmallVector< int64_t, 8 > > findIntegerSample()
Returns an integer sample point if one exists, or None otherwise.
Definition: Simplex.cpp:1956