MLIR  18.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<MPInt> point) const;
146  bool containsPoint(ArrayRef<int64_t> point) const {
147  return containsPoint(getMPIntVec(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 isPlainEmpty() const;
173 
174  /// Return true if the set is known to have one unconstrained disjunct, false
175  /// otherwise.
176  bool isPlainUniverse() 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 isPlainEqual(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<MPInt> 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  /// Print the set's internal state.
217  void print(raw_ostream &os) const;
218  void dump() const;
219 
220 protected:
221  /// Construct an empty PresburgerRelation with the specified number of
222  /// dimension and symbols.
224  assert(space.getNumLocalVars() == 0 &&
225  "PresburgerRelation cannot have local vars.");
226  }
227 
229 
230  /// The list of disjuncts that this set is the union of.
232 
233  friend class SetCoalescer;
234 };
235 
237 public:
238  /// Return a universe set of the specified type that contains all points.
240 
241  /// Return an empty set of the specified type that contains no points.
243 
244  /// Create a set from a relation.
245  explicit PresburgerSet(const IntegerPolyhedron &disjunct);
246  explicit PresburgerSet(const PresburgerRelation &set);
247 
248  /// These operations are the same as the ones in PresburgeRelation, they just
249  /// forward the arguement and return the result as a set instead of a
250  /// relation.
251  PresburgerSet unionSet(const PresburgerRelation &set) const;
252  PresburgerSet intersect(const PresburgerRelation &set) const;
253  PresburgerSet complement() const;
254  PresburgerSet subtract(const PresburgerRelation &set) const;
255  PresburgerSet coalesce() const;
256 
257 protected:
258  /// Construct an empty PresburgerRelation with the specified number of
259  /// dimension and symbols.
262  assert(space.getNumDomainVars() == 0 &&
263  "Set type cannot have domain vars.");
264  assert(space.getNumLocalVars() == 0 &&
265  "PresburgerRelation cannot have local vars.");
266  }
267 };
268 
269 } // namespace presburger
270 } // namespace mlir
271 
272 #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...
bool containsPoint(ArrayRef< MPInt > point) const
Return true if the set contains the given point, and false otherwise.
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.
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.
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.
std::optional< MPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the disjunct.
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.
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.
bool isPlainEqual(const PresburgerRelation &set) const
Perform a quick equality check on this and other.
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.
bool isPlainUniverse() const
Return true if the set is known to have one unconstrained disjunct, false otherwise.
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.
bool isPlainEmpty() const
Return true if there is no disjunct, false otherwise.
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.
SymbolicLexOpt findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation, i.e.
bool findIntegerSample(SmallVectorImpl< MPInt > &sample)
Find an integer sample from the given set.
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< 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:512
This header declares functions that assist transformations in the MemRef dialect.
Represents the result of a symbolic lexicographic optimization computation.
Definition: Simplex.h:533