[Mlir-commits] [mlir] [MLIR][Presburger] Add enum based dispatch for isEmpty (PR #93010)

llvmlistbot at llvm.org llvmlistbot at llvm.org
Wed May 22 02:32:58 PDT 2024


llvmbot wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-mlir

Author: Kunwar Grover (Groverkss)

<details>
<summary>Changes</summary>

This patch adds an enum to dispatch to different available solvers for emptiness check. This allows the user to make a more informed choice on what emptiness check they are using.

---

Patch is 26.42 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/93010.diff


12 Files Affected:

- (modified) mlir/include/mlir/Analysis/Presburger/IntegerRelation.h (+41-20) 
- (modified) mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h (+3-6) 
- (modified) mlir/lib/Analysis/Presburger/IntegerRelation.cpp (+22-3) 
- (modified) mlir/lib/Analysis/Presburger/PWMAFunction.cpp (+3-2) 
- (modified) mlir/lib/Analysis/Presburger/PresburgerRelation.cpp (+14-19) 
- (modified) mlir/lib/Dialect/Affine/Analysis/AffineAnalysis.cpp (+1-1) 
- (modified) mlir/lib/Dialect/Affine/Analysis/Utils.cpp (+7-7) 
- (modified) mlir/lib/Interfaces/ValueBoundsOpInterface.cpp (+2-2) 
- (modified) mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp (+17-17) 
- (modified) mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp (+4-4) 
- (modified) mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp (+6-6) 
- (modified) mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp (+4-2) 


``````````diff
diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
index 163f365c623d7..f8c45247d58ce 100644
--- a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h
+++ b/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.
diff --git a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h b/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
index 9634df6d58a1a..aeb73984bcc99 100644
--- a/mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h
+++ b/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.
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index b5a2ed6ccc369..8697d6d046e89 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/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.
diff --git a/mlir/lib/Analysis/Presburger/PWMAFunction.cpp b/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
index d55962616de17..4911b237e1425 100644
--- a/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
+++ b/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);
 }
 
diff --git a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
index 3af6baae0e700..25a443b6bf818 100644
--- a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
+++ b/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;
diff --git a/mlir/lib/Dialect/Affine/Analysis/AffineAnalysis.cpp b/mlir/lib/Dialect/Affine/Analysis/AffineAnalysis.cpp
index 9b776900c379a..7d20473f0b05f 100644
--- a/mlir/lib/Dialect/Affine/Analysis/AffineAnalysis.cpp
+++ b/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.
diff --git a/mlir/lib/Dialect/Affine/Analysis/Utils.cpp b/mlir/lib/Dialect/Affine/Analysis/Utils.cpp
index 194ee9115e3d7..4fd3e165f50c0 100644
--- a/mlir/lib/Dialect/Affine/Analysis/Utils.cpp
+++ b/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();
   }
 
diff --git a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
index 87937591e60ad..21f96b30c0d8b 100644
--- a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
+++ b/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;
 }
diff --git a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp
index ba035e84ff1fd..9261110b3a678 100644
--- a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp
@@ -93,7 +93,7 @@ static void checkSample(bool hasSample, const IntegerPolyhedron &poly,
     }
     break;
   case TestFunction::Empty:
-    EXPECT_EQ(!hasSample, poly.isIntegerEmpty());
+    EXPECT_EQ(!hasSample, poly.isEmpty(SolverKind::IntegerSimplex));
     break;
   }
 }
@@ -443,35 +443,35 @@ TEST(IntegerPolyhedronTest, FindSampleTest) {
 TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) {
   // 1 <= 5x and 5x <= 4 (no solution).
   EXPECT_TRUE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)")
-                  .isIntegerEmpty());
+                  .isEmpty(SolverKind::IntegerSimplex));
   // 1 <= 5x and 5x <= 9 (solution: x = 1).
   EXPECT_FALSE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)")
-                   .isIntegerEmpty());
+                   .isEmpty(SolverKind::IntegerSimplex));
 
   // Unbounded sets.
   EXPECT_TRUE(
       parseIntegerPolyhedron("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, "
                              "2 * z - 1 >= 0, 2 * x - 1 == 0)")
-          .isIntegerEmpty());
+          .isEmpty(SolverKind::IntegerSimplex));
 
   EXPECT_FALSE(parseIntegerPolyhedron(
                    "(x,y,z) : (2 * x - 1 >= 0, -3 * x + 3 >= 0, "
                    "5 * z - 6 >= 0, -7 * z + 17 >= 0, 3 * y - 2 >= 0)")
-                   .isIntegerEmpty());
+                   .isEmpty(SolverKind::IntegerSimplex));
 
   EXPECT_FALSE(parseIntegerPolyhedron(
                    "(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)")
-                   .isIntegerEmpty());
+                   .isEmpty(SolverKind::IntegerSimplex));
 
-  // IntegerPolyhedron::isEmpty() does not detect the following sets to be
-  // empty.
+  // IntegerPolyhedron::isEmpty(SolverKind::FourierMotzkin) does
+  // not detect the following sets to be empty.
 
   // 3x + 7y = 1 and 0 <= x, y <= 10.
   // Since x and y are non-negative, 3x + 7y can never be 1.
   EXPECT_TRUE(parseIntegerPolyhedron(
                   "(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, "
                   "3 * x + 7 * y - 1 == 0)")
-                  .isIntegerEmpty());
+                  .isEmpty(SolverKind::IntegerSimplex));
 
   // 2x = 3y and y = x - 1 and x + y = 6z + 2 and 0 <= x, y <= 100.
   // Substituting y = x - 1 in 3y = 2x, we obtain x = 3 and hence y = 2.
@@ -479,7 +479,7 @@ TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) {
   EXPECT_TRUE(parseIntegerPolyhedron(
                   "(x,y,z) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, "
                   "2 * x - 3 * y == 0, x - y - 1 == 0, x + y - 6 * z - 2 == 0)")
-                  .isIntegerEmpty());
+                  .isEmpty(SolverKind::IntegerSimplex));
 
   // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100.
   // 2x = 3y implies x is a multiple of 3 and y is even.
@@ -490,11 +490,11 @@ TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) {
       parseIntegerPolyhedron(
           "(x,y,z,q) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, "
           "2 * x - 3 * y == 0, x - y + 6 * z - 1 == 0, x + y - 6 * q - 2 == 0)")
-          .isIntegerEmpty());
+          .isEmpty(SolverKind::IntegerSimplex));
 
   // Set with symbols.
   EXPECT_FALSE(parseIntegerPolyhedron("(x)[s] : (x + s >= 0, x - s == 0)")
-                   .isIntegerEmpty());
+     ...
[truncated]

``````````

</details>


https://github.com/llvm/llvm-project/pull/93010


More information about the Mlir-commits mailing list