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