<table border="1" cellspacing="0" cellpadding="8">
    <tr>
        <th>Issue</th>
        <td>
            <a href=https://github.com/llvm/llvm-project/issues/55746>55746</a>
        </td>
    </tr>

    <tr>
        <th>Summary</th>
        <td>
            Implement division ordering for IntegerRelation local variables
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            mlir:presburger
      </td>
    </tr>

    <tr>
      <th>Assignees</th>
      <td>
      </td>
    </tr>

    <tr>
      <th>Reporter</th>
      <td>
          Groverkss
      </td>
    </tr>
</table>

<pre>
    Division ordering reorders local variables such that a division representation for local identifier at position `i` only depends on local identifiers at position < `i`.

In the [current implementation](https://github.com/llvm/llvm-project/blob/main/mlir/lib/Analysis/Presburger/IntegerRelation.cpp#L853-L870) of extracting divisions, we keep trying to find divisions until we reach a fixed point. The divisions found by this algorithm are not ordered. We can implement division reordering here, such that any divisions returned by this algorithm are always ordered properly.

The implementation I had in mind is that each time we find a new division representation, we swap it with the first local variable for which we do not have a division representation yet. We can prove by induction that this will make sure that the divisions are ordered.

I would also be happy to discuss any other implementation/strategies that are better than this. I would also like to see if it is possible to find all the divisions in one single go, instead of iterating until we find a fixed point.

Division reordering makes sure that later calls to `getLocalReprs` are done in a single go, as well as allows other algorithms to work in a single go.

</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJyVVE2P2zoM_DXOhajhtetNcvBh20WLBfZQFA94Z9mibXYVyRDldf3vS6lJNkk_gAJJbEWkOJwZsXV6bR7plZicBec1erIDeEyvDMZ1ysCr8qRagww8dyOEUQVQoE9pHiePjDaoEJe988c80vIn9YQeJGNyTCkguy9IvuCsWUHjhFazLH5J4uus6uMpM8-Kx6x4-Pn7ZAUQQlZ_6GbvJRfoMBk8nPBk9WNW7sYQJs6qh6z8JJ-Bwji3eecOsjDm9fR4N3n3Dbsgy9a4Vh4HRTY-DPkYQ_G_B6vMysTy-kUab2c_YNx9sgHl7SuaVDjvpikrq-ddXb173m2LrNyD6wG_B6-6EGk-MSgnfYQF4QVxguDXuBcc9GT1WwzMQouJYR6VqKBk_ztqIYhsyOE_4eAttnez5LarUENCoxmcl5YPoDyCdeGn0qhz-B-hU_aNsktVz3YYJTZCvFDfrhfVPIbZW_xTQWUWtfKpJgjHE3qzXqkY4V_rBk8wKg1k4RB5kFNT5dR7oANGJhJDCiwuf3LjkVle1AQUYBFQyS49eQ439k7OXUaSApKiXWJqVK_4F7OvGM4kSmMSKxwIqrlL2wlyomQhY-CgXgTLLJwcNy41i1SddLkyOCxuNtKnYQctCqJpWqM_NHE3MycxnJzlb51ffmLxmpiS8MherNFiCBIra5ug5XBVwZBglNMZRZE-kibo5RYyRYpOtlTSzTV8EcpZ6U4MI3GDi8yT5YAioovnoECJbjr7-KjepY0v-378jRMjgXzBoNw0aUVENByhyWwYMDxHVb-KThynTGxZR2QCUF3DUyILSiMqOta4hY80nu2bDl2cf7lJPuLc6KbS-2qvNoGCwebp11t0Rh69dTMgbqfrZvam-edBRcwzxllU19v395uxqfbV9g677W6rd-1dVxW16rqiqu7b7d22VtXGqBYNNzIxs7JMk616mC4GWSkjc0NNWZRlUZe7Yl8VZZ23XVXvyk6rquzLut9n7wuU6WjyiCd3ftj4JkFr54Fl0xAHfttUYqDBIqaycr6aw-h88zneGf_CvEl9NKmJH_GdUFU">