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

[arjunp]

Summary

Also support isEqual in IntegerPolyhedron.

[Groverkss]

LGTM. Some minor comments.

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

123–125

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

365

I think after this change, you can just write S is equal to T iff S \subset T and T \subset S.

[arjunp]

Address kunwar's comments

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

public:
 
   void reset(unsigned numDims = 0, unsigned numSymbols = 0,
              unsigned numLocals = 0);
 
   /// Appends constraints from `other` into `this`. This is equivalent to an
   /// intersection with no simplification of any sort attempted.
   void append(const IntegerPolyhedron &other);
 
+  /// Return whether the two IntegerPolyhedrons 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 IntegerPolyhedrons. 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); }
 
   /// Returns the value at the specified inequality row and column.
   inline int64_t atIneq(unsigned i, unsigned j) const {
     return inequalities(i, j);
   }

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

public:
   PresburgerSet complement() const;
 
   /// Return the set difference of this set and the given set, i.e.,
   /// return `this \ set`. All local variables in `set` must correspond
   /// to floor divisions, but local variables in `this` need not correspond to
   /// 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;
 
   /// Return a universe set of the specified type that contains all points.
   static PresburgerSet getUniverse(unsigned numDims = 0,
                                    unsigned numSymbols = 0);
   /// Return an empty set of the specified type that contains no points.

mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp

 //===- IntegerPolyhedron.cpp - MLIR IntegerPolyhedron Class ---------------===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
 // A class to represent an integer polyhedron.
 //
 //===----------------------------------------------------------------------===//
 
 #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"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/Support/Debug.h"
 
 #define DEBUG_TYPE "presburger"
 
void IntegerPolyhedron::append(const IntegerPolyhedron &other) {
   for (unsigned r = 0, e = other.getNumInequalities(); r < e; r++) {
     addInequality(other.getInequality(r));
   }
   for (unsigned r = 0, e = other.getNumEqualities(); r < e; r++) {
     addEquality(other.getEquality(r));
   }
 }
 
+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!");
   Optional<SmallVector<Fraction, 8>> maybeLexMin =
       LexSimplex(*this).getRationalLexMin();
 
   if (!maybeLexMin)
     return {};

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

PresburgerSet PresburgerSet::subtract(const PresburgerSet &set) const {
   assertDimensionsCompatible(set, *this);
   PresburgerSet result(getNumDimIds(), getNumSymbolIds());
   // We compute (U_i t_i) \ (U_i set_i) as U_i (t_i \ V_i set_i).
   for (const IntegerPolyhedron &poly : integerPolyhedrons)
     result.unionSetInPlace(getSetDifference(poly, set));
   return result;
 }
 
+/// 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 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.
 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,
 /// false otherwise.
 bool PresburgerSet::isIntegerEmpty() const {
   // The set is empty iff all of the disjuncts are empty.
   return std::all_of(
       integerPolyhedrons.begin(), integerPolyhedrons.end(),