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