[MLIR][Presburger] remove redundant constraints in coalesce

[webmiche]

Summary

This patch improves the representation size of individual
IntegerRelations by calling the function
IntegerRelation::removeRedundantConstraints. While this is only a
slight optimization in the current version, it will be necessary for
patches to come.

[arjunp]

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

492–498

Will there be an issue if disjuncts[i] loses some constraints and these are not present in simp? Should simp be constructed after removing redundant constraints here?

[webmiche]

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

492–498

AFAIK, the simp won't be updated when disjuncts[i] changes, so you are right, redundant constraints should be removed first, then the simplex should be constructed.

[webmiche]

remove redundant constraints before constructing the simplex

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

private:
   SmallVector<ArrayRef<int64_t>, 2> redundantIneqsB;
   SmallVector<ArrayRef<int64_t>, 2> cuttingIneqsB;
 
   /// Given a Simplex `simp` and one of its inequalities `ineq`, check
   /// that the facet of `simp` where `ineq` holds as an equality is contained
   /// within `a`.
   bool isFacetContained(ArrayRef<int64_t> ineq, Simplex &simp);
 
-  /// Adds `disjunct` to `disjuncts` and removes the disjuncts at position `i`
-  /// and `j`. Updates `simplices` to reflect the changes. `i` and `j` cannot
-  /// be equal.
+  /// Removes redundant constraints from `disjunct`, adds it to `disjuncts` and
+  /// removes the disjuncts at position `i` and `j`. Updates `simplices` to
+  /// reflect the changes. `i` and `j` cannot be equal.
   void addCoalescedDisjunct(unsigned i, unsigned j,
                             const IntegerRelation &disjunct);
 
   /// Checks whether `a` and `b` can be combined in a convex sense, if there
   /// exist cutting inequalities.
   ///
   /// An example of this case:
   ///    ___________        ___________

 /// `IntegerRelation`s to the `disjuncts` vector.
 SetCoalescer::SetCoalescer(const PresburgerRelation &s) {
 
   disjuncts = s.integerRelations;
 
   simplices.reserve(s.getNumDisjuncts());
   // Note that disjuncts.size() changes during the loop.
   for (unsigned i = 0; i < disjuncts.size();) {
+    disjuncts[i].removeRedundantConstraints();
     Simplex simp(disjuncts[i]);
     if (simp.isEmpty()) {
       disjuncts[i] = disjuncts[disjuncts.size() - 1];
       disjuncts.pop_back();
       continue;
     }
     ++i;
     simplices.push_back(simp);
   }
   numDomainIds = s.getNumDomainIds();
   numRangeIds = s.getNumRangeIds();
   numSymbolIds = s.getNumSymbolIds();
 }
 
 /// Simplifies the representation of a PresburgerSet.
void SetCoalescer::addCoalescedDisjunct(unsigned i, unsigned j,
   unsigned n = disjuncts.size();
   if (j == n - 1) {
     // This case needs special handling since position `n` - 1 is removed
     // from the vector, hence the `IntegerRelation` at position `n` - 2 is
     // lost otherwise.
     disjuncts[i] = disjuncts[n - 2];
     disjuncts.pop_back();
     disjuncts[n - 2] = disjunct;
+    disjuncts[n - 2].removeRedundantConstraints();
 
     simplices[i] = simplices[n - 2];
     simplices.pop_back();
-    simplices[n - 2] = Simplex(disjunct);
+    simplices[n - 2] = Simplex(disjuncts[n - 2]);
 
   } else {
     // Other possible edge cases are correct since for `j` or `i` == `n` -
     // 2, the `IntegerRelation` at position `n` - 2 should be lost. The
     // case `i` == `n` - 1 makes the first following statement a noop.
     // Hence, in this case the same thing is done as above, but with `j`
     // rather than `i`.
     disjuncts[i] = disjuncts[n - 1];
     disjuncts[j] = disjuncts[n - 2];
     disjuncts.pop_back();
     disjuncts[n - 2] = disjunct;
+    disjuncts[n - 2].removeRedundantConstraints();
 
     simplices[i] = simplices[n - 1];
     simplices[j] = simplices[n - 2];
     simplices.pop_back();
-    simplices[n - 2] = Simplex(disjunct);
+    simplices[n - 2] = Simplex(disjuncts[n - 2]);
   }
 }
 
 /// Given two polyhedra `a` and `b` at positions `i` and `j` in
 /// `disjuncts` and `redundantIneqsA` being the inequalities of `a` that
 /// are redundant for `b` (similarly for `cuttingIneqsA`, `redundantIneqsB`,
 /// and `cuttingIneqsB`), Checks whether the facets of all cutting
 /// inequalites of `a` are contained in `b`. If so, a new polyhedron