This patch adds better functions for parsing MultiAffineFunctions and
PWMAFunctions in Presburger unittests.
A PWMAFunction can now be parsed as:
```
PWMAFunction result = parsePWMAF({
{"(x, y) : (x >= 10, x <= 20, y >= 1)", "(x, y) -> (x + y)"},
{"(x, y) : (x >= 21)", "(x, y) -> (x + y)"},
{"(x, y) : (x <= 9)", "(x, y) -> (x - y)"},
{"(x, y) : (x >= 10, x <= 20, y <= 0)", "(x, y) -> (x - y)"},
});
```
which is much more readable than the old format since the output can be
described as an AffineMap, instead of coefficients.
This patch also adds support for parsing divisions in MultiAffineFunctions
and PWMAFunctions which was previously not possible.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D133654
This patch adds better functions for parsing MultiAffineFunctions and
PWMAFunctions in Presburger unittests.
A PWMAFunction can now be parsed as:
```
PWMAFunction result = parsePWMAF({
{"(x, y) : (x >= 10, x <= 20, y >= 1)", "(x, y) -> (x + y)"},
{"(x, y) : (x >= 21)", "(x, y) -> (x + y)"},
{"(x, y) : (x <= 9)", "(x, y) -> (x - y)"},
{"(x, y) : (x >= 10, x <= 20, y <= 0)", "(x, y) -> (x - y)"},
});
```
which is much more readable than the old format since the output can be
described as an AffineMap, instead of coefficients.
This patch also adds support for parsing divisions in MultiAffineFunctions
and PWMAFunctions which was previously not possible.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D133654
This patch adds hermite normal form computation to Matrix. Part of this algorithm
lived in LinearTransform, being used for compuing column echelon form. This
patch moves the implementation to Matrix::hermiteNormalForm and generalises it
to compute the hermite normal form.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D133510
Only the main Presburger library under the Presburger directory has been switched to use arbitrary precision. Users have been changed to just cast returned values back to int64_t or to use newly added convenience functions that perform the same cast internally.
The performance impact of this has been tested by checking test runtimes after copy-pasting 100 copies of each function. Affine/simplify-structures.mlir goes from 0.76s to 0.80s after this patch. Its performance sees no regression compared to its original performance at commit 18a06d4f3a before a series of patches that I landed to offset the performance overhead of switching to arbitrary precision.
Affine/canonicalize.mlir and SCF/canonicalize.mlir show no noticable difference, staying at 2.02s and about 2.35s respectively.
Also, for Affine and SCF tests as a whole (no copy-pasting), the runtime remains about 0.09s on average before and after.
Reviewed By: bondhugula
Differential Revision: https://reviews.llvm.org/D129510
This patch refactors MAF to be defined over the universe in a given space
instead of being defined over a restricted domain.
The reasoning for this refactor is to store division representation for local
variables explicitly for the function outputs. This change is required for
unionLexMax/Min to support local variables which will be upstreamed after this
patch. Another reason for this refactor is to have a flattened form of
AffineMap as MultiAffineFunction.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D131864
IntegerPolyhedron::findIntegerLexmin currently does not return values of
the local ids, so when a test for sampling includes a set with locals, the
result of findIntegerLexmin should be checked using containsPointNoLocal,
not containsPoint.
This uses an int64_t-based fastpath for the common case and falls back to
SlowMPInt to handle the rare cases where larger numbers occur.
It uses `__builtin_*` for performance through the support in LLVM MathExtras.
Using this in the Presburger library results in a minor performance
*improvement* over any commit hash before sequence of patches
starting at d5e31cf38a.
This was previously reverted in 1e10d35ea9 due
to a build failure; relanding now with an attempted fix.
Reviewed By: Groverkss, ftynse
Differential Revision: https://reviews.llvm.org/D128811
This uses an int64_t-based fastpath for the common case and falls back to
SlowMPInt to handle the rare cases where larger numbers occur.
It uses `__builtin_*` for performance through the support in LLVM MathExtras.
Using this in the Presburger library results in a minor performance
*improvement* over any commit hash before sequence of patches
starting at d5e31cf38a.
Reviewed By: Groverkss, ftynse
Differential Revision: https://reviews.llvm.org/D128811
This patch refactors existing implementations of division representation storage
into a new class, DivisionRepr. This refactoring is done so that the common
division utilities can be shared in an upcoming patch.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D129146
This patch implements a lexicographic max/min union of two PWMAFunctions.
The lexmax/lexmin union of two functions is defined as a function defined on
the union of the input domains of both functions, such that when only one of the
functions are defined, it outputs the same as that function, and if both are
defined, it outputs the lexmax/lexmin of the two outputs. On points where
neither function is defined, the union is not defined either.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D128829
"attachment" was a temporary name chosen for the information attached to a
variable in a PresburgerSpace. After the disambiguation of "variables" and
"identifiers" in PresburgerSpace, we use the word "identifiers" for this
information, since this information is used to "identify" these variables.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D128751
This also changes the space of the returned lexmin for IntegerPolyhedrons;
the symbols in the poly now correspond to symbols in the result rather than dims.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D128933
Also added test cases. Also extend support for `computeReprWithOnlyDivLocals` from `IntegerPolyhedron` to `IntegerRelation` and `PresburgerRelation`.
Depends on D128736.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D128737
Also added test cases to test this. Both IntegerRelation::addLocalFloorDiv and the fixed implementation of subtraction need to compute division inequalities from dividend and divisor, so this also adds helper util functions to avoid duplicating this logic.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D128736
Currently, in the Presburger library, we use the words "variables" and
"identifiers" interchangeably. This patch changes this to only use "variables" to
refer to the variables of PresburgerSpace.
The reasoning behind this change is that the current usage of the word "identifier"
is misleading. variables do not "identify" anything. The information attached to them is the
actual "identifier" for the variable. The word "identifier", will later be used
to refer to the information attached to each variable in space.
Reviewed By: ftynse
Differential Revision: https://reviews.llvm.org/D128585
This paves the way for integer-exact projection, and for supporting
non-division locals in subtraction, complement, and equality checks.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D127463
The Presburger library currently uses int64_t throughout for its integers.
This runs the risk of silently producing incorrect results when overflows occur.
Fixing this issue requires some sort of multiprecision integer
that transparently supports aribtrary arithmetic computations.
The class SlowMPInt provides this functionality, and is intended to be used
as the slow path fallback for a more optimized upcoming class, MPInt, that optimizes
for the Presburger library's workloads.
Reviewed By: ftynse
Differential Revision: https://reviews.llvm.org/D123758
This patch allows attaching user information, called "values" to each
identifier. The values are used to carry information along with variables and
are also used to determine if two variables are identical.
This patch is part of a series of patches to allow attaching user information
with variables in Presburger library.
Reviewed By: ftynse
Differential Revision: https://reviews.llvm.org/D127347
When constraints in the two operands make each other redundant, prefer constraints of the second because this affects the number of sets in the output at each level; reducing these can help prevent exponential blowup.
This is accomplished by adding extra overloads to Simplex::detectRedundant that only scan a subrange of the constraints for redundancy.
Reviewed By: Groverkss
Differential Revision: https://reviews.llvm.org/D127237
This patch fixes a bug in PresburgeRelation::subtract that made it process the
inequality at index 0, multiple times. This was caused by allocating memory
instead of reserving memory in llvm::SmallVector.
Reviewed By: arjunp
Differential Revision: https://reviews.llvm.org/D127228
This patch adds support for applying a relation on domain/range of a relation.
Reviewed By: arjunp, ftynse
Differential Revision: https://reviews.llvm.org/D126339
This patch adds support for obtaining a set corresponding to the domain/range
of the relation.
Reviewed By: ftynse
Differential Revision: https://reviews.llvm.org/D126326
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
Groverkss