[MLIR] Simplex: split some basic functionality out into a SimplexBase class

[arjunp]

Summary

This is a purely mechanical patch moving some functionality out from the
Simplex class out into a SimplexBase class. This pavees the way for
a future patch adding support for lexicographic optimization with a class
LexSimplex, which will inherit from SimplexBase. Inheriting directly
from Simplex would bring many additional functions that would not work in
LexSimplex because it operates slighty differently from Simplex. So We
split out only the basic functionality it needs to inherit into SimplexBase.

[Groverkss]

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

32–42

Since this documentation is now file specific instead of specific to Simplex class, should we change the "this class implements" specific things?

[arjunp]

Addressed Kunwar's comments.

[Groverkss]

LGTM.

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

 #include "llvm/ADT/SmallVector.h"
 #include "llvm/Support/StringSaver.h"
 #include "llvm/Support/raw_ostream.h"
 
 namespace mlir {
 
 class GBRSimplex;
 
-/// This class implements a version of the Simplex and Generalized Basis
+/// The Simplex class implements a version of the Simplex and Generalized Basis
 /// Reduction algorithms, which can perform analysis of integer sets with affine
 /// inequalities and equalities. A Simplex can be constructed
 /// by specifying the dimensionality of the set. It supports adding affine
 /// inequalities and equalities, and can perform emptiness checks, i.e., it can
 /// find a solution to the set of constraints if one exists, or say that the
 /// set is empty if no solution exists. Currently, this only works for bounded
 /// sets. Furthermore, it can find a subset of these constraints that are
 /// redundant, i.e. a subset of constraints that doesn't constrain the affine
 /// set further after adding the non-redundant constraints. Simplex can also be
 /// constructed from a FlatAffineConstraints object.
 ///
-/// The implementation of this Simplex class, other than the functionality
-/// for sampling, is based on the paper
+/// The implementation of the Simplex and SimplexBase classes, other than the
+/// functionality for sampling, is based on the paper
 /// "Simplify: A Theorem Prover for Program Checking"
 /// by D. Detlefs, G. Nelson, J. B. Saxe.
 ///
 /// We define variables, constraints, and unknowns. Consider the example of a
 /// two-dimensional set defined by 1 + 2x + 3y >= 0 and 2x - 3y >= 0. Here,
 /// x, y, are variables while 1 + 2x + 3y >= 0, 2x - 3y >= 0 are
 /// constraints. Unknowns are either variables or constraints, i.e., x, y,
 /// 1 + 2x + 3y >= 0, 2x - 3y >= 0 are all unknowns.

 /// This Simplex class also supports taking snapshots of the current state
 /// and rolling back to prior snapshots. This works by maintaining an undo log
 /// of operations. Snapshots are just pointers to a particular location in the
 /// log, and rolling back to a snapshot is done by reverting each log entry's
 /// operation from the end until we reach the snapshot's location.
 ///
 /// Finding an integer sample is done with the Generalized Basis Reduction
 /// algorithm. See the documentation for findIntegerSample and reduceBasis.
-class Simplex {
+///
+/// The SimplexBase class contains some basic functionality. In the future,
+/// lexicographic optimization will be supported by a class inheriting from
+/// SimplexBase. Functionality that will not supported by that class is placed
+/// in `Simplex`.
+
+class SimplexBase {
 public:
   enum class Direction { Up, Down };
 
-  Simplex() = delete;
-  explicit Simplex(unsigned nVar);
-  explicit Simplex(const FlatAffineConstraints &constraints);
+  SimplexBase() = delete;
+  explicit SimplexBase(unsigned nVar);
+  explicit SimplexBase(const FlatAffineConstraints &constraints);
 
   /// Returns true if the tableau is empty (has conflicting constraints),
   /// false otherwise.
   bool isEmpty() const;
 
   /// 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.
public:
   unsigned getSnapshot() const;
 
   /// Rollback to a snapshot. This invalidates all later snapshots.
   void rollback(unsigned snapshot);
 
   /// Add all the constraints from the given FlatAffineConstraints.
   void intersectFlatAffineConstraints(const FlatAffineConstraints &fac);
 
-  /// Compute the maximum or minimum value of the given row, depending on
-  /// direction. The specified row is never pivoted. On return, the row may
-  /// have a negative sample value if the direction is down.
-  ///
-  /// Returns a Fraction denoting the optimum, or a null value if no optimum
-  /// exists, i.e., if the expression is unbounded in this direction.
-  Optional<Fraction> computeRowOptimum(Direction direction, unsigned row);
-
-  /// Compute the maximum or minimum value of the given expression, depending on
-  /// direction. Should not be called when the Simplex is empty.
-  ///
-  /// Returns a Fraction denoting the optimum, or a null value if no optimum
-  /// exists, i.e., if the expression is unbounded in this direction.
-  Optional<Fraction> computeOptimum(Direction direction,
-                                    ArrayRef<int64_t> coeffs);
-
-  /// Returns whether the perpendicular of the specified constraint
-  /// is a direction along which the polytope is bounded.
-  bool isBoundedAlongConstraint(unsigned constraintIndex);
-
-  /// Returns whether the specified constraint has been marked as redundant.
-  /// Constraints are numbered from 0 starting at the first added inequality.
-  /// Equalities are added as a pair of inequalities and so correspond to two
-  /// inequalities with successive indices.
-  bool isMarkedRedundant(unsigned constraintIndex) const;
-
-  /// Finds a subset of constraints that is redundant, i.e., such that
-  /// the set of solutions does not change if these constraints are removed.
-  /// Marks these constraints as redundant. Whether a specific constraint has
-  /// been marked redundant can be queried using isMarkedRedundant.
-  void detectRedundant();
-
-  /// Returns a (min, max) pair denoting the minimum and maximum integer values
-  /// of the given expression.
-  std::pair<int64_t, int64_t> computeIntegerBounds(ArrayRef<int64_t> coeffs);
-
-  /// Returns true if the polytope is unbounded, i.e., extends to infinity in
-  /// some direction. Otherwise, returns false.
-  bool isUnbounded();
-
-  /// Make a tableau to represent a pair of points in the given tableaus, one in
-  /// tableau A and one in B.
-  static Simplex makeProduct(const Simplex &a, const Simplex &b);
-
   /// Returns a rational sample point. This should not be called when Simplex is
   /// empty.
   SmallVector<Fraction, 8> getRationalSample() const;
 
   /// Returns the current sample point if it is integral. Otherwise, returns
   /// None.
   Optional<SmallVector<int64_t, 8>> getSamplePointIfIntegral() const;
 
-  /// Returns an integer sample point if one exists, or None
-  /// otherwise. This should only be called for bounded sets.
-  Optional<SmallVector<int64_t, 8>> findIntegerSample();
-
   /// Print the tableau's internal state.
   void print(raw_ostream &os) const;
   void dump() const;
 
-  /// Check if the specified inequality already holds in the polytope.
-  bool isRedundantInequality(ArrayRef<int64_t> coeffs);
-
-  /// Check if the specified equality already holds in the polytope.
-  bool isRedundantEquality(ArrayRef<int64_t> coeffs);
-
-  /// Returns true if this Simplex's polytope is a rational subset of `fac`.
-  /// Otherwise, returns false.
-  bool isRationalSubsetOf(const FlatAffineConstraints &fac);
-
-private:
-  friend class GBRSimplex;
-
+protected:
   enum class Orientation { Row, Column };
 
   /// An Unknown is either a variable or a constraint. It is always associated
   /// with either a row or column. Whether it's a row or a column is specified
   /// by the orientation and pos identifies the specific row or column it is
   /// associated with. If the unknown is restricted, then it has a
   /// non-negativity constraint associated with it, i.e., its sample value must
   /// always be non-negative and if it cannot be made non-negative without
protected:
   void swapColumns(unsigned i, unsigned j);
 
   /// Restore the unknown to a non-negative sample value.
   ///
   /// Returns success if the unknown was successfully restored to a non-negative
   /// sample value, failure otherwise.
   LogicalResult restoreRow(Unknown &u);
 
-  /// Compute the maximum or minimum of the specified Unknown, depending on
-  /// direction. The specified unknown may be pivoted. If the unknown is
-  /// restricted, it will have a non-negative sample value on return.
-  /// Should not be called if the Simplex is empty.
-  ///
-  /// Returns a Fraction denoting the optimum, or a null value if no optimum
-  /// exists, i.e., if the expression is unbounded in this direction.
-  Optional<Fraction> computeOptimum(Direction direction, Unknown &u);
-
-  /// Mark the specified unknown redundant. This operation is added to the undo
-  /// log and will be undone by rollbacks. The specified unknown must be in row
-  /// orientation.
-  void markRowRedundant(Unknown &u);
-
   /// Enum to denote operations that need to be undone during rollback.
   enum class UndoLogEntry {
     RemoveLastConstraint,
     RemoveLastVariable,
     UnmarkEmpty,
     UnmarkLastRedundant
   };
 
   /// Undo the operation represented by the log entry.
   void undo(UndoLogEntry entry);
 
   /// Find a row that can be used to pivot the column in the specified
   /// direction. If skipRow is not null, then this row is excluded
   /// from consideration. The returned pivot will maintain all constraints
   /// except the column itself and skipRow, if it is set. (if these unknowns
   /// are restricted).
   ///
   /// Returns the row to pivot to, or an empty Optional if the column
   /// is unbounded in the specified direction.
   Optional<unsigned> findPivotRow(Optional<unsigned> skipRow,
                                   Direction direction, unsigned col) const;
 
-  /// Reduce the given basis, starting at the specified level, using general
-  /// basis reduction.
-  void reduceBasis(Matrix &basis, unsigned level);
-
   /// The number of rows in the tableau.
   unsigned nRow;
 
   /// The number of columns in the tableau, including the common denominator
   /// and the constant column.
   unsigned nCol;
 
   /// The number of redundant rows in the tableau. These are the first
protected:
   /// colUnknown is padded with two null indexes at the front since the first
   /// two columns don't correspond to any unknowns.
   SmallVector<int, 8> rowUnknown, colUnknown;
 
   /// These hold information about each unknown.
   SmallVector<Unknown, 8> con, var;
 };
 
+class Simplex : public SimplexBase {
+public:
+  Simplex() = delete;
+  explicit Simplex(unsigned nVar) : SimplexBase(nVar) {}
+  explicit Simplex(const FlatAffineConstraints &constraints)
+      : SimplexBase(constraints) {}
+
+  /// Compute the maximum or minimum value of the given row, depending on
+  /// direction. The specified row is never pivoted. On return, the row may
+  /// have a negative sample value if the direction is down.
+  ///
+  /// Returns a Fraction denoting the optimum, or a null value if no optimum
+  /// exists, i.e., if the expression is unbounded in this direction.
+  Optional<Fraction> computeRowOptimum(Direction direction, unsigned row);
+
+  /// Compute the maximum or minimum value of the given expression, depending on
+  /// direction. Should not be called when the Simplex is empty.
+  ///
+  /// Returns a Fraction denoting the optimum, or a null value if no optimum
+  /// exists, i.e., if the expression is unbounded in this direction.
+  Optional<Fraction> computeOptimum(Direction direction,
+                                    ArrayRef<int64_t> coeffs);
+
+  /// Returns whether the perpendicular of the specified constraint is a
+  /// is a direction along which the polytope is bounded.
+  bool isBoundedAlongConstraint(unsigned constraintIndex);
+
+  /// Returns whether the specified constraint has been marked as redundant.
+  /// Constraints are numbered from 0 starting at the first added inequality.
+  /// Equalities are added as a pair of inequalities and so correspond to two
+  /// inequalities with successive indices.
+  bool isMarkedRedundant(unsigned constraintIndex) const;
+
+  /// Finds a subset of constraints that is redundant, i.e., such that
+  /// the set of solutions does not change if these constraints are removed.
+  /// Marks these constraints as redundant. Whether a specific constraint has
+  /// been marked redundant can be queried using isMarkedRedundant.
+  void detectRedundant();
+
+  /// Returns a (min, max) pair denoting the minimum and maximum integer values
+  /// of the given expression.
+  std::pair<int64_t, int64_t> computeIntegerBounds(ArrayRef<int64_t> coeffs);
+
+  /// Returns true if the polytope is unbounded, i.e., extends to infinity in
+  /// some direction. Otherwise, returns false.
+  bool isUnbounded();
+
+  /// Make a tableau to represent a pair of points in the given tableaus, one in
+  /// tableau A and one in B.
+  static Simplex makeProduct(const Simplex &a, const Simplex &b);
+
+  /// Returns an integer sample point if one exists, or None
+  /// otherwise. This should only be called for bounded sets.
+  Optional<SmallVector<int64_t, 8>> findIntegerSample();
+
+  /// Check if the specified inequality already holds in the polytope.
+  bool isRedundantInequality(ArrayRef<int64_t> coeffs);
+
+  /// Check if the specified equality already holds in the polytope.
+  bool isRedundantEquality(ArrayRef<int64_t> coeffs);
+
+  /// Returns true if this Simplex's polytope is a rational subset of `fac`.
+  /// Otherwise, returns false.
+  bool isRationalSubsetOf(const FlatAffineConstraints &fac);
+
+private:
+  friend class GBRSimplex;
+
+  /// Compute the maximum or minimum of the specified Unknown, depending on
+  /// direction. The specified unknown may be pivoted. If the unknown is
+  /// restricted, it will have a non-negative sample value on return.
+  /// Should not be called if the Simplex is empty.
+  ///
+  /// Returns a Fraction denoting the optimum, or a null value if no optimum
+  /// exists, i.e., if the expression is unbounded in this direction.
+  Optional<Fraction> computeOptimum(Direction direction, Unknown &u);
+
+  /// Mark the specified unknown redundant. This operation is added to the undo
+  /// log and will be undone by rollbacks. The specified unknown must be in row
+  /// orientation.
+  void markRowRedundant(Unknown &u);
+
+  /// Reduce the given basis, starting at the specified level, using general
+  /// basis reduction.
+  void reduceBasis(Matrix &basis, unsigned level);
+};
+
 } // namespace mlir
 
 #endif // MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H

mlir/lib/Analysis/Presburger/Simplex.cpp

 #include "llvm/ADT/Optional.h"
 
 namespace mlir {
 using Direction = Simplex::Direction;
 
 const int nullIndex = std::numeric_limits<int>::max();
 
 /// Construct a Simplex object with `nVar` variables.
-Simplex::Simplex(unsigned nVar)
+SimplexBase::SimplexBase(unsigned nVar)
     : nRow(0), nCol(2), nRedundant(0), tableau(0, 2 + nVar), empty(false) {
   colUnknown.push_back(nullIndex);
   colUnknown.push_back(nullIndex);
   for (unsigned i = 0; i < nVar; ++i) {
     var.emplace_back(Orientation::Column, /*restricted=*/false, /*pos=*/nCol);
     colUnknown.push_back(i);
     nCol++;
   }
 }
 
-Simplex::Simplex(const FlatAffineConstraints &constraints)
-    : Simplex(constraints.getNumIds()) {
+SimplexBase::SimplexBase(const FlatAffineConstraints &constraints)
+    : SimplexBase(constraints.getNumIds()) {
   for (unsigned i = 0, numIneqs = constraints.getNumInequalities();
        i < numIneqs; ++i)
     addInequality(constraints.getInequality(i));
   for (unsigned i = 0, numEqs = constraints.getNumEqualities(); i < numEqs; ++i)
     addEquality(constraints.getEquality(i));
 }
 
-const Simplex::Unknown &Simplex::unknownFromIndex(int index) const {
+const Simplex::Unknown &SimplexBase::unknownFromIndex(int index) const {
   assert(index != nullIndex && "nullIndex passed to unknownFromIndex");
   return index >= 0 ? var[index] : con[~index];
 }
 
-const Simplex::Unknown &Simplex::unknownFromColumn(unsigned col) const {
+const Simplex::Unknown &SimplexBase::unknownFromColumn(unsigned col) const {
   assert(col < nCol && "Invalid column");
   return unknownFromIndex(colUnknown[col]);
 }
 
-const Simplex::Unknown &Simplex::unknownFromRow(unsigned row) const {
+const Simplex::Unknown &SimplexBase::unknownFromRow(unsigned row) const {
   assert(row < nRow && "Invalid row");
   return unknownFromIndex(rowUnknown[row]);
 }
 
-Simplex::Unknown &Simplex::unknownFromIndex(int index) {
+Simplex::Unknown &SimplexBase::unknownFromIndex(int index) {
   assert(index != nullIndex && "nullIndex passed to unknownFromIndex");
   return index >= 0 ? var[index] : con[~index];
 }
 
-Simplex::Unknown &Simplex::unknownFromColumn(unsigned col) {
+Simplex::Unknown &SimplexBase::unknownFromColumn(unsigned col) {
   assert(col < nCol && "Invalid column");
   return unknownFromIndex(colUnknown[col]);
 }
 
-Simplex::Unknown &Simplex::unknownFromRow(unsigned row) {
+Simplex::Unknown &SimplexBase::unknownFromRow(unsigned row) {
   assert(row < nRow && "Invalid row");
   return unknownFromIndex(rowUnknown[row]);
 }
 
 /// Add a new row to the tableau corresponding to the given constant term and
 /// list of coefficients. The coefficients are specified as a vector of
 /// (variable index, coefficient) pairs.
-unsigned Simplex::addRow(ArrayRef<int64_t> coeffs) {
+unsigned SimplexBase::addRow(ArrayRef<int64_t> coeffs) {
   assert(coeffs.size() == 1 + var.size() &&
          "Incorrect number of coefficients!");
 
   ++nRow;
   // If the tableau is not big enough to accomodate the extra row, we extend it.
   if (nRow >= tableau.getNumRows())
     tableau.resizeVertically(nRow);
   rowUnknown.push_back(~con.size());
unsigned SimplexBase::addRow(ArrayRef<int64_t> coeffs) {
   normalizeRow(nRow - 1);
   // Push to undo log along with the index of the new constraint.
   undoLog.push_back(UndoLogEntry::RemoveLastConstraint);
   return con.size() - 1;
 }
 
 /// Normalize the row by removing factors that are common between the
 /// denominator and all the numerator coefficients.
-void Simplex::normalizeRow(unsigned row) {
+void SimplexBase::normalizeRow(unsigned row) {
   int64_t gcd = 0;
   for (unsigned col = 0; col < nCol; ++col) {
     if (gcd == 1)
       break;
     gcd = llvm::greatestCommonDivisor(gcd, std::abs(tableau(row, col)));
   }
   for (unsigned col = 0; col < nCol; ++col)
     tableau(row, col) /= gcd;

 /// To increase (resp. decrease) the value of a row, we need to find a live
 /// column with a non-zero coefficient. If the coefficient is positive, we need
 /// to increase (decrease) the value of the column, and if the coefficient is
 /// negative, we need to decrease (increase) the value of the column. Also,
 /// we cannot decrease the sample value of restricted columns.
 ///
 /// If multiple columns are valid, we break ties by considering a lexicographic
 /// ordering where we prefer unknowns with lower index.
-Optional<Simplex::Pivot> Simplex::findPivot(int row,
+Optional<SimplexBase::Pivot> SimplexBase::findPivot(int row,
                                                     Direction direction) const {
   Optional<unsigned> col;
   for (unsigned j = 2; j < nCol; ++j) {
     int64_t elem = tableau(row, j);
     if (elem == 0)
       continue;
 
     if (unknownFromColumn(j).restricted &&
         !signMatchesDirection(elem, direction))
Optional<SimplexBase::Pivot> SimplexBase::findPivot(int row,
   Optional<unsigned> maybePivotRow = findPivotRow(row, newDirection, *col);
   return Pivot{maybePivotRow.getValueOr(row), *col};
 }
 
 /// Swap the associated unknowns for the row and the column.
 ///
 /// First we swap the index associated with the row and column. Then we update
 /// the unknowns to reflect their new position and orientation.
-void Simplex::swapRowWithCol(unsigned row, unsigned col) {
+void SimplexBase::swapRowWithCol(unsigned row, unsigned col) {
   std::swap(rowUnknown[row], colUnknown[col]);
   Unknown &uCol = unknownFromColumn(col);
   Unknown &uRow = unknownFromRow(row);
   uCol.orientation = Orientation::Column;
   uRow.orientation = Orientation::Row;
   uCol.pos = col;
   uRow.pos = row;
 }
 
-void Simplex::pivot(Pivot pair) { pivot(pair.row, pair.column); }
+void SimplexBase::pivot(Pivot pair) { pivot(pair.row, pair.column); }
 
 /// Pivot pivotRow and pivotCol.
 ///
 /// Let R be the pivot row unknown and let C be the pivot col unknown.
 /// Since initially R = a*C + sum b_i * X_i
 /// (where the sum is over the other column's unknowns, x_i)
 /// C = (R - (sum b_i * X_i))/a
 ///

 ///
 ///            pivot col    other col                    pivot col   other col
 /// pivot row     a/p          b/p     ->   pivot row      p/a         -b/a
 /// other row     c/q          d/q          other row     cp/aq    (da - bc)/aq
 ///
 /// The pivot row transform is accomplished be swapping a with the pivot row's
 /// common denominator and negating the pivot row except for the pivot column
 /// element.
-void Simplex::pivot(unsigned pivotRow, unsigned pivotCol) {
+void SimplexBase::pivot(unsigned pivotRow, unsigned pivotCol) {
   assert(pivotCol >= 2 && "Refusing to pivot invalid column");
 
   swapRowWithCol(pivotRow, pivotCol);
   std::swap(tableau(pivotRow, 0), tableau(pivotRow, pivotCol));
   // We need to negate the whole pivot row except for the pivot column.
   if (tableau(pivotRow, 0) < 0) {
     // If the denominator is negative, we negate the row by simply negating the
     // denominator.
for (unsigned row = 0; row < nRow; ++row) {
     tableau(row, pivotCol) *= tableau(pivotRow, pivotCol);
     normalizeRow(row);
   }
 }
 
 /// Perform pivots until the unknown has a non-negative sample value or until
 /// no more upward pivots can be performed. Return success if we were able to
 /// bring the row to a non-negative sample value, and failure otherwise.
-LogicalResult Simplex::restoreRow(Unknown &u) {
+LogicalResult SimplexBase::restoreRow(Unknown &u) {
   assert(u.orientation == Orientation::Row &&
          "unknown should be in row position");
 
   while (tableau(u.pos, 1) < 0) {
     Optional<Pivot> maybePivot = findPivot(u.pos, Direction::Up);
     if (!maybePivot)
       break;
 

 /// change in sample value (in the specified direction). (note that c is
 /// non-negative here since the row is restricted and the tableau is consistent)
 ///
 /// We iterate through the rows and pick the row which imposes the most
 /// stringent bound, since pivoting with a row changes the row's sample value to
 /// 0 and hence saturates the bound it imposes. We break ties between rows that
 /// impose the same bound by considering a lexicographic ordering where we
 /// prefer unknowns with lower index value.
-Optional<unsigned> Simplex::findPivotRow(Optional<unsigned> skipRow,
+Optional<unsigned> SimplexBase::findPivotRow(Optional<unsigned> skipRow,
                                              Direction direction,
                                              unsigned col) const {
   Optional<unsigned> retRow;
   int64_t retElem, retConst;
   for (unsigned row = nRedundant; row < nRow; ++row) {
     if (skipRow && row == *skipRow)
       continue;
     int64_t elem = tableau(row, col);
     if (elem == 0)
       continue;
if ((diff == 0 && rowUnknown[row] < rowUnknown[*retRow]) ||
       retRow = row;
       retElem = elem;
       retConst = constTerm;
     }
   }
   return retRow;
 }
 
-bool Simplex::isEmpty() const { return empty; }
+bool SimplexBase::isEmpty() const { return empty; }
 
-void Simplex::swapRows(unsigned i, unsigned j) {
+void SimplexBase::swapRows(unsigned i, unsigned j) {
   if (i == j)
     return;
   tableau.swapRows(i, j);
   std::swap(rowUnknown[i], rowUnknown[j]);
   unknownFromRow(i).pos = i;
   unknownFromRow(j).pos = j;
 }
 
-void Simplex::swapColumns(unsigned i, unsigned j) {
+void SimplexBase::swapColumns(unsigned i, unsigned j) {
   assert(i < nCol && j < nCol && "Invalid columns provided!");
   if (i == j)
     return;
   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() {
+void SimplexBase::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.
 ///
 /// We add the inequality and mark it as restricted. We then try to make its
 /// sample value non-negative. If this is not possible, the tableau has become
 /// empty and we mark it as such.
-void Simplex::addInequality(ArrayRef<int64_t> coeffs) {
+void SimplexBase::addInequality(ArrayRef<int64_t> coeffs) {
   unsigned conIndex = addRow(coeffs);
   Unknown &u = con[conIndex];
   u.restricted = true;
   LogicalResult result = restoreRow(u);
   if (failed(result))
     markEmpty();
 }
 
 /// Add an equality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
 /// is the current number of variables, then the corresponding equality is
 /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0.
 ///
 /// We simply add two opposing inequalities, which force the expression to
 /// be zero.
-void Simplex::addEquality(ArrayRef<int64_t> coeffs) {
+void SimplexBase::addEquality(ArrayRef<int64_t> coeffs) {
   addInequality(coeffs);
   SmallVector<int64_t, 8> negatedCoeffs;
   for (int64_t coeff : coeffs)
     negatedCoeffs.emplace_back(-coeff);
   addInequality(negatedCoeffs);
 }
 
-unsigned Simplex::getNumVariables() const { return var.size(); }
-unsigned Simplex::getNumConstraints() const { return con.size(); }
+unsigned SimplexBase::getNumVariables() const { return var.size(); }
+unsigned SimplexBase::getNumConstraints() const { return con.size(); }
 
 /// Return a snapshot of the current state. This is just the current size of the
 /// undo log.
-unsigned Simplex::getSnapshot() const { return undoLog.size(); }
+unsigned SimplexBase::getSnapshot() const { return undoLog.size(); }
 
-void Simplex::undo(UndoLogEntry entry) {
+void SimplexBase::undo(UndoLogEntry entry) {
   if (entry == UndoLogEntry::RemoveLastConstraint) {
     Unknown &constraint = con.back();
     if (constraint.orientation == Orientation::Column) {
       unsigned column = constraint.pos;
       Optional<unsigned> row;
 
       // Try to find any pivot row for this column that preserves tableau
       // consistency (except possibly the column itself, which is going to be
if (entry == UndoLogEntry::RemoveLastConstraint) {
     nRedundant--;
   }
 }
 
 /// Rollback to the specified snapshot.
 ///
 /// We undo all the log entries until the log size when the snapshot was taken
 /// is reached.
-void Simplex::rollback(unsigned snapshot) {
+void SimplexBase::rollback(unsigned snapshot) {
   while (undoLog.size() > snapshot) {
     undo(undoLog.back());
     undoLog.pop_back();
   }
 }
 
-void Simplex::appendVariable(unsigned count) {
+void SimplexBase::appendVariable(unsigned count) {
   if (count == 0)
     return;
   var.reserve(var.size() + count);
   colUnknown.reserve(colUnknown.size() + count);
   for (unsigned i = 0; i < count; ++i) {
     nCol++;
     var.emplace_back(Orientation::Column, /*restricted=*/false,
                      /*pos=*/nCol - 1);
     colUnknown.push_back(var.size() - 1);
   }
   tableau.resizeHorizontally(nCol);
   undoLog.insert(undoLog.end(), count, UndoLogEntry::RemoveLastVariable);
 }
 
 /// Add all the constraints from the given FlatAffineConstraints.
-void Simplex::intersectFlatAffineConstraints(const FlatAffineConstraints &fac) {
+void SimplexBase::intersectFlatAffineConstraints(
+    const FlatAffineConstraints &fac) {
   assert(fac.getNumIds() == getNumVariables() &&
          "FlatAffineConstraints must have same dimensionality as simplex");
   for (unsigned i = 0, e = fac.getNumInequalities(); i < e; ++i)
     addInequality(fac.getInequality(i));
   for (unsigned i = 0, e = fac.getNumEqualities(); i < e; ++i)
     addEquality(fac.getEquality(i));
 }
 
Simplex Simplex::makeProduct(const Simplex &a, const Simplex &b) {
   for (unsigned row = a.nRedundant; row < a.nRow; ++row)
     appendRowFromA(row);
   for (unsigned row = b.nRedundant; row < b.nRow; ++row)
     appendRowFromB(row);
 
   return result;
 }
 
-SmallVector<Fraction, 8> Simplex::getRationalSample() const {
+SmallVector<Fraction, 8> SimplexBase::getRationalSample() const {
   assert(!empty && "This should not be called when Simplex is empty.");
 
   SmallVector<Fraction, 8> sample;
   sample.reserve(var.size());
   // Push the sample value for each variable into the vector.
   for (const Unknown &u : var) {
     if (u.orientation == Orientation::Column) {
       // If the variable is in column position, its sample value is zero.
       sample.emplace_back(0, 1);
     } else {
       // If the variable is in row position, its sample value is the entry in
       // the constant column divided by the entry in the common denominator
       // column.
       sample.emplace_back(tableau(u.pos, 1), tableau(u.pos, 0));
     }
   }
   return sample;
 }
 
-Optional<SmallVector<int64_t, 8>> Simplex::getSamplePointIfIntegral() const {
+Optional<SmallVector<int64_t, 8>>
+SimplexBase::getSamplePointIfIntegral() const {
   // If the tableau is empty, no sample point exists.
   if (empty)
     return {};
   SmallVector<Fraction, 8> rationalSample = getRationalSample();
   SmallVector<int64_t, 8> integerSample;
   integerSample.reserve(var.size());
   for (const Fraction &coord : rationalSample) {
     // If the sample is non-integral, return None.
if (Optional<Fraction> maybeMax =
           computeOptimum(Simplex::Direction::Up, coeffs))
     maxRoundedDown = floor(*maybeMax);
   else
     llvm_unreachable("Tableau should not be unbounded");
 
   return {minRoundedUp, maxRoundedDown};
 }
 
-void Simplex::print(raw_ostream &os) const {
+void SimplexBase::print(raw_ostream &os) const {
   os << "rows = " << nRow << ", columns = " << nCol << "\n";
   if (empty)
     os << "Simplex marked empty!\n";
   os << "var: ";
   for (unsigned i = 0; i < var.size(); ++i) {
     if (i > 0)
       os << ", ";
     var[i].print(os);
void SimplexBase::print(raw_ostream &os) const {
   for (unsigned row = 0; row < nRow; ++row) {
     for (unsigned col = 0; col < nCol; ++col)
       os << tableau(row, col) << '\t';
     os << '\n';
   }
   os << '\n';
 }
 
-void Simplex::dump() const { print(llvm::errs()); }
+void SimplexBase::dump() const { print(llvm::errs()); }
 
 bool Simplex::isRationalSubsetOf(const FlatAffineConstraints &fac) {
   if (isEmpty())
     return true;
 
   for (unsigned i = 0, e = fac.getNumInequalities(); i < e; ++i)
     if (!isRedundantInequality(fac.getInequality(i)))
       return false;