diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h --- a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h +++ b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h @@ -14,44 +14,23 @@ #define MLIR_ANALYSIS_PRESBURGER_INTEGERPOLYHEDRON_H #include "mlir/Analysis/Presburger/Fraction.h" +#include "mlir/Analysis/Presburger/IntegerRelation.h" #include "mlir/Analysis/Presburger/Matrix.h" -#include "mlir/Analysis/Presburger/PresburgerSpace.h" #include "mlir/Analysis/Presburger/Utils.h" #include "mlir/Support/LogicalResult.h" namespace mlir { -/// An integer polyhedron is the set of solutions to a list of affine -/// constraints over n integer-valued variables/identifiers. Affine constraints -/// can be inequalities or equalities in the form: +/// An IntegerPolyhedron represents a convex polyhedron in space containing +/// integer points. /// -/// Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n >= 0 -/// Equality : c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n == 0 +/// An IntegerPolyhedron is similar to a IntegerRelation but it does not make a +/// distinction between Doman and Range identifiers. Internally, +/// IntegerPolyhedron is implemented as a IntegerRelation with zero domain. /// -/// where c_0, c_1, ..., c_n are integers. -/// -/// Such a set corresponds to the set of integer points lying in a convex -/// polyhedron. For example, consider the set: (x, y) : (1 <= x <= 7, x = 2y). -/// This set contains the points (2, 1), (4, 2), and (6, 3). -/// -/// The integer-valued variables are distinguished into 3 types of: -/// -/// Dimension: Ordinary variables over which the set is represented. -/// -/// Symbol: Symbol variables correspond to fixed but unknown values. -/// Mathematically, an integer polyhedron with symbolic variables is like a -/// family of integer polyhedra indexed by the symbolic variables. -/// -/// Local: Local variables correspond to existentially quantified variables. For -/// example, consider the set: (x) : (exists q : 1 <= x <= 7, x = 2q). An -/// assignment to symbolic and dimension variables is valid if there exists some -/// assignment to the local variable `q` satisfying these constraints. For this -/// example, the set is equivalent to {2, 4, 6}. Mathematically, existential -/// quantification can be thought of as the result of projection. In this -/// example, `q` is existentially quantified. This can be thought of as the -/// result of projecting out `q` from the previous example, i.e. we obtained {2, -/// 4, 6} by projecting out the second dimension from {(2, 1), (4, 2), (6, 2)}. -class IntegerPolyhedron : public PresburgerLocalSpace { +/// Since IntegerPolyhedron does not make a distinction between dimensions, +/// IdKind::SetDim should be used to refer to dimension identifiers. +class IntegerPolyhedron : public IntegerRelation { public: /// All derived classes of IntegerPolyhedron. enum class Kind { @@ -66,12 +45,8 @@ IntegerPolyhedron(unsigned numReservedInequalities, unsigned numReservedEqualities, unsigned numReservedCols, unsigned numDims, unsigned numSymbols, unsigned numLocals) - : PresburgerLocalSpace(numDims, numSymbols, numLocals), - equalities(0, getNumIds() + 1, numReservedEqualities, numReservedCols), - inequalities(0, getNumIds() + 1, numReservedInequalities, - numReservedCols) { - assert(numReservedCols >= getNumIds() + 1); - } + : IntegerRelation(numReservedInequalities, numReservedEqualities, + numReservedCols, numDims, numSymbols, numLocals) {} /// Constructs a constraint system with the specified number of /// dimensions and symbols. @@ -508,12 +483,6 @@ // don't expect an identifier to have more than 32 lower/upper/equality // constraints. This is conservatively set low and can be raised if needed. constexpr static unsigned kExplosionFactor = 32; - - /// Coefficients of affine equalities (in == 0 form). - Matrix equalities; - - /// Coefficients of affine inequalities (in >= 0 form). - Matrix inequalities; }; } // namespace mlir diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h new file mode 100644 --- /dev/null +++ b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h @@ -0,0 +1,88 @@ +//===- IntegerRelation.h - MLIR IntegerRelation Class -----*- C++ -*---===// +// +// 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 integer relation. +// +//===----------------------------------------------------------------------===// + +#ifndef MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H +#define MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H + +#include "mlir/Analysis/Presburger/Fraction.h" +#include "mlir/Analysis/Presburger/Matrix.h" +#include "mlir/Analysis/Presburger/PresburgerSpace.h" +#include "mlir/Analysis/Presburger/Utils.h" +#include "mlir/Support/LogicalResult.h" + +namespace mlir { + +/// An IntegerRelation is a PresburgerLocalSpace constrainted by affine +/// constraints. Affine constraints can be inequalities or equalities in the +/// form: +/// +/// Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n >= 0 +/// Equality : c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n == 0 +/// +/// where c_0, c_1, ..., c_n are integers and n is the total number of +/// identifiers in the PresburgerSpace. +/// +/// Such a relation corresponds to the set of integer points lying in a convex +/// polyhedron. For example, consider the relation: +/// (x) -> (y) : (1 <= x <= 7, x = 2y). +/// This relation contains the points (2, 1), (4, 2), and (6, 3). +/// +/// Since IntegerRelation makes a distinction between dimensions, IdKind::Range +/// and IdKind::Domain should be used to refer to dimension identifiers. +class IntegerRelation : public PresburgerLocalSpace { +public: + /// Constructs a relation reserving memory for the specified number + /// of constraints and identifiers. + IntegerRelation(unsigned numReservedInequalities, + unsigned numReservedEqualities, unsigned numReservedCols, + unsigned numDomain, unsigned numRange, unsigned numSymbols, + unsigned numLocals) + : PresburgerLocalSpace(numDomain, numRange, numSymbols, numLocals), + equalities(0, getNumIds() + 1, numReservedEqualities, numReservedCols), + inequalities(0, getNumIds() + 1, numReservedInequalities, + numReservedCols) { + assert(numReservedCols >= getNumIds() + 1); + } + + /// Constructs a relation with the specified number of dimensions and symbols. + IntegerRelation(unsigned numDomain = 0, unsigned numRange = 0, + unsigned numSymbols = 0, unsigned numLocals = 0) + : IntegerRelation(/*numReservedInequalities=*/0, + /*numReservedEqualities=*/0, + /*numReservedCols=*/numDomain + numRange + numSymbols + + numLocals + 1, + numDomain, numRange, numSymbols, numLocals) {} + +protected: + /// Constructs a set reserving memory for the specified number + /// of constraints and identifiers. This constructor should not be used + /// directly to create a relation and should only be used to create Sets. + IntegerRelation(unsigned numReservedInequalities, + unsigned numReservedEqualities, unsigned numReservedCols, + unsigned numDims, unsigned numSymbols, unsigned numLocals) + : PresburgerLocalSpace(numDims, numSymbols, numLocals), + equalities(0, getNumIds() + 1, numReservedEqualities, numReservedCols), + inequalities(0, getNumIds() + 1, numReservedInequalities, + numReservedCols) { + assert(numReservedCols >= getNumIds() + 1); + } + + /// Coefficients of affine equalities (in == 0 form). + Matrix equalities; + + /// Coefficients of affine inequalities (in >= 0 form). + Matrix inequalities; +}; + +} // namespace mlir + +#endif // MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H diff --git a/mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h b/mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h --- a/mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h +++ b/mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h @@ -21,8 +21,8 @@ class PresburgerLocalSpace; -/// PresburgerSpace is a tuple of identifiers with information about what kind -/// they correspond to. The identifiers can be split into three types: +/// PresburgerSpace is the space of all possible solutions of integer valued +/// variables/identifiers. Each identifier has one of the three types: /// /// Dimension: Ordinary variables over which the space is represented. /// @@ -31,18 +31,35 @@ /// family of spaces indexed by the symbolic identifiers. /// /// Local: Local identifiers correspond to existentially quantified variables. +/// For example, consider the space: `(x, exists q)` where x is a dimension +/// identifier and q is a local identifier. Let us put the constraints: +/// `1 <= x <= 7, x = 2q` +/// on this space to get the set: +/// `(x) : (exists q : q <= x <= 7, x = 2q)`. +/// An assignment to symbolic and dimension variables is valid if there +/// exists some assignment to the local variable `q` satisfying these +/// constraints. For this example, the set is equivalent to {2, 4, 6}. +/// Mathematically, existential quantification can be thought of as the result +/// of projection. In this example, `q` is existentially quantified. This can be +/// thought of as the result of projecting out `q` from the previous example, +/// i.e. we obtained {2, 4, 6} by projecting out the second dimension from +/// {(2, 1), (4, 2), (6, 2)}. /// /// Dimension identifiers are further divided into Domain and Range identifiers /// to support building relations. /// /// Spaces with distinction between domain and range identifiers should use /// IdKind::Domain and IdKind::Range to refer to domain and range identifiers. +/// Identifiers for space are stored in the following order: +/// [Domain, Range, Symbols, Locals] /// /// Spaces with no distinction between domain and range identifiers should use -/// IdKind::SetDim to refer to dimension identifiers. +/// IdKind::SetDim to refer to dimension identifiers. Identifiers for space are +/// stored in the following order: +/// [SetDim, Symbol, Locals] /// -/// PresburgerSpace does not support identifiers of kind Local. See -/// PresburgerLocalSpace for an extension that supports Local ids. +/// PresburgerSpace does not allow identifiers of kind Local. See +/// PresburgerLocalSpace for an extension that does allow local identifiers. class PresburgerSpace { friend PresburgerLocalSpace;