[Mlir-commits] [mlir] [mlir] [presburger] Add IntegerRelation::rangeProduct (PR #148092)

[Arjun P]

================
@@ -707,6 +707,21 @@ class IntegerRelation {
   /// this for uniformity with `applyDomain`.
   void applyRange(const IntegerRelation &rel);
 
+  /// Let the relation `this` be R1, and the relation `rel` be R2. Requires
+  /// R1 and R2 to have the same domain.
+  ///
+  /// This operation computes the relation whose domain is the same as R1 and
+  /// whose range is the product of the ranges of R1 and R2, and whose
+  /// constraints are the conjunction of the constraints of R1 and R2 applied
+  /// to the relevant subspaces of the range.
+  ///
+  /// Example:
----------------
Superty wrote:

although the example below gets most of the way there, I would like to have this formal description: let R3 be the rangeProduct of R1 and R2. then x R3 (y, z) iff (x R1 y and x R2 z)

https://github.com/llvm/llvm-project/pull/148092