[MLIR][Presburger][Simplex] addSymbolicCut: don't add symbol div if denom is 1

[arjunp]

Summary

This is unncessary, so we remove it as an optimization.

[arjunp]

Fix a comment and drop the unnecessary qualification for addCut

[arjunp]

make -> construct

[Groverkss]

LGTM.

mlir/lib/Analysis/Presburger/Simplex.cpp

 }
 
 bool SymbolicLexSimplex::isSymbolicSampleIntegral(unsigned row) const {
   int64_t denom = tableau(row, 0);
   return tableau(row, 1) % denom == 0 &&
          isRangeDivisibleBy(tableau.getRow(row).slice(3, nSymbol), denom);
 }
 
-/// This proceeds similarly to LexSimplex::addCut(). We are given a row that has
-/// a symbolic sample value with fractional coefficients.
+/// This proceeds similarly to LexSimplexBase::addCut(). We are given a row that
+/// has a symbolic sample value with fractional coefficients.
 ///
 /// Let the row be
 /// (c + coeffM*M + sum_i a_i*s_i + sum_j b_j*y_j)/d,
 /// where s_1, ... s_m are the symbols and
 ///       y_1, ... y_n are the other basis unknowns.
 ///
 /// As in LexSimplex::addCut, for this to be an integer, we want
 ///
 /// coeffM*M + sum_j b_j*y_j = -c + sum_i (-a_i*s_i) (mod d)
 ///
 /// This time, a_1*s_1 + ... + a_m*s_m may not be an integer. We find that
 ///
 /// sum_i (b_i%d)y_i = ((-c%d) + sum_i (-a_i%d)s_i)%d + k*d for some integer k
 ///
 /// where we take a modulo of the whole symbolic expression on the right to
-/// bring it into the range [0, d - 1]. Therefore, as in LexSimplex::addCut,
+/// bring it into the range [0, d - 1]. Therefore, as in addCut(),
 /// k is the quotient on dividing the LHS by d, and since LHS >= 0, we have
-/// k >= 0 as well. We realize the modulo of the symbolic expression by adding a
-/// division variable
+/// k >= 0 as well. If all the a_i are divisible by d, then we can add the
+/// constraint directly.  Otherwise, we realize the modulo of the symbolic
+/// expression by adding a division variable
 ///
 /// q = ((-c%d) + sum_i (-a_i%d)s_i)/d
 ///
 /// to the symbol domain, so the equality becomes
 ///
 /// sum_i (b_i%d)y_i = (-c%d) + sum_i (-a_i%d)s_i - q*d + k*d for some integer k
 ///
 /// So the cut is
 /// (sum_i (b_i%d)y_i - (-c%d) - sum_i (-a_i%d)s_i + q*d)/d >= 0
 /// This constraint is violated when added so we immediately try to move it to a
 /// column.
 LogicalResult SymbolicLexSimplex::addSymbolicCut(unsigned row) {
   int64_t d = tableau(row, 0);
 
-  // Add the division variable `q` described above to the symbol domain.
-  // q = ((-c%d) + sum_i (-a_i%d)s_i)/d.
+  // Construct the division variable `q = ((-c%d) + sum_i (-a_i%d)s_i)/d`.
   SmallVector<int64_t, 8> divCoeffs;
   divCoeffs.reserve(nSymbol + 1);
   int64_t divDenom = d;
   for (unsigned col = 3; col < 3 + nSymbol; ++col)
     divCoeffs.push_back(mod(-tableau(row, col), divDenom)); // (-a_i%d)s_i
   divCoeffs.push_back(mod(-tableau(row, 1), divDenom));     // -c%d.
-
   normalizeDiv(divCoeffs, divDenom);
+
+  if (divDenom == 1) {
+    // The symbolic sample numerator is divisible by the denominator,
+    // so the division isn't needed. We can add the constraint directly,
+    // i.e., ignore the symbols and add a regular cut as in addCut().
+    return addCut(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);