[Mlir-commits] [mlir] [mlir][affine][Analysis] Add conservative bounds for semi-affine mods (PR #93576)

[Benjamin Maxwell]

================
@@ -454,6 +454,20 @@ class IntegerRelation {
     addLocalFloorDiv(getMPIntVec(dividend), MPInt(divisor));
   }
 
+  /// Adds a new local variable as the mod of an affine function of other
+  /// variables. The coefficients of the operands of the mod are provided in
+  /// `lhs` and `rhs` respectively. Three constraints are added to provide a
+  /// conservative bound for the mod:
+  ///  1. rhs > 0 (assumption/precondition)
+  ///  2. lhs % rhs < rhs
+  ///  3. lhs % rhs >= 0
+  /// We ensure the rhs is positive so we can assume the result is positive.
+  void addLocalModConservativeBounds(ArrayRef<MPInt> lhs, ArrayRef<MPInt> rhs);
+  void addLocalModConservativeBounds(ArrayRef<int64_t> lhs,
+                                     ArrayRef<int64_t> rhs) {
+    addLocalModConservativeBounds(getMPIntVec(lhs), getMPIntVec(rhs));
+  }
+
----------------
MacDue wrote:

I've moved the logic here to the new `SemiAffineExprFlattener` (which lives in `FlatLinearValueConstraints`). I'm still passing a flag within `FlatLinearValueConstraints` to enable the semi-affine bounds rather than an entirely new method, as otherwise there's a fair bit of duplication in `flattenAlignedMapAndMergeLocals` down (since that would mostly be identical for the two methods).

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