[MLIR][Presburger] Fix subtract processing extra inequalities

[Groverkss]

Summary

This patch fixes a bug in PresburgeRelation::subtract that made it process the
inequality at index 0, multiple times. This was caused by allocating memory
instead of reserving memory in llvm::SmallVector.

[arjunp]

Thanks for fixing this. It should be SmallVector in the description.

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

if (level > frames.size()) {
 
       // Equalities are added to simplex as a pair of inequalities.
       unsigned totalNewSimplexInequalities =
           2 * sI.getNumEqualities() + sI.getNumInequalities();
       for (unsigned j = 0; j < totalNewSimplexInequalities; j++)
         canIgnoreIneq[j] = simplex.isMarkedRedundant(offset + j);
       simplex.rollback(snapshotBeforeIntersect);
 
-      SmallVector<unsigned, 8> ineqsToProcess(totalNewSimplexInequalities);
+      SmallVector<unsigned, 8> ineqsToProcess;
+      ineqsToProcess.reserve(totalNewSimplexInequalities);
       for (unsigned i = 0; i < totalNewSimplexInequalities; ++i)
         if (!canIgnoreIneq[i])
           ineqsToProcess.push_back(i);
 
       if (ineqsToProcess.empty()) {
         // Nothing to process; return. (we have no frame to pop.)
         level = frames.size();
         continue;

mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp

TEST(SetTest, computeVolume) {
   expectComputedVolumeIsValidOverapprox(unbounded, /*trueVolume=*/{},
                                         /*resultBound=*/{});
 
   // Union of unbounded with bounded is unbounded.
   expectComputedVolumeIsValidOverapprox(unbounded.unionSet(diamond),
                                         /*trueVolume=*/{},
                                         /*resultBound=*/{});
 }
+
+TEST(SetTest, subtractOutputSizeRegression) {
+  PresburgerSet set1 =
+      parsePresburgerSetFromPolyStrings(1, {"(i) : (i >= 0, 10 - i >= 0)"});
+  PresburgerSet set2 =
+      parsePresburgerSetFromPolyStrings(1, {"(i) : (i - 5 >= 0)"});
+
+  PresburgerSet set3 =
+      parsePresburgerSetFromPolyStrings(1, {"(i) : (i >= 0, 4 - i >= 0)"});
+
+  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);
+}