[Mlir-commits] [mlir] [MLIR][Presburger] Add simplify function (PR #69107)
llvmlistbot at llvm.org
llvmlistbot at llvm.org
Tue Oct 17 07:00:14 PDT 2023
https://github.com/gilsaia updated https://github.com/llvm/llvm-project/pull/69107
>From 670abc791f35d1e87f4527fa3d2df60ecb810ef8 Mon Sep 17 00:00:00 2001
From: gilsaia <794433219 at qq.com>
Date: Wed, 2 Aug 2023 21:11:59 +0800
Subject: [PATCH 1/7] [MLIR][Presburger] Add simplify function
Differential Revision: https://reviews.llvm.org/D156885
---
.../Analysis/Presburger/IntegerRelation.h | 19 +++
.../Analysis/Presburger/PresburgerRelation.h | 4 +
.../Analysis/Presburger/IntegerRelation.cpp | 141 ++++++++++++++++++
.../Presburger/PresburgerRelation.cpp | 9 ++
4 files changed, 173 insertions(+)
diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
index 56484622ec980cd..1e7af965720c920 100644
--- a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
@@ -324,6 +324,10 @@ class IntegerRelation {
/// Removes all equalities and inequalities.
void clearConstraints();
+ /// Clear all constraints and add an invalid equation indicating that the set
+ /// is empty.
+ void setEmpty();
+
/// Sets the `values.size()` variables starting at `po`s to the specified
/// values and removes them.
void setAndEliminate(unsigned pos, ArrayRef<MPInt> values);
@@ -545,6 +549,10 @@ class IntegerRelation {
void removeDuplicateDivs();
+ /// Attempts to simplify the constraints. The return value indicates whether
+ /// the set is empty.
+ bool simplify();
+
/// Converts variables of kind srcKind in the range [varStart, varLimit) to
/// variables of kind dstKind. If `pos` is given, the variables are placed at
/// position `pos` of dstKind, otherwise they are placed after all the other
@@ -724,6 +732,12 @@ class IntegerRelation {
/// Returns the number of variables eliminated.
unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit);
+ /// Perform a Gaussian elimination operation to reduce all equations to
+ /// standard form, and call setempty for cases that are clearly empty. the
+ /// return value indicates whether the number of constraints has been modified
+ /// or not.
+ bool gaussianEliminate();
+
/// Eliminates the variable at the specified position using Fourier-Motzkin
/// variable elimination, but uses Gaussian elimination if there is an
/// equality involving that variable. If the result of the elimination is
@@ -755,6 +769,11 @@ class IntegerRelation {
/// equalities.
bool isColZero(unsigned pos) const;
+ /// Checks for identical inequalities and eliminates redundant inequalities.
+ /// The return value indicates whether the number of constraints has been
+ /// modified.
+ bool removeDuplicateConstraints();
+
/// Returns false if the fields corresponding to various variable counts, or
/// equality/inequality buffer sizes aren't consistent; true otherwise. This
/// is meant to be used within an assert internally.
diff --git a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
index 0c9c5cf67b4c3c1..4ed4f62860bd85c 100644
--- a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
@@ -213,6 +213,10 @@ class PresburgerRelation {
/// also be a union of convex disjuncts.
PresburgerRelation computeReprWithOnlyDivLocals() const;
+ /// Simplify each disjunct, if it is empty it will not be merged into the new
+ /// set.
+ PresburgerRelation simplify();
+
/// Print the set's internal state.
void print(raw_ostream &os) const;
void dump() const;
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index be764bd7c9176b9..455fe01874c17cc 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -445,6 +445,15 @@ void IntegerRelation::clearConstraints() {
inequalities.resizeVertically(0);
}
+void IntegerRelation::setEmpty() {
+ clearConstraints();
+ auto col = getNumCols();
+ std::vector<int64_t> eqeff(col, 0);
+ eqeff.back() = 1;
+ ArrayRef<int64_t> eq(eqeff);
+ addEquality(eq);
+}
+
/// Gather all lower and upper bounds of the variable at `pos`, and
/// optionally any equalities on it. In addition, the bounds are to be
/// independent of variables in position range [`offset`, `offset` + `num`).
@@ -1079,6 +1088,57 @@ unsigned IntegerRelation::gaussianEliminateVars(unsigned posStart,
return posLimit - posStart;
}
+bool IntegerRelation::gaussianEliminate() {
+ gcdTightenInequalities();
+ unsigned firstVar = 0, vars = getNumVars();
+ unsigned nowDone, eqs, pivotRow;
+ for (nowDone = 0, eqs = getNumEqualities(); nowDone < eqs; ++nowDone) {
+ // Finds the first non-empty column.
+ for (; firstVar < vars; ++firstVar) {
+ if (!findConstraintWithNonZeroAt(firstVar, true, &pivotRow))
+ continue;
+ break;
+ }
+ // All columns have been normalized.
+ if (firstVar >= vars)
+ break;
+
+ // The first pivot row found is below where it should currently be placed.
+ if (pivotRow > nowDone) {
+ equalities.swapRows(pivotRow, nowDone);
+ pivotRow = nowDone;
+ }
+
+ // Normalize all lower equations and all inequalities.
+ for (unsigned i = nowDone + 1; i < eqs; ++i) {
+ eliminateFromConstraint(this, i, pivotRow, firstVar, 0, true);
+ equalities.normalizeRow(i);
+ }
+ for (unsigned i = 0, ineqs = getNumInequalities(); i < ineqs; ++i) {
+ eliminateFromConstraint(this, i, pivotRow, firstVar, 0, false);
+ inequalities.normalizeRow(i);
+ }
+ gcdTightenInequalities();
+ }
+
+ // No redundant rows.
+ if (nowDone == eqs)
+ return false;
+
+ // Check to see if the redundant rows constant is zero, a non-zero value means
+ // the set is empty.
+ for (unsigned i = nowDone; i < eqs; ++i) {
+ if (atEq(i, vars) == 0)
+ continue;
+
+ setEmpty();
+ return true;
+ }
+ // Rows that are confirmed to be all zeros can be eliminated.
+ removeEqualityRange(nowDone, eqs);
+ return true;
+}
+
// A more complex check to eliminate redundant inequalities. Uses FourierMotzkin
// to check if a constraint is redundant.
void IntegerRelation::removeRedundantInequalities() {
@@ -1269,6 +1329,21 @@ void IntegerRelation::removeDuplicateDivs() {
divs.removeDuplicateDivs(merge);
}
+bool IntegerRelation::simplify() {
+ bool changed = true;
+ // Repeat the attempt when there is a modification to the constraints.
+ while (changed) {
+ changed = false;
+ normalizeConstraintsByGCD();
+ changed |= gaussianEliminate();
+ if (isEmptyByGCDTest() || hasInvalidConstraint())
+ return false;
+ changed |= removeDuplicateConstraints();
+ }
+ // Current set is not empty.
+ return true;
+}
+
/// Removes local variables using equalities. Each equality is checked if it
/// can be reduced to the form: `e = affine-expr`, where `e` is a local
/// variable and `affine-expr` is an affine expression not containing `e`.
@@ -2216,6 +2291,72 @@ IntegerPolyhedron IntegerRelation::getDomainSet() const {
return IntegerPolyhedron(std::move(copyRel));
}
+bool IntegerRelation::removeDuplicateConstraints() {
+ bool changed = false;
+ SmallDenseMap<ArrayRef<MPInt>, unsigned> hashTable;
+ unsigned ineqs = getNumInequalities(), cols = getNumCols();
+
+ if (ineqs <= 1)
+ return changed;
+
+ // Check only the non-constant part of the constraint is the same.
+ auto row = getInequality(0).drop_back();
+ hashTable.insert({row, 0});
+ for (unsigned k = 1; k < ineqs; ++k) {
+ auto nRow = getInequality(k).drop_back();
+ if (!hashTable.contains(nRow)) {
+ hashTable.insert({nRow, k});
+ continue;
+ }
+
+ // For identical cases, keep only the smaller part of the constant term.
+ unsigned l = hashTable[nRow];
+ changed = true;
+ if (atIneq(k, cols - 1) <= atIneq(l, cols - 1))
+ inequalities.swapRows(k, l);
+ removeInequality(k);
+ --k;
+ --ineqs;
+ }
+
+ // Check the neg form of each inequality, need an extra space to store it.
+ inequalities.appendExtraRow();
+ bool negChanged = false;
+ for (unsigned k = 0; k < ineqs; ++k) {
+ inequalities.copyRow(k, ineqs);
+ inequalities.negateRow(ineqs);
+ auto nRow = getInequality(ineqs).drop_back();
+ if (!hashTable.contains(nRow))
+ continue;
+
+ // For cases where the neg is the same as other inequalities, check that the
+ // sum of their constant terms is positive.
+ unsigned l = hashTable[nRow];
+ auto sum = atIneq(l, cols - 1) + atIneq(k, cols - 1);
+ if (sum > 0)
+ continue;
+
+ // A sum of constant terms equal to zero combines two inequalities into one
+ // equation, less than zero means the set is empty.
+ negChanged = true;
+ changed = true;
+ if (sum == 0) {
+ addEquality(getInequality(k));
+ removeInequality(ineqs);
+ removeInequality(l);
+ removeInequality(k);
+ } else
+ setEmpty();
+ break;
+ }
+
+ // Need to remove the extra space requested.
+ if (!negChanged)
+ removeInequality(ineqs);
+
+ return changed;
+}
+
IntegerPolyhedron IntegerRelation::getRangeSet() const {
IntegerRelation copyRel = *this;
diff --git a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
index 5a9cf71fc86793f..7036c590e815e3c 100644
--- a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
@@ -1015,6 +1015,15 @@ bool PresburgerRelation::hasOnlyDivLocals() const {
});
}
+PresburgerRelation PresburgerRelation::simplify() {
+ PresburgerRelation rel = PresburgerRelation(getSpace());
+ for (IntegerRelation &disjunct : disjuncts) {
+ if (disjunct.simplify())
+ rel.unionInPlace(disjunct);
+ }
+ return rel;
+}
+
void PresburgerRelation::print(raw_ostream &os) const {
os << "Number of Disjuncts: " << getNumDisjuncts() << "\n";
for (const IntegerRelation &disjunct : disjuncts) {
>From 633332503e60322185f8dc550740e990652772d0 Mon Sep 17 00:00:00 2001
From: gilsaia <794433219 at qq.com>
Date: Tue, 8 Aug 2023 21:18:00 +0800
Subject: [PATCH 2/7] [fix] change comment & add isplainempty
---
.../Analysis/Presburger/IntegerRelation.h | 17 +++++------
.../Analysis/Presburger/IntegerRelation.cpp | 29 +++++++++++--------
.../Presburger/PresburgerRelation.cpp | 3 +-
3 files changed, 27 insertions(+), 22 deletions(-)
diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
index 1e7af965720c920..94ad0e6e6e9728d 100644
--- a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
@@ -326,7 +326,7 @@ class IntegerRelation {
/// Clear all constraints and add an invalid equation indicating that the set
/// is empty.
- void setEmpty();
+ void markSetEmpty();
/// Sets the `values.size()` variables starting at `po`s to the specified
/// values and removes them.
@@ -355,6 +355,9 @@ class IntegerRelation {
/// Returns false otherwise.
bool isEmpty() const;
+ /// Performs GCD checks and invalid constraint checks.
+ bool isPlainEmpty() const;
+
/// Runs the GCD test on all equality constraints. Returns true if this test
/// fails on any equality. Returns false otherwise.
/// This test can be used to disprove the existence of a solution. If it
@@ -549,9 +552,8 @@ class IntegerRelation {
void removeDuplicateDivs();
- /// Attempts to simplify the constraints. The return value indicates whether
- /// the set is empty.
- bool simplify();
+ /// Attempts to simplify the constraints.
+ void simplify();
/// Converts variables of kind srcKind in the range [varStart, varLimit) to
/// variables of kind dstKind. If `pos` is given, the variables are placed at
@@ -733,9 +735,7 @@ class IntegerRelation {
unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit);
/// Perform a Gaussian elimination operation to reduce all equations to
- /// standard form, and call setempty for cases that are clearly empty. the
- /// return value indicates whether the number of constraints has been modified
- /// or not.
+ /// standard form. The return value indicates if anything was modified.
bool gaussianEliminate();
/// Eliminates the variable at the specified position using Fourier-Motzkin
@@ -770,8 +770,7 @@ class IntegerRelation {
bool isColZero(unsigned pos) const;
/// Checks for identical inequalities and eliminates redundant inequalities.
- /// The return value indicates whether the number of constraints has been
- /// modified.
+ /// The return value indicates if anything has changed.
bool removeDuplicateConstraints();
/// Returns false if the fields corresponding to various variable counts, or
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index 455fe01874c17cc..439631307c167d5 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -445,13 +445,12 @@ void IntegerRelation::clearConstraints() {
inequalities.resizeVertically(0);
}
-void IntegerRelation::setEmpty() {
+void IntegerRelation::markSetEmpty() {
clearConstraints();
- auto col = getNumCols();
- std::vector<int64_t> eqeff(col, 0);
+ unsigned col = getNumCols();
+ SmallVector<int64_t> eqeff(col, 0);
eqeff.back() = 1;
- ArrayRef<int64_t> eq(eqeff);
- addEquality(eq);
+ addEquality(eqeff);
}
/// Gather all lower and upper bounds of the variable at `pos`, and
@@ -710,6 +709,12 @@ bool IntegerRelation::isEmpty() const {
return false;
}
+bool IntegerRelation::isPlainEmpty() const {
+ if (isEmptyByGCDTest() || hasInvalidConstraint())
+ return true;
+ return false;
+}
+
// Runs the GCD test on all equality constraints. Returns 'true' if this test
// fails on any equality. Returns 'false' otherwise.
// This test can be used to disprove the existence of a solution. If it returns
@@ -1131,7 +1136,7 @@ bool IntegerRelation::gaussianEliminate() {
if (atEq(i, vars) == 0)
continue;
- setEmpty();
+ markSetEmpty();
return true;
}
// Rows that are confirmed to be all zeros can be eliminated.
@@ -1329,19 +1334,19 @@ void IntegerRelation::removeDuplicateDivs() {
divs.removeDuplicateDivs(merge);
}
-bool IntegerRelation::simplify() {
+void IntegerRelation::simplify() {
bool changed = true;
- // Repeat the attempt when there is a modification to the constraints.
+ // Repeat until we reach a fixed point.
while (changed) {
changed = false;
normalizeConstraintsByGCD();
changed |= gaussianEliminate();
- if (isEmptyByGCDTest() || hasInvalidConstraint())
- return false;
+ if (isPlainEmpty())
+ return;
changed |= removeDuplicateConstraints();
}
// Current set is not empty.
- return true;
+ return;
}
/// Removes local variables using equalities. Each equality is checked if it
@@ -2346,7 +2351,7 @@ bool IntegerRelation::removeDuplicateConstraints() {
removeInequality(l);
removeInequality(k);
} else
- setEmpty();
+ markSetEmpty();
break;
}
diff --git a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
index 7036c590e815e3c..5b402944928ec9a 100644
--- a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
@@ -1018,7 +1018,8 @@ bool PresburgerRelation::hasOnlyDivLocals() const {
PresburgerRelation PresburgerRelation::simplify() {
PresburgerRelation rel = PresburgerRelation(getSpace());
for (IntegerRelation &disjunct : disjuncts) {
- if (disjunct.simplify())
+ disjunct.simplify();
+ if (!disjunct.isPlainEmpty())
rel.unionInPlace(disjunct);
}
return rel;
>From 5e8ffabfa9505366ef1ebae24a22c34e70e9a113 Mon Sep 17 00:00:00 2001
From: gilsaia <794433219 at qq.com>
Date: Sat, 19 Aug 2023 00:11:04 +0800
Subject: [PATCH 3/7] [fix] add comment & fix bug
---
.../mlir/Analysis/Presburger/IntegerRelation.h | 4 +++-
.../mlir/Analysis/Presburger/PresburgerRelation.h | 6 +++---
mlir/lib/Analysis/Presburger/IntegerRelation.cpp | 6 ++++--
.../lib/Analysis/Presburger/PresburgerRelation.cpp | 14 +++++++++-----
4 files changed, 19 insertions(+), 11 deletions(-)
diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
index 94ad0e6e6e9728d..14adeb66e93ad9e 100644
--- a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
@@ -552,7 +552,9 @@ class IntegerRelation {
void removeDuplicateDivs();
- /// Attempts to simplify the constraints.
+ /// Simplify iteratively attempt to remove redundant equations by Gaussian
+ /// elimination and attempt to remove duplicate inequalities until a fixed
+ /// point is reached.
void simplify();
/// Converts variables of kind srcKind in the range [varStart, varLimit) to
diff --git a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
index 4ed4f62860bd85c..e7461145f2653c1 100644
--- a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
@@ -213,9 +213,9 @@ class PresburgerRelation {
/// also be a union of convex disjuncts.
PresburgerRelation computeReprWithOnlyDivLocals() const;
- /// Simplify each disjunct, if it is empty it will not be merged into the new
- /// set.
- PresburgerRelation simplify();
+ /// Simplify each disjunct, see IntegerRelation::simplify for details. If
+ /// disjunct is empty it will not be merged into the new set.
+ PresburgerRelation simplify() const;
/// Print the set's internal state.
void print(raw_ostream &os) const;
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index 439631307c167d5..e3339b44888e920 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -2338,18 +2338,20 @@ bool IntegerRelation::removeDuplicateConstraints() {
// sum of their constant terms is positive.
unsigned l = hashTable[nRow];
auto sum = atIneq(l, cols - 1) + atIneq(k, cols - 1);
- if (sum > 0)
+ if (sum > 0 || l == k)
continue;
// A sum of constant terms equal to zero combines two inequalities into one
// equation, less than zero means the set is empty.
negChanged = true;
changed = true;
+ if (k < l)
+ std::swap(l, k);
if (sum == 0) {
addEquality(getInequality(k));
removeInequality(ineqs);
- removeInequality(l);
removeInequality(k);
+ removeInequality(l);
} else
markSetEmpty();
break;
diff --git a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
index 5b402944928ec9a..f5380db9192f0ce 100644
--- a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
@@ -576,6 +576,9 @@ static PresburgerRelation getSetDifference(IntegerRelation b,
}
}
+ // Try to simplify the results.
+ result = result.simplify();
+
return result;
}
@@ -1015,14 +1018,15 @@ bool PresburgerRelation::hasOnlyDivLocals() const {
});
}
-PresburgerRelation PresburgerRelation::simplify() {
- PresburgerRelation rel = PresburgerRelation(getSpace());
- for (IntegerRelation &disjunct : disjuncts) {
+PresburgerRelation PresburgerRelation::simplify() const {
+ PresburgerRelation origin = *this;
+ PresburgerRelation result = PresburgerRelation(getSpace());
+ for (IntegerRelation &disjunct : origin.disjuncts) {
disjunct.simplify();
if (!disjunct.isPlainEmpty())
- rel.unionInPlace(disjunct);
+ result.unionInPlace(disjunct);
}
- return rel;
+ return result;
}
void PresburgerRelation::print(raw_ostream &os) const {
>From cf459cd52e2a655049fe223011ab81d7e29ed400 Mon Sep 17 00:00:00 2001
From: gilsaia <794433219 at qq.com>
Date: Mon, 21 Aug 2023 22:42:07 +0800
Subject: [PATCH 4/7] [fix] from plain to obviously & add getEmpty
---
.../Analysis/Presburger/IntegerRelation.h | 17 +++++----
.../Analysis/Presburger/PresburgerRelation.h | 6 ++--
.../Analysis/Presburger/IntegerRelation.cpp | 18 +++-------
.../Presburger/PresburgerRelation.cpp | 36 ++++++++++---------
4 files changed, 39 insertions(+), 38 deletions(-)
diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
index 14adeb66e93ad9e..b2cfe57c55ba3d4 100644
--- a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
@@ -91,6 +91,15 @@ class IntegerRelation {
return IntegerRelation(space);
}
+ /// Return an empty system containing an invalid equation 0=1.
+ static IntegerRelation getEmpty(const PresburgerSpace &space) {
+ IntegerRelation relult(0, 1, space.getNumVars() + 1, space);
+ SmallVector<int64_t> eqeff(space.getNumVars() + 1, 0);
+ eqeff.back() = 1;
+ relult.addEquality(eqeff);
+ return relult;
+ }
+
/// Return the kind of this IntegerRelation.
virtual Kind getKind() const { return Kind::IntegerRelation; }
@@ -138,7 +147,7 @@ class IntegerRelation {
/// returns false. The equality check is performed in a plain manner, by
/// comparing if all the equalities and inequalities in `this` and `other`
/// are the same.
- bool isPlainEqual(const IntegerRelation &other) const;
+ bool isObviouslyEqual(const IntegerRelation &other) const;
/// Return whether this is a subset of the given IntegerRelation. This is
/// integer-exact and somewhat expensive, since it uses the integer emptiness
@@ -324,10 +333,6 @@ class IntegerRelation {
/// Removes all equalities and inequalities.
void clearConstraints();
- /// Clear all constraints and add an invalid equation indicating that the set
- /// is empty.
- void markSetEmpty();
-
/// Sets the `values.size()` variables starting at `po`s to the specified
/// values and removes them.
void setAndEliminate(unsigned pos, ArrayRef<MPInt> values);
@@ -356,7 +361,7 @@ class IntegerRelation {
bool isEmpty() const;
/// Performs GCD checks and invalid constraint checks.
- bool isPlainEmpty() const;
+ bool isObviouslyEmpty() const;
/// Runs the GCD test on all equality constraints. Returns true if this test
/// fails on any equality. Returns false otherwise.
diff --git a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
index e7461145f2653c1..0aeb26d2c28baae 100644
--- a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
@@ -169,17 +169,17 @@ class PresburgerRelation {
bool isIntegerEmpty() const;
/// Return true if there is no disjunct, false otherwise.
- bool isPlainEmpty() const;
+ bool isObviouslyEmpty() const;
/// Return true if the set is known to have one unconstrained disjunct, false
/// otherwise.
- bool isPlainUniverse() const;
+ bool isObviouslyUniverse() const;
/// Perform a quick equality check on `this` and `other`. The relations are
/// equal if the check return true, but may or may not be equal if the check
/// returns false. This is doing by directly comparing whether each internal
/// disjunct is the same.
- bool isPlainEqual(const PresburgerRelation &set) const;
+ bool isObviouslyEqual(const PresburgerRelation &set) const;
/// Return true if the set is consist of a single disjunct, without any local
/// variables, false otherwise.
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index e3339b44888e920..d77507fd45a8423 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -80,7 +80,7 @@ bool IntegerRelation::isEqual(const IntegerRelation &other) const {
return PresburgerRelation(*this).isEqual(PresburgerRelation(other));
}
-bool IntegerRelation::isPlainEqual(const IntegerRelation &other) const {
+bool IntegerRelation::isObviouslyEqual(const IntegerRelation &other) const {
if (!space.isEqual(other.getSpace()))
return false;
if (getNumEqualities() != other.getNumEqualities())
@@ -445,14 +445,6 @@ void IntegerRelation::clearConstraints() {
inequalities.resizeVertically(0);
}
-void IntegerRelation::markSetEmpty() {
- clearConstraints();
- unsigned col = getNumCols();
- SmallVector<int64_t> eqeff(col, 0);
- eqeff.back() = 1;
- addEquality(eqeff);
-}
-
/// Gather all lower and upper bounds of the variable at `pos`, and
/// optionally any equalities on it. In addition, the bounds are to be
/// independent of variables in position range [`offset`, `offset` + `num`).
@@ -709,7 +701,7 @@ bool IntegerRelation::isEmpty() const {
return false;
}
-bool IntegerRelation::isPlainEmpty() const {
+bool IntegerRelation::isObviouslyEmpty() const {
if (isEmptyByGCDTest() || hasInvalidConstraint())
return true;
return false;
@@ -1136,7 +1128,7 @@ bool IntegerRelation::gaussianEliminate() {
if (atEq(i, vars) == 0)
continue;
- markSetEmpty();
+ *this = getEmpty(getSpace());
return true;
}
// Rows that are confirmed to be all zeros can be eliminated.
@@ -1341,7 +1333,7 @@ void IntegerRelation::simplify() {
changed = false;
normalizeConstraintsByGCD();
changed |= gaussianEliminate();
- if (isPlainEmpty())
+ if (isObviouslyEmpty())
return;
changed |= removeDuplicateConstraints();
}
@@ -2353,7 +2345,7 @@ bool IntegerRelation::removeDuplicateConstraints() {
removeInequality(k);
removeInequality(l);
} else
- markSetEmpty();
+ *this = getEmpty(getSpace());
break;
}
diff --git a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
index f5380db9192f0ce..4ddc56aa21f1b9c 100644
--- a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
@@ -83,19 +83,19 @@ void PresburgerRelation::unionInPlace(const IntegerRelation &disjunct) {
void PresburgerRelation::unionInPlace(const PresburgerRelation &set) {
assert(space.isCompatible(set.getSpace()) && "Spaces should match");
- if (isPlainEqual(set))
+ if (isObviouslyEqual(set))
return;
- if (isPlainEmpty()) {
+ if (isObviouslyEmpty()) {
disjuncts = set.disjuncts;
return;
}
- if (set.isPlainEmpty())
+ if (set.isObviouslyEmpty())
return;
- if (isPlainUniverse())
+ if (isObviouslyUniverse())
return;
- if (set.isPlainUniverse()) {
+ if (set.isObviouslyUniverse()) {
disjuncts = set.disjuncts;
return;
}
@@ -144,10 +144,10 @@ PresburgerRelation::intersect(const PresburgerRelation &set) const {
// If the set is empty or the other set is universe,
// directly return the set
- if (isPlainEmpty() || set.isPlainUniverse())
+ if (isObviouslyEmpty() || set.isObviouslyUniverse())
return *this;
- if (set.isPlainEmpty() || isPlainUniverse())
+ if (set.isObviouslyEmpty() || isObviouslyUniverse())
return set;
PresburgerRelation result(getSpace());
@@ -596,7 +596,7 @@ PresburgerRelation::subtract(const PresburgerRelation &set) const {
// If we know that the two sets are clearly equal, we can simply return the
// empty set.
- if (isPlainEqual(set))
+ if (isObviouslyEqual(set))
return result;
// We compute (U_i t_i) \ (U_i set_i) as U_i (t_i \ V_i set_i).
@@ -618,7 +618,7 @@ bool PresburgerRelation::isEqual(const PresburgerRelation &set) const {
return this->isSubsetOf(set) && set.isSubsetOf(*this);
}
-bool PresburgerRelation::isPlainEqual(const PresburgerRelation &set) const {
+bool PresburgerRelation::isObviouslyEqual(const PresburgerRelation &set) const {
if (!space.isCompatible(set.getSpace()))
return false;
@@ -628,7 +628,7 @@ bool PresburgerRelation::isPlainEqual(const PresburgerRelation &set) const {
// Compare each disjunct in this PresburgerRelation with the corresponding
// disjunct in the other PresburgerRelation.
for (unsigned int i = 0, n = getNumDisjuncts(); i < n; ++i) {
- if (!getDisjunct(i).isPlainEqual(set.getDisjunct(i)))
+ if (!getDisjunct(i).isObviouslyEqual(set.getDisjunct(i)))
return false;
}
return true;
@@ -638,10 +638,12 @@ bool PresburgerRelation::isPlainEqual(const PresburgerRelation &set) const {
/// otherwise. It is a simple check that only check if the relation has at least
/// one unconstrained disjunct, indicating the absence of constraints or
/// conditions.
-bool PresburgerRelation::isPlainUniverse() const {
- return llvm::any_of(getAllDisjuncts(), [](const IntegerRelation &disjunct) {
- return disjunct.getNumConstraints() == 0;
- });
+bool PresburgerRelation::isObviouslyUniverse() const {
+ for (auto &disjunct : getAllDisjuncts()) {
+ if (disjunct.getNumConstraints() == 0)
+ return true;
+ }
+ return false;
}
bool PresburgerRelation::isConvexNoLocals() const {
@@ -649,7 +651,9 @@ bool PresburgerRelation::isConvexNoLocals() const {
}
/// Return true if there is no disjunct, false otherwise.
-bool PresburgerRelation::isPlainEmpty() const { return getNumDisjuncts() == 0; }
+bool PresburgerRelation::isObviouslyEmpty() const {
+ return getNumDisjuncts() == 0;
+}
/// Return true if all the sets in the union are known to be integer empty,
/// false otherwise.
@@ -1023,7 +1027,7 @@ PresburgerRelation PresburgerRelation::simplify() const {
PresburgerRelation result = PresburgerRelation(getSpace());
for (IntegerRelation &disjunct : origin.disjuncts) {
disjunct.simplify();
- if (!disjunct.isPlainEmpty())
+ if (!disjunct.isObviouslyEmpty())
result.unionInPlace(disjunct);
}
return result;
>From 92d39d5121953d34818aca04654537ab56bc5444 Mon Sep 17 00:00:00 2001
From: gilsaia <794433219 at qq.com>
Date: Tue, 17 Oct 2023 16:11:34 +0800
Subject: [PATCH 5/7] [fix] change include file comment & var name
---
.../Analysis/Presburger/IntegerRelation.h | 19 +++++++++----------
.../Analysis/Presburger/PresburgerRelation.h | 4 ++--
2 files changed, 11 insertions(+), 12 deletions(-)
diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
index b2cfe57c55ba3d4..613b098d6e8d0d8 100644
--- a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
@@ -91,13 +91,13 @@ class IntegerRelation {
return IntegerRelation(space);
}
- /// Return an empty system containing an invalid equation 0=1.
+ /// Return an empty system containing an invalid equation 0 = 1.
static IntegerRelation getEmpty(const PresburgerSpace &space) {
- IntegerRelation relult(0, 1, space.getNumVars() + 1, space);
- SmallVector<int64_t> eqeff(space.getNumVars() + 1, 0);
- eqeff.back() = 1;
- relult.addEquality(eqeff);
- return relult;
+ IntegerRelation result(0, 1, space.getNumVars() + 1, space);
+ SmallVector<int64_t> invalidEq(space.getNumVars() + 1, 0);
+ invalidEq.back() = 1;
+ result.addEquality(invalidEq);
+ return result;
}
/// Return the kind of this IntegerRelation.
@@ -557,9 +557,8 @@ class IntegerRelation {
void removeDuplicateDivs();
- /// Simplify iteratively attempt to remove redundant equations by Gaussian
- /// elimination and attempt to remove duplicate inequalities until a fixed
- /// point is reached.
+ /// Simplify the constraint system by removing canonicalizing constraints and
+ /// removing redundant constraints.
void simplify();
/// Converts variables of kind srcKind in the range [varStart, varLimit) to
@@ -742,7 +741,7 @@ class IntegerRelation {
unsigned gaussianEliminateVars(unsigned posStart, unsigned posLimit);
/// Perform a Gaussian elimination operation to reduce all equations to
- /// standard form. The return value indicates if anything was modified.
+ /// standard form. Returns whether the constraint system was modified.
bool gaussianEliminate();
/// Eliminates the variable at the specified position using Fourier-Motzkin
diff --git a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
index 0aeb26d2c28baae..c6b00eca90733a0 100644
--- a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
@@ -213,8 +213,8 @@ class PresburgerRelation {
/// also be a union of convex disjuncts.
PresburgerRelation computeReprWithOnlyDivLocals() const;
- /// Simplify each disjunct, see IntegerRelation::simplify for details. If
- /// disjunct is empty it will not be merged into the new set.
+ /// Simplify each disjunct, canonicalizing each disjunct and removing
+ /// redundencies.
PresburgerRelation simplify() const;
/// Print the set's internal state.
>From 900dae03382b1ef1a09fe362e85ac69f1f1356cd Mon Sep 17 00:00:00 2001
From: gilsaia <794433219 at qq.com>
Date: Tue, 17 Oct 2023 16:16:38 +0800
Subject: [PATCH 6/7] [fix] change include file comment
---
mlir/include/mlir/Analysis/Presburger/IntegerRelation.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
index 613b098d6e8d0d8..4c6b810f92e95af 100644
--- a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
+++ b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
@@ -776,7 +776,7 @@ class IntegerRelation {
bool isColZero(unsigned pos) const;
/// Checks for identical inequalities and eliminates redundant inequalities.
- /// The return value indicates if anything has changed.
+ /// Returns whether the constraint system was modified.
bool removeDuplicateConstraints();
/// Returns false if the fields corresponding to various variable counts, or
>From 2167004b21b731c0971b1bc5195db31b9dc1920c Mon Sep 17 00:00:00 2001
From: gilsaia <794433219 at qq.com>
Date: Tue, 17 Oct 2023 21:59:49 +0800
Subject: [PATCH 7/7] [fix] change var name & auto
---
.../Analysis/Presburger/IntegerRelation.cpp | 26 +++++++++----------
.../Presburger/PresburgerRelation.cpp | 2 +-
2 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index d77507fd45a8423..451157384baa4e0 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -1096,7 +1096,7 @@ bool IntegerRelation::gaussianEliminate() {
continue;
break;
}
- // All columns have been normalized.
+ // The matrix has been normalized to row echelon form.
if (firstVar >= vars)
break;
@@ -1131,7 +1131,7 @@ bool IntegerRelation::gaussianEliminate() {
*this = getEmpty(getSpace());
return true;
}
- // Rows that are confirmed to be all zeros can be eliminated.
+ // Eliminate rows that are confined to be all zeros.
removeEqualityRange(nowDone, eqs);
return true;
}
@@ -1330,11 +1330,11 @@ void IntegerRelation::simplify() {
bool changed = true;
// Repeat until we reach a fixed point.
while (changed) {
+ if (isObviouslyEmpty())
+ return;
changed = false;
normalizeConstraintsByGCD();
changed |= gaussianEliminate();
- if (isObviouslyEmpty())
- return;
changed |= removeDuplicateConstraints();
}
// Current set is not empty.
@@ -2296,18 +2296,18 @@ bool IntegerRelation::removeDuplicateConstraints() {
if (ineqs <= 1)
return changed;
- // Check only the non-constant part of the constraint is the same.
- auto row = getInequality(0).drop_back();
+ // Check if the non-constant part of the constraint is the same.
+ ArrayRef<MPInt> row = getInequality(0).drop_back();
hashTable.insert({row, 0});
for (unsigned k = 1; k < ineqs; ++k) {
- auto nRow = getInequality(k).drop_back();
- if (!hashTable.contains(nRow)) {
- hashTable.insert({nRow, k});
+ row = getInequality(k).drop_back();
+ if (!hashTable.contains(row)) {
+ hashTable.insert({row, k});
continue;
}
// For identical cases, keep only the smaller part of the constant term.
- unsigned l = hashTable[nRow];
+ unsigned l = hashTable[row];
changed = true;
if (atIneq(k, cols - 1) <= atIneq(l, cols - 1))
inequalities.swapRows(k, l);
@@ -2322,13 +2322,13 @@ bool IntegerRelation::removeDuplicateConstraints() {
for (unsigned k = 0; k < ineqs; ++k) {
inequalities.copyRow(k, ineqs);
inequalities.negateRow(ineqs);
- auto nRow = getInequality(ineqs).drop_back();
- if (!hashTable.contains(nRow))
+ row = getInequality(ineqs).drop_back();
+ if (!hashTable.contains(row))
continue;
// For cases where the neg is the same as other inequalities, check that the
// sum of their constant terms is positive.
- unsigned l = hashTable[nRow];
+ unsigned l = hashTable[row];
auto sum = atIneq(l, cols - 1) + atIneq(k, cols - 1);
if (sum > 0 || l == k)
continue;
diff --git a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
index 4ddc56aa21f1b9c..a82b60cddc73dac 100644
--- a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
@@ -639,7 +639,7 @@ bool PresburgerRelation::isObviouslyEqual(const PresburgerRelation &set) const {
/// one unconstrained disjunct, indicating the absence of constraints or
/// conditions.
bool PresburgerRelation::isObviouslyUniverse() const {
- for (auto &disjunct : getAllDisjuncts()) {
+ for (const IntegerRelation &disjunct : getAllDisjuncts()) {
if (disjunct.getNumConstraints() == 0)
return true;
}
More information about the Mlir-commits
mailing list