//===- IntegerRelation.cpp - MLIR IntegerRelation Class ---------------===// // // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. // See https://llvm.org/LICENSE.txt for license information. // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // // A class to represent an relation over integer tuples. A relation is // represented as a constraint system over a space of tuples of integer valued // variables supporting symbolic variables and existential quantification. // //===----------------------------------------------------------------------===// #include "mlir/Analysis/Presburger/IntegerRelation.h" #include "mlir/Analysis/Presburger/Fraction.h" #include "mlir/Analysis/Presburger/LinearTransform.h" #include "mlir/Analysis/Presburger/PWMAFunction.h" #include "mlir/Analysis/Presburger/PresburgerRelation.h" #include "mlir/Analysis/Presburger/PresburgerSpace.h" #include "mlir/Analysis/Presburger/Simplex.h" #include "mlir/Analysis/Presburger/Utils.h" #include "llvm/ADT/DenseMap.h" #include "llvm/ADT/DenseSet.h" #include "llvm/ADT/STLExtras.h" #include "llvm/ADT/Sequence.h" #include "llvm/ADT/SmallBitVector.h" #include "llvm/Support/Debug.h" #include "llvm/Support/LogicalResult.h" #include "llvm/Support/raw_ostream.h" #include <algorithm> #include <cassert> #include <functional> #include <memory> #include <numeric> #include <optional> #include <sstream> #include <string> #include <utility> #include <vector> #define DEBUG_TYPE … usingnamespacemlir; usingnamespacepresburger; SmallDenseMap; SmallDenseSet; std::unique_ptr<IntegerRelation> IntegerRelation::clone() const { … } std::unique_ptr<IntegerPolyhedron> IntegerPolyhedron::clone() const { … } void IntegerRelation::setSpace(const PresburgerSpace &oSpace) { … } void IntegerRelation::setSpaceExceptLocals(const PresburgerSpace &oSpace) { … } void IntegerRelation::setId(VarKind kind, unsigned i, Identifier id) { … } ArrayRef<Identifier> IntegerRelation::getIds(VarKind kind) { … } void IntegerRelation::append(const IntegerRelation &other) { … } IntegerRelation IntegerRelation::intersect(IntegerRelation other) const { … } bool IntegerRelation::isEqual(const IntegerRelation &other) const { … } bool IntegerRelation::isObviouslyEqual(const IntegerRelation &other) const { … } bool IntegerRelation::isSubsetOf(const IntegerRelation &other) const { … } MaybeOptimum<SmallVector<Fraction, 8>> IntegerRelation::findRationalLexMin() const { … } MaybeOptimum<SmallVector<DynamicAPInt, 8>> IntegerRelation::findIntegerLexMin() const { … } static bool rangeIsZero(ArrayRef<DynamicAPInt> range) { … } static void removeConstraintsInvolvingVarRange(IntegerRelation &poly, unsigned begin, unsigned count) { … } IntegerRelation::CountsSnapshot IntegerRelation::getCounts() const { … } void IntegerRelation::truncateVarKind(VarKind kind, unsigned num) { … } void IntegerRelation::truncateVarKind(VarKind kind, const CountsSnapshot &counts) { … } void IntegerRelation::truncate(const CountsSnapshot &counts) { … } PresburgerRelation IntegerRelation::computeReprWithOnlyDivLocals() const { … } SymbolicLexOpt IntegerRelation::findSymbolicIntegerLexMin() const { … } /// findSymbolicIntegerLexMax is implemented using findSymbolicIntegerLexMin as /// follows: /// 1. A new relation is created which is `this` relation with the sign of /// each dimension variable in range flipped; /// 2. findSymbolicIntegerLexMin is called on the range negated relation to /// compute the negated lexmax of `this` relation; /// 3. The sign of the negated lexmax is flipped and returned. SymbolicLexOpt IntegerRelation::findSymbolicIntegerLexMax() const { … } PresburgerRelation IntegerRelation::subtract(const PresburgerRelation &set) const { … } unsigned IntegerRelation::insertVar(VarKind kind, unsigned pos, unsigned num) { … } unsigned IntegerRelation::appendVar(VarKind kind, unsigned num) { … } void IntegerRelation::addEquality(ArrayRef<DynamicAPInt> eq) { … } void IntegerRelation::addInequality(ArrayRef<DynamicAPInt> inEq) { … } void IntegerRelation::removeVar(VarKind kind, unsigned pos) { … } void IntegerRelation::removeVar(unsigned pos) { … } void IntegerRelation::removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit) { … } void IntegerRelation::removeVarRange(unsigned varStart, unsigned varLimit) { … } void IntegerRelation::removeEquality(unsigned pos) { … } void IntegerRelation::removeInequality(unsigned pos) { … } void IntegerRelation::removeEqualityRange(unsigned start, unsigned end) { … } void IntegerRelation::removeInequalityRange(unsigned start, unsigned end) { … } void IntegerRelation::swapVar(unsigned posA, unsigned posB) { … } void IntegerRelation::clearConstraints() { … } /// Gather all lower and upper bounds of the variable at `pos`, and /// optionally any equalities on it. In addition, the bounds are to be /// independent of variables in position range [`offset`, `offset` + `num`). void IntegerRelation::getLowerAndUpperBoundIndices( unsigned pos, SmallVectorImpl<unsigned> *lbIndices, SmallVectorImpl<unsigned> *ubIndices, SmallVectorImpl<unsigned> *eqIndices, unsigned offset, unsigned num) const { … } bool IntegerRelation::hasConsistentState() const { … } void IntegerRelation::setAndEliminate(unsigned pos, ArrayRef<DynamicAPInt> values) { … } void IntegerRelation::clearAndCopyFrom(const IntegerRelation &other) { … } // Searches for a constraint with a non-zero coefficient at `colIdx` in // equality (isEq=true) or inequality (isEq=false) constraints. // Returns true and sets row found in search in `rowIdx`, false otherwise. bool IntegerRelation::findConstraintWithNonZeroAt(unsigned colIdx, bool isEq, unsigned *rowIdx) const { … } void IntegerRelation::normalizeConstraintsByGCD() { … } bool IntegerRelation::hasInvalidConstraint() const { … } /// Eliminate variable from constraint at `rowIdx` based on coefficient at /// pivotRow, pivotCol. Columns in range [elimColStart, pivotCol) will not be /// updated as they have already been eliminated. static void eliminateFromConstraint(IntegerRelation *constraints, unsigned rowIdx, unsigned pivotRow, unsigned pivotCol, unsigned elimColStart, bool isEq) { … } /// Returns the position of the variable that has the minimum <number of lower /// bounds> times <number of upper bounds> from the specified range of /// variables [start, end). It is often best to eliminate in the increasing /// order of these counts when doing Fourier-Motzkin elimination since FM adds /// that many new constraints. static unsigned getBestVarToEliminate(const IntegerRelation &cst, unsigned start, unsigned end) { … } // Checks for emptiness of the set by eliminating variables successively and // using the GCD test (on all equality constraints) and checking for trivially // invalid constraints. Returns 'true' if the constraint system is found to be // empty; false otherwise. bool IntegerRelation::isEmpty() const { … } bool IntegerRelation::isObviouslyEmpty() const { … } // Runs the GCD test on all equality constraints. Returns 'true' if this test // fails on any equality. Returns 'false' otherwise. // This test can be used to disprove the existence of a solution. If it returns // true, no integer solution to the equality constraints can exist. // // GCD test definition: // // The equality constraint: // // c_1*x_1 + c_2*x_2 + ... + c_n*x_n = c_0 // // has an integer solution iff: // // GCD of c_1, c_2, ..., c_n divides c_0. bool IntegerRelation::isEmptyByGCDTest() const { … } // Returns a matrix where each row is a vector along which the polytope is // bounded. The span of the returned vectors is guaranteed to contain all // such vectors. The returned vectors are NOT guaranteed to be linearly // independent. This function should not be called on empty sets. // // It is sufficient to check the perpendiculars of the constraints, as the set // of perpendiculars which are bounded must span all bounded directions. IntMatrix IntegerRelation::getBoundedDirections() const { … } bool IntegerRelation::isIntegerEmpty() const { … } /// Let this set be S. If S is bounded then we directly call into the GBR /// sampling algorithm. Otherwise, there are some unbounded directions, i.e., /// vectors v such that S extends to infinity along v or -v. In this case we /// use an algorithm described in the integer set library (isl) manual and used /// by the isl_set_sample function in that library. The algorithm is: /// /// 1) Apply a unimodular transform T to S to obtain S*T, such that all /// dimensions in which S*T is bounded lie in the linear span of a prefix of the /// dimensions. /// /// 2) Construct a set B by removing all constraints that involve /// the unbounded dimensions and then deleting the unbounded dimensions. Note /// that B is a Bounded set. /// /// 3) Try to obtain a sample from B using the GBR sampling /// algorithm. If no sample is found, return that S is empty. /// /// 4) Otherwise, substitute the obtained sample into S*T to obtain a set /// C. C is a full-dimensional Cone and always contains a sample. /// /// 5) Obtain an integer sample from C. /// /// 6) Return T*v, where v is the concatenation of the samples from B and C. /// /// The following is a sketch of a proof that /// a) If the algorithm returns empty, then S is empty. /// b) If the algorithm returns a sample, it is a valid sample in S. /// /// The algorithm returns empty only if B is empty, in which case S*T is /// certainly empty since B was obtained by removing constraints and then /// deleting unconstrained dimensions from S*T. Since T is unimodular, a vector /// v is in S*T iff T*v is in S. So in this case, since /// S*T is empty, S is empty too. /// /// Otherwise, the algorithm substitutes the sample from B into S*T. All the /// constraints of S*T that did not involve unbounded dimensions are satisfied /// by this substitution. All dimensions in the linear span of the dimensions /// outside the prefix are unbounded in S*T (step 1). Substituting values for /// the bounded dimensions cannot make these dimensions bounded, and these are /// the only remaining dimensions in C, so C is unbounded along every vector (in /// the positive or negative direction, or both). C is hence a full-dimensional /// cone and therefore always contains an integer point. /// /// Concatenating the samples from B and C gives a sample v in S*T, so the /// returned sample T*v is a sample in S. std::optional<SmallVector<DynamicAPInt, 8>> IntegerRelation::findIntegerSample() const { … } /// Helper to evaluate an affine expression at a point. /// The expression is a list of coefficients for the dimensions followed by the /// constant term. static DynamicAPInt valueAt(ArrayRef<DynamicAPInt> expr, ArrayRef<DynamicAPInt> point) { … } /// A point satisfies an equality iff the value of the equality at the /// expression is zero, and it satisfies an inequality iff the value of the /// inequality at that point is non-negative. bool IntegerRelation::containsPoint(ArrayRef<DynamicAPInt> point) const { … } /// Just substitute the values given and check if an integer sample exists for /// the local vars. /// /// TODO: this could be made more efficient by handling divisions separately. /// Instead of finding an integer sample over all the locals, we can first /// compute the values of the locals that have division representations and /// only use the integer emptiness check for the locals that don't have this. /// Handling this correctly requires ordering the divs, though. std::optional<SmallVector<DynamicAPInt, 8>> IntegerRelation::containsPointNoLocal(ArrayRef<DynamicAPInt> point) const { … } DivisionRepr IntegerRelation::getLocalReprs(std::vector<MaybeLocalRepr> *repr) const { … } /// Tightens inequalities given that we are dealing with integer spaces. This is /// analogous to the GCD test but applied to inequalities. The constant term can /// be reduced to the preceding multiple of the GCD of the coefficients, i.e., /// 64*i - 100 >= 0 => 64*i - 128 >= 0 (since 'i' is an integer). This is a /// fast method - linear in the number of coefficients. // Example on how this affects practical cases: consider the scenario: // 64*i >= 100, j = 64*i; without a tightening, elimination of i would yield // j >= 100 instead of the tighter (exact) j >= 128. void IntegerRelation::gcdTightenInequalities() { … } // Eliminates all variable variables in column range [posStart, posLimit). // Returns the number of variables eliminated. unsigned IntegerRelation::gaussianEliminateVars(unsigned posStart, unsigned posLimit) { … } bool IntegerRelation::gaussianEliminate() { … } // A more complex check to eliminate redundant inequalities. Uses FourierMotzkin // to check if a constraint is redundant. void IntegerRelation::removeRedundantInequalities() { … } // A more complex check to eliminate redundant inequalities and equalities. Uses // Simplex to check if a constraint is redundant. void IntegerRelation::removeRedundantConstraints() { … } std::optional<DynamicAPInt> IntegerRelation::computeVolume() const { … } void IntegerRelation::eliminateRedundantLocalVar(unsigned posA, unsigned posB) { … } /// mergeAndAlignSymbols's implementation can be broken down into two steps: /// 1. Merge and align identifiers into `other` from `this. If an identifier /// from `this` exists in `other` then we align it. Otherwise, we assume it is a /// new identifier and insert it into `other` in the same position as `this`. /// 2. Add identifiers that are in `other` but not `this to `this`. void IntegerRelation::mergeAndAlignSymbols(IntegerRelation &other) { … } /// Adds additional local ids to the sets such that they both have the union /// of the local ids in each set, without changing the set of points that /// lie in `this` and `other`. /// /// To detect local ids that always take the same value, each local id is /// represented as a floordiv with constant denominator in terms of other ids. /// After extracting these divisions, local ids in `other` with the same /// division representation as some other local id in any set are considered /// duplicate and are merged. /// /// It is possible that division representation for some local id cannot be /// obtained, and thus these local ids are not considered for detecting /// duplicates. unsigned IntegerRelation::mergeLocalVars(IntegerRelation &other) { … } bool IntegerRelation::hasOnlyDivLocals() const { … } void IntegerRelation::removeDuplicateDivs() { … } void IntegerRelation::simplify() { … } /// Removes local variables using equalities. Each equality is checked if it /// can be reduced to the form: `e = affine-expr`, where `e` is a local /// variable and `affine-expr` is an affine expression not containing `e`. /// If an equality satisfies this form, the local variable is replaced in /// each constraint and then removed. The equality used to replace this local /// variable is also removed. void IntegerRelation::removeRedundantLocalVars() { … } void IntegerRelation::convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit, VarKind dstKind, unsigned pos) { … } void IntegerRelation::addBound(BoundType type, unsigned pos, const DynamicAPInt &value) { … } void IntegerRelation::addBound(BoundType type, ArrayRef<DynamicAPInt> expr, const DynamicAPInt &value) { … } /// Adds a new local variable as the floordiv of an affine function of other /// variables, the coefficients of which are provided in 'dividend' and with /// respect to a positive constant 'divisor'. Two constraints are added to the /// system to capture equivalence with the floordiv. /// q = expr floordiv c <=> c*q <= expr <= c*q + c - 1. void IntegerRelation::addLocalFloorDiv(ArrayRef<DynamicAPInt> dividend, const DynamicAPInt &divisor) { … } /// Finds an equality that equates the specified variable to a constant. /// Returns the position of the equality row. If 'symbolic' is set to true, /// symbols are also treated like a constant, i.e., an affine function of the /// symbols is also treated like a constant. Returns -1 if such an equality /// could not be found. static int findEqualityToConstant(const IntegerRelation &cst, unsigned pos, bool symbolic = false) { … } LogicalResult IntegerRelation::constantFoldVar(unsigned pos) { … } void IntegerRelation::constantFoldVarRange(unsigned pos, unsigned num) { … } /// Returns a non-negative constant bound on the extent (upper bound - lower /// bound) of the specified variable if it is found to be a constant; returns /// std::nullopt if it's not a constant. This methods treats symbolic variables /// specially, i.e., it looks for constant differences between affine /// expressions involving only the symbolic variables. See comments at function /// definition for example. 'lb', if provided, is set to the lower bound /// associated with the constant difference. Note that 'lb' is purely symbolic /// and thus will contain the coefficients of the symbolic variables and the /// constant coefficient. // Egs: 0 <= i <= 15, return 16. // s0 + 2 <= i <= s0 + 17, returns 16. (s0 has to be a symbol) // s0 + s1 + 16 <= d0 <= s0 + s1 + 31, returns 16. // s0 - 7 <= 8*j <= s0 returns 1 with lb = s0, lbDivisor = 8 (since lb = // ceil(s0 - 7 / 8) = floor(s0 / 8)). std::optional<DynamicAPInt> IntegerRelation::getConstantBoundOnDimSize( unsigned pos, SmallVectorImpl<DynamicAPInt> *lb, DynamicAPInt *boundFloorDivisor, SmallVectorImpl<DynamicAPInt> *ub, unsigned *minLbPos, unsigned *minUbPos) const { … } template <bool isLower> std::optional<DynamicAPInt> IntegerRelation::computeConstantLowerOrUpperBound(unsigned pos) { … } std::optional<DynamicAPInt> IntegerRelation::getConstantBound(BoundType type, unsigned pos) const { … } // A simple (naive and conservative) check for hyper-rectangularity. bool IntegerRelation::isHyperRectangular(unsigned pos, unsigned num) const { … } /// Removes duplicate constraints, trivially true constraints, and constraints /// that can be detected as redundant as a result of differing only in their /// constant term part. A constraint of the form <non-negative constant> >= 0 is /// considered trivially true. // Uses a DenseSet to hash and detect duplicates followed by a linear scan to // remove duplicates in place. void IntegerRelation::removeTrivialRedundancy() { … } #undef DEBUG_TYPE #define DEBUG_TYPE … /// Eliminates variable at the specified position using Fourier-Motzkin /// variable elimination. This technique is exact for rational spaces but /// conservative (in "rare" cases) for integer spaces. The operation corresponds /// to a projection operation yielding the (convex) set of integer points /// contained in the rational shadow of the set. An emptiness test that relies /// on this method will guarantee emptiness, i.e., it disproves the existence of /// a solution if it says it's empty. /// If a non-null isResultIntegerExact is passed, it is set to true if the /// result is also integer exact. If it's set to false, the obtained solution /// *may* not be exact, i.e., it may contain integer points that do not have an /// integer pre-image in the original set. /// /// Eg: /// j >= 0, j <= i + 1 /// i >= 0, i <= N + 1 /// Eliminating i yields, /// j >= 0, 0 <= N + 1, j - 1 <= N + 1 /// /// If darkShadow = true, this method computes the dark shadow on elimination; /// the dark shadow is a convex integer subset of the exact integer shadow. A /// non-empty dark shadow proves the existence of an integer solution. The /// elimination in such a case could however be an under-approximation, and thus /// should not be used for scanning sets or used by itself for dependence /// checking. /// /// Eg: 2-d set, * represents grid points, 'o' represents a point in the set. /// ^ /// | /// | * * * * o o /// i | * * o o o o /// | o * * * * * /// ---------------> /// j -> /// /// Eliminating i from this system (projecting on the j dimension): /// rational shadow / integer light shadow: 1 <= j <= 6 /// dark shadow: 3 <= j <= 6 /// exact integer shadow: j = 1 \union 3 <= j <= 6 /// holes/splinters: j = 2 /// /// darkShadow = false, isResultIntegerExact = nullptr are default values. // TODO: a slight modification to yield dark shadow version of FM (tightened), // which can prove the existence of a solution if there is one. void IntegerRelation::fourierMotzkinEliminate(unsigned pos, bool darkShadow, bool *isResultIntegerExact) { … } #undef DEBUG_TYPE #define DEBUG_TYPE … void IntegerRelation::projectOut(unsigned pos, unsigned num) { … } namespace { enum BoundCmpResult { … }; /// Compares two affine bounds whose coefficients are provided in 'first' and /// 'second'. The last coefficient is the constant term. static BoundCmpResult compareBounds(ArrayRef<DynamicAPInt> a, ArrayRef<DynamicAPInt> b) { … } } // namespace // Returns constraints that are common to both A & B. static void getCommonConstraints(const IntegerRelation &a, const IntegerRelation &b, IntegerRelation &c) { … } // Computes the bounding box with respect to 'other' by finding the min of the // lower bounds and the max of the upper bounds along each of the dimensions. LogicalResult IntegerRelation::unionBoundingBox(const IntegerRelation &otherCst) { … } bool IntegerRelation::isColZero(unsigned pos) const { … } /// Find positions of inequalities and equalities that do not have a coefficient /// for [pos, pos + num) variables. static void getIndependentConstraints(const IntegerRelation &cst, unsigned pos, unsigned num, SmallVectorImpl<unsigned> &nbIneqIndices, SmallVectorImpl<unsigned> &nbEqIndices) { … } void IntegerRelation::removeIndependentConstraints(unsigned pos, unsigned num) { … } IntegerPolyhedron IntegerRelation::getDomainSet() const { … } bool IntegerRelation::removeDuplicateConstraints() { … } IntegerPolyhedron IntegerRelation::getRangeSet() const { … } void IntegerRelation::intersectDomain(const IntegerPolyhedron &poly) { … } void IntegerRelation::intersectRange(const IntegerPolyhedron &poly) { … } void IntegerRelation::inverse() { … } void IntegerRelation::compose(const IntegerRelation &rel) { … } void IntegerRelation::applyDomain(const IntegerRelation &rel) { … } void IntegerRelation::applyRange(const IntegerRelation &rel) { … } void IntegerRelation::printSpace(raw_ostream &os) const { … } void IntegerRelation::removeTrivialEqualities() { … } bool IntegerRelation::isFullDim() { … } void IntegerRelation::mergeAndCompose(const IntegerRelation &other) { … } void IntegerRelation::print(raw_ostream &os) const { … } void IntegerRelation::dump() const { … } unsigned IntegerPolyhedron::insertVar(VarKind kind, unsigned pos, unsigned num) { … } IntegerPolyhedron IntegerPolyhedron::intersect(const IntegerPolyhedron &other) const { … } PresburgerSet IntegerPolyhedron::subtract(const PresburgerSet &other) const { … }
Codebase Browser
llvm