[MLIR][Presburger] Simplex: remove redundant member vars nRow, nCol

[Groverkss]

mlir/lib/Analysis/Presburger/Simplex.cpp

60

Instead of tableau.getNumColumns, do you think it would make sense to have a Simplex::getNumColumns and call that instead?

[arjunp]

Incorporate Kunwar's comment

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

protected:
   /// Returns the unknown associated with index.
   Unknown &unknownFromIndex(int index);
   /// Returns the unknown associated with col.
   Unknown &unknownFromColumn(unsigned col);
   /// Returns the unknown associated with row.
   Unknown &unknownFromRow(unsigned row);
 
   /// Add a new row to the tableau and the associated data structures. The row
-  /// is initialized to zero.
+  /// is initialized to zero. Returns the index of the added row.
   unsigned addZeroRow(bool makeRestricted = false);
 
   /// Add a new row to the tableau and the associated data structures.
   /// The new row is considered to be a constraint; the new Unknown lives in
   /// con.
   ///
   /// Returns the index of the new Unknown in con.
   unsigned addRow(ArrayRef<int64_t> coeffs, bool makeRestricted = false);
protected:
   void removeLastConstraintRowOrientation();
 
   /// Undo the operation represented by the log entry.
   void undo(UndoLogEntry entry);
 
   /// Return the number of fixed columns, as described in the constructor above,
   /// this is the number of columns beyond those for the variables in var.
   unsigned getNumFixedCols() const { return usingBigM ? 3u : 2u; }
+  unsigned getNumRows() const { return tableau.getNumRows(); }
+  unsigned getNumColumns() const { return tableau.getNumColumns(); }
 
   /// Stores whether or not a big M column is present in the tableau.
   bool usingBigM;
 
-  /// 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
   /// nRedundant rows.
   unsigned nRedundant;
 
   /// The number of parameters. This must be consistent with the number of
   /// Unknowns in `var` below that have `isSymbol` set to true.
   unsigned nSymbol;
 

mlir/lib/Analysis/Presburger/Simplex.cpp

scaleAndAddForAssert(ArrayRef<int64_t> a, int64_t scale, ArrayRef<int64_t> b) {
   res.reserve(a.size());
   for (unsigned i = 0, e = a.size(); i < e; ++i)
     res.push_back(a[i] + scale * b[i]);
   return res;
 }
 
 SimplexBase::SimplexBase(unsigned nVar, bool mustUseBigM, unsigned symbolOffset,
                          unsigned nSymbol)
-    : usingBigM(mustUseBigM), nRow(0), nCol(getNumFixedCols() + nVar),
-      nRedundant(0), nSymbol(nSymbol), tableau(0, nCol), empty(false) {
+    : usingBigM(mustUseBigM), nRedundant(0), nSymbol(nSymbol),
+      tableau(0, getNumFixedCols() + nVar), empty(false) {
   assert(symbolOffset + nSymbol <= nVar);
 
   colUnknown.insert(colUnknown.begin(), getNumFixedCols(), nullIndex);
   for (unsigned i = 0; i < nVar; ++i) {
     var.emplace_back(Orientation::Column, /*restricted=*/false,
                      /*pos=*/getNumFixedCols() + i);
     colUnknown.push_back(i);
   }
 
   // Move the symbols to be in columns [3, 3 + nSymbol).
   for (unsigned i = 0; i < nSymbol; ++i) {
     var[symbolOffset + i].isSymbol = true;
     swapColumns(var[symbolOffset + i].pos, getNumFixedCols() + i);
   }
 }
 
 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 &SimplexBase::unknownFromColumn(unsigned col) const {
-  assert(col < nCol && "Invalid column");
+  assert(col < getNumColumns() && "Invalid column");
   return unknownFromIndex(colUnknown[col]);
 }
 
 const Simplex::Unknown &SimplexBase::unknownFromRow(unsigned row) const {
-  assert(row < nRow && "Invalid row");
+  assert(row < getNumRows() && "Invalid row");
   return unknownFromIndex(rowUnknown[row]);
 }
 
 Simplex::Unknown &SimplexBase::unknownFromIndex(int index) {
   assert(index != nullIndex && "nullIndex passed to unknownFromIndex");
   return index >= 0 ? var[index] : con[~index];
 }
 
 Simplex::Unknown &SimplexBase::unknownFromColumn(unsigned col) {
-  assert(col < nCol && "Invalid column");
+  assert(col < getNumColumns() && "Invalid column");
   return unknownFromIndex(colUnknown[col]);
 }
 
 Simplex::Unknown &SimplexBase::unknownFromRow(unsigned row) {
-  assert(row < nRow && "Invalid row");
+  assert(row < getNumRows() && "Invalid row");
   return unknownFromIndex(rowUnknown[row]);
 }
 
 unsigned SimplexBase::addZeroRow(bool makeRestricted) {
-  ++nRow;
   // Resize the tableau to accommodate the extra row.
-  tableau.resizeVertically(nRow);
-  // TODO: consider eliminating nRow, as it stores redundant information.
-  assert(tableau.getNumRows() == nRow && "Inconsistent tableau size");
+  unsigned newRow = tableau.appendExtraRow();
+  assert(getNumRows() == getNumRows() && "Inconsistent tableau size");
   rowUnknown.push_back(~con.size());
-  con.emplace_back(Orientation::Row, makeRestricted, nRow - 1);
+  con.emplace_back(Orientation::Row, makeRestricted, newRow);
   undoLog.push_back(UndoLogEntry::RemoveLastConstraint);
-  tableau(nRow - 1, 0) = 1;
-  return con.size() - 1;
+  tableau(newRow, 0) = 1;
+  return newRow;
 }
 
 /// 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 SimplexBase::addRow(ArrayRef<int64_t> coeffs, bool makeRestricted) {
   assert(coeffs.size() == var.size() + 1 &&
          "Incorrect number of coefficients!");
+  assert(var.size() + getNumFixedCols() == getNumColumns() &&
+         "inconsistent column count!");
 
-  addZeroRow(makeRestricted);
-  tableau(nRow - 1, 1) = coeffs.back();
+  unsigned newRow = addZeroRow(makeRestricted);
+  tableau(newRow, 1) = coeffs.back();
   if (usingBigM) {
     // When the lexicographic pivot rule is used, instead of the variables
     //
     // x, y, z ...
     //
     // we internally use the variables
     //
     // M, M + x, M + y, M + z, ...
     //
     // where M is the big M parameter. As such, when the user tries to add
     // a row ax + by + cz + d, we express it in terms of our internal variables
     // as -(a + b + c)M + a(M + x) + b(M + y) + c(M + z) + d.
     //
     // Symbols don't use the big M parameter since they do not get lex
     // optimized.
     int64_t bigMCoeff = 0;
     for (unsigned i = 0; i < coeffs.size() - 1; ++i)
       if (!var[i].isSymbol)
         bigMCoeff -= coeffs[i];
     // The coefficient to the big M parameter is stored in column 2.
-    tableau(nRow - 1, 2) = bigMCoeff;
+    tableau(newRow, 2) = bigMCoeff;
   }
 
   // Process each given variable coefficient.
   for (unsigned i = 0; i < var.size(); ++i) {
     unsigned pos = var[i].pos;
     if (coeffs[i] == 0)
       continue;
 
     if (var[i].orientation == Orientation::Column) {
       // If a variable is in column position at column col, then we just add the
       // coefficient for that variable (scaled by the common row denominator) to
       // the corresponding entry in the new row.
-      tableau(nRow - 1, pos) += coeffs[i] * tableau(nRow - 1, 0);
+      tableau(newRow, pos) += coeffs[i] * tableau(newRow, 0);
       continue;
     }
 
     // If the variable is in row position, we need to add that row to the new
     // row, scaled by the coefficient for the variable, accounting for the two
     // rows potentially having different denominators. The new denominator is
     // the lcm of the two.
-    int64_t lcm = mlir::lcm(tableau(nRow - 1, 0), tableau(pos, 0));
-    int64_t nRowCoeff = lcm / tableau(nRow - 1, 0);
+    int64_t lcm = mlir::lcm(tableau(newRow, 0), tableau(pos, 0));
+    int64_t nRowCoeff = lcm / tableau(newRow, 0);
     int64_t idxRowCoeff = coeffs[i] * (lcm / tableau(pos, 0));
-    tableau(nRow - 1, 0) = lcm;
-    for (unsigned col = 1; col < nCol; ++col)
-      tableau(nRow - 1, col) =
-          nRowCoeff * tableau(nRow - 1, col) + idxRowCoeff * tableau(pos, col);
+    tableau(newRow, 0) = lcm;
+    for (unsigned col = 1, e = getNumColumns(); col < e; ++col)
+      tableau(newRow, col) =
+          nRowCoeff * tableau(newRow, col) + idxRowCoeff * tableau(pos, col);
   }
 
-  tableau.normalizeRow(nRow - 1);
+  tableau.normalizeRow(newRow);
   // Push to undo log along with the index of the new constraint.
   return con.size() - 1;
 }
 
 namespace {
 bool signMatchesDirection(int64_t elem, Direction direction) {
   assert(elem != 0 && "elem should not be 0");
   return direction == Direction::Up ? elem > 0 : elem < 0;

 ///
 /// So we have
 /// ((b_1%d)y_1 + ... + (b_n%d)y_n - (-c%d))/d >= 0.
 ///
 /// The constraint is violated when added (it would be useless otherwise)
 /// so we immediately try to move it to a column.
 LogicalResult LexSimplexBase::addCut(unsigned row) {
   int64_t d = tableau(row, 0);
-  addZeroRow(/*makeRestricted=*/true);
-  tableau(nRow - 1, 0) = d;
-  tableau(nRow - 1, 1) = -mod(-tableau(row, 1), d); // -c%d.
-  tableau(nRow - 1, 2) = 0;
-  for (unsigned col = 3 + nSymbol; col < nCol; ++col)
-    tableau(nRow - 1, col) = mod(tableau(row, col), d); // b_i%d.
-  return moveRowUnknownToColumn(nRow - 1);
+  unsigned cutRow = addZeroRow(/*makeRestricted=*/true);
+  tableau(cutRow, 0) = d;
+  tableau(cutRow, 1) = -mod(-tableau(row, 1), d); // -c%d.
+  tableau(cutRow, 2) = 0;
+  for (unsigned col = 3 + nSymbol, e = getNumColumns(); col < e; ++col)
+    tableau(cutRow, col) = mod(tableau(row, col), d); // b_i%d.
+  return moveRowUnknownToColumn(cutRow);
 }
 
 Optional<unsigned> LexSimplex::maybeGetNonIntegralVarRow() const {
   for (const Unknown &u : var) {
     if (u.orientation == Orientation::Column)
       continue;
     // If the sample value is of the form (a/d)M + b/d, we need b to be
     // divisible by d. We assume M contains all possible
SymbolicLexSimplex::getSymbolicSampleIneq(unsigned row) const {
   SmallVector<int64_t, 8> sample = getSymbolicSampleNumerator(row);
   // The inequality is equivalent to the GCD-normalized one.
   normalizeRange(sample);
   return sample;
 }
 
 void LexSimplexBase::appendSymbol() {
   appendVariable();
-  swapColumns(3 + nSymbol, nCol - 1);
+  swapColumns(3 + nSymbol, getNumColumns() - 1);
   var.back().isSymbol = true;
   nSymbol++;
 }
 
 static bool isRangeDivisibleBy(ArrayRef<int64_t> range, int64_t divisor) {
   assert(divisor > 0 && "divisor must be positive!");
   return llvm::all_of(range, [divisor](int64_t x) { return x % divisor == 0; });
 }
LogicalResult SymbolicLexSimplex::addSymbolicCut(unsigned row) {
 
   domainSimplex.addDivisionVariable(divCoeffs, divDenom);
   domainPoly.addLocalFloorDiv(divCoeffs, divDenom);
 
   // Update `this` to account for the additional symbol we just added.
   appendSymbol();
 
   // Add the cut (sum_i (b_i%d)y_i - (-c%d) + sum_i -(-a_i%d)s_i + q*d)/d >= 0.
-  addZeroRow(/*makeRestricted=*/true);
-  tableau(nRow - 1, 0) = d;
-  tableau(nRow - 1, 2) = 0;
+  unsigned cutRow = addZeroRow(/*makeRestricted=*/true);
+  tableau(cutRow, 0) = d;
+  tableau(cutRow, 2) = 0;
 
-  tableau(nRow - 1, 1) = -mod(-tableau(row, 1), d); // -(-c%d).
+  tableau(cutRow, 1) = -mod(-tableau(row, 1), d); // -(-c%d).
   for (unsigned col = 3; col < 3 + nSymbol - 1; ++col)
-    tableau(nRow - 1, col) = -mod(-tableau(row, col), d); // -(-a_i%d)s_i.
-  tableau(nRow - 1, 3 + nSymbol - 1) = d;                 // q*d.
+    tableau(cutRow, col) = -mod(-tableau(row, col), d); // -(-a_i%d)s_i.
+  tableau(cutRow, 3 + nSymbol - 1) = d;                 // q*d.
 
-  for (unsigned col = 3 + nSymbol; col < nCol; ++col)
-    tableau(nRow - 1, col) = mod(tableau(row, col), d); // (b_i%d)y_i.
-  return moveRowUnknownToColumn(nRow - 1);
+  for (unsigned col = 3 + nSymbol, e = getNumColumns(); col < e; ++col)
+    tableau(cutRow, col) = mod(tableau(row, col), d); // (b_i%d)y_i.
+  return moveRowUnknownToColumn(cutRow);
 }
 
 void SymbolicLexSimplex::recordOutput(SymbolicLexMin &result) const {
   Matrix output(0, domainPoly.getNumIds() + 1);
   output.reserveRows(result.lexmin.getNumOutputs());
   for (const Unknown &u : var) {
     if (u.isSymbol)
       continue;
for (const Unknown &u : var) {
     output.appendExtraRow(sample);
   }
   result.lexmin.addPiece(domainPoly, output);
 }
 
 Optional<unsigned> SymbolicLexSimplex::maybeGetAlwaysViolatedRow() {
   // First look for rows that are clearly violated just from the big M
   // coefficient, without needing to perform any simplex queries on the domain.
-  for (unsigned row = 0; row < nRow; ++row)
+  for (unsigned row = 0, e = getNumRows(); row < e; ++row)
     if (tableau(row, 2) < 0)
       return row;
 
-  for (unsigned row = 0; row < nRow; ++row) {
+  for (unsigned row = 0, e = getNumRows(); row < e; ++row) {
     if (tableau(row, 2) > 0)
       continue;
     if (domainSimplex.isSeparateInequality(getSymbolicSampleIneq(row))) {
       // Sample numerator always takes negative values in the symbol domain.
       return row;
     }
   }
   return {};
if (level > stack.size()) {
       }
 
       if (doNonBranchingPivots().failed()) {
         // Could not find pivots for violated constraints; return.
         --level;
         continue;
       }
 
-      unsigned splitRow;
       SmallVector<int64_t, 8> symbolicSample;
-      for (splitRow = 0; splitRow < nRow; ++splitRow) {
+      unsigned splitRow = 0;
+      for (unsigned e = getNumRows(); splitRow < e; ++splitRow) {
         if (tableau(splitRow, 2) > 0)
           continue;
         assert(tableau(splitRow, 2) == 0 &&
                "Non-branching pivots should have been handled already!");
 
         symbolicSample = getSymbolicSampleIneq(splitRow);
         if (domainSimplex.isRedundantInequality(symbolicSample))
           continue;
 
         // It's neither redundant nor separate, so it takes both positive and
         // negative values, and hence constitutes a row for which we need to
         // split the domain and separately run each case.
         assert(!domainSimplex.isSeparateInequality(symbolicSample) &&
                "Non-branching pivots should have been handled already!");
         break;
       }
 
-      if (splitRow < nRow) {
+      if (splitRow < getNumRows()) {
         unsigned domainSnapshot = domainSimplex.getSnapshot();
         IntegerRelation::CountsSnapshot domainPolyCounts =
             domainPoly.getCounts();
 
         // First, we consider the part of the domain where the row is not
         // violated. We don't have to do any pivots for the row in this case,
         // but we record the additional constraint that defines this part of
         // the domain.
bool LexSimplex::rowIsViolated(unsigned row) const {
   if (tableau(row, 2) < 0)
     return true;
   if (tableau(row, 2) == 0 && tableau(row, 1) < 0)
     return true;
   return false;
 }
 
 Optional<unsigned> LexSimplex::maybeGetViolatedRow() const {
-  for (unsigned row = 0; row < nRow; ++row)
+  for (unsigned row = 0, e = getNumRows(); row < e; ++row)
     if (rowIsViolated(row))
       return row;
   return {};
 }
 
 /// We simply look for violated rows and keep trying to move them to column
 /// orientation, which always succeeds unless the constraints have no solution
 /// in which case we just give up and return.

 // 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) {
+  for (unsigned col = 3 + nSymbol, e = getNumColumns(); col < e; ++col) {
     if (tableau(row, col) <= 0)
       continue;
     maybeColumn =
         !maybeColumn ? col : getLexMinPivotColumn(row, *maybeColumn, col);
   }
 
   if (!maybeColumn)
     return failure();

 /// 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<SimplexBase::Pivot> Simplex::findPivot(int row,
                                                 Direction direction) const {
   Optional<unsigned> col;
-  for (unsigned j = 2; j < nCol; ++j) {
+  for (unsigned j = 2, e = getNumColumns(); j < e; ++j) {
     int64_t elem = tableau(row, j);
     if (elem == 0)
       continue;
 
     if (unknownFromColumn(j).restricted &&
         !signMatchesDirection(elem, direction))
       continue;
     if (!col || colUnknown[j] < colUnknown[*col])
void SimplexBase::pivot(unsigned pivotRow, unsigned 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.
     tableau(pivotRow, 0) = -tableau(pivotRow, 0);
     tableau(pivotRow, pivotCol) = -tableau(pivotRow, pivotCol);
   } else {
-    for (unsigned col = 1; col < nCol; ++col) {
+    for (unsigned col = 1, e = getNumColumns(); col < e; ++col) {
       if (col == pivotCol)
         continue;
       tableau(pivotRow, col) = -tableau(pivotRow, col);
     }
   }
   tableau.normalizeRow(pivotRow);
 
-  for (unsigned row = 0; row < nRow; ++row) {
+  for (unsigned row = 0, numRows = getNumRows(); row < numRows; ++row) {
     if (row == pivotRow)
       continue;
     if (tableau(row, pivotCol) == 0) // Nothing to do.
       continue;
     tableau(row, 0) *= tableau(pivotRow, 0);
-    for (unsigned j = 1; j < nCol; ++j) {
-      if (j == pivotCol)
+    for (unsigned col = 1, numCols = getNumColumns(); col < numCols; ++col) {
+      if (col == pivotCol)
         continue;
       // Add rather than subtract because the pivot row has been negated.
-      tableau(row, j) = tableau(row, j) * tableau(pivotRow, 0) +
-                        tableau(row, pivotCol) * tableau(pivotRow, j);
+      tableau(row, col) = tableau(row, col) * tableau(pivotRow, 0) +
+                          tableau(row, pivotCol) * tableau(pivotRow, col);
     }
     tableau(row, pivotCol) *= tableau(pivotRow, pivotCol);
     tableau.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
Optional<unsigned> Simplex::findPivotRow(Optional<unsigned> skipRow,
                                          Direction direction,
                                          unsigned col) const {
   Optional<unsigned> retRow;
   // Initialize these to zero in order to silence a warning about retElem and
   // retConst being used uninitialized in the initialization of `diff` below. In
   // reality, these are always initialized when that line is reached since these
   // are set whenever retRow is set.
   int64_t retElem = 0, retConst = 0;
-  for (unsigned row = nRedundant; row < nRow; ++row) {
+  for (unsigned row = nRedundant, e = getNumRows(); row < e; ++row) {
     if (skipRow && row == *skipRow)
       continue;
     int64_t elem = tableau(row, col);
     if (elem == 0)
       continue;
     if (!unknownFromRow(row).restricted)
       continue;
     if (signMatchesDirection(elem, direction))
if (i == j)
     return;
   tableau.swapRows(i, j);
   std::swap(rowUnknown[i], rowUnknown[j]);
   unknownFromRow(i).pos = i;
   unknownFromRow(j).pos = j;
 }
 
 void SimplexBase::swapColumns(unsigned i, unsigned j) {
-  assert(i < nCol && j < nCol && "Invalid columns provided!");
+  assert(i < getNumColumns() && j < getNumColumns() &&
+         "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;
 }
 
unsigned SimplexBase::getSnapshotBasis() {
   return undoLog.size() - 1;
 }
 
 void SimplexBase::removeLastConstraintRowOrientation() {
   assert(con.back().orientation == Orientation::Row);
 
   // Move this unknown to the last row and remove the last row from the
   // tableau.
-  swapRows(con.back().pos, nRow - 1);
+  swapRows(con.back().pos, getNumRows() - 1);
   // It is not strictly necessary to shrink the tableau, but for now we
-  // maintain the invariant that the tableau has exactly nRow rows.
-  tableau.resizeVertically(nRow - 1);
-  nRow--;
-  assert(tableau.getNumRows() == nRow && "inconsistent tableau size!");
+  // maintain the invariant that the tableau has exactly getNumRows()
+  // rows.
+  tableau.resizeVertically(getNumRows() - 1);
   rowUnknown.pop_back();
   con.pop_back();
 }
 
 // This doesn't find a pivot row only if the column has zero
 // coefficients for every row.
 //
 // If the unknown is a constraint, this can't happen, since it was added
 // initially as a row. Such a row could never have been pivoted to a column. So
 // a pivot row will always be found if we have a constraint.
 //
 // If we have a variable, then the column has zero coefficients for every row
 // iff no constraints have been added with a non-zero coefficient for this row.
 Optional<unsigned> SimplexBase::findAnyPivotRow(unsigned col) {
-  for (unsigned row = nRedundant; row < nRow; ++row)
+  for (unsigned row = nRedundant, e = getNumRows(); row < e; ++row)
     if (tableau(row, col) != 0)
       return row;
   return {};
 }
 
 // It's not valid to remove the constraint by deleting the column since this
 // would result in an invalid basis.
 void Simplex::undoLastConstraint() {
if (entry == UndoLogEntry::RemoveLastConstraint) {
     assert(var.back().orientation == Orientation::Column &&
            "Variable to be removed must be in column orientation!");
 
     if (var.back().isSymbol)
       nSymbol--;
 
     // Move this variable to the last column and remove the column from the
     // tableau.
-    swapColumns(var.back().pos, nCol - 1);
-    tableau.resizeHorizontally(nCol - 1);
+    swapColumns(var.back().pos, getNumColumns() - 1);
+    tableau.resizeHorizontally(getNumColumns() - 1);
     var.pop_back();
     colUnknown.pop_back();
-    nCol--;
-    assert(tableau.getNumColumns() == nCol && "inconsistent tableau size!");
   } else if (entry == UndoLogEntry::UnmarkEmpty) {
     empty = false;
   } else if (entry == UndoLogEntry::UnmarkLastRedundant) {
     nRedundant--;
   } else if (entry == UndoLogEntry::RestoreBasis) {
     assert(!savedBases.empty() && "No bases saved!");
 
     SmallVector<int, 8> basis = std::move(savedBases.back());
     savedBases.pop_back();
 
     for (int index : basis) {
       Unknown &u = unknownFromIndex(index);
       if (u.orientation == Orientation::Column)
         continue;
-      for (unsigned col = getNumFixedCols(); col < nCol; col++) {
+      for (unsigned col = getNumFixedCols(), e = getNumColumns(); col < e;
+           col++) {
         assert(colUnknown[col] != nullIndex &&
                "Column should not be a fixed column!");
         if (std::find(basis.begin(), basis.end(), colUnknown[col]) !=
             basis.end())
           continue;
         if (tableau(u.pos, col) == 0)
           continue;
         pivot(u.pos, col);

 }
 
 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);
+                     /*pos=*/getNumColumns() + i);
     colUnknown.push_back(var.size() - 1);
   }
-  tableau.resizeHorizontally(nCol);
-  assert(tableau.getNumColumns() == nCol);
+  tableau.resizeHorizontally(getNumColumns() + count);
   undoLog.insert(undoLog.end(), count, UndoLogEntry::RemoveLastVariable);
 }
 
 /// Add all the constraints from the given IntegerRelation.
 void SimplexBase::intersectIntegerRelation(const IntegerRelation &rel) {
   assert(rel.getNumIds() == getNumVariables() &&
          "IntegerRelation must have same dimensionality as simplex");
   for (unsigned i = 0, e = rel.getNumInequalities(); i < e; ++i)

 ///
 /// It has column layout:
 ///   denominator, constant, A's columns, B's columns.
 Simplex Simplex::makeProduct(const Simplex &a, const Simplex &b) {
   unsigned numVar = a.getNumVariables() + b.getNumVariables();
   unsigned numCon = a.getNumConstraints() + b.getNumConstraints();
   Simplex result(numVar);
 
-  result.tableau.resizeVertically(numCon);
+  result.tableau.reserveRows(numCon);
   result.empty = a.empty || b.empty;
 
   auto concat = [](ArrayRef<Unknown> v, ArrayRef<Unknown> w) {
     SmallVector<Unknown, 8> result;
     result.reserve(v.size() + w.size());
     result.insert(result.end(), v.begin(), v.end());
     result.insert(result.end(), w.begin(), w.end());
     return result;
   };
   result.con = concat(a.con, b.con);
   result.var = concat(a.var, b.var);
 
   auto indexFromBIndex = [&](int index) {
     return index >= 0 ? a.getNumVariables() + index
                       : ~(a.getNumConstraints() + ~index);
   };
 
   result.colUnknown.assign(2, nullIndex);
-  for (unsigned i = 2; i < a.nCol; ++i) {
+  for (unsigned i = 2, e = a.getNumColumns(); i < e; ++i) {
     result.colUnknown.push_back(a.colUnknown[i]);
     result.unknownFromIndex(result.colUnknown.back()).pos =
         result.colUnknown.size() - 1;
   }
-  for (unsigned i = 2; i < b.nCol; ++i) {
+  for (unsigned i = 2, e = b.getNumColumns(); i < e; ++i) {
     result.colUnknown.push_back(indexFromBIndex(b.colUnknown[i]));
     result.unknownFromIndex(result.colUnknown.back()).pos =
         result.colUnknown.size() - 1;
   }
 
   auto appendRowFromA = [&](unsigned row) {
-    for (unsigned col = 0; col < a.nCol; ++col)
-      result.tableau(result.nRow, col) = a.tableau(row, col);
+    unsigned resultRow = result.tableau.appendExtraRow();
+    for (unsigned col = 0, e = a.getNumColumns(); col < e; ++col)
+      result.tableau(resultRow, col) = a.tableau(row, col);
     result.rowUnknown.push_back(a.rowUnknown[row]);
     result.unknownFromIndex(result.rowUnknown.back()).pos =
         result.rowUnknown.size() - 1;
-    result.nRow++;
   };
 
   // Also fixes the corresponding entry in rowUnknown and var/con (as the case
   // may be).
   auto appendRowFromB = [&](unsigned row) {
-    result.tableau(result.nRow, 0) = b.tableau(row, 0);
-    result.tableau(result.nRow, 1) = b.tableau(row, 1);
-
-    unsigned offset = a.nCol - 2;
-    for (unsigned col = 2; col < b.nCol; ++col)
-      result.tableau(result.nRow, offset + col) = b.tableau(row, col);
+    unsigned resultRow = result.tableau.appendExtraRow();
+    result.tableau(resultRow, 0) = b.tableau(row, 0);
+    result.tableau(resultRow, 1) = b.tableau(row, 1);
+
+    unsigned offset = a.getNumColumns() - 2;
+    for (unsigned col = 2, e = b.getNumColumns(); col < e; ++col)
+      result.tableau(resultRow, offset + col) = b.tableau(row, col);
     result.rowUnknown.push_back(indexFromBIndex(b.rowUnknown[row]));
     result.unknownFromIndex(result.rowUnknown.back()).pos =
         result.rowUnknown.size() - 1;
-    result.nRow++;
   };
 
   result.nRedundant = a.nRedundant + b.nRedundant;
   for (unsigned row = 0; row < a.nRedundant; ++row)
     appendRowFromA(row);
   for (unsigned row = 0; row < b.nRedundant; ++row)
     appendRowFromB(row);
-  for (unsigned row = a.nRedundant; row < a.nRow; ++row)
+  for (unsigned row = a.nRedundant, e = a.getNumRows(); row < e; ++row)
     appendRowFromA(row);
-  for (unsigned row = b.nRedundant; row < b.nRow; ++row)
+  for (unsigned row = b.nRedundant, e = b.getNumRows(); row < e; ++row)
     appendRowFromB(row);
 
-  assert(result.tableau.getNumRows() == result.nRow &&
-         "inconsistent row size!");
-  assert(result.tableau.getNumColumns() == result.nCol &&
-         "inconsistent row size!");
   return result;
 }
 
 Optional<SmallVector<Fraction, 8>> Simplex::getRationalSample() const {
   if (empty)
     return {};
 
   SmallVector<Fraction, 8> sample;
Simplex::computeIntegerBounds(ArrayRef<int64_t> coeffs) {
   MaybeOptimum<int64_t> minRoundedUp(
       computeOptimum(Simplex::Direction::Down, coeffs).map(ceil));
   MaybeOptimum<int64_t> maxRoundedDown(
       computeOptimum(Simplex::Direction::Up, coeffs).map(floor));
   return {minRoundedUp, maxRoundedDown};
 }
 
 void SimplexBase::print(raw_ostream &os) const {
-  os << "rows = " << nRow << ", columns = " << nCol << "\n";
+  os << "rows = " << getNumRows() << ", columns = " << getNumColumns() << "\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);
   }
   os << "\ncon: ";
   for (unsigned i = 0; i < con.size(); ++i) {
     if (i > 0)
       os << ", ";
     con[i].print(os);
   }
   os << '\n';
-  for (unsigned row = 0; row < nRow; ++row) {
+  for (unsigned row = 0, e = getNumRows(); row < e; ++row) {
     if (row > 0)
       os << ", ";
     os << "r" << row << ": " << rowUnknown[row];
   }
   os << '\n';
   os << "c0: denom, c1: const";
-  for (unsigned col = 2; col < nCol; ++col)
+  for (unsigned col = 2, e = getNumColumns(); col < e; ++col)
     os << ", c" << col << ": " << colUnknown[col];
   os << '\n';
-  for (unsigned row = 0; row < nRow; ++row) {
-    for (unsigned col = 0; col < nCol; ++col)
+  for (unsigned row = 0, numRows = getNumRows(); row < numRows; ++row) {
+    for (unsigned col = 0, numCols = getNumColumns(); col < numCols; ++col)
       os << tableau(row, col) << '\t';
     os << '\n';
   }
   os << '\n';
 }
 
 void SimplexBase::dump() const { print(llvm::errs()); }