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