[MLIR][Presburger] Add enum based dispatch for isEmpty #93010
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
@llvm/pr-subscribers-mlir-presburger @llvm/pr-subscribers-mlir-affine Author: Kunwar Grover (Groverkss) ChangesThis 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:
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]
|
|
@llvm/pr-subscribers-mlir Author: Kunwar Grover (Groverkss) ChangesThis 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:
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]
|
MacDue
reviewed
Jun 4, 2024
| IntegerSimplex, | ||
| // Rational Exact algorithm. | ||
| RationalSimplex, | ||
| // Rationly Exact algorithm. |
There was a problem hiding this comment.
Typo?
Suggested change
| // Rationly Exact algorithm. | |
| // Rational Exact algorithm. |
| /// 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; |
There was a problem hiding this comment.
Can some of these tests conservatively return "false" or "true" if no certain decision could be made? I.e., false positives / negatives? If so, can we explicitly mention that for each of the function calls?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.