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