1 | //===- IntegerRelation.h - MLIR IntegerRelation Class ---------*- C++ -*---===// |
2 | // |
3 | // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. |
4 | // See https://llvm.org/LICENSE.txt for license information. |
5 | // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception |
6 | // |
7 | //===----------------------------------------------------------------------===// |
8 | // |
9 | // A class to represent a relation over integer tuples. A relation is |
10 | // represented as a constraint system over a space of tuples of integer valued |
11 | // variables supporting symbolic variables and existential quantification. |
12 | // |
13 | //===----------------------------------------------------------------------===// |
14 | |
15 | #ifndef MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H |
16 | #define MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H |
17 | |
18 | #include "mlir/Analysis/Presburger/Fraction.h" |
19 | #include "mlir/Analysis/Presburger/Matrix.h" |
20 | #include "mlir/Analysis/Presburger/PresburgerSpace.h" |
21 | #include "mlir/Analysis/Presburger/Utils.h" |
22 | #include "mlir/Support/LogicalResult.h" |
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. |
56 | class IntegerRelation { |
57 | public: |
58 | /// All derived classes of IntegerRelation. |
59 | enum class Kind { |
60 | IntegerRelation, |
61 | IntegerPolyhedron, |
62 | FlatLinearConstraints, |
63 | FlatLinearValueConstraints, |
64 | FlatAffineValueConstraints, |
65 | FlatAffineRelation |
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. |
81 | explicit IntegerRelation(const PresburgerSpace &space) |
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. |
90 | static IntegerRelation getUniverse(const PresburgerSpace &space) { |
91 | return IntegerRelation(space); |
92 | } |
93 | |
94 | /// Return an empty system containing an invalid equation 0 = 1. |
95 | static IntegerRelation getEmpty(const PresburgerSpace &space) { |
96 | IntegerRelation result(0, 1, space.getNumVars() + 1, space); |
97 | SmallVector<int64_t> invalidEq(space.getNumVars() + 1, 0); |
98 | invalidEq.back() = 1; |
99 | result.addEquality(eq: invalidEq); |
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. |
134 | ArrayRef<Identifier> getIds(VarKind kind); |
135 | |
136 | /// Returns a copy of the space without locals. |
137 | PresburgerSpace getSpaceWithoutLocals() const { |
138 | return PresburgerSpace::getRelationSpace(numDomain: space.getNumDomainVars(), |
139 | numRange: space.getNumRangeVars(), |
140 | numSymbols: space.getNumSymbolVars()); |
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. |
149 | IntegerRelation intersect(IntegerRelation other) const; |
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 { |
189 | return getNumInequalities() + getNumEqualities(); |
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 { |
213 | return equalities.getNumReservedRows(); |
214 | } |
215 | |
216 | inline unsigned getNumReservedInequalities() const { |
217 | return inequalities.getNumReservedRows(); |
218 | } |
219 | |
220 | inline ArrayRef<MPInt> getEquality(unsigned idx) const { |
221 | return equalities.getRow(row: idx); |
222 | } |
223 | inline ArrayRef<MPInt> getInequality(unsigned idx) const { |
224 | return inequalities.getRow(row: 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(range: equalities.getRow(row: idx)); |
230 | } |
231 | inline SmallVector<int64_t, 8> getInequality64(unsigned idx) const { |
232 | return getInt64Vec(range: inequalities.getRow(row: 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`. |
300 | void addInequality(ArrayRef<MPInt> inEq); |
301 | void addInequality(ArrayRef<int64_t> inEq) { |
302 | addInequality(inEq: getMPIntVec(range: inEq)); |
303 | } |
304 | /// Adds an equality from the coefficients specified in `eq`. |
305 | void addEquality(ArrayRef<MPInt> eq); |
306 | void addEquality(ArrayRef<int64_t> eq) { addEquality(eq: getMPIntVec(range: 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. |
334 | MaybeOptimum<SmallVector<Fraction, 8>> findRationalLexMin() const; |
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. |
341 | MaybeOptimum<SmallVector<MPInt, 8>> findIntegerLexMin() const; |
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 `po`s 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, values: getMPIntVec(range: 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. |
394 | IntMatrix getBoundedDirections() const; |
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(point: getMPIntVec(range: 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>> |
418 | containsPointNoLocal(ArrayRef<MPInt> point) const; |
419 | std::optional<SmallVector<MPInt, 8>> |
420 | containsPointNoLocal(ArrayRef<int64_t> point) const { |
421 | return containsPointNoLocal(point: getMPIntVec(range: 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) { |
438 | addBound(type, pos, value: MPInt(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) { |
444 | addBound(type, expr: getMPIntVec(range: expr), value: MPInt(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) { |
454 | addLocalFloorDiv(dividend: getMPIntVec(range: dividend), divisor: MPInt(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, num: 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} |
492 | LogicalResult unionBoundingBox(const IntegerRelation &other); |
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, lb: &lbMPInt, boundFloorDivisor: &boundFloorDivisorMPInt, ub: &ubMPInt, minLbPos, minUbPos); |
525 | if (lb) |
526 | *lb = getInt64Vec(range: lbMPInt); |
527 | if (ub) |
528 | *ub = getInt64Vec(range: ubMPInt); |
529 | if (boundFloorDivisor) |
530 | *boundFloorDivisor = static_cast<int64_t>(boundFloorDivisorMPInt); |
531 | return llvm::transformOptional(O: result, F&: 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(O: getConstantBound(type, pos), F&: 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. |
558 | void removeTrivialRedundancy(); |
559 | |
560 | /// A more expensive check than `removeTrivialRedundancy` to detect redundant |
561 | /// inequalities. |
562 | void removeRedundantInequalities(); |
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. |
569 | void removeRedundantConstraints(); |
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 | pos: getNumVarKind(kind: dstKind)); |
588 | } |
589 | void convertToLocal(VarKind kind, unsigned varStart, unsigned varLimit) { |
590 | convertVarKind(srcKind: kind, varStart, varLimit, dstKind: 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. |
596 | void mergeAndAlignSymbols(IntegerRelation &other); |
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. |
634 | IntegerPolyhedron getDomainSet() const; |
635 | |
636 | /// Return a set corresponding to all points in the range of the relation. |
637 | IntegerPolyhedron getRangeSet() const; |
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. |
692 | PresburgerRelation computeReprWithOnlyDivLocals() const; |
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`. |
716 | SymbolicLexOpt findSymbolicIntegerLexMin() const; |
717 | |
718 | /// Same as findSymbolicIntegerLexMin but produces lexmax instead of lexmin |
719 | SymbolicLexOpt findSymbolicIntegerLexMax() const; |
720 | |
721 | /// Return the set difference of this set and the given set, i.e., |
722 | /// return `this \ set`. |
723 | PresburgerRelation subtract(const PresburgerRelation &set) const; |
724 | |
725 | // Remove equalities which have only zero coefficients. |
726 | void removeTrivialEqualities(); |
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(isSuccess: gaussianEliminateVars(posStart: position, posLimit: 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. |
770 | void removeRedundantLocalVars(); |
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 |
786 | /// shadow / exact integer shadow is computed. |
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. |
800 | void normalizeConstraintsByGCD(); |
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. |
814 | bool removeDuplicateConstraints(); |
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 | |
850 | PresburgerSpace space; |
851 | |
852 | /// Coefficients of affine equalities (in == 0 form). |
853 | IntMatrix equalities; |
854 | |
855 | /// Coefficients of affine inequalities (in >= 0 form). |
856 | IntMatrix inequalities; |
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. |
876 | class IntegerPolyhedron : public IntegerRelation { |
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. |
891 | explicit IntegerPolyhedron(const PresburgerSpace &space) |
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. |
898 | explicit IntegerPolyhedron(const PresburgerSpace &space, |
899 | IntMatrix inequalities) |
900 | : IntegerPolyhedron(space) { |
901 | for (unsigned i = 0, e = inequalities.getNumRows(); i < e; i++) |
902 | addInequality(inEq: inequalities.getRow(row: 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. |
908 | explicit IntegerPolyhedron(const PresburgerSpace &space, |
909 | FracMatrix inequalities) |
910 | : IntegerPolyhedron(space) { |
911 | IntMatrix ineqsNormalized = inequalities.normalizeRows(); |
912 | for (unsigned i = 0, e = inequalities.getNumRows(); i < e; i++) |
913 | addInequality(inEq: ineqsNormalized.getRow(row: 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. |
926 | explicit IntegerPolyhedron(IntegerRelation &&rel) : IntegerRelation(rel) { |
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. |
933 | static IntegerPolyhedron getUniverse(const PresburgerSpace &space) { |
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 && |
942 | cst->getKind() <= Kind::FlatAffineRelation; |
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 |
951 | /// first added variable. |
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 |
967 | |