This patch modifies mergeLocalIds to not delete duplicate local ids in
`this` relation. This allows the ordering of the final local ids for `this`
to be determined more easily, which is generally required when other objects
refer to these local ids.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D123866
Add support for computing the symbolic integer lexmin of a polyhedron.
This finds, for every assignment to the symbols, the lexicographically
minimum value attained by the dimensions. For example, the symbolic lexmin
of the set
`(x, y)[a, b, c] : (a <= x, b <= x, x <= c)`
can be written as
```
x = a if b <= a, a <= c
x = b if a < b, b <= c
```
This also finds the set of assignments to the symbols that make the lexmin unbounded.
This was previously landed in da92f92621 and
reverted in b238c252e8 due to a build failure
in the code. Re-landing now with a fixed build.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D122985
Add support for computing the symbolic integer lexmin of a polyhedron.
This finds, for every assignment to the symbols, the lexicographically
minimum value attained by the dimensions. For example, the symbolic lexmin
of the set
`(x, y)[a, b, c] : (a <= x, b <= x, x <= c)`
can be written as
```
x = a if b <= a, a <= c
x = b if a < b, b <= c
```
This also finds the set of assignments to the symbols that make the lexmin unbounded.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D122985
Add integer-exact checks for inequalities being separate and redundant in LexSimplex.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D122921
Previously, when an input set had a duplicate division, the duplicates might
be removed by a call to mergeLocalIds due to being detected as being duplicate
for the first time. The subtraction implementation cannot handle existing
locals being removed, so this would lead to unexpected behaviour. Resolve this
by removing all the duplicates up front.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D122826
This patch modifies IntegerPolyhedron, IntegerRelation, PresburgerRelation,
PresburgerSet, PWMAFunction, constructors to take PresburgerSpace instead of
dimensions. This allows information present in PresburgerSpace to be carried
better and allows for a general interface.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D122842
Previously, when updating the outputs matrix, the local offset was not being considered.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D122812
This reverts commit 5630143af3. The
implementation in this commit was incorrect. Also, handling this representation
of equalities in the upcoming support for symbolic lexicographic minimization
makes that patch much more complex. It will be easier to review that without
this representaiton and then reintroduce the fixed column representation
later, hence the revert rather than a bug fix.
Add a baseline implementation of support for local ids for `PWMAFunction::valueAt`. This can be made more efficient later if needed by handling locals with known div representations separately.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D122144
In LexSimplex, instead of adding equalities as a pair of inequalities,
add them as a single row, move them into the basis, and keep them there.
There will always be a valid basis involving all non-redundant equalities. Such
equalities will then be ignored in some other operations, such as when looking
for pivot columns. This speeds them up a little bit.
More importantly, this is an important precursor patch to adding support for
symbolic integer lexmin, as this heuristic can sometimes make a big difference there.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D122165
This is a convenience function for adding new divisions to the Simplex given the numerator and denominator.
This will be needed for symbolic integer lexmin support.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D122159
This patch adds supports for union of relations (PresburgerRelation). Along
with this, support for PresburgerSet is also maintained.
This patch is part of a series of patches to add support for relations in
Presburger library.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D121417
This patch remove `spaceKind` from PresburgerSpace, making PresburgerSpace only
a space supporting relations.
Sets are still implemented in the same way, i.e. with a zero domain but instead
the asserts to check if the space is still set are added to users of
PresburgerSpace which treat it as a Set space.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D121357
When `addCoalescedPolyhedron` was called with `j == n - 1`,
the `polyhedrons`-vector was not properly updated (the
`IntegerPolyhedron` at position `n - 2` was "lost"). This patch adds
special handling to that case and a regression testcase.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D121356
This patch moves PresburgerSpace::removeIdRange(idStart, idLimit) to
PresburgerSpace::removeIdRange(kind, idStart, idLimit), i.e. identifiers
can only be removed at once for a single kind.
This makes users of PresburgerSpace to not assume any inside ordering of
identifier kinds.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D121079
This patch cleans up the interface to PresburgerSet. At a high level it does
the following changes:
- Move member functions around to have constructors at top and print/dump
at end.
- Move a private function to be a static function instead.
- Change member functions of type "getAllIntegerPolyhedron" to "getAllPolys"
instead.
- Improve documentation for PresburgerSet.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D121027
This patch makes coalesce skip the comparison of all pairs of IntegerPolyhedrons with LocalIds rather than crash. The heuristics to handle these cases will be upstreamed later on.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D120995
This patch introduces the cut case. If one polytope has only cutting and
redundant inequalities for the other and the facet of the cutting
inequalities are contained within the other polytope, then the polytopes are
be combined into a polytope consisting only of their respective
redundant constraints.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D120614
This patch moves all functionality from IntegerPolyhedron to IntegerRelation.
IntegerPolyhedron is now implemented as a relation with no domain. All existing
functionality is extended to work on relations.
This patch does not affect external users like FlatAffineConstraints as they
can still continue to use IntegerPolyhedron abstraction.
This patch is part of a series of patches to support relations in Presburger
library.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D120652
This patch moves identifier kind specific insert/append functions like
`insertDimId`, `appendSymbolId`, etc. from IntegerPolyhedron to
FlatAffineConstraints.
This change allows for a smoother transition to IntegerRelation.
This change is part of a series of patches to introduce Relations in Presburger
library.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D120576
In the main-loop of the current coalesce implementation `i` was incremented
twice for some cases. This patch fixes this bug and adds a regression
testcase.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D120613
This patch refactors the looping strategy of coalesce for future patches. The new strategy works in-place and uses IneqType to organize inequalities into vectors of the same type. Future coalesce cases will pattern match on this organization. E.g. the contained case needs all inequalities and equalities to be redundant, so this case becomes checking whether the respective vectors are empty. For other cases, the patterns consider the types of all inequalities of both sets making it wasteful to only consider whether a can be coalesced with b in one step, as inequalities would need to be typed again for the opposite case. Therefore, the new strategy tries to coalesce a with b and b with a in a single step.
Reviewed By: Groverkss, arjunp
Differential Revision: https://reviews.llvm.org/D120392
This patch moves the Presburger library to a new `presburger` namespace.
This allows to shorten some names, helps to avoid polluting the mlir namespace,
and also provides some structure.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D120505
Use an `MLIRContext` declared in a single place in the `parsePoly` function that almost all Presburger unit tests use for parsing sets. This function is only used in tests.
This saves us from having to declare and pass a new `MLIRContext` in every test.
Reviewed By: bondhugula, mehdi_amini
Differential Revision: https://reviews.llvm.org/D119251
This patch adds typing of inequalities to the simplex. This is a cental part of the coalesce algorithm and will be heavily used in later coalesce patches. Currently, only the three most basic types are supported with more to be introduced when they are needed.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D119925
This allows to differentiate between the cases where the optimum does not
exist due to being unbounded and due to the polytope being empty.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D120127
This patch introducing seperating dimensions into two types: Domain and Range.
This allows building relations over PresburgerSpace.
This patch is part of a series of patches to introduce relations in Presburger
library.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D119709
Add support for computing an overapproximation of the number of integer points
in a polyhedron. The returned result is actually the number of integer points
one gets by computing the "rational shadow" obtained by projecting out the
local IDs, finding the minimal axis-parallel hyperrectangular approximation
of the shadow, and returning the number of integer points in that. This does
not currently support symbols.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D119228
Add the class MultiAffineFunction which represents functions whose domain is an
IntegerPolyhedron and which produce an output given by a tuple of affine
expressions in the IntegerPolyhedron's ids.
Also add support for piece-wise MultiAffineFunctions, which are defined on a
union of IntegerPolyhedrons, and may have different output affine expressions
on each IntegerPolyhedron. Thus the function is affine on each individual
IntegerPolyhedron piece in the domain.
This is part of a series of patches leading up to parametric integer programming.
Depends on D118778.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D118779
Use `SmallVector` instead of `std::vector` in `getLocalRepr` function.
Also, fix the casing of a variable.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D118722
Extract the division representation from equality constraints.
For example:
32*k == 16*i + j - 31 <-- k is the localVariable
expr = 16*i + j - 31, divisor = 32
k = (16*i + j - 32) floordiv 32
The dividend of the division is set to [16, 1, -32] and the divisor is set
to 32.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D117959
This patch introduces a class LexSimplex that can currently be used to find the
lexicographically minimal rational point in an IntegerPolyhedron. This is a
series of patches leading to computing the lexicographically minimal integer
lattice point as well parametric lexicographic minimization.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D117437
Groverkss