[MLIR][Presburger] Optimize for union & subtract

Added a series of optimization to the Subtract & Union function of PresburgerRelation, referring to the ISL implementation.
Add isPlainEqual to Subtract & union,also some basic check to union.
Tested it on a simple Benchmark implemented by myself to see that it can speed up the Subtract operation and Union operation, also decrease the result size.

The Benchmark can be found here: [[ https://github.com/gilsaia/llvm-project-test-fpl/blob/develop_benchmark/mlir/benchmark/presburger/Benchmark.cpp | benchmark]]

The overall results for Union & Subtract are as follows (previous benchmark has a bug,after fix that,the figure below is new)
{F28455229}

The results for each case are as follows
{F28455234}
{F28455239}

{F28455245}
{F28455246}

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D156241

Author: gilsaia

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

@@ -133,6 +133,13 @@ class IntegerRelation {
   /// (see IntegerRelation::findIntegerSample()).
   bool isEqual(const IntegerRelation &other) const;
 
+  /// Perform a quick equality check on `this` and `other`. The relations are
+  /// equal if the check return true, but may or may not be equal if the check
+  /// returns false. The equality check is performed in a plain manner, by
+  /// comparing if all the equalities and inequalities in `this` and `other`
+  /// are the same.
+  bool isPlainEqual(const IntegerRelation &other) const;
+
   /// Return whether this is a subset of the given IntegerRelation. This is
   /// integer-exact and somewhat expensive, since it uses the integer emptiness
   /// check (see IntegerRelation::findIntegerSample()).

mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h

@@ -152,6 +152,12 @@ class PresburgerRelation {
   /// otherwise.
   bool isPlainUniverse() const;
 
+  /// Perform a quick equality check on `this` and `other`. The relations are
+  /// equal if the check return true, but may or may not be equal if the check
+  /// returns false. This is doing by directly comparing whether each internal
+  /// disjunct is the same.
+  bool isPlainEqual(const PresburgerRelation &set) const;
+
   /// Return true if the set is consist of a single disjunct, without any local
   /// variables, false otherwise.
   bool isConvexNoLocals() const;

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

@@ -80,6 +80,30 @@ bool IntegerRelation::isEqual(const IntegerRelation &other) const {
   return PresburgerRelation(*this).isEqual(PresburgerRelation(other));
 }
 
+bool IntegerRelation::isPlainEqual(const IntegerRelation &other) const {
+  if (!space.isEqual(other.getSpace()))
+    return false;
+  if (getNumEqualities() != other.getNumEqualities())
+    return false;
+  if (getNumInequalities() != other.getNumInequalities())
+    return false;
+
+  unsigned cols = getNumCols();
+  for (unsigned i = 0, eqs = getNumEqualities(); i < eqs; ++i) {
+    for (unsigned j = 0; j < cols; ++j) {
+      if (atEq(i, j) != other.atEq(i, j))
+        return false;
+    }
+  }
+  for (unsigned i = 0, ineqs = getNumInequalities(); i < ineqs; ++i) {
+    for (unsigned j = 0; j < cols; ++j) {
+      if (atIneq(i, j) != other.atIneq(i, j))
+        return false;
+    }
+  }
+  return true;
+}
+
 bool IntegerRelation::isSubsetOf(const IntegerRelation &other) const {
   assert(space.isCompatible(other.getSpace()) && "Spaces must be compatible.");
   return PresburgerRelation(*this).isSubsetOf(PresburgerRelation(other));

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

@@ -63,6 +63,24 @@ void PresburgerRelation::unionInPlace(const IntegerRelation &disjunct) {
 /// to this set.
 void PresburgerRelation::unionInPlace(const PresburgerRelation &set) {
   assert(space.isCompatible(set.getSpace()) && "Spaces should match");
+
+  if (isPlainEqual(set))
+    return;
+
+  if (isPlainEmpty()) {
+    disjuncts = set.disjuncts;
+    return;
+  }
+  if (set.isPlainEmpty())
+    return;
+
+  if (isPlainUniverse())
+    return;
+  if (set.isPlainUniverse()) {
+    disjuncts = set.disjuncts;
+    return;
+  }
+
   for (const IntegerRelation &disjunct : set.disjuncts)
     unionInPlace(disjunct);
 }
@@ -511,6 +529,12 @@ PresburgerRelation
 PresburgerRelation::subtract(const PresburgerRelation &set) const {
   assert(space.isCompatible(set.getSpace()) && "Spaces should match");
   PresburgerRelation result(getSpace());
+
+  // If we know that the two sets are clearly equal, we can simply return the
+  // empty set.
+  if (isPlainEqual(set))
+    return result;
+
   // We compute (U_i t_i) \ (U_i set_i) as U_i (t_i \ V_i set_i).
   for (const IntegerRelation &disjunct : disjuncts)
     result.unionInPlace(getSetDifference(disjunct, set));
@@ -530,6 +554,22 @@ bool PresburgerRelation::isEqual(const PresburgerRelation &set) const {
   return this->isSubsetOf(set) && set.isSubsetOf(*this);
 }
 
+bool PresburgerRelation::isPlainEqual(const PresburgerRelation &set) const {
+  if (!space.isCompatible(set.getSpace()))
+    return false;
+
+  if (getNumDisjuncts() != set.getNumDisjuncts())
+    return false;
+
+  // Compare each disjunct in this PresburgerRelation with the corresponding
+  // disjunct in the other PresburgerRelation.
+  for (unsigned int i = 0, n = getNumDisjuncts(); i < n; ++i) {
+    if (!getDisjunct(i).isPlainEqual(set.getDisjunct(i)))
+      return false;
+  }
+  return true;
+}
+
 /// Return true if the Presburger relation represents the universe set, false
 /// otherwise. It is a simple check that only check if the relation has at least
 /// one unconstrained disjunct, indicating the absence of constraints or