[Mlir-commits] [mlir] ec10ff3 - [MLIR][Presburger] Support isSubsetOf in PresburgerSet and IntegerPolyhedron

[Arjun P]

Author: Arjun P
Date: 2022-02-02T18:44:14+05:30
New Revision: ec10ff37e2c3a2294e6bf795d1692a13c168bb2b

URL: https://github.com/llvm/llvm-project/commit/ec10ff37e2c3a2294e6bf795d1692a13c168bb2b
DIFF: https://github.com/llvm/llvm-project/commit/ec10ff37e2c3a2294e6bf795d1692a13c168bb2b.diff

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

Also support isEqual in IntegerPolyhedron.

Reviewed By: Groverkss

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

Added: 
    

Modified: 
    mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
    mlir/include/mlir/Analysis/Presburger/PresburgerSet.h
    mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp
    mlir/lib/Analysis/Presburger/PresburgerSet.cpp

Removed: 
    


################################################################################
diff  --git a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
index 0747c553ee35..8156b7b71f3a 100644
--- a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
+++ b/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); }

diff  --git a/mlir/include/mlir/Analysis/Presburger/PresburgerSet.h b/mlir/include/mlir/Analysis/Presburger/PresburgerSet.h
index e6be93902759..a8037d63ead8 100644
--- a/mlir/include/mlir/Analysis/Presburger/PresburgerSet.h
+++ b/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;

diff  --git a/mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp b/mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp
index a7172ed8e284..578f85472970 100644
--- a/mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp
+++ b/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!");

diff  --git a/mlir/lib/Analysis/Presburger/PresburgerSet.cpp b/mlir/lib/Analysis/Presburger/PresburgerSet.cpp
index 49c04381e1c2..02bc7a30192b 100644
--- a/mlir/lib/Analysis/Presburger/PresburgerSet.cpp
+++ b/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,