[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

338

markSetEmpty is a better name maybe.

338

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?

562

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

745

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

745

746

"Return value indicates if anything was modified"

780–781

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.

1331

[grosser]

Does this function some correspondence to isl?

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

780–781

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

338

I just added isPlainEmpty function to IntegerRelation.

780–781

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

780–781

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

338

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

560–561

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

704

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

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

966

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

967

[gilsaia]

• [fix] add comment & fix bug

[gilsaia]

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

338

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

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

704

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

338

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

704

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:
   virtual ~IntegerRelation() = default;
 
   /// Return a system with no constraints, i.e., one which is satisfied by all
   /// points.
   static IntegerRelation getUniverse(const PresburgerSpace &space) {
     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; }
 
   static bool classof(const IntegerRelation *cst) { return true; }
 
   // Clones this object.
   std::unique_ptr<IntegerRelation> clone() const;
 
public:
   /// (see IntegerRelation::findIntegerSample()).
   bool isEqual(const IntegerRelation &other) 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. 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
   /// check (see IntegerRelation::findIntegerSample()).
   bool isSubsetOf(const IntegerRelation &other) const;
 
   /// Returns the value at the specified equality row and column.
   inline MPInt atEq(unsigned i, unsigned j) const { return equalities(i, j); }
public:
   /// Swap the posA^th variable with the posB^th variable.
   virtual void swapVar(unsigned posA, unsigned posB);
 
   /// Removes all equalities and inequalities.
   void clearConstraints();
 
   /// 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`.
   virtual void clearAndCopyFrom(const IntegerRelation &other);
 
   /// Gather positions of 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
   getLowerAndUpperBoundIndices(unsigned pos,
                                SmallVectorImpl<unsigned> *lbIndices,
                                SmallVectorImpl<unsigned> *ubIndices,
                                SmallVectorImpl<unsigned> *eqIndices = nullptr,
                                unsigned offset = 0, unsigned num = 0) const;
 
   /// 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 isObviouslyEmpty() 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:
   /// All local variables in both sets must correspond to floor divisions.
   bool isEqual(const PresburgerRelation &set) const;
 
   /// Return true if all the sets in the union are known to be integer empty
   /// false otherwise.
   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.
   bool isConvexNoLocals() const;
 
   /// Find an integer sample from the given set. This should not be called if
   /// any of the disjuncts in the union are unbounded.
   bool findIntegerSample(SmallVectorImpl<MPInt> &sample);
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

IntegerRelation IntegerRelation::intersect(IntegerRelation other) const {
   return result;
 }
 
 bool IntegerRelation::isEqual(const IntegerRelation &other) const {
   assert(space.isCompatible(other.getSpace()) && "Spaces must be compatible.");
   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())
     return false;
   if (getNumInequalities() != other.getNumInequalities())
     return false;
 
   unsigned cols = getNumCols();

 
 void IntegerRelation::clearConstraints() {
   equalities.resizeVertically(0);
   inequalities.resizeVertically(0);
 }
 
 /// 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");
   assert(offset + num < getNumCols() && "invalid range");
 
   // Checks for a constraint that has a non-zero coeff for the variables in
   // the position range [offset, offset + num) while ignoring `pos`.
   auto containsConstraintDependentOnRange = [&](unsigned r, bool isEq) {
     unsigned c, f;
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::isObviouslyEmpty() 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;
+
+    *this = getEmpty(getSpace());
+    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 (isObviouslyEmpty())
+      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
+      *this = getEmpty(getSpace());
+    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

 
 /// Mutate this set, turning it into the union of this set and the given set.
 ///
 /// This is accomplished by simply adding all the disjuncts of the given set
 /// to this set.
 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;
   }
 
   for (const IntegerRelation &disjunct : set.disjuncts)
     unionInPlace(disjunct);
 }
 

 // If S_i or T_j have local variables, then S_i and T_j contains the local
 // variables of both.
 PresburgerRelation
 PresburgerRelation::intersect(const PresburgerRelation &set) const {
   assert(space.isCompatible(set.getSpace()) && "Spaces should match");
 
   // 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());
   for (const IntegerRelation &csA : disjuncts) {
     for (const IntegerRelation &csB : set.disjuncts) {
       IntegerRelation intersection = csA.intersect(csB);
       if (!intersection.isEmpty())
         result.unionInPlace(intersection);
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);
 }
 
 /// Return the result of subtract the given set from this set, i.e.,
 /// return `this \ set`.
 PresburgerRelation
 PresburgerRelation::subtract(const PresburgerRelation &set) const {
   assert(space.isCompatible(set.getSpace()) && "Spaces should match");
   PresburgerRelation result(getSpace());
 
   // 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).
   for (const IntegerRelation &disjunct : disjuncts)
     result.unionInPlace(getSetDifference(disjunct, set));
   return result;
 }
 
 /// T is a subset of S iff T \ S is empty, since if T \ S contains a
 /// point then this is a point that is contained in T but not S, and
 /// if T contains a point that is not in S, this also lies in T \ S.
 bool PresburgerRelation::isSubsetOf(const PresburgerRelation &set) const {
   return this->subtract(set).isIntegerEmpty();
 }
 
 /// Two sets are equal iff they are subsets of each other.
 bool PresburgerRelation::isEqual(const PresburgerRelation &set) const {
   assert(space.isCompatible(set.getSpace()) && "Spaces should match");
   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;
 
   if (getNumDisjuncts() != set.getNumDisjuncts())
     return false;
 
   // 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;
 }
 
 /// Return true if the Presburger relation represents the universe set, false
 /// 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 {
+bool PresburgerRelation::isObviouslyUniverse() const {
   for (auto &disjunct : getAllDisjuncts()) {
     if (disjunct.getNumConstraints() == 0)
       return true;
   }
   return false;
 }
 
 bool PresburgerRelation::isConvexNoLocals() const {
   if (getNumDisjuncts() == 1 && getSpace().getNumLocalVars() == 0)
     return true;
   return false;
 }
 
 /// 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.
 bool PresburgerRelation::isIntegerEmpty() const {
   // The set is empty iff all of the disjuncts are empty.
   return llvm::all_of(disjuncts, std::mem_fn(&IntegerRelation::isIntegerEmpty));
 }
 

 }
 
 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.isObviouslyEmpty())
+      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';
   }
 }