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