MLIR  18.0.0git
IntegerRelation.h
Go to the documentation of this file.
1 //===- IntegerRelation.h - MLIR IntegerRelation Class ---------*- C++ -*---===//
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 a 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 
15 #ifndef MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H
16 #define MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H
17 
23 #include <optional>
24 
25 namespace mlir {
26 namespace presburger {
27 
28 class IntegerRelation;
29 class IntegerPolyhedron;
30 class PresburgerSet;
31 class PresburgerRelation;
32 struct SymbolicLexOpt;
33 
34 /// The type of bound: equal, lower bound or upper bound.
35 enum class BoundType { EQ, LB, UB };
36 
37 /// An IntegerRelation represents the set of points from a PresburgerSpace that
38 /// satisfy a list of affine constraints. Affine constraints can be inequalities
39 /// or equalities in the form:
40 ///
41 /// Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n >= 0
42 /// Equality : c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n == 0
43 ///
44 /// where c_0, c_1, ..., c_n are integers and n is the total number of
45 /// variables in the space.
46 ///
47 /// Such a relation corresponds to the set of integer points lying in a convex
48 /// polyhedron. For example, consider the relation:
49 /// (x) -> (y) : (1 <= x <= 7, x = 2y)
50 /// These can be thought of as points in the polyhedron:
51 /// (x, y) : (1 <= x <= 7, x = 2y)
52 /// This relation contains the pairs (2, 1), (4, 2), and (6, 3).
53 ///
54 /// Since IntegerRelation makes a distinction between dimensions, VarKind::Range
55 /// and VarKind::Domain should be used to refer to dimension variables.
57 public:
58  /// All derived classes of IntegerRelation.
59  enum class Kind {
66  };
67 
68  /// Constructs a relation reserving memory for the specified number
69  /// of constraints and variables.
70  IntegerRelation(unsigned numReservedInequalities,
71  unsigned numReservedEqualities, unsigned numReservedCols,
72  const PresburgerSpace &space)
73  : space(space), equalities(0, space.getNumVars() + 1,
74  numReservedEqualities, numReservedCols),
75  inequalities(0, space.getNumVars() + 1, numReservedInequalities,
76  numReservedCols) {
77  assert(numReservedCols >= space.getNumVars() + 1);
78  }
79 
80  /// Constructs a relation with the specified number of dimensions and symbols.
82  : IntegerRelation(/*numReservedInequalities=*/0,
83  /*numReservedEqualities=*/0,
84  /*numReservedCols=*/space.getNumVars() + 1, space) {}
85 
86  virtual ~IntegerRelation() = default;
87 
88  /// Return a system with no constraints, i.e., one which is satisfied by all
89  /// points.
91  return IntegerRelation(space);
92  }
93 
94  /// Return the kind of this IntegerRelation.
95  virtual Kind getKind() const { return Kind::IntegerRelation; }
96 
97  static bool classof(const IntegerRelation *cst) { return true; }
98 
99  // Clones this object.
100  std::unique_ptr<IntegerRelation> clone() const;
101 
102  /// Returns a reference to the underlying space.
103  const PresburgerSpace &getSpace() const { return space; }
104 
105  /// Set the space to `oSpace`, which should have the same number of ids as
106  /// the current space.
107  void setSpace(const PresburgerSpace &oSpace);
108 
109  /// Set the space to `oSpace`, which should not have any local ids.
110  /// `oSpace` can have fewer ids than the current space; in that case, the
111  /// the extra ids in `this` that are not accounted for by `oSpace` will be
112  /// considered as local ids. `oSpace` should not have more ids than the
113  /// current space; this will result in an assert failure.
114  void setSpaceExceptLocals(const PresburgerSpace &oSpace);
115 
116  /// Returns a copy of the space without locals.
121  }
122 
123  /// Appends constraints from `other` into `this`. This is equivalent to an
124  /// intersection with no simplification of any sort attempted.
125  void append(const IntegerRelation &other);
126 
127  /// Return the intersection of the two relations.
128  /// If there are locals, they will be merged.
130 
131  /// Return whether `this` and `other` are equal. This is integer-exact
132  /// and somewhat expensive, since it uses the integer emptiness check
133  /// (see IntegerRelation::findIntegerSample()).
134  bool isEqual(const IntegerRelation &other) const;
135 
136  /// Perform a quick equality check on `this` and `other`. The relations are
137  /// equal if the check return true, but may or may not be equal if the check
138  /// returns false. The equality check is performed in a plain manner, by
139  /// comparing if all the equalities and inequalities in `this` and `other`
140  /// are the same.
141  bool isPlainEqual(const IntegerRelation &other) const;
142 
143  /// Return whether this is a subset of the given IntegerRelation. This is
144  /// integer-exact and somewhat expensive, since it uses the integer emptiness
145  /// check (see IntegerRelation::findIntegerSample()).
146  bool isSubsetOf(const IntegerRelation &other) const;
147 
148  /// Returns the value at the specified equality row and column.
149  inline MPInt atEq(unsigned i, unsigned j) const { return equalities(i, j); }
150  /// The same, but casts to int64_t. This is unsafe and will assert-fail if the
151  /// value does not fit in an int64_t.
152  inline int64_t atEq64(unsigned i, unsigned j) const {
153  return int64_t(equalities(i, j));
154  }
155  inline MPInt &atEq(unsigned i, unsigned j) { return equalities(i, j); }
156 
157  /// Returns the value at the specified inequality row and column.
158  inline MPInt atIneq(unsigned i, unsigned j) const {
159  return inequalities(i, j);
160  }
161  /// The same, but casts to int64_t. This is unsafe and will assert-fail if the
162  /// value does not fit in an int64_t.
163  inline int64_t atIneq64(unsigned i, unsigned j) const {
164  return int64_t(inequalities(i, j));
165  }
166  inline MPInt &atIneq(unsigned i, unsigned j) { return inequalities(i, j); }
167 
168  unsigned getNumConstraints() const {
170  }
171 
172  unsigned getNumDomainVars() const { return space.getNumDomainVars(); }
173  unsigned getNumRangeVars() const { return space.getNumRangeVars(); }
174  unsigned getNumSymbolVars() const { return space.getNumSymbolVars(); }
175  unsigned getNumLocalVars() const { return space.getNumLocalVars(); }
176 
177  unsigned getNumDimVars() const { return space.getNumDimVars(); }
178  unsigned getNumDimAndSymbolVars() const {
179  return space.getNumDimAndSymbolVars();
180  }
181  unsigned getNumVars() const { return space.getNumVars(); }
182 
183  /// Returns the number of columns in the constraint system.
184  inline unsigned getNumCols() const { return space.getNumVars() + 1; }
185 
186  inline unsigned getNumEqualities() const { return equalities.getNumRows(); }
187 
188  inline unsigned getNumInequalities() const {
189  return inequalities.getNumRows();
190  }
191 
192  inline unsigned getNumReservedEqualities() const {
194  }
195 
196  inline unsigned getNumReservedInequalities() const {
198  }
199 
200  inline ArrayRef<MPInt> getEquality(unsigned idx) const {
201  return equalities.getRow(idx);
202  }
203  inline ArrayRef<MPInt> getInequality(unsigned idx) const {
204  return inequalities.getRow(idx);
205  }
206  /// The same, but casts to int64_t. This is unsafe and will assert-fail if the
207  /// value does not fit in an int64_t.
208  inline SmallVector<int64_t, 8> getEquality64(unsigned idx) const {
209  return getInt64Vec(equalities.getRow(idx));
210  }
211  inline SmallVector<int64_t, 8> getInequality64(unsigned idx) const {
212  return getInt64Vec(inequalities.getRow(idx));
213  }
214 
215  /// Get the number of vars of the specified kind.
216  unsigned getNumVarKind(VarKind kind) const {
217  return space.getNumVarKind(kind);
218  }
219 
220  /// Return the index at which the specified kind of vars starts.
221  unsigned getVarKindOffset(VarKind kind) const {
222  return space.getVarKindOffset(kind);
223  }
224 
225  /// Return the index at Which the specified kind of vars ends.
226  unsigned getVarKindEnd(VarKind kind) const {
227  return space.getVarKindEnd(kind);
228  }
229 
230  /// Get the number of elements of the specified kind in the range
231  /// [varStart, varLimit).
232  unsigned getVarKindOverlap(VarKind kind, unsigned varStart,
233  unsigned varLimit) const {
234  return space.getVarKindOverlap(kind, varStart, varLimit);
235  }
236 
237  /// Return the VarKind of the var at the specified position.
238  VarKind getVarKindAt(unsigned pos) const { return space.getVarKindAt(pos); }
239 
240  /// The struct CountsSnapshot stores the count of each VarKind, and also of
241  /// each constraint type. getCounts() returns a CountsSnapshot object
242  /// describing the current state of the IntegerRelation. truncate() truncates
243  /// all vars of each VarKind and all constraints of both kinds beyond the
244  /// counts in the specified CountsSnapshot object. This can be used to achieve
245  /// rudimentary rollback support. As long as none of the existing constraints
246  /// or vars are disturbed, and only additional vars or constraints are added,
247  /// this addition can be rolled back using truncate.
248  struct CountsSnapshot {
249  public:
250  CountsSnapshot(const PresburgerSpace &space, unsigned numIneqs,
251  unsigned numEqs)
252  : space(space), numIneqs(numIneqs), numEqs(numEqs) {}
253  const PresburgerSpace &getSpace() const { return space; };
254  unsigned getNumIneqs() const { return numIneqs; }
255  unsigned getNumEqs() const { return numEqs; }
256 
257  private:
258  PresburgerSpace space;
259  unsigned numIneqs, numEqs;
260  };
261  CountsSnapshot getCounts() const;
262  void truncate(const CountsSnapshot &counts);
263 
264  /// Insert `num` variables of the specified kind at position `pos`.
265  /// Positions are relative to the kind of variable. The coefficient columns
266  /// corresponding to the added variables are initialized to zero. Return the
267  /// absolute column position (i.e., not relative to the kind of variable)
268  /// of the first added variable.
269  virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num = 1);
270 
271  /// Append `num` variables of the specified kind after the last variable
272  /// of that kind. The coefficient columns corresponding to the added variables
273  /// are initialized to zero. Return the absolute column position (i.e., not
274  /// relative to the kind of variable) of the first appended variable.
275  unsigned appendVar(VarKind kind, unsigned num = 1);
276 
277  /// Adds an inequality (>= 0) from the coefficients specified in `inEq`.
278  void addInequality(ArrayRef<MPInt> inEq);
280  addInequality(getMPIntVec(inEq));
281  }
282  /// Adds an equality from the coefficients specified in `eq`.
283  void addEquality(ArrayRef<MPInt> eq);
285 
286  /// Eliminate the `posB^th` local variable, replacing every instance of it
287  /// with the `posA^th` local variable. This should be used when the two
288  /// local variables are known to always take the same values.
289  virtual void eliminateRedundantLocalVar(unsigned posA, unsigned posB);
290 
291  /// Removes variables of the specified kind with the specified pos (or
292  /// within the specified range) from the system. The specified location is
293  /// relative to the first variable of the specified kind.
294  void removeVar(VarKind kind, unsigned pos);
295  virtual void removeVarRange(VarKind kind, unsigned varStart,
296  unsigned varLimit);
297 
298  /// Removes the specified variable from the system.
299  void removeVar(unsigned pos);
300 
301  void removeEquality(unsigned pos);
302  void removeInequality(unsigned pos);
303 
304  /// Remove the (in)equalities at positions [start, end).
305  void removeEqualityRange(unsigned start, unsigned end);
306  void removeInequalityRange(unsigned start, unsigned end);
307 
308  /// Get the lexicographically minimum rational point satisfying the
309  /// constraints. Returns an empty optional if the relation is empty or if
310  /// the lexmin is unbounded. Symbols are not supported and will result in
311  /// assert-failure. Note that Domain is minimized first, then range.
313 
314  /// Same as above, but returns lexicographically minimal integer point.
315  /// Note: this should be used only when the lexmin is really required.
316  /// For a generic integer sampling operation, findIntegerSample is more
317  /// robust and should be preferred. Note that Domain is minimized first, then
318  /// range.
320 
321  /// Swap the posA^th variable with the posB^th variable.
322  virtual void swapVar(unsigned posA, unsigned posB);
323 
324  /// Removes all equalities and inequalities.
325  void clearConstraints();
326 
327  /// Sets the `values.size()` variables starting at `po`s to the specified
328  /// values and removes them.
329  void setAndEliminate(unsigned pos, ArrayRef<MPInt> values);
330  void setAndEliminate(unsigned pos, ArrayRef<int64_t> values) {
331  setAndEliminate(pos, getMPIntVec(values));
332  }
333 
334  /// Replaces the contents of this IntegerRelation with `other`.
335  virtual void clearAndCopyFrom(const IntegerRelation &other);
336 
337  /// Gather positions of all lower and upper bounds of the variable at `pos`,
338  /// and optionally any equalities on it. In addition, the bounds are to be
339  /// independent of variables in position range [`offset`, `offset` + `num`).
340  void
341  getLowerAndUpperBoundIndices(unsigned pos,
342  SmallVectorImpl<unsigned> *lbIndices,
343  SmallVectorImpl<unsigned> *ubIndices,
344  SmallVectorImpl<unsigned> *eqIndices = nullptr,
345  unsigned offset = 0, unsigned num = 0) const;
346 
347  /// Checks for emptiness by performing variable elimination on all
348  /// variables, running the GCD test on each equality constraint, and
349  /// checking for invalid constraints. Returns true if the GCD test fails for
350  /// any equality, or if any invalid constraints are discovered on any row.
351  /// Returns false otherwise.
352  bool isEmpty() const;
353 
354  /// Runs the GCD test on all equality constraints. Returns true if this test
355  /// fails on any equality. Returns false otherwise.
356  /// This test can be used to disprove the existence of a solution. If it
357  /// returns true, no integer solution to the equality constraints can exist.
358  bool isEmptyByGCDTest() const;
359 
360  /// Returns true if the set of constraints is found to have no solution,
361  /// false if a solution exists. Uses the same algorithm as
362  /// `findIntegerSample`.
363  bool isIntegerEmpty() const;
364 
365  /// Returns a matrix where each row is a vector along which the polytope is
366  /// bounded. The span of the returned vectors is guaranteed to contain all
367  /// such vectors. The returned vectors are NOT guaranteed to be linearly
368  /// independent. This function should not be called on empty sets.
370 
371  /// Find an integer sample point satisfying the constraints using a
372  /// branch and bound algorithm with generalized basis reduction, with some
373  /// additional processing using Simplex for unbounded sets.
374  ///
375  /// Returns an integer sample point if one exists, or an empty Optional
376  /// otherwise. The returned value also includes values of local ids.
377  std::optional<SmallVector<MPInt, 8>> findIntegerSample() const;
378 
379  /// Compute an overapproximation of the number of integer points in the
380  /// relation. Symbol vars currently not supported. If the computed
381  /// overapproximation is infinite, an empty optional is returned.
382  std::optional<MPInt> computeVolume() const;
383 
384  /// Returns true if the given point satisfies the constraints, or false
385  /// otherwise. Takes the values of all vars including locals.
386  bool containsPoint(ArrayRef<MPInt> point) const;
387  bool containsPoint(ArrayRef<int64_t> point) const {
388  return containsPoint(getMPIntVec(point));
389  }
390  /// Given the values of non-local vars, return a satisfying assignment to the
391  /// local if one exists, or an empty optional otherwise.
392  std::optional<SmallVector<MPInt, 8>>
394  std::optional<SmallVector<MPInt, 8>>
396  return containsPointNoLocal(getMPIntVec(point));
397  }
398 
399  /// Returns a `DivisonRepr` representing the division representation of local
400  /// variables in the constraint system.
401  ///
402  /// If `repr` is not `nullptr`, the equality and pairs of inequality
403  /// constraints identified by their position indices using which an explicit
404  /// representation for each local variable can be computed are set in `repr`
405  /// in the form of a `MaybeLocalRepr` struct. If no such inequality
406  /// pair/equality can be found, the kind attribute in `MaybeLocalRepr` is set
407  /// to None.
408  DivisionRepr getLocalReprs(std::vector<MaybeLocalRepr> *repr = nullptr) const;
409 
410  /// Adds a constant bound for the specified variable.
411  void addBound(BoundType type, unsigned pos, const MPInt &value);
412  void addBound(BoundType type, unsigned pos, int64_t value) {
413  addBound(type, pos, MPInt(value));
414  }
415 
416  /// Adds a constant bound for the specified expression.
417  void addBound(BoundType type, ArrayRef<MPInt> expr, const MPInt &value);
418  void addBound(BoundType type, ArrayRef<int64_t> expr, int64_t value) {
419  addBound(type, getMPIntVec(expr), MPInt(value));
420  }
421 
422  /// Adds a new local variable as the floordiv of an affine function of other
423  /// variables, the coefficients of which are provided in `dividend` and with
424  /// respect to a positive constant `divisor`. Two constraints are added to the
425  /// system to capture equivalence with the floordiv:
426  /// q = dividend floordiv c <=> c*q <= dividend <= c*q + c - 1.
427  void addLocalFloorDiv(ArrayRef<MPInt> dividend, const MPInt &divisor);
428  void addLocalFloorDiv(ArrayRef<int64_t> dividend, int64_t divisor) {
429  addLocalFloorDiv(getMPIntVec(dividend), MPInt(divisor));
430  }
431 
432  /// Projects out (aka eliminates) `num` variables starting at position
433  /// `pos`. The resulting constraint system is the shadow along the dimensions
434  /// that still exist. This method may not always be integer exact.
435  // TODO: deal with integer exactness when necessary - can return a value to
436  // mark exactness for example.
437  void projectOut(unsigned pos, unsigned num);
438  inline void projectOut(unsigned pos) { return projectOut(pos, 1); }
439 
440  /// Tries to fold the specified variable to a constant using a trivial
441  /// equality detection; if successful, the constant is substituted for the
442  /// variable everywhere in the constraint system and then removed from the
443  /// system.
444  LogicalResult constantFoldVar(unsigned pos);
445 
446  /// This method calls `constantFoldVar` for the specified range of variables,
447  /// `num` variables starting at position `pos`.
448  void constantFoldVarRange(unsigned pos, unsigned num);
449 
450  /// Updates the constraints to be the smallest bounding (enclosing) box that
451  /// contains the points of `this` set and that of `other`, with the symbols
452  /// being treated specially. For each of the dimensions, the min of the lower
453  /// bounds (symbolic) and the max of the upper bounds (symbolic) is computed
454  /// to determine such a bounding box. `other` is expected to have the same
455  /// dimensional variables as this constraint system (in the same order).
456  ///
457  /// E.g.:
458  /// 1) this = {0 <= d0 <= 127},
459  /// other = {16 <= d0 <= 192},
460  /// output = {0 <= d0 <= 192}
461  /// 2) this = {s0 + 5 <= d0 <= s0 + 20},
462  /// other = {s0 + 1 <= d0 <= s0 + 9},
463  /// output = {s0 + 1 <= d0 <= s0 + 20}
464  /// 3) this = {0 <= d0 <= 5, 1 <= d1 <= 9}
465  /// other = {2 <= d0 <= 6, 5 <= d1 <= 15},
466  /// output = {0 <= d0 <= 6, 1 <= d1 <= 15}
468 
469  /// Returns the smallest known constant bound for the extent of the specified
470  /// variable (pos^th), i.e., the smallest known constant that is greater
471  /// than or equal to 'exclusive upper bound' - 'lower bound' of the
472  /// variable. This constant bound is guaranteed to be non-negative. Returns
473  /// std::nullopt if it's not a constant. This method employs trivial (low
474  /// complexity / cost) checks and detection. Symbolic variables are treated
475  /// specially, i.e., it looks for constant differences between affine
476  /// expressions involving only the symbolic variables. `lb` and `ub` (along
477  /// with the `boundFloorDivisor`) are set to represent the lower and upper
478  /// bound associated with the constant difference: `lb`, `ub` have the
479  /// coefficients, and `boundFloorDivisor`, their divisor. `minLbPos` and
480  /// `minUbPos` if non-null are set to the position of the constant lower bound
481  /// and upper bound respectively (to the same if they are from an
482  /// equality). Ex: if the lower bound is [(s0 + s2 - 1) floordiv 32] for a
483  /// system with three symbolic variables, *lb = [1, 0, 1], lbDivisor = 32. See
484  /// comments at function definition for examples.
485  std::optional<MPInt> getConstantBoundOnDimSize(
486  unsigned pos, SmallVectorImpl<MPInt> *lb = nullptr,
487  MPInt *boundFloorDivisor = nullptr, SmallVectorImpl<MPInt> *ub = nullptr,
488  unsigned *minLbPos = nullptr, unsigned *minUbPos = nullptr) const;
489  /// The same, but casts to int64_t. This is unsafe and will assert-fail if the
490  /// value does not fit in an int64_t.
491  std::optional<int64_t> getConstantBoundOnDimSize64(
492  unsigned pos, SmallVectorImpl<int64_t> *lb = nullptr,
493  int64_t *boundFloorDivisor = nullptr,
494  SmallVectorImpl<int64_t> *ub = nullptr, unsigned *minLbPos = nullptr,
495  unsigned *minUbPos = nullptr) const {
496  SmallVector<MPInt, 8> ubMPInt, lbMPInt;
497  MPInt boundFloorDivisorMPInt;
498  std::optional<MPInt> result = getConstantBoundOnDimSize(
499  pos, &lbMPInt, &boundFloorDivisorMPInt, &ubMPInt, minLbPos, minUbPos);
500  if (lb)
501  *lb = getInt64Vec(lbMPInt);
502  if (ub)
503  *ub = getInt64Vec(ubMPInt);
504  if (boundFloorDivisor)
505  *boundFloorDivisor = static_cast<int64_t>(boundFloorDivisorMPInt);
506  return llvm::transformOptional(result, int64FromMPInt);
507  }
508 
509  /// Returns the constant bound for the pos^th variable if there is one;
510  /// std::nullopt otherwise.
511  std::optional<MPInt> getConstantBound(BoundType type, unsigned pos) const;
512  /// The same, but casts to int64_t. This is unsafe and will assert-fail if the
513  /// value does not fit in an int64_t.
514  std::optional<int64_t> getConstantBound64(BoundType type,
515  unsigned pos) const {
516  return llvm::transformOptional(getConstantBound(type, pos), int64FromMPInt);
517  }
518 
519  /// Removes constraints that are independent of (i.e., do not have a
520  /// coefficient) variables in the range [pos, pos + num).
521  void removeIndependentConstraints(unsigned pos, unsigned num);
522 
523  /// Returns true if the set can be trivially detected as being
524  /// hyper-rectangular on the specified contiguous set of variables.
525  bool isHyperRectangular(unsigned pos, unsigned num) const;
526 
527  /// Removes duplicate constraints, trivially true constraints, and constraints
528  /// that can be detected as redundant as a result of differing only in their
529  /// constant term part. A constraint of the form <non-negative constant> >= 0
530  /// is considered trivially true. This method is a linear time method on the
531  /// constraints, does a single scan, and updates in place. It also normalizes
532  /// constraints by their GCD and performs GCD tightening on inequalities.
534 
535  /// A more expensive check than `removeTrivialRedundancy` to detect redundant
536  /// inequalities.
538 
539  /// Removes redundant constraints using Simplex. Although the algorithm can
540  /// theoretically take exponential time in the worst case (rare), it is known
541  /// to perform much better in the average case. If V is the number of vertices
542  /// in the polytope and C is the number of constraints, the algorithm takes
543  /// O(VC) time.
545 
546  void removeDuplicateDivs();
547 
548  /// Converts variables of kind srcKind in the range [varStart, varLimit) to
549  /// variables of kind dstKind. If `pos` is given, the variables are placed at
550  /// position `pos` of dstKind, otherwise they are placed after all the other
551  /// variables of kind dstKind. The internal ordering among the moved variables
552  /// is preserved.
553  void convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit,
554  VarKind dstKind, unsigned pos);
555  void convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit,
556  VarKind dstKind) {
557  convertVarKind(srcKind, varStart, varLimit, dstKind,
558  getNumVarKind(dstKind));
559  }
560  void convertToLocal(VarKind kind, unsigned varStart, unsigned varLimit) {
561  convertVarKind(kind, varStart, varLimit, VarKind::Local);
562  }
563 
564  /// Adds additional local vars to the sets such that they both have the union
565  /// of the local vars in each set, without changing the set of points that
566  /// lie in `this` and `other`.
567  ///
568  /// While taking union, if a local var in `other` has a division
569  /// representation which is a duplicate of division representation, of another
570  /// local var, it is not added to the final union of local vars and is instead
571  /// merged. The new ordering of local vars is:
572  ///
573  /// [Local vars of `this`] [Non-merged local vars of `other`]
574  ///
575  /// The relative ordering of local vars is same as before.
576  ///
577  /// After merging, if the `i^th` local variable in one set has a known
578  /// division representation, then the `i^th` local variable in the other set
579  /// either has the same division representation or no known division
580  /// representation.
581  ///
582  /// The spaces of both relations should be compatible.
583  ///
584  /// Returns the number of non-merged local vars of `other`, i.e. the number of
585  /// locals that have been added to `this`.
586  unsigned mergeLocalVars(IntegerRelation &other);
587 
588  /// Check whether all local ids have a division representation.
589  bool hasOnlyDivLocals() const;
590 
591  /// Changes the partition between dimensions and symbols. Depending on the new
592  /// symbol count, either a chunk of dimensional variables immediately before
593  /// the split become symbols, or some of the symbols immediately after the
594  /// split become dimensions.
595  void setDimSymbolSeparation(unsigned newSymbolCount) {
596  space.setVarSymbolSeperation(newSymbolCount);
597  }
598 
599  /// Return a set corresponding to all points in the domain of the relation.
601 
602  /// Return a set corresponding to all points in the range of the relation.
604 
605  /// Intersect the given `poly` with the domain in-place.
606  ///
607  /// Formally, let the relation `this` be R: A -> B and poly is C, then this
608  /// operation modifies R to be (A intersection C) -> B.
609  void intersectDomain(const IntegerPolyhedron &poly);
610 
611  /// Intersect the given `poly` with the range in-place.
612  ///
613  /// Formally, let the relation `this` be R: A -> B and poly is C, then this
614  /// operation modifies R to be A -> (B intersection C).
615  void intersectRange(const IntegerPolyhedron &poly);
616 
617  /// Invert the relation i.e., swap its domain and range.
618  ///
619  /// Formally, let the relation `this` be R: A -> B, then this operation
620  /// modifies R to be B -> A.
621  void inverse();
622 
623  /// Let the relation `this` be R1, and the relation `rel` be R2. Modifies R1
624  /// to be the composition of R1 and R2: R1;R2.
625  ///
626  /// Formally, if R1: A -> B, and R2: B -> C, then this function returns a
627  /// relation R3: A -> C such that a point (a, c) belongs to R3 iff there
628  /// exists b such that (a, b) is in R1 and, (b, c) is in R2.
629  void compose(const IntegerRelation &rel);
630 
631  /// Given a relation `rel`, apply the relation to the domain of this relation.
632  ///
633  /// R1: i -> j : (0 <= i < 2, j = i)
634  /// R2: i -> k : (k = i floordiv 2)
635  /// R3: k -> j : (0 <= k < 1, 2k <= j <= 2k + 1)
636  ///
637  /// R1 = {(0, 0), (1, 1)}. R2 maps both 0 and 1 to 0.
638  /// So R3 = {(0, 0), (0, 1)}.
639  ///
640  /// Formally, R1.applyDomain(R2) = R2.inverse().compose(R1).
641  void applyDomain(const IntegerRelation &rel);
642 
643  /// Given a relation `rel`, apply the relation to the range of this relation.
644  ///
645  /// Formally, R1.applyRange(R2) is the same as R1.compose(R2) but we provide
646  /// this for uniformity with `applyDomain`.
647  void applyRange(const IntegerRelation &rel);
648 
649  /// Compute an equivalent representation of the same set, such that all local
650  /// vars in all disjuncts have division representations. This representation
651  /// may involve local vars that correspond to divisions, and may also be a
652  /// union of convex disjuncts.
654 
655  /// Compute the symbolic integer lexmin of the relation.
656  ///
657  /// This finds, for every assignment to the symbols and domain,
658  /// the lexicographically minimum value attained by the range.
659  ///
660  /// For example, the symbolic lexmin of the set
661  ///
662  /// (x, y)[a, b, c] : (a <= x, b <= x, x <= c)
663  ///
664  /// can be written as
665  ///
666  /// x = a if b <= a, a <= c
667  /// x = b if a < b, b <= c
668  ///
669  /// This function is stored in the `lexopt` function in the result.
670  /// Some assignments to the symbols might make the set empty.
671  /// Such points are not part of the function's domain.
672  /// In the above example, this happens when max(a, b) > c.
673  ///
674  /// For some values of the symbols, the lexmin may be unbounded.
675  /// `SymbolicLexOpt` stores these parts of the symbolic domain in a separate
676  /// `PresburgerSet`, `unboundedDomain`.
678 
679  /// Same as findSymbolicIntegerLexMin but produces lexmax instead of lexmin
681 
682  /// Return the set difference of this set and the given set, i.e.,
683  /// return `this \ set`.
685 
686  void print(raw_ostream &os) const;
687  void dump() const;
688 
689 protected:
690  /// Checks all rows of equality/inequality constraints for trivial
691  /// contradictions (for example: 1 == 0, 0 >= 1), which may have surfaced
692  /// after elimination. Returns true if an invalid constraint is found;
693  /// false otherwise.
694  bool hasInvalidConstraint() const;
695 
696  /// Returns the constant lower bound if isLower is true, and the upper
697  /// bound if isLower is false.
698  template <bool isLower>
699  std::optional<MPInt> computeConstantLowerOrUpperBound(unsigned pos);
700  /// The same, but casts to int64_t. This is unsafe and will assert-fail if the
701  /// value does not fit in an int64_t.
702  template <bool isLower>
703  std::optional<int64_t> computeConstantLowerOrUpperBound64(unsigned pos) {
704  return computeConstantLowerOrUpperBound<isLower>(pos).map(int64FromMPInt);
705  }
706 
707  /// Eliminates a single variable at `position` from equality and inequality
708  /// constraints. Returns `success` if the variable was eliminated, and
709  /// `failure` otherwise.
710  inline LogicalResult gaussianEliminateVar(unsigned position) {
711  return success(gaussianEliminateVars(position, position + 1) == 1);
712  }
713 
714  /// Removes local variables using equalities. Each equality is checked if it
715  /// can be reduced to the form: `e = affine-expr`, where `e` is a local
716  /// variable and `affine-expr` is an affine expression not containing `e`.
717  /// If an equality satisfies this form, the local variable is replaced in
718  /// each constraint and then removed. The equality used to replace this local
719  /// variable is also removed.
721 
722  /// Eliminates variables from equality and inequality constraints
723  /// in column range [posStart, posLimit).
724  /// Returns the number of variables eliminated.
725  unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit);
726 
727  /// Eliminates the variable at the specified position using Fourier-Motzkin
728  /// variable elimination, but uses Gaussian elimination if there is an
729  /// equality involving that variable. If the result of the elimination is
730  /// integer exact, `*isResultIntegerExact` is set to true. If `darkShadow` is
731  /// set to true, a potential under approximation (subset) of the rational
732  /// shadow / exact integer shadow is computed.
733  // See implementation comments for more details.
734  virtual void fourierMotzkinEliminate(unsigned pos, bool darkShadow = false,
735  bool *isResultIntegerExact = nullptr);
736 
737  /// Tightens inequalities given that we are dealing with integer spaces. This
738  /// is similar to the GCD test but applied to inequalities. The constant term
739  /// can be reduced to the preceding multiple of the GCD of the coefficients,
740  /// i.e.,
741  /// 64*i - 100 >= 0 => 64*i - 128 >= 0 (since 'i' is an integer). This is a
742  /// fast method (linear in the number of coefficients).
743  void gcdTightenInequalities();
744 
745  /// Normalized each constraints by the GCD of its coefficients.
747 
748  /// Searches for a constraint with a non-zero coefficient at `colIdx` in
749  /// equality (isEq=true) or inequality (isEq=false) constraints.
750  /// Returns true and sets row found in search in `rowIdx`, false otherwise.
751  bool findConstraintWithNonZeroAt(unsigned colIdx, bool isEq,
752  unsigned *rowIdx) const;
753 
754  /// Returns true if the pos^th column is all zero for both inequalities and
755  /// equalities.
756  bool isColZero(unsigned pos) const;
757 
758  /// Returns false if the fields corresponding to various variable counts, or
759  /// equality/inequality buffer sizes aren't consistent; true otherwise. This
760  /// is meant to be used within an assert internally.
761  virtual bool hasConsistentState() const;
762 
763  /// Prints the number of constraints, dimensions, symbols and locals in the
764  /// IntegerRelation.
765  virtual void printSpace(raw_ostream &os) const;
766 
767  /// Removes variables in the column range [varStart, varLimit), and copies any
768  /// remaining valid data into place, updates member variables, and resizes
769  /// arrays as needed.
770  void removeVarRange(unsigned varStart, unsigned varLimit);
771 
772  /// Truncate the vars of the specified kind to the specified number by
773  /// dropping some vars at the end. `num` must be less than the current number.
774  void truncateVarKind(VarKind kind, unsigned num);
775 
776  /// Truncate the vars to the number in the space of the specified
777  /// CountsSnapshot.
778  void truncateVarKind(VarKind kind, const CountsSnapshot &counts);
779 
780  /// A parameter that controls detection of an unrealistic number of
781  /// constraints. If the number of constraints is this many times the number of
782  /// variables, we consider such a system out of line with the intended use
783  /// case of IntegerRelation.
784  // The rationale for 32 is that in the typical simplest of cases, an
785  // variable is expected to have one lower bound and one upper bound
786  // constraint. With a level of tiling or a connection to another variable
787  // through a div or mod, an extra pair of bounds gets added. As a limit, we
788  // don't expect a variable to have more than 32 lower/upper/equality
789  // constraints. This is conservatively set low and can be raised if needed.
790  constexpr static unsigned kExplosionFactor = 32;
791 
793 
794  /// Coefficients of affine equalities (in == 0 form).
796 
797  /// Coefficients of affine inequalities (in >= 0 form).
799 };
800 
801 /// An IntegerPolyhedron represents the set of points from a PresburgerSpace
802 /// that satisfy a list of affine constraints. Affine constraints can be
803 /// inequalities or equalities in the form:
804 ///
805 /// Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n >= 0
806 /// Equality : c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n == 0
807 ///
808 /// where c_0, c_1, ..., c_n are integers and n is the total number of
809 /// variables in the space.
810 ///
811 /// An IntegerPolyhedron is similar to an IntegerRelation but it does not make a
812 /// distinction between Domain and Range variables. Internally,
813 /// IntegerPolyhedron is implemented as a IntegerRelation with zero domain vars.
814 ///
815 /// Since IntegerPolyhedron does not make a distinction between kinds of
816 /// dimensions, VarKind::SetDim should be used to refer to dimension
817 /// variables.
819 public:
820  /// Constructs a set reserving memory for the specified number
821  /// of constraints and variables.
822  IntegerPolyhedron(unsigned numReservedInequalities,
823  unsigned numReservedEqualities, unsigned numReservedCols,
824  const PresburgerSpace &space)
825  : IntegerRelation(numReservedInequalities, numReservedEqualities,
826  numReservedCols, space) {
827  assert(space.getNumDomainVars() == 0 &&
828  "Number of domain vars should be zero in Set kind space.");
829  }
830 
831  /// Constructs a relation with the specified number of dimensions and
832  /// symbols.
834  : IntegerPolyhedron(/*numReservedInequalities=*/0,
835  /*numReservedEqualities=*/0,
836  /*numReservedCols=*/space.getNumVars() + 1, space) {}
837 
838  /// Construct a set from an IntegerRelation. The relation should have
839  /// no domain vars.
840  explicit IntegerPolyhedron(const IntegerRelation &rel)
841  : IntegerRelation(rel) {
842  assert(space.getNumDomainVars() == 0 &&
843  "Number of domain vars should be zero in Set kind space.");
844  }
845 
846  /// Construct a set from an IntegerRelation, but instead of creating a copy,
847  /// use move constructor. The relation should have no domain vars.
849  assert(space.getNumDomainVars() == 0 &&
850  "Number of domain vars should be zero in Set kind space.");
851  }
852 
853  /// Return a system with no constraints, i.e., one which is satisfied by all
854  /// points.
856  return IntegerPolyhedron(space);
857  }
858 
859  /// Return the kind of this IntegerRelation.
860  Kind getKind() const override { return Kind::IntegerPolyhedron; }
861 
862  static bool classof(const IntegerRelation *cst) {
863  return cst->getKind() >= Kind::IntegerPolyhedron &&
865  }
866 
867  // Clones this object.
868  std::unique_ptr<IntegerPolyhedron> clone() const;
869 
870  /// Insert `num` variables of the specified kind at position `pos`.
871  /// Positions are relative to the kind of variable. Return the absolute
872  /// column position (i.e., not relative to the kind of variable) of the
873  /// first added variable.
874  unsigned insertVar(VarKind kind, unsigned pos, unsigned num = 1) override;
875 
876  /// Return the intersection of the two relations.
877  /// If there are locals, they will be merged.
878  IntegerPolyhedron intersect(const IntegerPolyhedron &other) const;
879 
880  /// Return the set difference of this set and the given set, i.e.,
881  /// return `this \ set`.
882  PresburgerSet subtract(const PresburgerSet &other) const;
883 };
884 
885 } // namespace presburger
886 } // namespace mlir
887 
888 #endif // MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H
Class storing division representation of local variables of a constraint system.
Definition: Utils.h:118
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
IntegerPolyhedron(IntegerRelation &&rel)
Construct a set from an IntegerRelation, but instead of creating a copy, use move constructor.
IntegerPolyhedron(const IntegerRelation &rel)
Construct a set from an IntegerRelation.
static bool classof(const IntegerRelation *cst)
IntegerPolyhedron intersect(const IntegerPolyhedron &other) const
Return the intersection of the two relations.
Kind getKind() const override
Return the kind of this IntegerRelation.
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(const PresburgerSpace &space)
Constructs a relation with the specified number of dimensions and symbols.
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
static IntegerPolyhedron getUniverse(const PresburgerSpace &space)
Return a system with no constraints, i.e., one which is satisfied by all points.
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
Kind
All derived classes of IntegerRelation.
void addInequality(ArrayRef< int64_t > inEq)
virtual void swapVar(unsigned posA, unsigned posB)
Swap the posA^th variable with the posB^th variable.
void setAndEliminate(unsigned pos, ArrayRef< int64_t > values)
MPInt atEq(unsigned i, unsigned j) const
Returns the value at the specified equality row and column.
void removeIndependentConstraints(unsigned pos, unsigned num)
Removes constraints that are independent of (i.e., do not have a coefficient) variables in the range ...
ArrayRef< MPInt > getEquality(unsigned idx) const
void compose(const IntegerRelation &rel)
Let the relation this be R1, and the relation rel be R2.
int64_t atEq64(unsigned i, unsigned j) const
The same, but casts to int64_t.
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.
PresburgerSpace getSpaceWithoutLocals() const
Returns a copy of the space without locals.
void addInequality(ArrayRef< MPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
std::optional< MPInt > getConstantBound(BoundType type, unsigned pos) const
Returns the constant bound for the pos^th variable if there is one; std::nullopt otherwise.
void removeTrivialRedundancy()
Removes duplicate constraints, trivially true constraints, and constraints that can be detected as re...
MPInt & atEq(unsigned i, unsigned j)
void addBound(BoundType type, unsigned pos, int64_t value)
void addEquality(ArrayRef< MPInt > eq)
Adds an equality from the coefficients specified in eq.
void removeInequalityRange(unsigned start, unsigned end)
void convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit, VarKind dstKind)
std::optional< int64_t > getConstantBoundOnDimSize64(unsigned pos, SmallVectorImpl< int64_t > *lb=nullptr, int64_t *boundFloorDivisor=nullptr, SmallVectorImpl< int64_t > *ub=nullptr, unsigned *minLbPos=nullptr, unsigned *minUbPos=nullptr) const
The same, but casts to int64_t.
void normalizeConstraintsByGCD()
Normalized each constraints by the GCD of its coefficients.
static bool classof(const IntegerRelation *cst)
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.
SmallVector< int64_t, 8 > getEquality64(unsigned idx) const
The same, but casts to int64_t.
void removeEqualityRange(unsigned start, unsigned end)
Remove the (in)equalities at positions [start, end).
std::optional< MPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the relation.
LogicalResult constantFoldVar(unsigned pos)
Tries to fold the specified variable to a constant using a trivial equality detection; if successful,...
std::optional< int64_t > getConstantBound64(BoundType type, unsigned pos) const
The same, but casts to int64_t.
IntegerPolyhedron getRangeSet() const
Return a set corresponding to all points in the range of the relation.
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
bool isEmptyByGCDTest() const
Runs the GCD test on all equality constraints.
void convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit, VarKind dstKind, unsigned pos)
Converts variables of kind srcKind in the range [varStart, varLimit) to variables of kind dstKind.
unsigned appendVar(VarKind kind, unsigned num=1)
Append num variables of the specified kind after the last variable of that kind.
void intersectRange(const IntegerPolyhedron &poly)
Intersect the given poly with the range in-place.
void print(raw_ostream &os) const
bool isIntegerEmpty() const
Returns true if the set of constraints is found to have no solution, false if a solution exists.
std::optional< SmallVector< MPInt, 8 > > findIntegerSample() const
Find an integer sample point satisfying the constraints using a branch and bound algorithm with gener...
VarKind getVarKindAt(unsigned pos) const
Return the VarKind of the var at the specified position.
void addEquality(ArrayRef< int64_t > eq)
MaybeOptimum< SmallVector< MPInt, 8 > > findIntegerLexMin() const
Same as above, but returns lexicographically minimal integer point.
MPInt & atIneq(unsigned i, unsigned j)
virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
bool hasInvalidConstraint() const
Checks all rows of equality/inequality constraints for trivial contradictions (for example: 1 == 0,...
LogicalResult unionBoundingBox(const IntegerRelation &other)
Updates the constraints to be the smallest bounding (enclosing) box that contains the points of this ...
IntegerRelation(unsigned numReservedInequalities, unsigned numReservedEqualities, unsigned numReservedCols, const PresburgerSpace &space)
Constructs a relation reserving memory for the specified number of constraints and variables.
bool containsPoint(ArrayRef< int64_t > point) const
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.
IntegerRelation intersect(IntegerRelation other) const
Return the intersection of the two relations.
void addLocalFloorDiv(ArrayRef< MPInt > dividend, const MPInt &divisor)
Adds a new local variable as the floordiv of an affine function of other variables,...
ArrayRef< MPInt > getInequality(unsigned idx) const
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.
std::optional< SmallVector< MPInt, 8 > > containsPointNoLocal(ArrayRef< MPInt > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists,...
static IntegerRelation getUniverse(const PresburgerSpace &space)
Return a system with no constraints, i.e., one which is satisfied by all points.
MPInt atIneq(unsigned i, unsigned j) const
Returns the value at the specified inequality row and column.
void inverse()
Invert the relation i.e., swap its domain and range.
void append(const IntegerRelation &other)
Appends constraints from other into this.
void applyDomain(const IntegerRelation &rel)
Given a relation rel, apply the relation to the domain of this relation.
void intersectDomain(const IntegerPolyhedron &poly)
Intersect the given poly with the domain in-place.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
bool isEqual(const IntegerRelation &other) const
Return whether this and other are equal.
virtual void printSpace(raw_ostream &os) const
Prints the number of constraints, dimensions, symbols and locals in the IntegerRelation.
void setDimSymbolSeparation(unsigned newSymbolCount)
Changes the partition between dimensions and symbols.
unsigned getNumReservedInequalities() const
std::optional< SmallVector< MPInt, 8 > > containsPointNoLocal(ArrayRef< int64_t > point) const
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.
IntMatrix equalities
Coefficients of affine equalities (in == 0 form).
SymbolicLexOpt findSymbolicIntegerLexMax() const
Same as findSymbolicIntegerLexMin but produces lexmax instead of lexmin.
void addLocalFloorDiv(ArrayRef< int64_t > dividend, int64_t divisor)
void truncateVarKind(VarKind kind, unsigned num)
Truncate the vars of the specified kind to the specified number by dropping some vars at the end.
virtual Kind getKind() const
Return the kind of this IntegerRelation.
void constantFoldVarRange(unsigned pos, unsigned num)
This method calls constantFoldVar for the specified range of variables, num variables starting at pos...
std::optional< MPInt > getConstantBoundOnDimSize(unsigned pos, SmallVectorImpl< MPInt > *lb=nullptr, MPInt *boundFloorDivisor=nullptr, SmallVectorImpl< MPInt > *ub=nullptr, unsigned *minLbPos=nullptr, unsigned *minUbPos=nullptr) const
Returns the smallest known constant bound for the extent of the specified variable (pos^th),...
bool isEmpty() const
Checks for emptiness by performing variable elimination on all variables, running the GCD test on eac...
unsigned getNumCols() const
Returns the number of columns in the constraint system.
IntegerRelation(const PresburgerSpace &space)
Constructs a relation with the specified number of dimensions and symbols.
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.
std::optional< int64_t > computeConstantLowerOrUpperBound64(unsigned pos)
The same, but casts to int64_t.
void removeVar(VarKind kind, unsigned pos)
Removes variables of the specified kind with the specified pos (or within the specified range) from t...
void setSpaceExceptLocals(const PresburgerSpace &oSpace)
Set the space to oSpace, which should not have any local ids.
unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit)
Eliminates variables from equality and inequality constraints in column range [posStart,...
void addBound(BoundType type, unsigned pos, const MPInt &value)
Adds a constant bound for the specified variable.
IntegerPolyhedron getDomainSet() const
Return a set corresponding to all points in the domain of the relation.
void addBound(BoundType type, ArrayRef< int64_t > expr, int64_t value)
DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const
Returns a DivisonRepr representing the division representation of local variables in the constraint s...
bool hasOnlyDivLocals() const
Check whether all local ids have a division representation.
constexpr static unsigned kExplosionFactor
A parameter that controls detection of an unrealistic number of constraints.
void setAndEliminate(unsigned pos, ArrayRef< MPInt > values)
Sets the values.size() variables starting at pos to the specified values and removes them.
virtual void clearAndCopyFrom(const IntegerRelation &other)
Replaces the contents of this IntegerRelation with other.
void projectOut(unsigned pos, unsigned num)
Projects out (aka eliminates) num variables starting at position pos.
bool isPlainEqual(const IntegerRelation &other) const
Perform a quick equality check on this and other.
unsigned getVarKindOverlap(VarKind kind, unsigned varStart, unsigned varLimit) const
Get the number of elements of the specified kind in the range [varStart, varLimit).
std::optional< MPInt > computeConstantLowerOrUpperBound(unsigned pos)
Returns the constant lower bound if isLower is true, and the upper bound if isLower is false.
void removeRedundantLocalVars()
Removes local variables using equalities.
unsigned mergeLocalVars(IntegerRelation &other)
Adds additional local vars to the sets such that they both have the union of the local vars in each s...
virtual ~IntegerRelation()=default
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...
SmallVector< int64_t, 8 > getInequality64(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.
bool containsPoint(ArrayRef< MPInt > point) const
Returns true if the given point satisfies the constraints, or false otherwise.
bool isColZero(unsigned pos) const
Returns true if the pos^th column is all zero for both inequalities and equalities.
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of vars starts.
int64_t atIneq64(unsigned i, unsigned j) const
The same, but casts to int64_t.
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,...
This class provides support for multi-precision arithmetic.
Definition: MPInt.h:87
unsigned getNumRows() const
Definition: Matrix.h:82
MutableArrayRef< T > getRow(unsigned row)
Get a [Mutable]ArrayRef corresponding to the specified row.
Definition: Matrix.cpp:88
unsigned getNumReservedRows() const
Return the maximum number of rows/columns that can be added without incurring a reallocation.
Definition: Matrix.cpp:32
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of var starts.
void setVarSymbolSeperation(unsigned newSymbolCount)
Changes the partition between dimensions and symbols.
unsigned getVarKindEnd(VarKind kind) const
Return the index at Which the specified kind of var ends.
VarKind getVarKindAt(unsigned pos) const
Return the VarKind of the var at the specified position.
unsigned getVarKindOverlap(VarKind kind, unsigned varStart, unsigned varLimit) const
Get the number of elements of the specified kind in the range [varStart, varLimit).
static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)
BoundType
The type of bound: equal, lower bound or upper bound.
VarKind
Kind of variable.
static int64_t int64FromMPInt(const MPInt &x)
This just calls through to the operator int64_t, but it's useful when a function pointer is required.
Definition: MPInt.h:261
SmallVector< MPInt, 8 > getMPIntVec(ArrayRef< int64_t > range)
Check if the pos^th variable can be expressed as a floordiv of an affine function of other variables ...
Definition: Utils.cpp:512
SmallVector< int64_t, 8 > getInt64Vec(ArrayRef< MPInt > range)
Return the given array as an array of int64_t.
Definition: Utils.cpp:518
This header declares functions that assist transformations in the MemRef dialect.
LogicalResult success(bool isSuccess=true)
Utility function to generate a LogicalResult.
Definition: LogicalResult.h:56
This class represents an efficient way to signal success or failure.
Definition: LogicalResult.h:26
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type.
CountsSnapshot(const PresburgerSpace &space, unsigned numIneqs, unsigned numEqs)
Represents the result of a symbolic lexicographic optimization computation.
Definition: Simplex.h:533
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.