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

[Arjun P]

Superty wrote:

By the way, here's a simpler reproducer

```
TEST(reproduce, reproduce) {
  IntegerPolyhedron poly = parseIntegerPolyhedron("(x, p, q, r)[] : ("
                             "r >= 0,"
                             "p >= 0,"
                             "q >= 0,"
                             "x >= 0,"
                             "6 - r >= 0,"
                             "6 - p >= 0,"
                             "6 - q >= 0,"
                             "x - r * 18 - q * 2 - p >= 0,"
                             "- x + r * 18 + q * 2 + p >= 0)");

/*
    Input problem:
    x = 18r + 2q + p
    0 <= p, q, r <= 6

    Solution:
    0 <= x <= 18*6 + 2*6 + 6 = 21*6 = 126

    if x == 126, p = q = r = 6
    else (x < 126)
      y := x % 18, r := x // 18
      if y < 12, p := y % 2, q := y // 2
      else p := y - 12, q := 6
*/

  llvm::SmallBitVector isSymbol(4, false);
  isSymbol[0] = true;
  SymbolicLexOpt result =
      SymbolicLexSimplex(poly,
                         IntegerPolyhedron(PresburgerSpace::getSetSpace(
                             /*numDims=*/0,
                             /*numSymbols=*/1)),
                         isSymbol)
          .computeSymbolicIntegerLexMin();

  result.lexopt.dump();
}
```

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