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