[all-commits] [llvm/llvm-project] d257f7: [MLIR][FlatAffineConstraints] Remove duplicate div...

[Kunwar Shaanjeet Singh Grover via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: d257f7c1bff3521053d925c616f6f60d0a5c22ec
      https://github.com/llvm/llvm-project/commit/d257f7c1bff3521053d925c616f6f60d0a5c22ec
  Author: Groverkss <groverkss at gmail.com>
  Date:   2021-12-03 (Fri, 03 Dec 2021)

  Changed paths:
    M mlir/include/mlir/Analysis/AffineStructures.h
    M mlir/lib/Analysis/AffineStructures.cpp
    M mlir/unittests/Analysis/AffineStructuresTest.cpp

  Log Message:
  -----------
  [MLIR][FlatAffineConstraints] Remove duplicate divisions while merging local ids

This patch implements detecting duplicate local identifiers by extracting their
division representation while merging local identifiers.

For example, given the FACs A, B:

```
A: (x, y)[s0] : (exists d0 = [x / 4], d1 = [y / 4]: d0 <= s0, d1 <= s0, x + y >= 2)
B: (x, y)[s0] : (exists d0 = [x / 4], d1 = [y / 4]: d0 <= s0, d1 <= s0, x + y >= 5)
```

The intersection of A and B without this patch would lead to the following FAC:

```
(x, y)[s0] : (exists d0 = [x / 4], d1 = [y / 4], d2 = [x / 4], d3 = [x / 4]: d0 <= s0, d1 <= s0, d2 <= s0, d3 <= s0, x + y >= 2, x + y >= 5)
```

after this patch, merging of local ids will detect that `d0 = d2` and `d1 = d3`,
and the intersection of these two FACs will be (after removing duplicate constraints):

```
(x, y)[s0] : (exists d0 = [x / 4], d1 = [y / 4] : d0 <= s0, d1 <= s0, x + y >= 2, x + y >= 5)
```

This reduces the number of constraints by 2 (constraints) + 4 (2 constraints for each extra division) for this case.

This is used to reduce the output size representation of operations like
PresburgerSet::subtract, PresburgerSet::intersect which require merging local
variables.

Reviewed By: arjunp, bondhugula

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