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