[MLIR][Presburger] Support isSubsetOf in PresburgerSet and IntegerPolyhedron

Also support isEqual in IntegerPolyhedron.

Reviewed By: Groverkss

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

Author: Superty

mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h

@@ -115,6 +115,16 @@ class IntegerPolyhedron {
   /// intersection with no simplification of any sort attempted.
   void append(const IntegerPolyhedron &other);
 
+  /// Return whether `this` and `other` are equal. This is integer-exact
+  /// and somewhat expensive, since it uses the integer emptiness check
+  /// (see IntegerPolyhedron::findIntegerSample()).
+  bool isEqual(const IntegerPolyhedron &other) const;
+
+  /// Return whether this is a subset of the given IntegerPolyhedron. This is
+  /// integer-exact and somewhat expensive, since it uses the integer emptiness
+  /// check (see IntegerPolyhedron::findIntegerSample()).
+  bool isSubsetOf(const IntegerPolyhedron &other) const;
+
   /// Returns the value at the specified equality row and column.
   inline int64_t atEq(unsigned i, unsigned j) const { return equalities(i, j); }
   inline int64_t &atEq(unsigned i, unsigned j) { return equalities(i, j); }

mlir/include/mlir/Analysis/Presburger/PresburgerSet.h

@@ -77,6 +77,9 @@ class PresburgerSet {
   /// divisions.
   PresburgerSet subtract(const PresburgerSet &set) const;
 
+  /// Return true if this set is a subset of the given set, and false otherwise.
+  bool isSubsetOf(const PresburgerSet &set) const;
+
   /// 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 PresburgerSet &set) const;

mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp

@@ -12,6 +12,7 @@
 
 #include "mlir/Analysis/Presburger/IntegerPolyhedron.h"
 #include "mlir/Analysis/Presburger/LinearTransform.h"
+#include "mlir/Analysis/Presburger/PresburgerSet.h"
 #include "mlir/Analysis/Presburger/Simplex.h"
 #include "mlir/Analysis/Presburger/Utils.h"
 #include "llvm/ADT/DenseMap.h"
@@ -63,6 +64,14 @@ void IntegerPolyhedron::append(const IntegerPolyhedron &other) {
   }
 }
 
+bool IntegerPolyhedron::isEqual(const IntegerPolyhedron &other) const {
+  return PresburgerSet(*this).isEqual(PresburgerSet(other));
+}
+
+bool IntegerPolyhedron::isSubsetOf(const IntegerPolyhedron &other) const {
+  return PresburgerSet(*this).isSubsetOf(PresburgerSet(other));
+}
+
 Optional<SmallVector<Fraction, 8>>
 IntegerPolyhedron::getRationalLexMin() const {
   assert(numSymbols == 0 && "Symbols are not supported!");

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

@@ -352,17 +352,17 @@ PresburgerSet PresburgerSet::subtract(const PresburgerSet &set) const {
   return result;
 }
 
-/// Two sets S and T are equal iff S contains T and T contains S.
-/// By "S contains T", we mean that S is a superset of or equal to T.
-///
-/// S contains T iff T \ S is empty, since if T \ S contains a
-/// point then this is a point that is contained in T but not S.
-///
-/// Therefore, S is equal to T iff S \ T and T \ S are both empty.
+/// T is a subset of S iff T \ S is empty, since if T \ S contains a
+/// point then this is a point that is contained in T but not S, and
+/// if T contains a point that is not in S, this also lies in T \ S.
+bool PresburgerSet::isSubsetOf(const PresburgerSet &set) const {
+  return this->subtract(set).isIntegerEmpty();
+}
+
+/// Two sets are equal iff they are subsets of each other.
 bool PresburgerSet::isEqual(const PresburgerSet &set) const {
   assertDimensionsCompatible(set, *this);
-  return this->subtract(set).isIntegerEmpty() &&
-         set.subtract(*this).isIntegerEmpty();
+  return this->isSubsetOf(set) && set.isSubsetOf(*this);
 }
 
 /// Return true if all the sets in the union are known to be integer empty,