[MLIR][Presburger][Simplex] moveRowUnknownToColumn: support the row sample value being zero

[arjunp]

Summary

When the sample value is zero, everything is the same except that failure to
pivot does not imply emptiness. So, leave it to the user to mark as empty if
necessary, if they know the sample value is strictly negative. This is needed
for an upcoming symbolic lexmin heuristic.

[Groverkss]

LGTM.

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

explicit LexSimplexBase(const IntegerRelation &constraints)
                        constraints.getNumSymbolIds()) {
     intersectIntegerRelation(constraints);
   }
 
   /// Add new symbolic variables to the end of the list of variables.
   void appendSymbol();
 
   /// Try to move the specified row to column orientation while preserving the
-  /// lexicopositivity of the basis transform. The row must have a negative
-  /// sample value. If this is not possible, return failure. This only occurs
-  /// when the constraints have no solution; the tableau will be marked empty in
-  /// such a case.
+  /// lexicopositivity of the basis transform. The row must have a non-positive
+  /// sample value. If this is not possible, return failure. This occurs when
+  /// the constraints have no solution or the sample value is zero.
   LogicalResult moveRowUnknownToColumn(unsigned row);
 
   /// Given a row that has a non-integer sample value, add an inequality to cut
   /// away this fractional sample value from the polytope without removing any
   /// integer points. The integer lexmin, if one existed, remains the same on
   /// return.
   ///
   /// This assumes that the symbolic part of the sample is integral,

mlir/lib/Analysis/Presburger/Simplex.cpp

 /// and we can completely ignore these columns of A. We now continue downwards,
 /// looking for rows of A that have a non-zero element other than in the ignored
 /// columns. If we find one, say A_k, once again these elements must be positive
 /// since they are the first non-zero element in each of these columns, so if
 /// (A_k)*y is not zero then we have that A*y is lexicopositive and if not we
 /// add these to the set of ignored columns and continue to the next row. If we
 /// run out of rows, then A*y is zero and we are done.
 MaybeOptimum<SmallVector<Fraction, 8>> LexSimplex::findRationalLexMin() {
-  if (restoreRationalConsistency().failed())
+  if (restoreRationalConsistency().failed()) {
+    markEmpty();
     return OptimumKind::Empty;
+  }
   return getRationalSample();
 }
 
 /// Given a row that has a non-integer sample value, add an inequality such
 /// that this fractional sample value is cut away from the polytope. The added
 /// inequality will be such that no integer points are removed. i.e., the
 /// integer lexmin, if it exists, is the same with and without this constraint.
 ///
if (empty)
     return failure();
   while (Optional<unsigned> maybeViolatedRow = maybeGetViolatedRow())
     if (moveRowUnknownToColumn(*maybeViolatedRow).failed())
       return failure();
   return success();
 }
 
 // Move the row unknown to column orientation while preserving lexicopositivity
-// of the basis transform. The sample value of the row must be negative.
+// of the basis transform. The sample value of the row must be non-positive.
 //
 // We only consider pivots where the pivot element is positive. Suppose no such
 // pivot exists, i.e., some violated row has no positive coefficient for any
 // basis unknown. The row can be represented as (s + c_1*u_1 + ... + c_n*u_n)/d,
 // where d is the denominator, s is the sample value and the c_i are the basis
-// coefficients. Since any feasible assignment of the basis satisfies u_i >= 0
-// for all i, and we have s < 0 as well as c_i < 0 for all i, any feasible
-// assignment would violate this row and therefore the constraints have no
-// solution.
+// coefficients. If s != 0, then since any feasible assignment of the basis
+// satisfies u_i >= 0 for all i, and we have s < 0 as well as c_i < 0 for all i,
+// any feasible assignment would violate this row and therefore the constraints
+// have no solution.
 //
 // We can preserve lexicopositivity by picking the pivot column with positive
 // pivot element that makes the lexicographically smallest change to the sample
 // point.
 //
 // Proof. Let
 // x = (x_1, ... x_n) be the variables,
 // z = (z_1, ... z_m) be the constraints,

 // between the tableau and these matrices B and B' is that there is no special
 // case for the pivot row, since it continues to represent the same unknown. The
 // same formula applies for all rows:
 //
 // B'.col(j) = B.col(j) / B(i,j)
 // B'.col(k) = B.col(k) - B(i,k) * B.col(j) / B(i,j) for k != j
 // and similarly, s' = s - s_i * B.col(j) / B(i,j).
 //
-// Since the row is violated, we have s_i < 0, so the change in sample value
-// when pivoting with column a is lexicographically smaller than that when
-// pivoting with column b iff B.col(a) / B(i, a) is lexicographically smaller
-// than B.col(b) / B(i, b).
+// If s_i == 0, then the sample value remains unchanged. Otherwise, if s_i < 0,
+// the change in sample value when pivoting with column a is lexicographically
+// smaller than that when pivoting with column b iff B.col(a) / B(i, a) is
+// lexicographically smaller than B.col(b) / B(i, b).
 //
 // Since B(i, j) > 0, column j remains lexicopositive.
 //
 // For the other columns, suppose C.col(k) is not lexicopositive.
 // This means that for some p, for all t < p,
 // C(t,k) = 0 => B(t,k) = B(t,j) * B(i,k) / B(i,j) and
 // C(t,k) < 0 => B(p,k) < B(t,j) * B(i,k) / B(i,j),
 // which is in contradiction to the fact that B.col(j) / B(i,j) must be
 // lexicographically smaller than B.col(k) / B(i,k), since it lexicographically
 // minimizes the change in sample value.
 LogicalResult LexSimplexBase::moveRowUnknownToColumn(unsigned row) {
   Optional<unsigned> maybeColumn;
   for (unsigned col = 3 + nSymbol; col < nCol; ++col) {
     if (tableau(row, col) <= 0)
       continue;
     maybeColumn =
         !maybeColumn ? col : getLexMinPivotColumn(row, *maybeColumn, col);
   }
 
-  if (!maybeColumn) {
-    markEmpty();
+  if (!maybeColumn)
     return failure();
-  }
 
   pivot(row, *maybeColumn);
   return success();
 }
 
 unsigned LexSimplexBase::getLexMinPivotColumn(unsigned row, unsigned colA,
                                               unsigned colB) const {
   // First, let's consider the non-symbolic case.