[Mlircommits] [mlir] e119196  [MLIR][Presburger] Add support for IntegerRelation
llvmlistbot at llvm.org
llvmlistbot at llvm.org
Mon Feb 21 13:12:10 PST 2022
Author: Groverkss
Date: 20220222T02:41:06+05:30
New Revision: e1191965da38b5f9e8ce29becfef9e35c3730109
URL: https://github.com/llvm/llvmproject/commit/e1191965da38b5f9e8ce29becfef9e35c3730109
DIFF: https://github.com/llvm/llvmproject/commit/e1191965da38b5f9e8ce29becfef9e35c3730109.diff
LOG: [MLIR][Presburger] Add support for IntegerRelation
This patch adds a class to represent a relation in Presburger Library.
This patch only adds the skeleton class. Functionality from IntegerPolyhedron
will be moved to IntegerRelation in later patches to make it easier to review.
This patch is a part of a series of patches adding support for relations in
Presburger Library.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D120156
Added:
Modified:
mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h
Removed:
################################################################################
diff git a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
index 711a34950e75..834e3b0edce1 100644
 a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
+++ b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
@@ 21,37 +21,86 @@
namespace mlir {
/// An integer polyhedron is the set of solutions to a list of affine
/// constraints over n integervalued variables/identifiers. Affine constraints
/// can be inequalities or equalities in the form:
+/// An IntegerRelation is a PresburgerLocalSpace subject to affine constraints.
+/// Affine constraints can be inequalities or equalities in the form:
///
/// Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n1}*x_{n1} + c_n >= 0
/// Equality : c_0*x_0 + c_1*x_1 + .... + c_{n1}*x_{n1} + c_n == 0
///
/// where c_0, c_1, ..., c_n are integers.
+/// where c_0, c_1, ..., c_n are integers and n is the total number of
+/// identifiers in the space.
///
/// 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).
+/// 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)
+/// These can be thought of as points in the polyhedron:
+/// (x, y) : (1 <= x <= 7, x = 2y)
+/// This relation contains the pairs (2, 1), (4, 2), and (6, 3).
///
/// The integervalued variables are distinguished into 3 types of:
+/// 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;
+};
+
+/// An IntegerPolyhedron is a PresburgerLocalSpace subject to affine
+/// constraints. Affine constraints can be inequalities or equalities in the
+/// form:
+///
+/// Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n1}*x_{n1} + c_n >= 0
+/// Equality : c_0*x_0 + c_1*x_1 + .... + c_{n1}*x_{n1} + c_n == 0
///
/// Dimension: Ordinary variables over which the set is represented.
+/// where c_0, c_1, ..., c_n are integers and n is the total number of
+/// identifiers in the space.
///
/// 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.
+/// An IntegerPolyhedron is similar to a IntegerRelation but it does not make a
+/// distinction between Domain and Range identifiers. Internally,
+/// IntegerPolyhedron is implemented as a IntegerRelation with zero domain ids.
///
/// 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 +115,8 @@ class IntegerPolyhedron : public PresburgerLocalSpace {
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.
@@ 516,12 +561,6 @@ class IntegerPolyhedron : public PresburgerLocalSpace {
// 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/PresburgerSpace.h b/mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h
index a7a93980d4ae..bff48f6a5662 100644
 a/mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h
+++ b/mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h
@@ 21,8 +21,8 @@ namespace mlir {
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 values of a tuple 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 @@ class PresburgerLocalSpace;
/// 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 such spaces 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 such
+/// spaces 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;
More information about the Mlircommits
mailing list