[RFC] Introduce PresburgerSet

[multiverstack-intellif]

This RFC proposes to introduce PresburgerSet as another integer set utility, aiming to tackle more complex analysis problems.
rendered

cc @wrongtest-intellif @Hzfengsy @spectrometerHBH @tqchen

[tqchen]

Thank you for the proposal. There is a general tradeoff in terms between speed of solving, generality of the solution, and extra capabilities(eg ability to handle symbolic division/mod that may go beyond normal).

The current hyperbox based analysis was chosen because of its speed efficiency, of course that also comes with limitations. Additionally, there is a relaxation in analysis so to handle arithmetics that may not be exactly captured by intset.

Normal constraint solver based solution might come with some extra capabilities, the question here being whether the efficiency can be kept up.

My recommendation would be to start with a different class first under arith for us to understand the overall space. Likely fewer passes will need such analysis, then we go from there

[tqchen]

To get extra clarity, we could rename the current IntSet explicitly as IntervalSet.

[multiverstack-intellif]

@tqchen Thanks for you recommendation. Agree with the efficiency risk and it's now updated. Could you take another look?

[tqchen]

Thank you @multiverstack-intellif i think it is a good starting pt. We can iterate on APIs and other things as we start improving the overall toolset. Can you also change RFC title to Introduce PresburgerSet ? otherwise it looks good to me

[Hzfengsy]

Let's keep it open for one week for enough visibility 😄

[Lunderberg]

I very much like the proposed improvements, especially the use cases for inner-block and inter-block analysis. While I have made some development for similar applications, the additional formalism and reliability proposed here would be very useful.

[multiverstack-intellif]

I very much like the proposed improvements, especially the use cases for inner-block and inter-block analysis. While I have made some development for similar applications, the additional formalism and reliability proposed here would be very useful.

Thanks, @Lunderberg. What you mentioned is a great analysis tool, and most part of its capability is beyond what integer set targets to achieve. It seems to me that data-flow analysis focuses more on global/high-level info and integer set focuses more on local info inside iteration. They are expected to benefit the overall analysis tools together.

[Hzfengsy]

Thanks for everyone's input. We are going to merge in 24 hours if there are no additional comments.

[Hzfengsy]

Thanks, @multiverstack-intellif for the proposal and @tqchen @vinx13 's review.