[MLIR][Presburger] addSymbolicCut: fix the integral symbols heuristic to match the docs

[arjunp]

Summary

Previously this checked if the entire symbolic numerator was divisible by the
denominator, which is never the case when this function is called. Fixed this to
check only the non-const coefficients in the numerator, which was what was
intended and documented.

[Groverkss]

LGTM.

mlir/lib/Analysis/Presburger/Simplex.cpp

 /// 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);
+  if (isRangeDivisibleBy(tableau.getRow(row).slice(3, nSymbol), d)) {
+    // The coefficients of symbols in the symbol numerator are divisible
+    // by the denominator, so we can add the constraint directly,
+    // i.e., ignore the symbols and add a regular cut as in addCut().
+    return addCut(row);
+  }
 
   // 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);