[MLIR][Presburger] Add support for IntegerRelation

[Groverkss]

Summary

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.

[arjunp]

mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h

24–25

I prefer to keep the original first sentence

30

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

24 ↗

(On Diff #410001)

37 ↗

(On Diff #410001)

I would add that these can be thought of as points in the polyhedron (x, y) : (1 <= x <= 7, x = 2y).

It's not really a polyhedron per se when it's actually a relation I guess though you can view it as one.

mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h

24–25

Not sure if they are solutions when there are no constraints really. Maybe call them space of all possible values of a tuple of integral variables/identifiers

53

57–59

[grosser]

mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h

29

Doman -> Domain

[Groverkss]

• Address comments

[arjunp]

IMO, IntegerRelation and IntegerPolyhedron are so interrelated that you can keep them in the same file.

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

36 ↗

(On Diff #410078)

[Groverkss]

• Address comments

[arjunp]

LGTM, please fix the minor comment below.

mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h

36–38

mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.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 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 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_{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.
+/// 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).
-///
-/// 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 {
+/// 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).
+///
+/// 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_{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 space.
+///
+/// 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.
+///
+/// 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 {
     FlatAffineConstraints,
     FlatAffineValueConstraints,
     MultiAffineFunction,
     IntegerPolyhedron
   };
 
   /// Constructs a constraint system reserving memory for the specified number
   /// of constraints and identifiers.
   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.
   IntegerPolyhedron(unsigned numDims = 0, unsigned numSymbols = 0,
                     unsigned numLocals = 0)
       : IntegerPolyhedron(/*numReservedInequalities=*/0,
                           /*numReservedEqualities=*/0,
                           /*numReservedCols=*/numDims + numSymbols + numLocals +
protected:
   /// case of IntegerPolyhedron.
   // The rationale for 32 is that in the typical simplest of cases, an
   // identifier is expected to have one lower bound and one upper bound
   // constraint. With a level of tiling or a connection to another identifier
   // through a div or mod, an extra pair of bounds gets added. As a limit, we
   // 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
 
 #endif // MLIR_ANALYSIS_PRESBURGER_INTEGERPOLYHEDRON_H

mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h

 
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/raw_ostream.h"
 
 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.
 ///
 /// Symbol: Symbol identifiers correspond to fixed but unknown values.
 /// Mathematically, a space with symbolic identifiers is like a
 /// 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;
 
 public:
   /// Kind of identifier. Implementation wise SetDims are treated as Range
   /// ids, and spaces with no distinction between dimension ids are treated
   /// as relations with zero domain ids.
   enum IdKind { Symbol, Local, Domain, Range, SetDim = Range };