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