[MLIR][Presburger] subtract: improve redundant constraint detection

[arjunp]

Summary

When constraints in the two operands make each other redundant, prefer constraints of the second because this affects the number of sets in the output at each level; reducing these can help prevent exponential blowup.

This is accomplished by adding extra overloads to Simplex::detectRedundant that only scan a subrange of the constraints for redundancy.

[Groverkss]

LGTM with a minor comment

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

298–306

I feel this comment can explain the code better. Currently, it explains why we do detectRedundant(offset, count) instead of detectRedundant(). I think only the first paragraph is fine.

[arjunp]

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

298–306

I didn't understand the first sentence. What do you mean by "can explain the code better"?

I think just the first paragraph is not sufficient to explain why we are specifically calling detectrRedundant (offset, count)?

[arjunp]

clang-format

[Groverkss]

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

298–306

I just meant it's already clear that you are checking if the inequalities from the range offset, offset + totalNewInequalities are redundant from the first comment.

For the second paragraph, if you could write "The reason we use detectRedundant(offset, count) instead of detectRedundant() ..."

[arjunp]

Address Kunwar's comment

[Groverkss]

LGTM.

mlir/include/mlir/Analysis/Presburger/Simplex.h

public:
   /// Equalities are added as a pair of inequalities and so correspond to two
   /// inequalities with successive indices.
   bool isMarkedRedundant(unsigned constraintIndex) const;
 
   /// Finds a subset of constraints that is redundant, i.e., such that
   /// the set of solutions does not change if these constraints are removed.
   /// Marks these constraints as redundant. Whether a specific constraint has
   /// been marked redundant can be queried using isMarkedRedundant.
-  void detectRedundant();
+  ///
+  /// The first overload only tries to find redundant constraints with indices
+  /// in the range [offset, offset + count), by scanning constraints from left
+  /// to right in this range. If `count` is not provided, all constraints
+  /// starting at `offset` are scanned, and if neither are provided, all
+  /// constraints are scanned, starting from 0 and going to the last constraint.
+  ///
+  /// As an example, in the set (x) : (x >= 0, x >= 0, x >= 0), calling
+  /// `detectRedundant` with no parameters will result in the first two
+  /// constraints being marked redundant. All copies cannot be marked redundant
+  /// because removing all the constraints changes the set. The first two are
+  /// the ones marked redundant because we scan from left to right. Thus, when
+  /// there is some preference among the constraints as to which should be
+  /// marked redundant with priority when there are multiple possibilities, this
+  /// could be accomplished by succesive calls to detectRedundant(offset,
+  /// count).
+  void detectRedundant(unsigned offset, unsigned count);
+  void detectRedundant(unsigned offset) {
+    assert(offset <= con.size() && "invalid offset!");
+    detectRedundant(offset, con.size() - offset);
+  }
+  void detectRedundant() { detectRedundant(0, con.size()); }
 
   /// Returns a (min, max) pair denoting the minimum and maximum integer values
   /// of the given expression. If no integer value exists, both results will be
   /// of kind Empty.
   std::pair<MaybeOptimum<int64_t>, MaybeOptimum<int64_t>>
   computeIntegerBounds(ArrayRef<int64_t> coeffs);
 
   /// Returns true if the polytope is unbounded, i.e., extends to infinity in

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

if (level > frames.size()) {
         // relevant for performance.
         frames.push_back(Frame{initialSnapshot, initBCounts, sI,
                                /*ineqsToProcess=*/{},
                                /*lastIneqProcessed=*/{}});
         ++level;
         continue;
       }
 
-      simplex.detectRedundant();
 
       // Equalities are added to simplex as a pair of inequalities.
       unsigned totalNewSimplexInequalities =
           2 * sI.getNumEqualities() + sI.getNumInequalities();
+      // Look for redundant constraints among the constraints of sI. We don't
+      // care about redundant constraints in `b` at this point.
+      //
+      // When there are two copies of a constraint in `simplex`, i.e., among the
+      // constraints of `b` and `sI`, only one of them can be marked redundant.
+      // (Assuming no other constraint makes these redundant.)
+      //
+      // In a case where there is one copy in `b` and one in `sI`, we want the
+      // one in `sI` to be marked, not the one in `b`.
+      simplex.detectRedundant(offset, totalNewSimplexInequalities);
       for (unsigned j = 0; j < totalNewSimplexInequalities; j++)
         canIgnoreIneq[j] = simplex.isMarkedRedundant(offset + j);
       simplex.rollback(snapshotBeforeIntersect);
 
       SmallVector<unsigned, 8> ineqsToProcess;
       ineqsToProcess.reserve(totalNewSimplexInequalities);
       for (unsigned i = 0; i < totalNewSimplexInequalities; ++i)
         if (!canIgnoreIneq[i])

mlir/lib/Analysis/Presburger/Simplex.cpp

assert(u.orientation == Orientation::Row &&
          "Unknown should be in row position!");
   assert(u.pos >= nRedundant && "Unknown is already marked redundant!");
   swapRows(u.pos, nRedundant);
   ++nRedundant;
   undoLog.emplace_back(UndoLogEntry::UnmarkLastRedundant);
 }
 
 /// Find a subset of constraints that is redundant and mark them redundant.
-void Simplex::detectRedundant() {
+void Simplex::detectRedundant(unsigned offset, unsigned count) {
+  assert(offset + count <= con.size() && "invalid range!");
   // It is not meaningful to talk about redundancy for empty sets.
   if (empty)
     return;
 
   // Iterate through the constraints and check for each one if it can attain
   // negative sample values. If it can, it's not redundant. Otherwise, it is.
   // We mark redundant constraints redundant.
   //
   // Constraints that get marked redundant in one iteration are not respected
   // when checking constraints in later iterations. This prevents, for example,
   // two identical constraints both being marked redundant since each is
   // redundant given the other one. In this example, only the first of the
   // constraints that is processed will get marked redundant, as it should be.
-  for (Unknown &u : con) {
+  for (unsigned i = 0; i < count; ++i) {
+    Unknown &u = con[offset + i];
     if (u.orientation == Orientation::Column) {
       unsigned column = u.pos;
       Optional<unsigned> pivotRow = findPivotRow({}, Direction::Down, column);
       // If no downward pivot is returned, the constraint is unbounded below
       // and hence not redundant.
       if (!pivotRow)
         continue;
       pivot(*pivotRow, column);

mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp

TEST(SetTest, subtractOutputSizeRegression) {
 
   PresburgerSet result = set1.subtract(set2);
 
   EXPECT_TRUE(result.isEqual(set3));
 
   // Previously, the subtraction result was producing an extra empty set, which
   // is correct, but bad for output size.
   EXPECT_EQ(result.getNumDisjuncts(), 1u);
+
+  PresburgerSet subtractSelf = set1.subtract(set1);
+  EXPECT_TRUE(subtractSelf.isIntegerEmpty());
+  // Previously, the subtraction result was producing several unnecessary empty
+  // sets, which is correct, but bad for output size.
+  EXPECT_EQ(subtractSelf.getNumDisjuncts(), 0u);
 }