diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h --- a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h +++ b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h @@ -115,6 +115,16 @@ /// 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 --- a/mlir/include/mlir/Analysis/Presburger/PresburgerSet.h +++ b/mlir/include/mlir/Analysis/Presburger/PresburgerSet.h @@ -77,6 +77,9 @@ /// 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 --- 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 @@ } } +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> 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 --- a/mlir/lib/Analysis/Presburger/PresburgerSet.cpp +++ b/mlir/lib/Analysis/Presburger/PresburgerSet.cpp @@ -352,17 +352,17 @@ 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,