[Mlir-commits] [mlir] ef8b2a7 - [MLIR][Presburger] addSymbolicCut: fix the integral symbols heuristic to match the docs

[Arjun P]

Author: Arjun P
Date: 2022-04-15T20:34:06+01:00
New Revision: ef8b2a7cea2e12653d812f173370fda7b955fd22

URL: https://github.com/llvm/llvm-project/commit/ef8b2a7cea2e12653d812f173370fda7b955fd22
DIFF: https://github.com/llvm/llvm-project/commit/ef8b2a7cea2e12653d812f173370fda7b955fd22.diff

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

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.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D123592

Added: 
    

Modified: 
    mlir/lib/Analysis/Presburger/Simplex.cpp

Removed: 
    


################################################################################
diff  --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp
index c274ae259940d..45b1a26e79cf0 100644
--- a/mlir/lib/Analysis/Presburger/Simplex.cpp
+++ b/mlir/lib/Analysis/Presburger/Simplex.cpp
@@ -394,6 +394,12 @@ bool SymbolicLexSimplex::isSymbolicSampleIntegral(unsigned row) const {
 /// 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;
@@ -404,13 +410,6 @@ LogicalResult SymbolicLexSimplex::addSymbolicCut(unsigned row) {
   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);