[Mlir-commits] [mlir] [MLIR][Presburger] Add simplify function (PR #69107)

llvmlistbot at llvm.org llvmlistbot at llvm.org
Sat Oct 21 22:26:32 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/8] [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/8] [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/8] [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/8] [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/8] [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/8] [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/8] [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;
   }

>From 333591aa124bc8e5cde36646259cae55bdbe38d8 Mon Sep 17 00:00:00 2001
From: gilsaia <794433219 at qq.com>
Date: Sun, 22 Oct 2023 13:25:55 +0800
Subject: [PATCH 8/8] [fix] use smallvector to store

---
 .../Analysis/Presburger/IntegerRelation.cpp   | 20 +++++++------------
 1 file changed, 7 insertions(+), 13 deletions(-)

diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index 451157384baa4e0..a18947a04602a57 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -2316,14 +2316,14 @@ bool IntegerRelation::removeDuplicateConstraints() {
     --ineqs;
   }
 
-  // Check the neg form of each inequality, need an extra space to store it.
-  inequalities.appendExtraRow();
-  bool negChanged = false;
+  // Check the neg form of each inequality, need an extra vector to store it.
+  SmallVector<MPInt> negIneq(cols - 1);
   for (unsigned k = 0; k < ineqs; ++k) {
-    inequalities.copyRow(k, ineqs);
-    inequalities.negateRow(ineqs);
-    row = getInequality(ineqs).drop_back();
-    if (!hashTable.contains(row))
+    row = getInequality(k).drop_back();
+    negIneq.assign(row.begin(), row.end());
+    for (MPInt &ele : negIneq)
+      ele = -ele;
+    if (!hashTable.contains(negIneq))
       continue;
 
     // For cases where the neg is the same as other inequalities, check that the
@@ -2335,13 +2335,11 @@ bool IntegerRelation::removeDuplicateConstraints() {
 
     // 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(k);
       removeInequality(l);
     } else
@@ -2349,10 +2347,6 @@ bool IntegerRelation::removeDuplicateConstraints() {
     break;
   }
 
-  // Need to remove the extra space requested.
-  if (!negChanged)
-    removeInequality(ineqs);
-
   return changed;
 }
 



More information about the Mlir-commits mailing list