[MLIR][Presburger] Optimize for intersect

[gilsaia]

Summary

Added a series of optimizations to the Intersect function of PresburgerRelation, referring to the ISL implementation.
Tested it on a simple Benchmark implemented by myself to see that it can speed up the Intersect operation

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

The overall results for Intersect are as follows

The results for each case are as follows

[Groverkss]

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

134

This method should be private.

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

100

Could you make a method for this called isPlainEmpty?

100

Could you write a comment here that describes what this early exit does? Also, I don't think you need to do a space check here. The space check was done by space.isCompatible in the assert earlier.

112

No need for the space equality check.

117

The result here is not captured.

[gilsaia]

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

134

Do we still need this method now?

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

100

But I think isEqual also check NumLocalVar,which isCompatible not check

[Groverkss]

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

134

Probably not. You can remove it.

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

100

The space of a PresburgerSet never has locals :), so it does not matter.

[gilsaia]

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

100

Allright，i'll remove this check

[gilsaia]

Remove wrong optim, add comment, remove useless check space

[gilsaia]

fix patch wrong

[Groverkss]

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

116–117

Can you rename this to "isPlainUniverse" as well? Since this is just a quick check, not a complete check.

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

100–101

477–480

I don't think this is a complete check for the universe. You should mention that this is just a quick check.

[gilsaia]

[fix] change func name

[gilsaia]

[fix] change comment

[Groverkss]

LGTM. Nice!

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

public:
   /// Appends constraints from `other` into `this`. This is equivalent to an
   /// intersection with no simplification of any sort attempted.
   void append(const IntegerRelation &other);
 
   /// Return the intersection of the two relations.
   /// If there are locals, they will be merged.
   IntegerRelation intersect(IntegerRelation other) const;
 
+  /// Return the intersection of the two relations by directly adding the
+  /// current relation's constraint to the other relation. This specialized
+  /// version does not perform additional checks or modifications.
+  IntegerRelation intersectAddConstraint(IntegerRelation other) const;
+
   /// Return whether `this` and `other` are equal. This is integer-exact
   /// and somewhat expensive, since it uses the integer emptiness check
   /// (see IntegerRelation::findIntegerSample()).
   bool isEqual(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

public:
   /// Return true if this set is equal to the given set, and false otherwise.
   /// All local variables in both sets must correspond to floor divisions.
   bool isEqual(const PresburgerRelation &set) const;
 
   /// Return true if all the sets in the union are known to be integer empty
   /// false otherwise.
   bool isIntegerEmpty() const;
 
+  /// Return true if the set is known to be the universe set, false otherwise.
+  bool isUniverse() const;
+
+  /// Return true if the set is consist of a single disjunct, without any local
+  /// variables, false otherwise.
+  bool isConvexNoLocals() const;
+
   /// Find an integer sample from the given set. This should not be called if
   /// any of the disjuncts in the union are unbounded.
   bool findIntegerSample(SmallVectorImpl<MPInt> &sample);
 
   /// Compute an overapproximation of the number of integer points in the
   /// disjunct. Symbol vars are currently not supported. If the computed
   /// overapproximation is infinite, an empty optional is returned.
   ///

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

 
 IntegerRelation IntegerRelation::intersect(IntegerRelation other) const {
   IntegerRelation result = *this;
   result.mergeLocalVars(other);
   result.append(other);
   return result;
 }
 
+IntegerRelation
+IntegerRelation::intersectAddConstraint(IntegerRelation other) const {
+  IntegerRelation result = *this;
+  result.append(other);
+  return result;
+}
+
 bool IntegerRelation::isEqual(const IntegerRelation &other) const {
   assert(space.isCompatible(other.getSpace()) && "Spaces must be compatible.");
   return PresburgerRelation(*this).isEqual(PresburgerRelation(other));
 }
 
 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

 // as (S_1 and T_1) or (S_1 and T_2) or ...
 //
 // If S_i or T_j have local variables, then S_i and T_j contains the local
 // variables of both.
 PresburgerRelation
 PresburgerRelation::intersect(const PresburgerRelation &set) const {
   assert(space.isCompatible(set.getSpace()) && "Spaces should match");
 
+  if ((getNumDisjuncts() == 0 || set.isUniverse()) &&
+      space.isEqual(set.getSpace()))
+    return *this;
+
+  if ((set.getNumDisjuncts() == 0 || isUniverse()) &&
+      space.isEqual(set.getSpace()))
+    return set;
+
+  // Special case, where both relation are convex, without any divs and such
+  // that either one of it contains a single constraint. Simply add constraint
+  // to the other relation.
+  if (isConvexNoLocals() && set.isConvexNoLocals() &&
+      space.isEqual(set.getSpace()) &&
+      (getDisjunct(0).getNumConstraints() == 1 ||
+       set.getDisjunct(0).getNumConstraints() == 1)) {
+    PresburgerRelation result(getSpace());
+    result.unionInPlace(getDisjunct(0));
+    result.getDisjunct(0).intersectAddConstraint(set.getDisjunct(0));
+    return result;
+  }
+
   PresburgerRelation result(getSpace());
   for (const IntegerRelation &csA : disjuncts) {
     for (const IntegerRelation &csB : set.disjuncts) {
       IntegerRelation intersection = csA.intersect(csB);
       if (!intersection.isEmpty())
         result.unionInPlace(intersection);
     }
   }

 }
 
 /// Two sets are equal iff they are subsets of each other.
 bool PresburgerRelation::isEqual(const PresburgerRelation &set) const {
   assert(space.isCompatible(set.getSpace()) && "Spaces should match");
   return this->isSubsetOf(set) && set.isSubsetOf(*this);
 }
 
+/// Return true if the Presburger relation is known to represent the universe
+/// set, false otherwise. A Presburger relation is considered to be the universe
+/// set if it contains at least one disjunct that is unconstrained, i.e., it
+/// does not have any constraints or conditions.
+bool PresburgerRelation::isUniverse() const {
+  for (auto &disjunct : getAllDisjuncts()) {
+    if (disjunct.getNumConstraints() == 0)
+      return true;
+  }
+  return false;
+}
+
+bool PresburgerRelation::isConvexNoLocals() const {
+  if (getNumDisjuncts() == 1 && getSpace().getNumLocalVars() == 0)
+    return true;
+  return false;
+}
+
 /// Return true if all the sets in the union are known to be integer empty,
 /// false otherwise.
 bool PresburgerRelation::isIntegerEmpty() const {
   // The set is empty iff all of the disjuncts are empty.
   return llvm::all_of(disjuncts, std::mem_fn(&IntegerRelation::isIntegerEmpty));
 }
 
 bool PresburgerRelation::findIntegerSample(SmallVectorImpl<MPInt> &sample) {