This is an archive of the discontinued LLVM Phabricator instance.

[MLIR] Move Presburger Math from FlatAffineConstraints to Presburger/IntegerPolyhedron
ClosedPublic

Authored by Groverkss on Nov 28 2021, 5:01 AM.

Details

Summary

This patch factors out math functionality that is a subset of Presburger arithmetic and moves it from FlatAffineConstraints to Presburger/IntegerPolyhedron. This patch only moves some parts of the functionality planned to be moved, with subsequent patches moving more functionality. There are three main reasons for this:

  1. This split makes the Presburger Library easier and more flexible to use across MLIR, by not depending on IR.
  2. This split allows the Presburger library to be developed independently from Affine Analysis, with Affine Analysis using this library.
  3. With more functionality being upstreamed to the Presburger Library, the mlir/Analysis directory will be cluttered with Presburger library components since they depend on math functionality from FlatAffineConstraints. Moving this functionality to the Presburger directory allows keeping the new functionality in the Presburger directory.

This patch is part of an ongoing effort to make the Presburger Library easier to use. The motivation for this effort is the feedback received at the LLVM conference from Mehdi and others.

Diff Detail

Event Timeline

Groverkss created this revision.Nov 28 2021, 5:01 AM
Groverkss requested review of this revision.Nov 28 2021, 5:01 AM
Groverkss edited the summary of this revision. (Show Details)Nov 28 2021, 5:03 AM
Groverkss edited the summary of this revision. (Show Details)Nov 28 2021, 5:08 AM
ljmf00 retitled this revision from MLIR] Move Presburger Math from FlatAffineConstraints to Presburger/PresburgerBasicSet to [MLIR] Move Presburger Math from FlatAffineConstraints to Presburger/PresburgerBasicSet.Nov 28 2021, 5:45 AM
bondhugula added inline comments.Nov 29 2021, 5:00 AM
mlir/include/mlir/Analysis/Presburger/PresburgerBasicSet.h
1 ↗(On Diff #390196)

While refactoring this out looks fine, PresburgerBasicSet is too heavy a name for what this comprises. I can't immediately think of a better one though.

mlir/lib/Analysis/Presburger/PresburgerBasicSet.cpp
1 ↗(On Diff #390196)

Wrong file extension here. Also, no need of the C++.

Groverkss updated this revision to Diff 390310.Nov 29 2021, 5:21 AM
Groverkss marked 2 inline comments as done.
  • Fix Presburger.cpp file header
mlir/include/mlir/Analysis/Presburger/PresburgerBasicSet.h
1 ↗(On Diff #390196)

I think there is some misunderstanding. PresburgerBasicSet is meant to represent all functionality of FlatAffineConstraints that does not interact with the IR. This patch only moves some functionality so as to not make it harder to review. Subsequent patches will move more functionality to PresburgerBasicSet from FlatAffineConstraints.

grosser added inline comments.Nov 29 2021, 5:31 AM
mlir/include/mlir/Analysis/Presburger/PresburgerBasicSet.h
1 ↗(On Diff #390196)

What about just calling it "BasicSet". This could help to clarify that this is not just for Presburger arithmetic?

Best,
Tobias

Groverkss added inline comments.Dec 3 2021, 5:23 AM
mlir/include/mlir/Analysis/Presburger/PresburgerBasicSet.h
1 ↗(On Diff #390196)

I do not have any preference for what we call it :)

We can go with BasicSet, IntegerPolyhedra, Polyhedra, PresburgerBasicSet, or any other name you may have in mind.

@bondhugula Which one do you think will be good?

ftynse added inline comments.Dec 3 2021, 7:41 AM
mlir/include/mlir/Analysis/Presburger/PresburgerBasicSet.h
1 ↗(On Diff #390196)

Fly-by comment: polyhedra is plural of polyhedron. So if you chose that name, please use the singular form unless you explicitly refer to plurality.

bondhugula added inline comments.Dec 6 2021, 7:07 AM
mlir/include/mlir/Analysis/Presburger/PresburgerBasicSet.h
1 ↗(On Diff #390196)

BasicSet, IntegerPolyhedron, and Polyhedron are all candidates. BasicSet may only make sense when there is another one named Set - otherwise, Basic is only adding ambiguity or noise. Polyhedron or IntegerPolyhedron?

Groverkss added inline comments.Dec 6 2021, 7:23 AM
mlir/include/mlir/Analysis/Presburger/PresburgerBasicSet.h
1 ↗(On Diff #390196)

IntegerPolyhedron sounds good to me.

Groverkss updated this revision to Diff 392065.Dec 6 2021, 7:50 AM

Change name from PresburgerBasicSet to IntegerPolyhedron

Groverkss retitled this revision from [MLIR] Move Presburger Math from FlatAffineConstraints to Presburger/PresburgerBasicSet to [MLIR] Move Presburger Math from FlatAffineConstraints to Presburger/IntegerPolyhedron.Dec 6 2021, 7:52 AM
Groverkss edited the summary of this revision. (Show Details)
bondhugula added inline comments.Dec 6 2021, 10:03 AM
mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
14

...INTEGERPOLYHEDRON_H

mlir/lib/Analysis/Presburger/CMakeLists.txt
4

Please maintain these in sorted order - order above should be fixed as well.

mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp
16

These shouldn't be enclosed in a namespace this way. Instead, just using namespace mlir;.

Address clang-format issues.

Groverkss updated this revision to Diff 392192.Dec 6 2021, 2:43 PM
Groverkss marked 3 inline comments as done.
  • Address bondhugula's comments
arjunp added a comment.Dec 7 2021, 3:11 AM

SGTM. Some nits and minor comments below.

mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
31
40
42–43

It seems strange to say that local variables represent existential quantification. I would rather say that local variables are existentially quantified.

44

May as well use similar constraints 1 <= x <= 7, x = 2q to the set above. Also, it would be good to not break the set across two lines. Also, I think you can move the example to the bottom.

For example, consider the set: (x) : (exists q : 1 <= x <= 7, x = 2q). This set is is equivalent to {2, 4, 6}.`

Also, I think you can mention that mathematically, existential quantification can be thought of as the result of projection. In the above example q is existentially quantified; this can be thought of as the result of projecting out q from the previous example, i.e. we obtained {2, 4, 6} by projecting out the second dimension from {(2, 1), (4, 2), (6, 3)}.

If you use this then remember to change y to q in the first example

mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp
164–170

I think these have some tests. You can probably move them to an IntegerPolyhedronTest.

Groverkss updated this revision to Diff 392823.Dec 8 2021, 10:07 AM
Groverkss marked 5 inline comments as done.
  • Update docs
  • Move tests for IntegerPolyhedron to Presburger/IntegerPolyhedronTest
bondhugula accepted this revision.Dec 8 2021, 7:03 PM
bondhugula added inline comments.
mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h
10

polyhedra is plural. Drop "an".

This revision is now accepted and ready to land.Dec 8 2021, 7:03 PM
Groverkss updated this revision to Diff 393084.Dec 9 2021, 2:40 AM
Groverkss marked an inline comment as done.
  • Update docs