MLIR  19.0.0git
PresburgerRelation.h
Go to the documentation of this file.
1 //===- PresburgerRelation.h - MLIR PresburgerRelation 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 unions of IntegerRelations.
10 //
11 //===----------------------------------------------------------------------===//
12 
13 #ifndef MLIR_ANALYSIS_PRESBURGER_PRESBURGERRELATION_H
14 #define MLIR_ANALYSIS_PRESBURGER_PRESBURGERRELATION_H
15 
17 #include <optional>
18 
19 namespace mlir {
20 namespace presburger {
21 
22 /// The SetCoalescer class contains all functionality concerning the coalesce
23 /// heuristic. It is built from a `PresburgerRelation` and has the `coalesce()`
24 /// function as its main API.
25 class SetCoalescer;
26 
27 /// A PresburgerRelation represents a union of IntegerRelations that live in
28 /// the same PresburgerSpace with support for union, intersection, subtraction,
29 /// and complement operations, as well as sampling.
30 ///
31 /// The IntegerRelations (disjuncts) are stored in a vector, and the set
32 /// represents the union of these relations. An empty list corresponds to
33 /// the empty set.
34 ///
35 /// Note that there are no invariants guaranteed on the list of disjuncts
36 /// other than that they are all in the same PresburgerSpace. For example, the
37 /// relations may overlap with each other.
39 public:
40  /// Return a universe set of the specified type that contains all points.
42 
43  /// Return an empty set of the specified type that contains no points.
45 
46  explicit PresburgerRelation(const IntegerRelation &disjunct);
47 
48  unsigned getNumDomainVars() const { return space.getNumDomainVars(); }
49  unsigned getNumRangeVars() const { return space.getNumRangeVars(); }
50  unsigned getNumSymbolVars() const { return space.getNumSymbolVars(); }
51  unsigned getNumLocalVars() const { return space.getNumLocalVars(); }
52  unsigned getNumVars() const { return space.getNumVars(); }
53 
54  /// Return the number of disjuncts in the union.
55  unsigned getNumDisjuncts() const;
56 
57  const PresburgerSpace &getSpace() const { return space; }
58 
59  /// Set the space to `oSpace`. `oSpace` should not contain any local ids.
60  /// `oSpace` need not have the same number of ids as the current space;
61  /// it could have more or less. If it has less, the extra ids become
62  /// locals of the disjuncts. It can also have more, in which case the
63  /// disjuncts will have fewer locals. If its total number of ids
64  /// exceeds that of some disjunct, an assert failure will occur.
65  void setSpace(const PresburgerSpace &oSpace);
66 
67  void insertVarInPlace(VarKind kind, unsigned pos, unsigned num = 1);
68 
69  /// Converts variables of the specified kind in the column range [srcPos,
70  /// srcPos + num) to variables of the specified kind at position dstPos. The
71  /// ranges are relative to the kind of variable.
72  ///
73  /// srcKind and dstKind must be different.
74  void convertVarKind(VarKind srcKind, unsigned srcPos, unsigned num,
75  VarKind dstKind, unsigned dstPos);
76 
77  /// Return a reference to the list of disjuncts.
79 
80  /// Return the disjunct at the specified index.
81  const IntegerRelation &getDisjunct(unsigned index) const;
82 
83  /// Mutate this set, turning it into the union of this set and the given
84  /// disjunct.
85  void unionInPlace(const IntegerRelation &disjunct);
86 
87  /// Mutate this set, turning it into the union of this set and the given set.
88  void unionInPlace(const PresburgerRelation &set);
89 
90  /// Return the union of this set and the given set.
92 
93  /// Return the intersection of this set and the given set.
95 
96  /// Return the range intersection of the given `set` with `this` relation.
97  ///
98  /// Formally, let the relation `this` be R: A -> B and `set` is C, then this
99  /// operation returns A -> (B intersection C).
101 
102  /// Return the domain intersection of the given `set` with `this` relation.
103  ///
104  /// Formally, let the relation `this` be R: A -> B and `set` is C, then this
105  /// operation returns (A intersection C) -> B.
107 
108  /// Return a set corresponding to the domain of the relation.
109  PresburgerSet getDomainSet() const;
110  /// Return a set corresponding to the range of the relation.
111  PresburgerSet getRangeSet() const;
112 
113  /// Invert the relation, i.e. swap its domain and range.
114  ///
115  /// Formally, if `this`: A -> B then `inverse` updates `this` in-place to
116  /// `this`: B -> A.
117  void inverse();
118 
119  /// Compose `this` relation with the given relation `rel` in-place.
120  ///
121  /// Formally, if `this`: A -> B, and `rel`: B -> C, then this function updates
122  /// `this` to `result`: A -> C where a point (a, c) belongs to `result`
123  /// iff there exists b such that (a, b) is in `this` and, (b, c) is in rel.
124  void compose(const PresburgerRelation &rel);
125 
126  /// Apply the domain of given relation `rel` to `this` relation.
127  ///
128  /// Formally, R1.applyDomain(R2) = R2.inverse().compose(R1).
129  void applyDomain(const PresburgerRelation &rel);
130 
131  /// Same as compose, provided for uniformity with applyDomain.
132  void applyRange(const PresburgerRelation &rel);
133 
134  /// Compute the symbolic integer lexmin of the relation, i.e. for every
135  /// assignment of the symbols and domain the lexicographically minimum value
136  /// attained by the range.
138 
139  /// Compute the symbolic integer lexmax of the relation, i.e. for every
140  /// assignment of the symbols and domain the lexicographically maximum value
141  /// attained by the range.
143 
144  /// Return true if the set contains the given point, and false otherwise.
145  bool containsPoint(ArrayRef<DynamicAPInt> point) const;
146  bool containsPoint(ArrayRef<int64_t> point) const {
147  return containsPoint(getDynamicAPIntVec(point));
148  }
149 
150  /// Return the complement of this set. All local variables in the set must
151  /// correspond to floor divisions.
153 
154  /// Return the set difference of this set and the given set, i.e.,
155  /// return `this \ set`. All local variables in `set` must correspond
156  /// to floor divisions, but local variables in `this` need not correspond to
157  /// divisions.
159 
160  /// Return true if this set is a subset of the given set, and false otherwise.
161  bool isSubsetOf(const PresburgerRelation &set) const;
162 
163  /// Return true if this set is equal to the given set, and false otherwise.
164  /// All local variables in both sets must correspond to floor divisions.
165  bool isEqual(const PresburgerRelation &set) const;
166 
167  /// Return true if all the sets in the union are known to be integer empty
168  /// false otherwise.
169  bool isIntegerEmpty() const;
170 
171  /// Return true if there is no disjunct, false otherwise.
172  bool isObviouslyEmpty() const;
173 
174  /// Return true if the set is known to have one unconstrained disjunct, false
175  /// otherwise.
176  bool isObviouslyUniverse() const;
177 
178  /// Perform a quick equality check on `this` and `other`. The relations are
179  /// equal if the check return true, but may or may not be equal if the check
180  /// returns false. This is doing by directly comparing whether each internal
181  /// disjunct is the same.
182  bool isObviouslyEqual(const PresburgerRelation &set) const;
183 
184  /// Return true if the set is consist of a single disjunct, without any local
185  /// variables, false otherwise.
186  bool isConvexNoLocals() const;
187 
188  /// Find an integer sample from the given set. This should not be called if
189  /// any of the disjuncts in the union are unbounded.
191 
192  /// Compute an overapproximation of the number of integer points in the
193  /// disjunct. Symbol vars are currently not supported. If the computed
194  /// overapproximation is infinite, an empty optional is returned.
195  ///
196  /// This currently just sums up the overapproximations of the volumes of the
197  /// disjuncts, so the approximation might be far from the true volume in the
198  /// case when there is a lot of overlap between disjuncts.
199  std::optional<DynamicAPInt> computeVolume() const;
200 
201  /// Simplifies the representation of a PresburgerRelation.
202  ///
203  /// In particular, removes all disjuncts which are subsets of other
204  /// disjuncts in the union.
206 
207  /// Check whether all local ids in all disjuncts have a div representation.
208  bool hasOnlyDivLocals() const;
209 
210  /// Compute an equivalent representation of the same relation, such that all
211  /// local ids in all disjuncts have division representations. This
212  /// representation may involve local ids that correspond to divisions, and may
213  /// also be a union of convex disjuncts.
215 
216  /// Simplify each disjunct, canonicalizing each disjunct and removing
217  /// redundencies.
219 
220  /// Return whether the given PresburgerRelation is full-dimensional. By full-
221  /// dimensional we mean that it is not flat along any dimension.
222  bool isFullDim() const;
223 
224  /// Print the set's internal state.
225  void print(raw_ostream &os) const;
226  void dump() const;
227 
228 protected:
229  /// Construct an empty PresburgerRelation with the specified number of
230  /// dimension and symbols.
232  assert(space.getNumLocalVars() == 0 &&
233  "PresburgerRelation cannot have local vars.");
234  }
235 
237 
238  /// The list of disjuncts that this set is the union of.
240 
241  friend class SetCoalescer;
242 };
243 
245 public:
246  /// Return a universe set of the specified type that contains all points.
248 
249  /// Return an empty set of the specified type that contains no points.
251 
252  /// Create a set from a relation.
253  explicit PresburgerSet(const IntegerPolyhedron &disjunct);
254  explicit PresburgerSet(const PresburgerRelation &set);
255 
256  /// These operations are the same as the ones in PresburgeRelation, they just
257  /// forward the arguement and return the result as a set instead of a
258  /// relation.
259  PresburgerSet unionSet(const PresburgerRelation &set) const;
260  PresburgerSet intersect(const PresburgerRelation &set) const;
261  PresburgerSet complement() const;
262  PresburgerSet subtract(const PresburgerRelation &set) const;
263  PresburgerSet coalesce() const;
264 
265 protected:
266  /// Construct an empty PresburgerRelation with the specified number of
267  /// dimension and symbols.
270  assert(space.getNumDomainVars() == 0 &&
271  "Set type cannot have domain vars.");
272  assert(space.getNumLocalVars() == 0 &&
273  "PresburgerRelation cannot have local vars.");
274  }
275 };
276 
277 } // namespace presburger
278 } // namespace mlir
279 
280 #endif // MLIR_ANALYSIS_PRESBURGER_PRESBURGERRELATION_H
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace.
PresburgerRelation(const PresburgerSpace &space)
Construct an empty PresburgerRelation with the specified number of dimension and symbols.
PresburgerRelation intersect(const PresburgerRelation &set) const
Return the intersection of this set and the given set.
bool hasOnlyDivLocals() const
Check whether all local ids in all disjuncts have a div representation.
bool containsPoint(ArrayRef< DynamicAPInt > point) const
Return true if the set contains the given point, and false otherwise.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
PresburgerRelation(const IntegerRelation &disjunct)
PresburgerSet getRangeSet() const
Return a set corresponding to the range of the relation.
bool isConvexNoLocals() const
Return true if the set is consist of a single disjunct, without any local variables,...
PresburgerRelation computeReprWithOnlyDivLocals() const
Compute an equivalent representation of the same relation, such that all local ids in all disjuncts h...
bool isSubsetOf(const PresburgerRelation &set) const
Return true if this set is a subset of the given set, and false otherwise.
bool containsPoint(ArrayRef< int64_t > point) const
bool isIntegerEmpty() const
Return true if all the sets in the union are known to be integer empty false otherwise.
PresburgerRelation intersectRange(const PresburgerSet &set) const
Return the range intersection of the given set with this relation.
void unionInPlace(const IntegerRelation &disjunct)
Mutate this set, turning it into the union of this set and the given disjunct.
std::optional< DynamicAPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the disjunct.
void convertVarKind(VarKind srcKind, unsigned srcPos, unsigned num, VarKind dstKind, unsigned dstPos)
Converts variables of the specified kind in the column range [srcPos, srcPos + num) to variables of t...
PresburgerRelation intersectDomain(const PresburgerSet &set) const
Return the domain intersection of the given set with this relation.
bool isEqual(const PresburgerRelation &set) const
Return true if this set is equal to the given set, and false otherwise.
static PresburgerRelation getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
void applyDomain(const PresburgerRelation &rel)
Apply the domain of given relation rel to this relation.
unsigned getNumDisjuncts() const
Return the number of disjuncts in the union.
void applyRange(const PresburgerRelation &rel)
Same as compose, provided for uniformity with applyDomain.
bool findIntegerSample(SmallVectorImpl< DynamicAPInt > &sample)
Find an integer sample from the given set.
bool isObviouslyEmpty() const
Return true if there is no disjunct, false otherwise.
bool isObviouslyUniverse() const
Return true if the set is known to have one unconstrained disjunct, false otherwise.
PresburgerRelation coalesce() const
Simplifies the representation of a PresburgerRelation.
static PresburgerRelation getUniverse(const PresburgerSpace &space)
Return a universe set of the specified type that contains all points.
const IntegerRelation & getDisjunct(unsigned index) const
Return the disjunct at the specified index.
ArrayRef< IntegerRelation > getAllDisjuncts() const
Return a reference to the list of disjuncts.
SmallVector< IntegerRelation, 2 > disjuncts
The list of disjuncts that this set is the union of.
PresburgerRelation simplify() const
Simplify each disjunct, canonicalizing each disjunct and removing redundencies.
void compose(const PresburgerRelation &rel)
Compose this relation with the given relation rel in-place.
const PresburgerSpace & getSpace() const
void print(raw_ostream &os) const
Print the set's internal state.
void inverse()
Invert the relation, i.e.
PresburgerSet getDomainSet() const
Return a set corresponding to the domain of the relation.
SymbolicLexOpt findSymbolicIntegerLexMax() const
Compute the symbolic integer lexmax of the relation, i.e.
void insertVarInPlace(VarKind kind, unsigned pos, unsigned num=1)
PresburgerRelation unionSet(const PresburgerRelation &set) const
Return the union of this set and the given set.
bool isObviouslyEqual(const PresburgerRelation &set) const
Perform a quick equality check on this and other.
SymbolicLexOpt findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation, i.e.
bool isFullDim() const
Return whether the given PresburgerRelation is full-dimensional.
PresburgerRelation complement() const
Return the complement of this set.
PresburgerSet intersect(const PresburgerRelation &set) const
PresburgerSet(const IntegerPolyhedron &disjunct)
Create a set from a relation.
PresburgerSet unionSet(const PresburgerRelation &set) const
These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...
PresburgerSet subtract(const PresburgerRelation &set) const
static PresburgerSet getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
PresburgerSet(const PresburgerSpace &space)
Construct an empty PresburgerRelation with the specified number of dimension and symbols.
static PresburgerSet getUniverse(const PresburgerSpace &space)
Return a universe set of the specified type that contains all points.
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
The SetCoalescer class contains all functionality concerning the coalesce heuristic.
VarKind
Kind of variable.
SmallVector< DynamicAPInt, 8 > getDynamicAPIntVec(ArrayRef< int64_t > range)
Check if the pos^th variable can be expressed as a floordiv of an affine function of other variables ...
Definition: Utils.cpp:524
Include the generated interface declarations.
Represents the result of a symbolic lexicographic optimization computation.
Definition: Simplex.h:529