[MLIR] Simplex::pivot: also update the redundant rows when pivoting

[arjunp]

Summary

Previously, the pivot function would only update the non-redundant rows when
pivoting. This is incorrect because in some cases, when rolling back past a
detectRedundant call, the basis being used could be different from that which
was used at the time of returning from the detectRedundant call. Therefore,
it is important to update the redundant rows as well during pivots. This could
also be triggered by pivots that occur when testing successive constraints for
being redundant in detectRedundant after some initial constraints are marked redundant.

[grosser]

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

14

This header is unused except in the commented code.

410

I guess you do not want to add this commented code?

[arjunp]

Remove commented out test and header. Improve test documentation.

[arjunp]

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

410

Right. Thanks for pointing it out.

[grosser]

There is a typo in the commit message: deteectRedundant

[arjunp]

Fixed the commit message.

[Groverkss]

LGTM! Thank you for the fix.

[arjunp]

Try to rebase. I don't understand why the windows build fails on something in flang, and consistently as well.

[arjunp]

I accidentally replaced this with a different patch, fixed now.

[grosser]

Maybe the windows build is just broken. If this is clearly unrelated, I would not hold this patch back.

[arjunp]

It seems to have worked now.

mlir/lib/Analysis/Presburger/Simplex.cpp

void Simplex::swapColumns(unsigned i, unsigned j) {
   tableau.swapColumns(i, j);
   std::swap(colUnknown[i], colUnknown[j]);
   unknownFromColumn(i).pos = i;
   unknownFromColumn(j).pos = j;
 }
 
 /// Mark this tableau empty and push an entry to the undo stack.
 void Simplex::markEmpty() {
+  // If the set is already empty, then we shouldn't add another UnmarkEmpty log
+  // entry, since in that case the Simplex will be erroneously marked as
+  // non-empty when rolling back past this point.
+  if (empty)
+    return;
   undoLog.push_back(UndoLogEntry::UnmarkEmpty);
   empty = true;
 }
 
 /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
 /// is the current number of variables, then the corresponding inequality is
 /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0.
 ///

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

 //===- SimplexTest.cpp - Tests for Simplex --------------------------------===//
 //
 // 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
 //
 //===----------------------------------------------------------------------===//
 
 #include "mlir/Analysis/Presburger/Simplex.h"
 
 #include <gmock/gmock.h>
 #include <gtest/gtest.h>
 
 namespace mlir {
 
 /// Take a snapshot, add constraints making the set empty, and rollback.
-/// The set should not be empty after rolling back.
+/// The set should not be empty after rolling back. We add additional
+/// constraints after the set is already empty and roll back the addition
+/// of these. The set should be marked non-empty only once we rollback
+/// past the addition of the first constraint that made it empty.
 TEST(SimplexTest, emptyRollback) {
   Simplex simplex(2);
   // (u - v) >= 0
   simplex.addInequality({1, -1, 0});
-  EXPECT_FALSE(simplex.isEmpty());
+  ASSERT_FALSE(simplex.isEmpty());
 
   unsigned snapshot = simplex.getSnapshot();
   // (u - v) <= -1
   simplex.addInequality({-1, 1, -1});
-  EXPECT_TRUE(simplex.isEmpty());
+  ASSERT_TRUE(simplex.isEmpty());
+
+  unsigned snapshot2 = simplex.getSnapshot();
+  // (u - v) <= -3
+  simplex.addInequality({-1, 1, -3});
+  ASSERT_TRUE(simplex.isEmpty());
+
+  simplex.rollback(snapshot2);
+  ASSERT_TRUE(simplex.isEmpty());
+
   simplex.rollback(snapshot);
-  EXPECT_FALSE(simplex.isEmpty());
+  ASSERT_FALSE(simplex.isEmpty());
 }
 
 /// Check that the set gets marked as empty when we add contradictory
 /// constraints.
 TEST(SimplexTest, addEquality_separate) {
   Simplex simplex(1);
   simplex.addInequality({1, -1}); // x >= 1.
   ASSERT_FALSE(simplex.isEmpty());
TEST(SimplexTest, appendVariable) {
   simplex.appendVariable();
   simplex.appendVariable(0);
   EXPECT_EQ(simplex.getNumVariables(), 2u);
 
   int64_t yMin = 2, yMax = 5;
   simplex.addInequality({0, 1, -yMin}); // y >= 2.
   simplex.addInequality({0, -1, yMax}); // y <= 5.
 
   unsigned snapshot2 = simplex.getSnapshot();
   simplex.appendVariable(2);
   EXPECT_EQ(simplex.getNumVariables(), 4u);
   simplex.rollback(snapshot2);
 
   EXPECT_EQ(simplex.getNumVariables(), 2u);
   EXPECT_EQ(simplex.getNumConstraints(), 2u);
   EXPECT_EQ(simplex.computeIntegerBounds({0, 1, 0}),
             std::make_pair(yMin, yMax));
 
   simplex.rollback(snapshot1);
   EXPECT_EQ(simplex.getNumVariables(), 1u);
   EXPECT_EQ(simplex.getNumConstraints(), 0u);
 }
 
 } // namespace mlir