maxjhandsome
/
llvm-project
forked from OSchip/llvm-project
1
0
Fork 0
Code Issues Pull Requests Packages Releases Wiki Activity

[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
This commit is contained in:
Arjun P 2022-04-11 21:21:34 +01:00
parent bb1a1f42db
commit 4aeb2a57f4
1 changed files with 15 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
mlir/lib/Analysis/Presburger/Simplex.cpp
View File

@ -357,8 +357,8 @@ bool SymbolicLexSimplex::isSymbolicSampleIntegral(unsigned row) const {
isRangeDivisibleBy(tableau.getRow(row).slice(3, nSymbol), denom);
}
/// This proceeds similarly to LexSimplex::addCut(). We are given a row that has
/// a symbolic sample value with fractional coefficients.
/// This proceeds similarly to LexSimplexBase::addCut(). We are given a row that
/// has a symbolic sample value with fractional coefficients.
///
/// Let the row be
/// (c + coeffM*M + sum_i a_i*s_i + sum_j b_j*y_j)/d,
@ -374,10 +374,11 @@ bool SymbolicLexSimplex::isSymbolicSampleIntegral(unsigned row) const {
/// sum_i (b_i%d)y_i = ((-c%d) + sum_i (-a_i%d)s_i)%d + k*d for some integer k
///
/// where we take a modulo of the whole symbolic expression on the right to
/// bring it into the range [0, d - 1]. Therefore, as in LexSimplex::addCut,
/// bring it into the range [0, d - 1]. Therefore, as in addCut(),
/// k is the quotient on dividing the LHS by d, and since LHS >= 0, we have
/// k >= 0 as well. We realize the modulo of the symbolic expression by adding a
/// division variable
/// k >= 0 as well. If all the a_i are divisible by d, then we can add the
/// constraint directly. Otherwise, we realize the modulo of the symbolic
/// expression by adding a division variable
///
/// q = ((-c%d) + sum_i (-a_i%d)s_i)/d
///
@ -392,16 +393,22 @@ bool SymbolicLexSimplex::isSymbolicSampleIntegral(unsigned row) const {
LogicalResult SymbolicLexSimplex::addSymbolicCut(unsigned row) {
int64_t d = tableau(row, 0);
// Add the division variable `q` described above to the symbol domain.
// q = ((-c%d) + sum_i (-a_i%d)s_i)/d.
// Construct the division variable `q = ((-c%d) + sum_i (-a_i%d)s_i)/d`.
SmallVector<int64_t, 8> divCoeffs;
divCoeffs.reserve(nSymbol + 1);
int64_t divDenom = d;
for (unsigned col = 3; col < 3 + nSymbol; ++col)
divCoeffs.push_back(mod(-tableau(row, col), divDenom)); // (-a_i%d)s_i
divCoeffs.push_back(mod(-tableau(row, 1), divDenom)); // -c%d.
normalizeDiv(divCoeffs, divDenom);
if (divDenom == 1) {
// The symbolic sample numerator is divisible by the denominator,
// so the division isn't needed. We can add the constraint directly,
// i.e., ignore the symbols and add a regular cut as in addCut().
return addCut(row);
}
domainSimplex.addDivisionVariable(divCoeffs, divDenom);
domainPoly.addLocalFloorDiv(divCoeffs, divDenom);