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
25namespace mlir {
26namespace presburger {
27
28class IntegerRelation;
29class IntegerPolyhedron;
30class PresburgerSet;
31class PresburgerRelation;
32struct SymbolicLexOpt;
33
34/// The type of bound: equal, lower bound or upper bound.
35enum 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.
56class IntegerRelation {
57public:
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
739protected:
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.
876class IntegerPolyhedron : public IntegerRelation {
877public:
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

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