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