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
16#include "mlir/Analysis/Presburger/IntegerRelation.h"
17#include <optional>
18
19namespace mlir {
20namespace 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.
25class 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.
38class PresburgerRelation {
39public:
40 /// Return a universe set of the specified type that contains all points.
41 static PresburgerRelation getUniverse(const PresburgerSpace &space);
42
43 /// Return an empty set of the specified type that contains no points.
44 static PresburgerRelation getEmpty(const PresburgerSpace &space);
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.
78 ArrayRef<IntegerRelation> getAllDisjuncts() const;
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.
91 PresburgerRelation unionSet(const PresburgerRelation &set) const;
92
93 /// Return the intersection of this set and the given set.
94 PresburgerRelation intersect(const PresburgerRelation &set) const;
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).
100 PresburgerRelation intersectRange(const PresburgerSet &set) const;
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.
106 PresburgerRelation intersectDomain(const PresburgerSet &set) const;
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.
137 SymbolicLexOpt findSymbolicIntegerLexMin() const;
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.
142 SymbolicLexOpt findSymbolicIntegerLexMax() const;
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(point: getDynamicAPIntVec(range: point));
148 }
149
150 /// Return the complement of this set. All local variables in the set must
151 /// correspond to floor divisions.
152 PresburgerRelation complement() const;
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.
158 PresburgerRelation subtract(const PresburgerRelation &set) const;
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.
190 bool findIntegerSample(SmallVectorImpl<DynamicAPInt> &sample);
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.
205 PresburgerRelation coalesce() const;
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.
214 PresburgerRelation computeReprWithOnlyDivLocals() const;
215
216 /// Simplify each disjunct, canonicalizing each disjunct and removing
217 /// redundencies.
218 PresburgerRelation simplify() const;
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
228protected:
229 /// Construct an empty PresburgerRelation with the specified number of
230 /// dimension and symbols.
231 explicit PresburgerRelation(const PresburgerSpace &space) : space(space) {
232 assert(space.getNumLocalVars() == 0 &&
233 "PresburgerRelation cannot have local vars.");
234 }
235
236 PresburgerSpace space;
237
238 /// The list of disjuncts that this set is the union of.
239 SmallVector<IntegerRelation, 2> disjuncts;
240
241 friend class SetCoalescer;
242};
243
244class PresburgerSet : public PresburgerRelation {
245public:
246 /// Return a universe set of the specified type that contains all points.
247 static PresburgerSet getUniverse(const PresburgerSpace &space);
248
249 /// Return an empty set of the specified type that contains no points.
250 static PresburgerSet getEmpty(const PresburgerSpace &space);
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
265protected:
266 /// Construct an empty PresburgerRelation with the specified number of
267 /// dimension and symbols.
268 explicit PresburgerSet(const PresburgerSpace &space)
269 : PresburgerRelation(space) {
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
281

source code of mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h