[MLIR][Presburger] Add enum based dispatch for isEmpty

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

@@ -34,6 +34,20 @@ struct SymbolicLexOpt;
 /// The type of bound: equal, lower bound or upper bound.
 enum class BoundType { EQ, LB, UB };
 
+/// The kind of solver to use for emptiness check.
+/// TODO: We should have some docs to explain the user what kind of solver
+/// should fit best for their use case.
+enum class SolverKind {
+  // Integer Exact algorithm.
+  IntegerSimplex,
+  // Rational Exact algorithm.
+  RationalSimplex,
+  // Rationly Exact algorithm.
+  FourierMotzkin,
+  // Fast heuristic based algorithm (no guarantees).
+  FastHeuristics
+};
+
 /// An IntegerRelation represents the set of points from a PresburgerSpace that
 /// satisfy a list of affine constraints. Affine constraints can be inequalities
 /// or equalities in the form:
@@ -366,26 +380,9 @@ class IntegerRelation {
                                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
-  /// `findIntegerSample`.
-  bool isIntegerEmpty() const;
+  /// Check if the given relation/polyhedron is empty. The emptiness guarantees
+  /// depend on the solver used.
+  bool isEmpty(SolverKind kind) const;
 
   /// Returns a matrix where each row is a vector along which the polytope is
   /// bounded. The span of the returned vectors is guaranteed to contain all
@@ -754,6 +751,30 @@ class IntegerRelation {
     return computeConstantLowerOrUpperBound<isLower>(pos).map(int64FromMPInt);
   }
 
+  /// 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 isEmptyByFMTest() 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 integer
+  /// solution, false if a solution exists.
+  bool isIntegerEmpty() const;
+
+  /// Returns true if the set of constraints is found to have no rational
+  /// solution, false if a solution exists.
+  bool isRationalEmpty() const;
+
   /// Eliminates a single variable at `position` from equality and inequality
   /// constraints. Returns `success` if the variable was eliminated, and
   /// `failure` otherwise.

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

@@ -164,12 +164,9 @@ class PresburgerRelation {
   /// 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 isObviouslyEmpty() const;
+  /// Check if the given relation/polyhedron is empty. The emptiness guarantees
+  /// depend on the solver used.
+  bool isEmpty(SolverKind kind) const;
 
   /// Return true if the set is known to have one unconstrained disjunct, false
   /// otherwise.

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

@@ -689,7 +689,7 @@ static unsigned getBestVarToEliminate(const IntegerRelation &cst,
 // using the GCD test (on all equality constraints) and checking for trivially
 // invalid constraints. Returns 'true' if the constraint system is found to be
 // empty; false otherwise.
-bool IntegerRelation::isEmpty() const {
+bool IntegerRelation::isEmptyByFMTest() const {
   if (isEmptyByGCDTest() || hasInvalidConstraint())
     return true;
 
@@ -817,8 +817,27 @@ IntMatrix IntegerRelation::getBoundedDirections() const {
   return dirs;
 }
 
+bool IntegerRelation::isEmpty(SolverKind kind) const {
+  switch (kind) {
+  case SolverKind::IntegerSimplex:
+    return isIntegerEmpty();
+  case SolverKind::RationalSimplex:
+    return isRationalEmpty();
+  case SolverKind::FourierMotzkin:
+    return isEmptyByFMTest();
+  case SolverKind::FastHeuristics:
+    return isObviouslyEmpty();
+  }
+}
+
 bool IntegerRelation::isIntegerEmpty() const { return !findIntegerSample(); }
 
+bool IntegerRelation::isRationalEmpty() const {
+  // TODO: We should cache the simplex at some point.
+  Simplex simplex(*this);
+  return simplex.isEmpty();
+}
+
 /// Let this set be S. If S is bounded then we directly call into the GBR
 /// sampling algorithm. Otherwise, there are some unbounded directions, i.e.,
 /// vectors v such that S extends to infinity along v or -v. In this case we
@@ -1180,7 +1199,7 @@ void IntegerRelation::removeRedundantInequalities() {
     // Change the inequality to its complement.
     tmpCst.inequalities.negateRow(r);
     --tmpCst.atIneq(r, tmpCst.getNumCols() - 1);
-    if (tmpCst.isEmpty()) {
+    if (tmpCst.isEmpty(SolverKind::FourierMotzkin)) {
       redun[r] = true;
       // Zero fill the redundant inequality.
       inequalities.fillRow(r, /*value=*/0);
@@ -2506,7 +2525,7 @@ void IntegerRelation::removeTrivialEqualities() {
 bool IntegerRelation::isFullDim() {
   if (getNumVars() == 0)
     return true;
-  if (isEmpty())
+  if (isEmpty(SolverKind::FourierMotzkin))
     return false;
 
   // If there is a non-trivial equality, the space cannot be full-dimensional.

mlir/lib/Analysis/Presburger/PWMAFunction.cpp

@@ -293,8 +293,9 @@ bool PWMAFunction::isEqual(const PWMAFunction &other) const {
 
 void PWMAFunction::addPiece(const Piece &piece) {
   assert(piece.isConsistent() && "Piece should be consistent");
-  assert(piece.domain.intersect(getDomain()).isIntegerEmpty() &&
-         "Piece should be disjoint from the function");
+  assert(
+      piece.domain.intersect(getDomain()).isEmpty(SolverKind::IntegerSimplex) &&
+      "Piece should be disjoint from the function");
   pieces.push_back(piece);
 }
 

mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

@@ -94,11 +94,11 @@ void PresburgerRelation::unionInPlace(const PresburgerRelation &set) {
   if (isObviouslyEqual(set))
     return;
 
-  if (isObviouslyEmpty()) {
+  if (isEmpty(SolverKind::FastHeuristics)) {
     disjuncts = set.disjuncts;
     return;
   }
-  if (set.isObviouslyEmpty())
+  if (set.isEmpty(SolverKind::FastHeuristics))
     return;
 
   if (isObviouslyUniverse())
@@ -152,17 +152,17 @@ PresburgerRelation::intersect(const PresburgerRelation &set) const {
 
   // If the set is empty or the other set is universe,
   // directly return the set
-  if (isObviouslyEmpty() || set.isObviouslyUniverse())
+  if (isEmpty(SolverKind::FastHeuristics) || set.isObviouslyUniverse())
     return *this;
 
-  if (set.isObviouslyEmpty() || isObviouslyUniverse())
+  if (set.isEmpty(SolverKind::FastHeuristics) || 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())
+      if (!intersection.isEmpty(SolverKind::IntegerSimplex))
         result.unionInPlace(intersection);
     }
   }
@@ -224,7 +224,7 @@ void PresburgerRelation::compose(const PresburgerRelation &rel) {
     for (const IntegerRelation &csB : rel.disjuncts) {
       IntegerRelation composition = csA;
       composition.compose(csB);
-      if (!composition.isEmpty())
+      if (!composition.isEmpty(SolverKind::IntegerSimplex))
         result.unionInPlace(composition);
     }
   }
@@ -347,7 +347,7 @@ PresburgerRelation PresburgerRelation::computeReprWithOnlyDivLocals() const {
 static PresburgerRelation getSetDifference(IntegerRelation b,
                                            const PresburgerRelation &s) {
   assert(b.getSpace().isCompatible(s.getSpace()) && "Spaces should match");
-  if (b.isEmptyByGCDTest())
+  if (b.isEmpty(SolverKind::FastHeuristics))
     return PresburgerRelation::getEmpty(b.getSpaceWithoutLocals());
 
   if (!s.hasOnlyDivLocals())
@@ -617,7 +617,7 @@ PresburgerRelation::subtract(const PresburgerRelation &set) const {
 /// 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();
+  return this->subtract(set).isEmpty(SolverKind::IntegerSimplex);
 }
 
 /// Two sets are equal iff they are subsets of each other.
@@ -658,16 +658,11 @@ bool PresburgerRelation::isConvexNoLocals() const {
   return getNumDisjuncts() == 1 && getSpace().getNumLocalVars() == 0;
 }
 
-/// Return true if there is no disjunct, false otherwise.
-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::isEmpty(SolverKind kind) const {
+  auto disjunctCheck = [&kind](const IntegerRelation &disjunct) {
+    return disjunct.isEmpty(kind);
+  };
+  return llvm::all_of(disjuncts, disjunctCheck);
 }
 
 bool PresburgerRelation::findIntegerSample(SmallVectorImpl<MPInt> &sample) {
@@ -1035,7 +1030,7 @@ PresburgerRelation PresburgerRelation::simplify() const {
   PresburgerRelation result = PresburgerRelation(getSpace());
   for (IntegerRelation &disjunct : origin.disjuncts) {
     disjunct.simplify();
-    if (!disjunct.isObviouslyEmpty())
+    if (!disjunct.isEmpty(SolverKind::FastHeuristics))
       result.unionInPlace(disjunct);
   }
   return result;

mlir/lib/Dialect/Affine/Analysis/AffineAnalysis.cpp

@@ -668,7 +668,7 @@ DependenceResult mlir::affine::checkMemrefAccessDependence(
   addOrderingConstraints(srcDomain, dstDomain, loopDepth, &dependenceDomain);
 
   // Return 'NoDependence' if the solution space is empty: no dependence.
-  if (dependenceDomain.isEmpty())
+  if (dependenceDomain.isEmpty(SolverKind::FourierMotzkin))
     return DependenceResult::NoDependence;
 
   // Compute dependence direction vector and return true.

mlir/lib/Dialect/Affine/Analysis/Utils.cpp

@@ -875,7 +875,7 @@ std::optional<bool> ComputationSliceState::isSliceValid() const {
   PresburgerSet sliceSet(sliceConstraints);
   PresburgerSet diffSet = sliceSet.subtract(srcSet);
 
-  if (!diffSet.isIntegerEmpty()) {
+  if (!diffSet.isEmpty(SolverKind::IntegerSimplex)) {
     LLVM_DEBUG(llvm::dbgs() << "Incorrect slice\n");
     return false;
   }
@@ -932,7 +932,7 @@ std::optional<bool> ComputationSliceState::isMaximal() const {
   PresburgerSet srcSet(srcConstraints);
   PresburgerSet sliceSet(sliceConstraints);
   PresburgerSet diffSet = srcSet.subtract(sliceSet);
-  return diffSet.isIntegerEmpty();
+  return diffSet.isEmpty(SolverKind::IntegerSimplex);
 }
 
 unsigned MemRefRegion::getRank() const {
@@ -1294,7 +1294,7 @@ LogicalResult mlir::affine::boundCheckLoadOrStoreOp(LoadOrStoreOp loadOrStoreOp,
 
     // Check for overflow: d_i >= memref dim size.
     ucst.addBound(BoundType::LB, r, dimSize);
-    outOfBounds = !ucst.isEmpty();
+    outOfBounds = !ucst.isEmpty(SolverKind::FourierMotzkin);
     if (outOfBounds && emitError) {
       loadOrStoreOp.emitOpError()
           << "memref out of upper bound access along dimension #" << (r + 1);
@@ -1305,7 +1305,7 @@ LogicalResult mlir::affine::boundCheckLoadOrStoreOp(LoadOrStoreOp loadOrStoreOp,
     std::fill(ineq.begin(), ineq.end(), 0);
     // d_i <= -1;
     lcst.addBound(BoundType::UB, r, -1);
-    outOfBounds = !lcst.isEmpty();
+    outOfBounds = !lcst.isEmpty(SolverKind::FourierMotzkin);
     if (outOfBounds && emitError) {
       loadOrStoreOp.emitOpError()
           << "memref out of lower bound access along dimension #" << (r + 1);
@@ -1979,7 +1979,7 @@ void mlir::affine::getSequentialLoops(
 
 IntegerSet mlir::affine::simplifyIntegerSet(IntegerSet set) {
   FlatAffineValueConstraints fac(set);
-  if (fac.isEmpty())
+  if (fac.isEmpty(SolverKind::FourierMotzkin))
     return IntegerSet::getEmptySet(set.getNumDims(), set.getNumSymbols(),
                                    set.getContext());
   fac.removeTrivialRedundancy();
@@ -2108,7 +2108,7 @@ FailureOr<AffineValueMap> mlir::affine::simplifyConstrainedMinMaxOp(
 
   // If the constraint system is empty, there is an inconsistency. (E.g., this
   // can happen if loop lb > ub.)
-  if (constraints.isEmpty())
+  if (constraints.isEmpty(SolverKind::FourierMotzkin))
     return failure();
 
   // In the case of `isMin` (`!isMin` is inversed):
@@ -2141,7 +2141,7 @@ FailureOr<AffineValueMap> mlir::affine::simplifyConstrainedMinMaxOp(
     ineq[i] = isMin ? -1 : 1;
     ineq[newConstr.getNumCols() - 1] = -1;
     newConstr.addInequality(ineq);
-    if (!newConstr.isEmpty())
+    if (!newConstr.isEmpty(SolverKind::FourierMotzkin))
       return failure();
   }
 

mlir/lib/Interfaces/ValueBoundsOpInterface.cpp

@@ -692,7 +692,7 @@ bool ValueBoundsConstraintSet::comparePos(int64_t lhsPos,
   // lhs > rhs must be incorrect and we can deduce that lhs <= rhs holds.
 
   // We cannot prove anything if the constraint set is already empty.
-  if (cstr.isEmpty()) {
+  if (cstr.isEmpty(presburger::SolverKind::FourierMotzkin)) {
     LLVM_DEBUG(
         llvm::dbgs()
         << "cannot compare value/dims: constraint system is already empty");
@@ -722,7 +722,7 @@ bool ValueBoundsConstraintSet::comparePos(int64_t lhsPos,
   // set empty.
   int64_t ineqPos = cstr.getNumInequalities();
   cstr.addInequality(eq);
-  bool isEmpty = cstr.isEmpty();
+  bool isEmpty = cstr.isEmpty(presburger::SolverKind::FourierMotzkin);
   cstr.removeInequality(ineqPos);
   return isEmpty;
 }