[MLIR][Presburger] Factor out some functionality from LexSimplex into a LexSimplexBase

[arjunp]

Summary

LexSimplex cannot be made to support symbols for symbolic lexmin; this requires
a second class. In preparation for upstreaming support for symbolic lexmin,
keep the part of LexSimplex that are specific to non-symbolic lexmin in LexSimplex
and move the parts that are required to a common class LexSimplexBase for both to
inherit from.

[Groverkss]

LGTM.

[arjunp]

lint

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

 /// element in A_i, y_j is zero. Thus these columns have no contribution to A*y
 /// 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
 /// ignore more columns; eventually if all these dot products become zero then
 /// A*y is zero and we are done.
-class LexSimplex : public SimplexBase {
+class LexSimplexBase : public SimplexBase {
 public:
-  explicit LexSimplex(unsigned nVar)
-      : SimplexBase(nVar, /*mustUseBigM=*/true) {}
-  explicit LexSimplex(const IntegerRelation &constraints)
-      : LexSimplex(constraints.getNumIds()) {
-    intersectIntegerRelation(constraints);
-  }
-  ~LexSimplex() override = default;
+  ~LexSimplexBase() override = default;
 
   /// 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.
   ///
   /// This just adds the inequality to the tableau and does not try to create a
   /// consistent tableau configuration.
-  void addInequality(ArrayRef<int64_t> coeffs) final {
-    addRow(coeffs, /*makeRestricted=*/true);
-  }
+  void addInequality(ArrayRef<int64_t> coeffs) final;
 
   /// Get a snapshot of the current state. This is used for rolling back.
   unsigned getSnapshot() { return SimplexBase::getSnapshotBasis(); }
 
+protected:
+  LexSimplexBase(unsigned nVar) : SimplexBase(nVar, /*mustUseBigM=*/true) {}
+  explicit LexSimplexBase(const IntegerRelation &constraints)
+      : LexSimplexBase(constraints.getNumIds()) {
+    intersectIntegerRelation(constraints);
+  }
+
+  /// Try to move the specified row to column orientation while preserving the
+  /// lexicopositivity of the basis transform. 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.
+  LogicalResult moveRowUnknownToColumn(unsigned row);
+
+  /// 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.
+  ///
+  /// Returns whether the cut constraint could be enforced, i.e. failure if the
+  /// cut made the polytope empty, and success if it didn't. Failure status
+  /// indicates that the polytope didn't have any integer points.
+  LogicalResult addCut(unsigned row);
+
+  /// Undo the addition of the last constraint. This is only called while
+  /// rolling back.
+  void undoLastConstraint() final;
+
+  /// Given two potential pivot columns for a row, return the one that results
+  /// in the lexicographically smallest sample vector.
+  unsigned getLexMinPivotColumn(unsigned row, unsigned colA,
+                                unsigned colB) const;
+};
+
+class LexSimplex : public LexSimplexBase {
+public:
+  explicit LexSimplex(unsigned nVar) : LexSimplexBase(nVar) {}
+  explicit LexSimplex(const IntegerRelation &constraints)
+      : LexSimplexBase(constraints) {
+    assert(constraints.getNumSymbolIds() == 0 &&
+           "LexSimplex does not support symbols!");
+  }
+
   /// Return the lexicographically minimum rational solution to the constraints.
   MaybeOptimum<SmallVector<Fraction, 8>> findRationalLexMin();
 
   /// Return the lexicographically minimum integer solution to the constraints.
   ///
   /// Note: this should be used only when the lexmin is really needed. To obtain
   /// any integer sample, use Simplex::findIntegerSample as that is more robust.
   MaybeOptimum<SmallVector<int64_t, 8>> findIntegerLexMin();
 
-protected:
+private:
   /// Returns the current sample point, which may contain non-integer (rational)
   /// coordinates. Returns an empty optimum when the tableau is empty.
   ///
   /// Returns an unbounded optimum when the big M parameter is used and a
   /// variable has a non-zero big M coefficient, meaning its value is infinite
   /// or unbounded.
   MaybeOptimum<SmallVector<Fraction, 8>> getRationalSample() const;
 
-  /// 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.
-  ///
-  /// Returns whether the cut constraint could be enforced, i.e. failure if the
-  /// cut made the polytope empty, and success if it didn't. Failure status
-  /// indicates that the polytope didn't have any integer points.
-  LogicalResult addCut(unsigned row);
-
-  /// Undo the addition of the last constraint. This is only called while
-  /// rolling back.
-  void undoLastConstraint() final;
-
   /// Make the tableau configuration consistent.
   void restoreRationalConsistency();
 
   /// Return whether the specified row is violated;
   bool rowIsViolated(unsigned row) const;
 
   /// Get a constraint row that is violated, if one exists.
   /// Otherwise, return an empty optional.
   Optional<unsigned> maybeGetViolatedRow() const;
 
   /// Get a row corresponding to a var that has a non-integral sample value, if
   /// one exists. Otherwise, return an empty optional.
   Optional<unsigned> maybeGetNonIntegralVarRow() const;
 
   /// Given two potential pivot columns for a row, return the one that results
   /// in the lexicographically smallest sample vector.
   unsigned getLexMinPivotColumn(unsigned row, unsigned colA,
                                 unsigned colB) const;
-
-  /// Try to move the specified row to column orientation while preserving the
-  /// lexicopositivity of the basis transform. 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.
-  LogicalResult moveRowUnknownToColumn(unsigned row);
 };
 
 /// The Simplex class uses the Normal pivot rule and supports integer emptiness
 /// checks as well as detecting redundancies.
 ///
 /// The Simplex class supports redundancy checking via detectRedundant and
 /// isMarkedRedundant. A redundant constraint is one which is never violated as
 /// long as the other constraints are not violated, i.e., removing a redundant

mlir/lib/Analysis/Presburger/Simplex.cpp

 }
 } // namespace
 
 MaybeOptimum<SmallVector<Fraction, 8>> LexSimplex::findRationalLexMin() {
   restoreRationalConsistency();
   return getRationalSample();
 }
 
-LogicalResult LexSimplex::addCut(unsigned row) {
+LogicalResult LexSimplexBase::addCut(unsigned row) {
   int64_t denom = tableau(row, 0);
   addZeroRow(/*makeRestricted=*/true);
   tableau(nRow - 1, 0) = denom;
   tableau(nRow - 1, 1) = -mod(-tableau(row, 1), denom);
   tableau(nRow - 1, 2) = 0; // M has all factors in it.
   for (unsigned col = 3; col < nCol; ++col)
     tableau(nRow - 1, col) = mod(tableau(row, col), denom);
   return moveRowUnknownToColumn(nRow - 1);

 //
 // 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 LexSimplex::moveRowUnknownToColumn(unsigned row) {
+LogicalResult LexSimplexBase::moveRowUnknownToColumn(unsigned row) {
   Optional<unsigned> maybeColumn;
   for (unsigned col = 3; col < nCol; ++col) {
     if (tableau(row, col) <= 0)
       continue;
     maybeColumn =
         !maybeColumn ? col : getLexMinPivotColumn(row, *maybeColumn, col);
   }
 
   if (!maybeColumn) {
     markEmpty();
     return failure();
   }
 
   pivot(row, *maybeColumn);
   return success();
 }
 
-unsigned LexSimplex::getLexMinPivotColumn(unsigned row, unsigned colA,
+unsigned LexSimplexBase::getLexMinPivotColumn(unsigned row, unsigned colA,
                                               unsigned colB) const {
   // A pivot causes the following change. (in the diagram the matrix elements
   // are shown as rationals and there is no common denominator used)
   //
   //            pivot col    big M col      const col
   // pivot row     a            p               b
   // other row     c            q               d
   //                        |
   //                        v
if (Optional<unsigned> maybeRow = findPivotRow({}, Direction::Up, column)) {
       pivot(*row, column);
     }
   }
   removeLastConstraintRowOrientation();
 }
 
 // It's not valid to remove the constraint by deleting the column since this
 // would result in an invalid basis.
-void LexSimplex::undoLastConstraint() {
+void LexSimplexBase::undoLastConstraint() {
   if (con.back().orientation == Orientation::Column) {
     // When removing the last constraint during a rollback, we just need to find
     // any pivot at all, i.e., any row with non-zero coefficient for the
     // column, because when rolling back a lexicographic simplex, we always
     // end by restoring the exact basis that was present at the time of the
     // snapshot, so what pivots we perform while undoing doesn't matter as
     // long as we get the unknown to row orientation and remove it.
     unsigned column = con.back().pos;
if (u.orientation == Orientation::Column) {
       // entry in the constant column divided by the denominator.
       int64_t denom = tableau(u.pos, 0);
       sample.emplace_back(tableau(u.pos, 1), denom);
     }
   }
   return sample;
 }
 
+void LexSimplexBase::addInequality(ArrayRef<int64_t> coeffs) {
+  addRow(coeffs, /*makeRestricted=*/true);
+}
+
 MaybeOptimum<SmallVector<Fraction, 8>> LexSimplex::getRationalSample() const {
   if (empty)
     return OptimumKind::Empty;
 
   SmallVector<Fraction, 8> sample;
   sample.reserve(var.size());
   // Push the sample value for each variable into the vector.
   for (const Unknown &u : var) {