@@ -1111,15 +1111,28 @@ unsigned IntegerRelation::gaussianEliminateVars(unsigned posStart,
11111111 return posLimit - posStart;
11121112}
11131113
1114+ static std::optional<unsigned >
1115+ findEqualityWithNonZeroAfterRow (IntegerRelation &rel, unsigned fromRow,
1116+ unsigned colIdx) {
1117+ assert (fromRow < rel.getNumVars () && colIdx < rel.getNumCols () &&
1118+ " position out of bounds" );
1119+ for (unsigned rowIdx = fromRow; rowIdx < rel.getNumEqualities (); ++rowIdx) {
1120+ if (rel.atEq (rowIdx, colIdx) != 0 )
1121+ return rowIdx;
1122+ }
1123+ return std::nullopt ;
1124+ }
1125+
11141126bool IntegerRelation::gaussianEliminate () {
11151127 gcdTightenInequalities ();
11161128 unsigned firstVar = 0 , vars = getNumVars ();
11171129 unsigned nowDone, eqs;
11181130 std::optional<unsigned > pivotRow;
11191131 for (nowDone = 0 , eqs = getNumEqualities (); nowDone < eqs; ++nowDone) {
1120- // Finds the first non-empty column.
1132+ // Finds the first non-empty column that we haven't dealt with .
11211133 for (; firstVar < vars; ++firstVar) {
1122- if ((pivotRow = findConstraintWithNonZeroAt (firstVar, /* isEq=*/ true )))
1134+ if ((pivotRow =
1135+ findEqualityWithNonZeroAfterRow (*this , nowDone, firstVar)))
11231136 break ;
11241137 }
11251138 // The matrix has been normalized to row echelon form.
@@ -1142,6 +1155,10 @@ bool IntegerRelation::gaussianEliminate() {
11421155 inequalities.normalizeRow (i);
11431156 }
11441157 gcdTightenInequalities ();
1158+
1159+ // The column is finished. Tell the next iteration to start at the next
1160+ // column.
1161+ firstVar++;
11451162 }
11461163
11471164 // No redundant rows.
0 commit comments