[Mlir-commits] [mlir] [mlir][presburger] Preserve relative ordering of symbols and non-symbol vars when setting up SymbolicLexSimplex (PR #119036)

[Christopher Bate]

christopherbate wrote:

Sorry for the delayed update/response. Planning to address your comments tonight then will push an update.

> That test case will still be slow even after this patch. Is that correct? Thanks!


Oh, yes, I think I can create a test-case that shows the slowness even after the patch (it just has to do with the ordering of the variables, we can use the test case I added in the patch and just change the order).

However, when I was in the middle of debugging this two weeks ago, I convinced myself that the slowness was correct (but now I'm not so sure). I'd like to know the algorithm well enough to verify using pen-and-paper, but I'm still studying it.
My slow test case is based on the following:

You have an iteration space of shape `(16, 8, 6, 4)` and let's say you have coordinates `(a, b, c, d)` in this iteration space and `e` is the linearization of these coordinates. The test case I added in this change was created by eliminating one variable (`d`):

```
(a, b, c, e)[] : (
                             "a >= 0,"
                             "b >= 0,"
                             "c >= 0,"
                             "e >= 0,"
                             "15 - a >= 0,"
                             "7 - b >= 0,"
                             "5 - c >= 0,"
                             "e - a * 192 - c * 32 - b * 4 >= 0,"
                             "3 - e + a * 192 + c * 32 + b * 4 >= 0)"
)
```

When phrased this way, if you treat `a`, `b`, or `c` as locals then they can not currently be recognized as having a division representation (but that might be irrelveant to whether there's a bug in the simplex solver).

Let's say you reorder the variables to `(e, c, b, a)` and then populate SymbolicLexSimplex with this information , specifying that `e` is a symbol and `c, b, a,` are non-symbols. 

Now `SymbolicLexSimplex` sees the order as `(e, c, b, a)` from the start. Running the symbolic lex-min optimization attempts to produce the PWMA function that maps different symbol regions `e` to lex min of `c, b, a`.

Regardless of the order of how variables `c, b, a` were specified, the algorithm always seems to output the first piece with domain `0 <= e <= 3`, but after that the paths taken diverge. If you then add the constraint `e >= 4` and compute lex min, you'd get `(c, b, a) = (0, 0, 1)` because the original order when `SymbolicLexSimplex` was created was `c, b, a`; it didn't do the reordering itself

The working symbol domain would have added the constraint `e >= 192`. The "jumps" in the symbol domain when computing the PWMA are different than if the ordering is `(a, b, c)`. If the ordering is `(a, b, c)` then you would natural expect to enumerate each of the segments "` e ` in `[i * 4, i*4+4)`" in order. The large jumps somehow result in a sequence of pivots that cause the coefficient size to eventually explode, and when I profiled the code, it is spending all its time going through slow paths of `DynamicAPInt`. My original intuition was that it could be correctly computing the PWMA but in a highly inefficient manner.  When I inspected the intermediate output, the PWMA piece domains looked to be individual points in the range of `e` rather than a segment of 4 points as you would expect. I need to study the algorithm a bit more and go back to re-verify this last point, however. 








https://github.com/llvm/llvm-project/pull/119036