[MLIR][Presburger] Fix Gaussian elimination

[AdUhTkJm]

In the Presburger library, there are two minor bugs of Gaussian elimination.

In Barvinok.cpp, the if (equations(i, i) != 0) continue; is intended to skip only the row-swapping, but it in fact skipped the whole loop body altogether, including the elimination parts.

In IntegerRelation.cpp, the Gaussian elimination forgets to advance firstVar (the number of finished columns) when it finishes a column. Moreover, when it checks the pivot row of each column, it didn't ignore the rows considered.

As an example, suppose the constraints are

1 0 0 1 2 = 0
0 1 0 0 3 = 0
0 0 0 1 4 = 0
...

For the 4th column, it will think the pivot is the first row 1 0 0 1 2 = 0, rather than the correct 3rd row 0 0 0 1 4 = 0.

(This bug is left undiscovered, because if we don't advance firstVar then this Gaussian elimination process will simply do nothing. Moreover, it is called only in simplify(), and the existing test cases doesn't care whether a set has been simplified.)

[llvmbot]

@llvm/pr-subscribers-mlir-presburger

Author: Yue Huang (AdUhTkJm)

Changes

In the Presburger library, there are two minor bugs of Gaussian elimination.

In Barvinok.cpp, the if (equations(i, i) != 0) continue; is intended to skip only the row-swapping, but it in fact skipped the whole loop body, altogether with the elimination parts.

In IntegerRelation.cpp, the Gaussian elimination forgets to advance firstVar (the number of finished columns) when it finishes a column.

P.S. I have tested that the implementation works, but how might I add test cases for it? I don't think we have related tests in mlir/test.

---

Full diff: https://github.com/llvm/llvm-project/pull/164437.diff

2 Files Affected:

• (modified) mlir/lib/Analysis/Presburger/Barvinok.cpp (+7-7)
• (modified) mlir/lib/Analysis/Presburger/IntegerRelation.cpp (+4)

diff --git a/mlir/lib/Analysis/Presburger/Barvinok.cpp b/mlir/lib/Analysis/Presburger/Barvinok.cpp
index 75d592e976edf..c31b27794f01e 100644
--- a/mlir/lib/Analysis/Presburger/Barvinok.cpp
+++ b/mlir/lib/Analysis/Presburger/Barvinok.cpp
@@ -178,13 +178,13 @@ mlir::presburger::detail::solveParametricEquations(FracMatrix equations) {
   for (unsigned i = 0; i < d; ++i) {
     // First ensure that the diagonal element is nonzero, by swapping
     // it with a row that is non-zero at column i.
-    if (equations(i, i) != 0)
-      continue;
-    for (unsigned j = i + 1; j < d; ++j) {
-      if (equations(j, i) == 0)
-        continue;
-      equations.swapRows(j, i);
-      break;
+    if (equations(i, i) == 0) {
+      for (unsigned j = i + 1; j < d; ++j) {
+        if (equations(j, i) == 0)
+          continue;
+        equations.swapRows(j, i);
+        break;
+      }
     }
 
     Fraction diagElement = equations(i, i);
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index 0dcdd5bb97bc8..7bafd070d13d3 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -1142,6 +1142,10 @@ bool IntegerRelation::gaussianEliminate() {
       inequalities.normalizeRow(i);
     }
     gcdTightenInequalities();
+
+    // The column is finished. Tell the next iteration to start at the next
+    // column.
+    firstVar++;
   }
 
   // No redundant rows.

[llvmbot]

@llvm/pr-subscribers-mlir

Author: Yue Huang (AdUhTkJm)

Changes

In the Presburger library, there are two minor bugs of Gaussian elimination.

In Barvinok.cpp, the if (equations(i, i) != 0) continue; is intended to skip only the row-swapping, but it in fact skipped the whole loop body, altogether with the elimination parts.

In IntegerRelation.cpp, the Gaussian elimination forgets to advance firstVar (the number of finished columns) when it finishes a column.

P.S. I have tested that the implementation works, but how might I add test cases for it? I don't think we have related tests in mlir/test.

---

Full diff: https://github.com/llvm/llvm-project/pull/164437.diff

2 Files Affected:

• (modified) mlir/lib/Analysis/Presburger/Barvinok.cpp (+7-7)
• (modified) mlir/lib/Analysis/Presburger/IntegerRelation.cpp (+4)

diff --git a/mlir/lib/Analysis/Presburger/Barvinok.cpp b/mlir/lib/Analysis/Presburger/Barvinok.cpp
index 75d592e976edf..c31b27794f01e 100644
--- a/mlir/lib/Analysis/Presburger/Barvinok.cpp
+++ b/mlir/lib/Analysis/Presburger/Barvinok.cpp
@@ -178,13 +178,13 @@ mlir::presburger::detail::solveParametricEquations(FracMatrix equations) {
   for (unsigned i = 0; i < d; ++i) {
     // First ensure that the diagonal element is nonzero, by swapping
     // it with a row that is non-zero at column i.
-    if (equations(i, i) != 0)
-      continue;
-    for (unsigned j = i + 1; j < d; ++j) {
-      if (equations(j, i) == 0)
-        continue;
-      equations.swapRows(j, i);
-      break;
+    if (equations(i, i) == 0) {
+      for (unsigned j = i + 1; j < d; ++j) {
+        if (equations(j, i) == 0)
+          continue;
+        equations.swapRows(j, i);
+        break;
+      }
     }
 
     Fraction diagElement = equations(i, i);
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index 0dcdd5bb97bc8..7bafd070d13d3 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -1142,6 +1142,10 @@ bool IntegerRelation::gaussianEliminate() {
       inequalities.normalizeRow(i);
     }
     gcdTightenInequalities();
+
+    // The column is finished. Tell the next iteration to start at the next
+    // column.
+    firstVar++;
   }
 
   // No redundant rows.

[Superty]

Thanks for your contribution. There are tests in mlir/unittests. Could you add regression tests there? (I haven't read your fix yet.)

Also, I'm in Cambridge UK too so if you're around I'd be curious to chat about what you're using the library for!

[AdUhTkJm]

Hi, I've added tests for the fixes.

Also, I'm in Cambridge UK too so if you're around I'd be curious to chat about what you're using the library for!

I'm a Cambridge student, and I'm using this library for my Part II project. It's about implementing a polyhedral model with FPL.