[MLIR][Presburger] Add simplify function

[gilsaia]

Summary

Added the simplify function to reduce the size of the constraint system, referencing the ISL implementation.

Tested it on a simple Benchmark implemented by myself, calling SImplify before the operation and calling Simplify on the result after Subtract were tested, respectively.

The Benchmark can be found here: benchmark

For the case of calling Simplify before each operation, the overall result is shown in the following figure.

A comparison of the constraint system sizes and time for each operation is as follows

For the case of calling Simplify on the result after Subtract, the overall results are as follows

A comparison of the constraint system sizes and time for subtract is as follows

[Groverkss]

Some initial comments.

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

329

markSetEmpty is a better name maybe.

329

If you are marking something as empty using this special constraint, could you add a check in isPlainEmpty which checks if the set is exactly this condition at start?

557

Do we have to return this "empty" thing here? Simplify should just simplify it and emptiness should be checked with "isPlainEmpty".

740

You don't need to specify this, I feel.

740

741

"Return value indicates if anything was modified"

775–776

Instead of number of constraints, its better if you say "If anything has changed", because you could be changing coefficient values also.

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

450

Please avoid the use of auto unless needed.

451

Use SmallVector instead.

453

You don't need to do this. Just pass eqeff to addEquality.

1339

[grosser]

Does this function some correspondence to isl?

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

775–776

Also, I am not sure what redundant means here. The 'identical' seems to imply that you just drop syntactically identical constraints, but constraints might also be implied by others. Are these implied constraints also eliminated?

[gilsaia]

• [fix] change comment & add isplainempty

[gilsaia]

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

329

I just added isPlainEmpty function to IntegerRelation.

775–776

In addition to the same inequality, it checks if there is a completely opposite inequality except for the constant term, and either discards or converts it to an equation based on the result of the constant term.

[gilsaia]

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

775–776

Also, there is a function in ISL that does essentially the same thing called isl_basic_map_remove_duplicate_constraints.

[arjunp]

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

329

I would prefer a getEmpty() like in PresburgerRelation and then *this = getEmpty(getSpace())

555–556

Maybe briefly describe the kind of simplifications and how long they take to run here.

mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h

193

I prefer "Simplify each disjunct; see IntegerRelation::simplify for details."

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

712

I prefer a name like isObviouslyEmpty. "plain" isn't very clear IMO (I know isl uses it)

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

964

Why does this function modify this as well as return a new relation. It should be one or the other.

965

[gilsaia]

• [fix] add comment & fix bug

[gilsaia]

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

329

But I think that in IntegerRelation, empty means Universe, so markempty here actually adds an impossible constraint

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

712

I think the naming here should be kept uniform with other similar functions, so do we need to change all the similar function names？

[arjunp]

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

329

It's true that an empty list of constraints in IntegerRelation corresponds to the universe, the set of all points. But "empty" doesn't refer to universe! It means the empty set. I would suggest making both getUniverse and getEmpty functions, so it's clear which is which.

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

712

AFAIK there is no currently upstream function that uses it. Yes, I would suggest that for your functions.

[gilsaia]

• [fix] from plain to obviously & add getEmpty

mlir/include/mlir/Analysis/Presburger/IntegerRelation.h

public:
   MaybeOptimum<SmallVector<MPInt, 8>> findIntegerLexMin() const;
 
   /// Swap the posA^th variable with the posB^th variable.
   virtual void swapVar(unsigned posA, unsigned posB);
 
   /// 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);
   void setAndEliminate(unsigned pos, ArrayRef<int64_t> values) {
     setAndEliminate(pos, getMPIntVec(values));
   }
 
   /// Replaces the contents of this IntegerRelation with `other`.
public:
 
   /// Checks for emptiness by performing variable elimination on all
   /// variables, running the GCD test on each equality constraint, and
   /// checking for invalid constraints. Returns true if the GCD test fails for
   /// any equality, or if any invalid constraints are discovered on any row.
   /// 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
   /// returns true, no integer solution to the equality constraints can exist.
   bool isEmptyByGCDTest() const;
 
   /// Returns true if the set of constraints is found to have no solution,
   /// false if a solution exists. Uses the same algorithm as
public:
   /// theoretically take exponential time in the worst case (rare), it is known
   /// to perform much better in the average case. If V is the number of vertices
   /// in the polytope and C is the number of constraints, the algorithm takes
   /// O(VC) time.
   void removeRedundantConstraints();
 
   void removeDuplicateDivs();
 
+  /// 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
   /// 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
   /// variables of kind dstKind. The internal ordering among the moved variables
   /// is preserved.
   void convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit,
                       VarKind dstKind, unsigned pos);
   void convertVarKind(VarKind srcKind, unsigned varStart, unsigned varLimit,
protected:
   /// variable is also removed.
   void removeRedundantLocalVars();
 
   /// Eliminates variables from equality and inequality constraints
   /// in column range [posStart, posLimit).
   /// Returns the number of variables eliminated.
   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.
+  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
   /// integer exact, `*isResultIntegerExact` is set to true. If `darkShadow` is
   /// set to true, a potential under approximation (subset) of the rational
   /// shadow / exact integer shadow is computed.
   // See implementation comments for more details.
   virtual void fourierMotzkinEliminate(unsigned pos, bool darkShadow = false,
protected:
   /// Returns true and sets row found in search in `rowIdx`, false otherwise.
   bool findConstraintWithNonZeroAt(unsigned colIdx, bool isEq,
                                    unsigned *rowIdx) const;
 
   /// Returns true if the pos^th column is all zero for both inequalities and
   /// equalities.
   bool isColZero(unsigned pos) const;
 
+  /// Checks for identical inequalities and eliminates redundant inequalities.
+  /// The return value indicates if anything has changed.
+  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.
   virtual bool hasConsistentState() const;
 
   /// Prints the number of constraints, dimensions, symbols and locals in the
   /// IntegerRelation.
   virtual void printSpace(raw_ostream &os) const;

mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h

public:
   bool hasOnlyDivLocals() const;
 
   /// Compute an equivalent representation of the same relation, such that all
   /// local ids in all disjuncts have division representations. This
   /// representation may involve local ids that correspond to divisions, and may
   /// 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.
+  PresburgerRelation simplify() const;
+
   /// Print the set's internal state.
   void print(raw_ostream &os) const;
   void dump() const;
 
 protected:
   /// Construct an empty PresburgerRelation with the specified number of
   /// dimension and symbols.
   explicit PresburgerRelation(const PresburgerSpace &space) : space(space) {

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

void IntegerRelation::swapVar(unsigned posA, unsigned posB) {
   equalities.swapColumns(posA, posB);
 }
 
 void IntegerRelation::clearConstraints() {
   equalities.resizeVertically(0);
   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`).
 void IntegerRelation::getLowerAndUpperBoundIndices(
     unsigned pos, SmallVectorImpl<unsigned> *lbIndices,
     SmallVectorImpl<unsigned> *ubIndices, SmallVectorImpl<unsigned> *eqIndices,
     unsigned offset, unsigned num) const {
   assert(pos < getNumVars() && "invalid position");
for (unsigned i = 0, e = tmpCst.getNumVars(); i < e; i++) {
     // FM wouldn't have modified the equalities in any way. So no need to again
     // run GCD test. Check for trivial invalid constraints.
     if (tmpCst.hasInvalidConstraint())
       return true;
   }
   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
 // true, no integer solution to the equality constraints can exist.
 //
 // GCD test definition:
 //
 // The equality constraint:
unsigned IntegerRelation::gaussianEliminateVars(unsigned posStart,
   }
   // Update position limit based on number eliminated.
   posLimit = pivotCol;
   // Remove eliminated columns from all constraints.
   removeVarRange(posStart, posLimit);
   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;
+
+    markSetEmpty();
+    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() {
   SmallVector<bool, 32> redun(getNumInequalities(), false);
   // To check if an inequality is redundant, we replace the inequality by its
   // complement (for eg., i - 1 >= 0 by i <= 0), and check if the resulting
   // system is empty. If it is, the inequality is redundant.
   IntegerRelation tmpCst(*this);
void IntegerRelation::removeDuplicateDivs() {
   DivisionRepr divs = getLocalReprs();
   auto merge = [this](unsigned i, unsigned j) -> bool {
     eliminateRedundantLocalVar(i, j);
     return true;
   };
   divs.removeDuplicateDivs(merge);
 }
 
+void IntegerRelation::simplify() {
+  bool changed = true;
+  // Repeat until we reach a fixed point.
+  while (changed) {
+    changed = false;
+    normalizeConstraintsByGCD();
+    changed |= gaussianEliminate();
+    if (isPlainEmpty())
+      return;
+    changed |= removeDuplicateConstraints();
+  }
+  // Current set is not empty.
+  return;
+}
+
 /// 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`.
 /// If an equality satisfies this form, the local variable is replaced in
 /// each constraint and then removed. The equality used to replace this local
 /// variable is also removed.
 void IntegerRelation::removeRedundantLocalVars() {
   // Normalize the equality constraints to reduce coefficients of local
IntegerPolyhedron IntegerRelation::getDomainSet() const {
 
   // Convert Domain variables to SetDim(Range) variables.
   copyRel.convertVarKind(VarKind::Domain, 0, getNumVarKind(VarKind::Domain),
                          VarKind::SetDim);
 
   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 || 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(k);
+      removeInequality(l);
+    } else
+      markSetEmpty();
+    break;
+  }
+
+  // Need to remove the extra space requested.
+  if (!negChanged)
+    removeInequality(ineqs);
+
+  return changed;
+}
+
 IntegerPolyhedron IntegerRelation::getRangeSet() const {
   IntegerRelation copyRel = *this;
 
   // Convert Domain variables to Local variables.
   copyRel.convertVarKind(VarKind::Domain, 0, getNumVarKind(VarKind::Domain),
                          VarKind::Local);
 
   // We do not need to do anything to Range variables since they are already in

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

if (level == frames.size()) {
 
       frame.ineqsToProcess.pop_back();
       frame.lastIneqProcessed = idx;
       ++level;
       continue;
     }
   }
 
+  // Try to simplify the results.
+  result = result.simplify();
+
   return result;
 }
 
 /// Return the complement of this set.
 PresburgerRelation PresburgerRelation::complement() const {
   return getSetDifference(IntegerRelation::getUniverse(getSpace()), *this);
 }
 

 }
 
 bool PresburgerRelation::hasOnlyDivLocals() const {
   return llvm::all_of(disjuncts, [](const IntegerRelation &rel) {
     return rel.hasOnlyDivLocals();
   });
 }
 
+PresburgerRelation PresburgerRelation::simplify() const {
+  PresburgerRelation origin = *this;
+  PresburgerRelation result = PresburgerRelation(getSpace());
+  for (IntegerRelation &disjunct : origin.disjuncts) {
+    disjunct.simplify();
+    if (!disjunct.isPlainEmpty())
+      result.unionInPlace(disjunct);
+  }
+  return result;
+}
+
 void PresburgerRelation::print(raw_ostream &os) const {
   os << "Number of Disjuncts: " << getNumDisjuncts() << "\n";
   for (const IntegerRelation &disjunct : disjuncts) {
     disjunct.print(os);
     os << '\n';
   }
 }