llvm-project
b4149a01 - [MLIR][Presburger] Fix Gaussian elimination (#164437)

Commit
140 days ago
[MLIR][Presburger] Fix Gaussian elimination (#164437) 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.)
Author
Parents
Loading