[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 ↗

(On Diff #538380)

This method should be private.

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

101

Could you make a method for this called isPlainEmpty?

101

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.

113

No need for the space equality check.

118

The result here is not captured.

[gilsaia]

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

134 ↗

(On Diff #538380)

Do we still need this method now?

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

101

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

[Groverkss]

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

134 ↗

(On Diff #538380)

Probably not. You can remove it.

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

101

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

[gilsaia]

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

101

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

137–138

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

101–102

506–509

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/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 there is no disjunct, false otherwise.
+  bool isPlainEmpty() const;
+
+  /// Return true if the set is known to have one unconstrained disjunct, false
+  /// otherwise.
+  bool isPlainUniverse() 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/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 the set is empty or the other set is universe,
+  // directly return the set
+  if (isPlainEmpty() || set.isPlainUniverse())
+    return *this;
+
+  if (set.isPlainEmpty() || isPlainUniverse())
+    return set;
+
   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);
     }
   }
   return result;
 }
 
 void PresburgerRelation::inverse() {
   for (IntegerRelation &cs : disjuncts)
     cs.inverse();
 
   if (getNumDisjuncts())
     setSpace(getDisjunct(0).getSpaceWithoutLocals());
 }

 }
 
 /// 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 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
+/// conditions.
+bool PresburgerRelation::isPlainUniverse() 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 there is no disjunct, false otherwise.
+bool PresburgerRelation::isPlainEmpty() const { return getNumDisjuncts() == 0; }
+
 /// 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) {