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