[MLIR][Presburger] subtract: fix bug in the non-recursive implementation

[arjunp]

Summary

When making the subtract implementation non-recursive, tail calls were
implemented by incrementing the level but not pushing a frame, and returning
was implemented as returning to the level corresponding to the number of frames in the stack.

This is incorrect, as there could be a case where we tail-recurse at level,
and then recurse at level + 1, pushing a frame. However, because the previous
frame was missing, this new frame would be interpreted as corresponding to
level and not level + 1. Fix this by removing the special handling of tail
calls and just doing them as normal recursion, as this is the simplest correct
implementation and handling them specifically would be a premature optimization.

The impact of this bug is only on performance as this can only lead to
unnecessary subtractions of the same disjuncts multiples times. As subtraction
is idempotent, and rationally empty disjuncts are always discarded, this
does not affect the output, so this patch does not include a regression test.
(This also does not affect termination.)

[Groverkss]

LGTM.

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

271

Add a TODO here that this can probably be optimized later?

[arjunp]

address comment

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

struct Frame {
     SmallVector<unsigned, 8> ineqsToProcess;
     // The index of the last inequality that was processed at this level.
     // This is empty when we are coming to this level for the first time.
     Optional<unsigned> lastIneqProcessed;
   };
   SmallVector<Frame, 2> frames;
 
   // When we "recurse", we ensure the current frame is stored in `frames` and
-  // increment `level`. When we "tail recurse", we just increment `level`,
-  // without storing any frame. Accordingly, when we return, we return to the
-  // last level that has a frame associated with it.
+  // increment `level`. When we return, we decrement `level`.
   unsigned level = 1;
   while (level > 0) {
     if (level - 1 >= s.getNumDisjuncts()) {
       // No more parts to subtract; add to the result and return.
       result.unionInPlace(b);
       level = frames.size();
       continue;
     }
if (level > frames.size()) {
       simplex.appendVariable(numLocalsAdded);
 
       unsigned snapshotBeforeIntersect = simplex.getSnapshot();
       simplex.intersectIntegerRelation(sI);
 
       if (simplex.isEmpty()) {
         // b /\ s_i is empty, so b \ s_i = b. We move directly to i + 1.
         // We are ignoring level i completely, so we restore the state
-        // *before* going to the next level. We are "tail recursing", so
-        // we don't add a frame before going to the next level.
+        // *before* going to the next level.
         b.truncate(initBCounts);
         simplex.rollback(initialSnapshot);
+        // Recurse. We haven't processed any inequalities and
+        // we don't need to process anything when we return.
+        //
+        // TODO: consider supporting tail recursion directly if this becomes
+        // 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 =