[MLIR][Presburger] Simplex: refactor (symbolic)lex to support specifying multiple varKinds as symbols

This is also required to support lexmin for relations.

Reviewed By: Groverkss

Differential Rev

[MLIR][Presburger] Simplex: refactor (symbolic)lex to support specifying multiple varKinds as symbols

This is also required to support lexmin for relations.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D128931

show more ...

[MLIR][Presburger] Rename variable/identifier -> variable

Currently, in the Presburger library, we use the words "variables" and
"identifiers" interchangeably. This patch changes this to only use "v

[MLIR][Presburger] Rename variable/identifier -> variable

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

show more ...

Don't use Optional::hasValue (NFC)

Use value_or instead of getValueOr (NFC)

[MLIR][Presburger] subtract: improve redundant constraint detection

When constraints in the two operands make each other redundant, prefer constraints of the second because this affects the number o

[MLIR][Presburger] subtract: improve redundant constraint detection

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

show more ...

[MLIR][Presburger] Simplex: remove redundant member vars nRow, nCol

Reviewed By: ftynse

Differential Revision: https://reviews.llvm.org/D126790

[MLIR][Presburger] Simplex: remove redundant zeroing out of row

This fillRow(..., 0) is redundant because when the size of the tableau is
consistent, the resize always creates a new row, which is ze

[MLIR][Presburger] Simplex: remove redundant zeroing out of row

This fillRow(..., 0) is redundant because when the size of the tableau is
consistent, the resize always creates a new row, which is zero-initialized.

Also added asserts throughout to ensure the dimensions of the tableau remain
consistent.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D126709

show more ...

[MLIR][Presburger] Simplex::computeOptimum: slightly simplify code (NFC)

[MLIR][Presburger] addSymbolicCut: fix the integral symbols heuristic to match the docs

Previously this checked if the entire symbolic numerator was divisible by the
denominator, which is never the

[MLIR][Presburger] addSymbolicCut: fix the integral symbols heuristic to match the docs

Previously this checked if the entire symbolic numerator was divisible by the
denominator, which is never the case when this function is called. Fixed this to
check only the non-const coefficients in the numerator, which was what was
intended and documented.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D123592

show more ...

[MLIR][Presburger][Simplex] moveRowUnknownToColumn: support the row sample value being zero

When the sample value is zero, everything is the same except that failure to
pivot does not imply emptines

[MLIR][Presburger][Simplex] moveRowUnknownToColumn: support the row sample value being zero

When the sample value is zero, everything is the same except that failure to
pivot does not imply emptiness. So, leave it to the user to mark as empty if
necessary, if they know the sample value is strictly negative. This is needed
for an upcoming symbolic lexmin heuristic.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D123604

show more ...

[MLIR][Presburger] change some `push_back`s to `emplace_back`s

[MLIR][Presburger] change some post-increments/decrements to pre-increments/decrements

[MLIR][Presburger][Simplex] addSymbolicCut: don't add symbol div if denom is 1

This is unncessary, so we remove it as an optimization.

Reviewed By: Groverkss

Differential Revision: https://reviews

[MLIR][Presburger][Simplex] addSymbolicCut: don't add symbol div if denom is 1

This is unncessary, so we remove it as an optimization.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D123540

show more ...

[MLIR][Presburger][Simplex] symbolic lexmin: add some normalization heuristics

Normalize some of the division and inequality expressions used,
which can improve performance. Also deduplicate some of

[MLIR][Presburger][Simplex] symbolic lexmin: add some normalization heuristics

Normalize some of the division and inequality expressions used,
which can improve performance. Also deduplicate some of the
normalization functionality throughout the Presburger library.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D123314

show more ...

NFC: Silence unused function 'scaleAndAdd' in release build.

Differential Revision: https://reviews.llvm.org/D123354

[MLIR][Presburger] IntegerPolyhedron: add support for symbolic integer lexmin

Add support for computing the symbolic integer lexmin of a polyhedron.
This finds, for every assignment to the symbols,

[MLIR][Presburger] IntegerPolyhedron: add support for symbolic integer lexmin

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 da92f92621e28a56fe8ad79d82eb60e436bf1d39 and
reverted in b238c252e8b1bbebc7ed79c08e06c23514d0dfb4 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

show more ...

Revert "[MLIR][Presburger] IntegerPolyhedron: add support for symbolic integer lexmin"

This reverts commit da92f92621e28a56fe8ad79d82eb60e436bf1d39.

[MLIR][Presburger] IntegerPolyhedron: add support for symbolic integer lexmin

Add support for computing the symbolic integer lexmin of a polyhedron.
This finds, for every assignment to the symbols,

[MLIR][Presburger] IntegerPolyhedron: add support for symbolic integer lexmin

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

show more ...

[MLIR][Presburger] LexSimplex: support is{Redundant,Separate}Inequality

Add integer-exact checks for inequalities being separate and redundant in LexSimplex.

Reviewed By: Groverkss

Differential Re

[MLIR][Presburger] LexSimplex: support is{Redundant,Separate}Inequality

Add integer-exact checks for inequalities being separate and redundant in LexSimplex.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D122921

show more ...

[MLIR][Presburger] Factor out some functionality from LexSimplex into a LexSimplexBase

LexSimplex cannot be made to support symbols for symbolic lexmin; this requires
a second class. In preparation

[MLIR][Presburger] Factor out some functionality from LexSimplex into a LexSimplexBase

LexSimplex cannot be made to support symbols for symbolic lexmin; this requires
a second class. In preparation for upstreaming support for symbolic lexmin,
keep the part of LexSimplex that are specific to non-symbolic lexmin in LexSimplex
and move the parts that are required to a common class LexSimplexBase for both to
inherit from.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D122828

show more ...

Revert "[MLIR][Presburger] LexSimplex::addEquality: add equalities as fixed columns"

This reverts commit 5630143af33f7e6e0dabdf38982cc9800140bb75. The
implementation in this commit was incorrect. Al

Revert "[MLIR][Presburger] LexSimplex::addEquality: add equalities as fixed columns"

This reverts commit 5630143af33f7e6e0dabdf38982cc9800140bb75. 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.

show more ...

[MLIR][Presburger] Simplify std::{all,any}_of -> llvm::{all,any}_of (NFC)

Also simplify [](const F &f){ return f.foo(); } -> std::mem_fn(&F::foo)

[MLIR][Presburger] LexSimplex::addEquality: add equalities as fixed columns

In LexSimplex, instead of adding equalities as a pair of inequalities,
add them as a single row, move them into the basis,

[MLIR][Presburger] LexSimplex::addEquality: add equalities as fixed columns

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

show more ...

[MLIR][Presburger] Introduce SimplexRollbackScopeExit to rollback on scope exit

This simplifies many places where we just want to do something in a "transient context"
and return some value.

Review

[MLIR][Presburger] Introduce SimplexRollbackScopeExit to rollback on scope exit

This simplifies many places where we just want to do something in a "transient context"
and return some value.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D122172

show more ...

[MLIR][Presburger] add Simplex:addDivisionVariable

This is a convenience function for adding new divisions to the Simplex given the numerator and denominator.

This will be needed for symbolic integ

[MLIR][Presburger] add Simplex:addDivisionVariable

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

show more ...