[Mlir-commits] [mlir] [MLIR][Presburger] Add enum based dispatch for isEmpty (PR #93010)
Kunwar Grover
llvmlistbot at llvm.org
Wed May 22 02:32:25 PDT 2024
https://github.com/Groverkss created https://github.com/llvm/llvm-project/pull/93010
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.
>From f2d88341c24f51ff731865148be555ddd5ebc3c4 Mon Sep 17 00:00:00 2001
From: Kunwar Grover <groverkss at gmail.com>
Date: Wed, 22 May 2024 09:27:00 +0000
Subject: [PATCH 1/3] save
---
.../Analysis/Presburger/IntegerRelation.h | 61 +++++++++++++------
.../Analysis/Presburger/PresburgerRelation.h | 9 +--
.../Analysis/Presburger/IntegerRelation.cpp | 25 +++++++-
mlir/lib/Analysis/Presburger/PWMAFunction.cpp | 3 +-
.../Presburger/PresburgerRelation.cpp | 33 +++++-----
.../Affine/Analysis/AffineAnalysis.cpp | 2 +-
mlir/lib/Dialect/Affine/Analysis/Utils.cpp | 14 ++---
.../lib/Interfaces/ValueBoundsOpInterface.cpp | 5 +-
.../Presburger/IntegerPolyhedronTest.cpp | 36 +++++------
.../Presburger/IntegerRelationTest.cpp | 8 +--
.../Presburger/PresburgerRelationTest.cpp | 12 ++--
.../Analysis/Presburger/PresburgerSetTest.cpp | 6 +-
12 files changed, 126 insertions(+), 88 deletions(-)
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..5ffad95d62915 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::IntegerExactSimplex:
+ return isIntegerEmpty();
+ case SolverKind::RationalExactSimplex:
+ return isRationalEmpty();
+ case SolverKind::RationalExactFourierMotzkin:
+ 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::RationalExactFourierMotzkin)) {
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::RationalExactFourierMotzkin))
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..23ff724d2cc43 100644
--- a/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
+++ b/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
@@ -293,7 +293,8 @@ 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() &&
+ assert(piece.domain.intersect(getDomain())
+ .isEmpty(SolverKind::IntegerExactSimplex) &&
"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..76316676e8827 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::IntegerExactSimplex))
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::IntegerExactSimplex))
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::IntegerExactSimplex);
}
/// 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..273af1f27f88d 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::RationalExactFourierMotzkin))
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..3f9234ef103a8 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::IntegerExactSimplex)) {
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::IntegerExactSimplex);
}
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::RationalExactFourierMotzkin);
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::RationalExactFourierMotzkin);
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::RationalExactFourierMotzkin))
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::RationalExactFourierMotzkin))
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::RationalExactFourierMotzkin))
return failure();
}
diff --git a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
index 87937591e60ad..0e1513b1359a2 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::RationalExactFourierMotzkin)) {
LLVM_DEBUG(
llvm::dbgs()
<< "cannot compare value/dims: constraint system is already empty");
@@ -722,7 +722,8 @@ 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::RationalExactFourierMotzkin);
cstr.removeInequality(ineqPos);
return isEmpty;
}
diff --git a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp
index ba035e84ff1fd..66457f783b5a9 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::IntegerExactSimplex));
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::IntegerExactSimplex));
// 1 <= 5x and 5x <= 9 (solution: x = 1).
EXPECT_FALSE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)")
- .isIntegerEmpty());
+ .isEmpty(SolverKind::IntegerExactSimplex));
// 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::IntegerExactSimplex));
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::IntegerExactSimplex));
EXPECT_FALSE(parseIntegerPolyhedron(
"(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)")
- .isIntegerEmpty());
+ .isEmpty(SolverKind::IntegerExactSimplex));
- // IntegerPolyhedron::isEmpty() does not detect the following sets to be
- // empty.
+ // IntegerPolyhedron::isEmpty(SolverKind::RationalExactFourierMotzkin) 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::IntegerExactSimplex));
// 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::IntegerExactSimplex));
// 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::IntegerExactSimplex));
// Set with symbols.
EXPECT_FALSE(parseIntegerPolyhedron("(x)[s] : (x + s >= 0, x - s == 0)")
- .isIntegerEmpty());
+ .isEmpty(SolverKind::IntegerExactSimplex));
}
TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) {
@@ -823,7 +823,7 @@ TEST(IntegerPolyhedronTest, simplifyLocalsTest) {
poly.addEquality({2, 1, -1});
poly.addEquality({0, 1, -2});
- EXPECT_TRUE(poly.isEmpty());
+ EXPECT_TRUE(poly.isEmpty(SolverKind::RationalExactFourierMotzkin));
// (x) : (exists y, z, w: 3x + y = 1 and 2y = z and 3y = w and z = w).
IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1, 0, 3));
@@ -832,7 +832,7 @@ TEST(IntegerPolyhedronTest, simplifyLocalsTest) {
poly2.addEquality({0, 3, 0, -1, 0});
poly2.addEquality({0, 0, 1, -1, 0});
- EXPECT_TRUE(poly2.isEmpty());
+ EXPECT_TRUE(poly2.isEmpty(SolverKind::RationalExactFourierMotzkin));
// (x) : (exists y: x >= y + 1 and 2x + y = 0 and y >= -1).
IntegerPolyhedron poly3(PresburgerSpace::getSetSpace(1, 0, 1));
@@ -840,7 +840,7 @@ TEST(IntegerPolyhedronTest, simplifyLocalsTest) {
poly3.addInequality({0, 1, 1});
poly3.addEquality({2, 1, 0});
- EXPECT_TRUE(poly3.isEmpty());
+ EXPECT_TRUE(poly3.isEmpty(SolverKind::RationalExactFourierMotzkin));
}
TEST(IntegerPolyhedronTest, mergeDivisionsSimple) {
@@ -1201,14 +1201,16 @@ void expectSymbolicIntegerLexMin(
SymbolicLexOpt result = poly.findSymbolicIntegerLexMin();
if (expectedLexminRepr.empty()) {
- EXPECT_TRUE(result.lexopt.getDomain().isIntegerEmpty());
+ EXPECT_TRUE(
+ result.lexopt.getDomain().isEmpty(SolverKind::IntegerExactSimplex));
} else {
PWMAFunction expectedLexmin = parsePWMAF(expectedLexminRepr);
EXPECT_TRUE(result.lexopt.isEqual(expectedLexmin));
}
if (expectedUnboundedDomainRepr.empty()) {
- EXPECT_TRUE(result.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(
+ result.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
} else {
PresburgerSet expectedUnboundedDomain =
parsePresburgerSet(expectedUnboundedDomainRepr);
diff --git a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
index 7df500bc9568a..46d49e46f7018 100644
--- a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
@@ -127,7 +127,7 @@ TEST(IntegerRelationTest, symbolicLexmin) {
{"(a)[b] : (a - b >= 0)", "(a)[b] -> (a)"}, // a
{"(a)[b] : (b - a - 1 >= 0)", "(a)[b] -> (b)"}, // b
});
- EXPECT_TRUE(lexmin.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmin.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmin.lexopt.isEqual(expectedLexmin));
}
@@ -161,11 +161,11 @@ TEST(IntegerRelationTest, symbolicLexmax) {
{"(x)[N] : (x >= 0, 2 * N - x >= 0, -x + N >= 0)",
"(x)[N] -> (x + 2 * N)"}});
- EXPECT_TRUE(lexmax1.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmax1.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmax1.lexopt.isEqual(expectedLexmax1));
- EXPECT_TRUE(lexmax2.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmax2.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmax2.lexopt.isEqual(expectedLexmax2));
- EXPECT_TRUE(lexmax3.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmax3.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmax3.lexopt.isEqual(expectedLexmax3));
}
diff --git a/mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp b/mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp
index ad71bb32a0688..514191f0c507c 100644
--- a/mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp
@@ -175,9 +175,9 @@ TEST(PresburgerRelationTest, symbolicLexOpt) {
"(x)[N, M] -> (M)"},
});
- EXPECT_TRUE(lexmin1.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmin1.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmin1.lexopt.isEqual(expectedLexMin1));
- EXPECT_TRUE(lexmax1.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmax1.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmax1.lexopt.isEqual(expectedLexMax1));
PresburgerRelation rel2 = parsePresburgerRelationFromPresburgerSet(
@@ -208,9 +208,9 @@ TEST(PresburgerRelationTest, symbolicLexOpt) {
PWMAFunction expectedLexMax2 =
parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (1, 1)"}});
- EXPECT_TRUE(lexmin2.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmin2.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmin2.lexopt.isEqual(expectedLexMin2));
- EXPECT_TRUE(lexmax2.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmax2.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmax2.lexopt.isEqual(expectedLexMax2));
PresburgerRelation rel3 = parsePresburgerRelationFromPresburgerSet(
@@ -245,9 +245,9 @@ TEST(PresburgerRelationTest, symbolicLexOpt) {
PWMAFunction expectedLexMax3 =
parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (1, 1, x)"}});
- EXPECT_TRUE(lexmin3.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmin3.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmin3.lexopt.isEqual(expectedLexMin3));
- EXPECT_TRUE(lexmax3.unboundedDomain.isIntegerEmpty());
+ EXPECT_TRUE(lexmax3.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
EXPECT_TRUE(lexmax3.lexopt.isEqual(expectedLexMax3));
}
diff --git a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
index 8e31a8bb2030b..0925e1781cd79 100644
--- a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
@@ -419,7 +419,9 @@ void expectEqual(const IntegerPolyhedron &s, const IntegerPolyhedron &t) {
EXPECT_TRUE(s.isEqual(t));
}
-void expectEmpty(const PresburgerSet &s) { EXPECT_TRUE(s.isIntegerEmpty()); }
+void expectEmpty(const PresburgerSet &s) {
+ EXPECT_TRUE(s.isEmpty(SolverKind::IntegerExactSimplex));
+}
TEST(SetTest, divisions) {
// evens = {x : exists q, x = 2q}.
@@ -872,7 +874,7 @@ TEST(SetTest, subtractOutputSizeRegression) {
EXPECT_EQ(result.getNumDisjuncts(), 1u);
PresburgerSet subtractSelf = set1.subtract(set1);
- EXPECT_TRUE(subtractSelf.isIntegerEmpty());
+ EXPECT_TRUE(subtractSelf.isEmpty(SolverKind::IntegerExactSimplex));
// Previously, the subtraction result was producing several unnecessary empty
// sets, which is correct, but bad for output size.
EXPECT_EQ(subtractSelf.getNumDisjuncts(), 0u);
>From 05dbc9709faf3b5544a201eade5c6c2679e5ea75 Mon Sep 17 00:00:00 2001
From: Kunwar Grover <groverkss at gmail.com>
Date: Wed, 22 May 2024 09:29:46 +0000
Subject: [PATCH 2/3] s11
---
.../Analysis/Presburger/IntegerRelation.cpp | 10 +++---
mlir/lib/Analysis/Presburger/PWMAFunction.cpp | 2 +-
.../Presburger/PresburgerRelation.cpp | 6 ++--
.../Affine/Analysis/AffineAnalysis.cpp | 2 +-
mlir/lib/Dialect/Affine/Analysis/Utils.cpp | 14 ++++----
.../lib/Interfaces/ValueBoundsOpInterface.cpp | 4 +--
.../Presburger/IntegerPolyhedronTest.cpp | 32 +++++++++----------
.../Presburger/IntegerRelationTest.cpp | 8 ++---
.../Presburger/PresburgerRelationTest.cpp | 12 +++----
.../Analysis/Presburger/PresburgerSetTest.cpp | 4 +--
10 files changed, 47 insertions(+), 47 deletions(-)
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index 5ffad95d62915..8697d6d046e89 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -819,11 +819,11 @@ IntMatrix IntegerRelation::getBoundedDirections() const {
bool IntegerRelation::isEmpty(SolverKind kind) const {
switch (kind) {
- case SolverKind::IntegerExactSimplex:
+ case SolverKind::IntegerSimplex:
return isIntegerEmpty();
- case SolverKind::RationalExactSimplex:
+ case SolverKind::RationalSimplex:
return isRationalEmpty();
- case SolverKind::RationalExactFourierMotzkin:
+ case SolverKind::FourierMotzkin:
return isEmptyByFMTest();
case SolverKind::FastHeuristics:
return isObviouslyEmpty();
@@ -1199,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(SolverKind::RationalExactFourierMotzkin)) {
+ if (tmpCst.isEmpty(SolverKind::FourierMotzkin)) {
redun[r] = true;
// Zero fill the redundant inequality.
inequalities.fillRow(r, /*value=*/0);
@@ -2525,7 +2525,7 @@ void IntegerRelation::removeTrivialEqualities() {
bool IntegerRelation::isFullDim() {
if (getNumVars() == 0)
return true;
- if (isEmpty(SolverKind::RationalExactFourierMotzkin))
+ 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 23ff724d2cc43..7acf32ab5751c 100644
--- a/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
+++ b/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
@@ -294,7 +294,7 @@ 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())
- .isEmpty(SolverKind::IntegerExactSimplex) &&
+ .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 76316676e8827..25a443b6bf818 100644
--- a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
@@ -162,7 +162,7 @@ PresburgerRelation::intersect(const PresburgerRelation &set) const {
for (const IntegerRelation &csA : disjuncts) {
for (const IntegerRelation &csB : set.disjuncts) {
IntegerRelation intersection = csA.intersect(csB);
- if (!intersection.isEmpty(SolverKind::IntegerExactSimplex))
+ 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(SolverKind::IntegerExactSimplex))
+ if (!composition.isEmpty(SolverKind::IntegerSimplex))
result.unionInPlace(composition);
}
}
@@ -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).isEmpty(SolverKind::IntegerExactSimplex);
+ return this->subtract(set).isEmpty(SolverKind::IntegerSimplex);
}
/// Two sets are equal iff they are subsets of each other.
diff --git a/mlir/lib/Dialect/Affine/Analysis/AffineAnalysis.cpp b/mlir/lib/Dialect/Affine/Analysis/AffineAnalysis.cpp
index 273af1f27f88d..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(SolverKind::RationalExactFourierMotzkin))
+ 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 3f9234ef103a8..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.isEmpty(SolverKind::IntegerExactSimplex)) {
+ 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.isEmpty(SolverKind::IntegerExactSimplex);
+ 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(SolverKind::RationalExactFourierMotzkin);
+ 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(SolverKind::RationalExactFourierMotzkin);
+ 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(SolverKind::RationalExactFourierMotzkin))
+ 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(SolverKind::RationalExactFourierMotzkin))
+ 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(SolverKind::RationalExactFourierMotzkin))
+ if (!newConstr.isEmpty(SolverKind::FourierMotzkin))
return failure();
}
diff --git a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
index 0e1513b1359a2..38bae85ca7549 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(presburger::SolverKind::RationalExactFourierMotzkin)) {
+ if (cstr.isEmpty(presburger::SolverKind::FourierMotzkin)) {
LLVM_DEBUG(
llvm::dbgs()
<< "cannot compare value/dims: constraint system is already empty");
@@ -723,7 +723,7 @@ bool ValueBoundsConstraintSet::comparePos(int64_t lhsPos,
int64_t ineqPos = cstr.getNumInequalities();
cstr.addInequality(eq);
bool isEmpty =
- cstr.isEmpty(presburger::SolverKind::RationalExactFourierMotzkin);
+ 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 66457f783b5a9..d8a08377dad76 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.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_EQ(!hasSample, poly.isEmpty(SolverKind::IntegerSimplex));
break;
}
}
@@ -443,27 +443,27 @@ 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)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .isEmpty(SolverKind::IntegerSimplex));
// 1 <= 5x and 5x <= 9 (solution: x = 1).
EXPECT_FALSE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .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)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .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)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .isEmpty(SolverKind::IntegerSimplex));
EXPECT_FALSE(parseIntegerPolyhedron(
"(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .isEmpty(SolverKind::IntegerSimplex));
- // IntegerPolyhedron::isEmpty(SolverKind::RationalExactFourierMotzkin) does
+ // IntegerPolyhedron::isEmpty(SolverKind::FourierMotzkin) does
// not detect the following sets to be empty.
// 3x + 7y = 1 and 0 <= x, y <= 10.
@@ -471,7 +471,7 @@ TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) {
EXPECT_TRUE(parseIntegerPolyhedron(
"(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, "
"3 * x + 7 * y - 1 == 0)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .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)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .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)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .isEmpty(SolverKind::IntegerSimplex));
// Set with symbols.
EXPECT_FALSE(parseIntegerPolyhedron("(x)[s] : (x + s >= 0, x - s == 0)")
- .isEmpty(SolverKind::IntegerExactSimplex));
+ .isEmpty(SolverKind::IntegerSimplex));
}
TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) {
@@ -823,7 +823,7 @@ TEST(IntegerPolyhedronTest, simplifyLocalsTest) {
poly.addEquality({2, 1, -1});
poly.addEquality({0, 1, -2});
- EXPECT_TRUE(poly.isEmpty(SolverKind::RationalExactFourierMotzkin));
+ EXPECT_TRUE(poly.isEmpty(SolverKind::FourierMotzkin));
// (x) : (exists y, z, w: 3x + y = 1 and 2y = z and 3y = w and z = w).
IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1, 0, 3));
@@ -832,7 +832,7 @@ TEST(IntegerPolyhedronTest, simplifyLocalsTest) {
poly2.addEquality({0, 3, 0, -1, 0});
poly2.addEquality({0, 0, 1, -1, 0});
- EXPECT_TRUE(poly2.isEmpty(SolverKind::RationalExactFourierMotzkin));
+ EXPECT_TRUE(poly2.isEmpty(SolverKind::FourierMotzkin));
// (x) : (exists y: x >= y + 1 and 2x + y = 0 and y >= -1).
IntegerPolyhedron poly3(PresburgerSpace::getSetSpace(1, 0, 1));
@@ -840,7 +840,7 @@ TEST(IntegerPolyhedronTest, simplifyLocalsTest) {
poly3.addInequality({0, 1, 1});
poly3.addEquality({2, 1, 0});
- EXPECT_TRUE(poly3.isEmpty(SolverKind::RationalExactFourierMotzkin));
+ EXPECT_TRUE(poly3.isEmpty(SolverKind::FourierMotzkin));
}
TEST(IntegerPolyhedronTest, mergeDivisionsSimple) {
@@ -1202,7 +1202,7 @@ void expectSymbolicIntegerLexMin(
if (expectedLexminRepr.empty()) {
EXPECT_TRUE(
- result.lexopt.getDomain().isEmpty(SolverKind::IntegerExactSimplex));
+ result.lexopt.getDomain().isEmpty(SolverKind::IntegerSimplex));
} else {
PWMAFunction expectedLexmin = parsePWMAF(expectedLexminRepr);
EXPECT_TRUE(result.lexopt.isEqual(expectedLexmin));
@@ -1210,7 +1210,7 @@ void expectSymbolicIntegerLexMin(
if (expectedUnboundedDomainRepr.empty()) {
EXPECT_TRUE(
- result.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ result.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
} else {
PresburgerSet expectedUnboundedDomain =
parsePresburgerSet(expectedUnboundedDomainRepr);
diff --git a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
index 46d49e46f7018..a5a4cf2f80b41 100644
--- a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
@@ -127,7 +127,7 @@ TEST(IntegerRelationTest, symbolicLexmin) {
{"(a)[b] : (a - b >= 0)", "(a)[b] -> (a)"}, // a
{"(a)[b] : (b - a - 1 >= 0)", "(a)[b] -> (b)"}, // b
});
- EXPECT_TRUE(lexmin.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmin.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmin.lexopt.isEqual(expectedLexmin));
}
@@ -161,11 +161,11 @@ TEST(IntegerRelationTest, symbolicLexmax) {
{"(x)[N] : (x >= 0, 2 * N - x >= 0, -x + N >= 0)",
"(x)[N] -> (x + 2 * N)"}});
- EXPECT_TRUE(lexmax1.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmax1.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmax1.lexopt.isEqual(expectedLexmax1));
- EXPECT_TRUE(lexmax2.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmax2.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmax2.lexopt.isEqual(expectedLexmax2));
- EXPECT_TRUE(lexmax3.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmax3.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmax3.lexopt.isEqual(expectedLexmax3));
}
diff --git a/mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp b/mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp
index 514191f0c507c..149f2bad3945a 100644
--- a/mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp
@@ -175,9 +175,9 @@ TEST(PresburgerRelationTest, symbolicLexOpt) {
"(x)[N, M] -> (M)"},
});
- EXPECT_TRUE(lexmin1.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmin1.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmin1.lexopt.isEqual(expectedLexMin1));
- EXPECT_TRUE(lexmax1.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmax1.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmax1.lexopt.isEqual(expectedLexMax1));
PresburgerRelation rel2 = parsePresburgerRelationFromPresburgerSet(
@@ -208,9 +208,9 @@ TEST(PresburgerRelationTest, symbolicLexOpt) {
PWMAFunction expectedLexMax2 =
parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (1, 1)"}});
- EXPECT_TRUE(lexmin2.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmin2.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmin2.lexopt.isEqual(expectedLexMin2));
- EXPECT_TRUE(lexmax2.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmax2.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmax2.lexopt.isEqual(expectedLexMax2));
PresburgerRelation rel3 = parsePresburgerRelationFromPresburgerSet(
@@ -245,9 +245,9 @@ TEST(PresburgerRelationTest, symbolicLexOpt) {
PWMAFunction expectedLexMax3 =
parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (1, 1, x)"}});
- EXPECT_TRUE(lexmin3.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmin3.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmin3.lexopt.isEqual(expectedLexMin3));
- EXPECT_TRUE(lexmax3.unboundedDomain.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(lexmax3.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
EXPECT_TRUE(lexmax3.lexopt.isEqual(expectedLexMax3));
}
diff --git a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
index 0925e1781cd79..d5a1b03e4b36b 100644
--- a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
@@ -420,7 +420,7 @@ void expectEqual(const IntegerPolyhedron &s, const IntegerPolyhedron &t) {
}
void expectEmpty(const PresburgerSet &s) {
- EXPECT_TRUE(s.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(s.isEmpty(SolverKind::IntegerSimplex));
}
TEST(SetTest, divisions) {
@@ -874,7 +874,7 @@ TEST(SetTest, subtractOutputSizeRegression) {
EXPECT_EQ(result.getNumDisjuncts(), 1u);
PresburgerSet subtractSelf = set1.subtract(set1);
- EXPECT_TRUE(subtractSelf.isEmpty(SolverKind::IntegerExactSimplex));
+ EXPECT_TRUE(subtractSelf.isEmpty(SolverKind::IntegerSimplex));
// Previously, the subtraction result was producing several unnecessary empty
// sets, which is correct, but bad for output size.
EXPECT_EQ(subtractSelf.getNumDisjuncts(), 0u);
>From c2855b2f32c11c60b3a65a13dc8db603def98c57 Mon Sep 17 00:00:00 2001
From: Kunwar Grover <groverkss at gmail.com>
Date: Wed, 22 May 2024 09:30:02 +0000
Subject: [PATCH 3/3] clang-format
---
mlir/lib/Analysis/Presburger/PWMAFunction.cpp | 6 +++---
mlir/lib/Interfaces/ValueBoundsOpInterface.cpp | 3 +--
.../unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp | 6 ++----
3 files changed, 6 insertions(+), 9 deletions(-)
diff --git a/mlir/lib/Analysis/Presburger/PWMAFunction.cpp b/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
index 7acf32ab5751c..4911b237e1425 100644
--- a/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
+++ b/mlir/lib/Analysis/Presburger/PWMAFunction.cpp
@@ -293,9 +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())
- .isEmpty(SolverKind::IntegerSimplex) &&
- "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/Interfaces/ValueBoundsOpInterface.cpp b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
index 38bae85ca7549..21f96b30c0d8b 100644
--- a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
+++ b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
@@ -722,8 +722,7 @@ bool ValueBoundsConstraintSet::comparePos(int64_t lhsPos,
// set empty.
int64_t ineqPos = cstr.getNumInequalities();
cstr.addInequality(eq);
- bool isEmpty =
- cstr.isEmpty(presburger::SolverKind::FourierMotzkin);
+ 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 d8a08377dad76..9261110b3a678 100644
--- a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp
@@ -1201,16 +1201,14 @@ void expectSymbolicIntegerLexMin(
SymbolicLexOpt result = poly.findSymbolicIntegerLexMin();
if (expectedLexminRepr.empty()) {
- EXPECT_TRUE(
- result.lexopt.getDomain().isEmpty(SolverKind::IntegerSimplex));
+ EXPECT_TRUE(result.lexopt.getDomain().isEmpty(SolverKind::IntegerSimplex));
} else {
PWMAFunction expectedLexmin = parsePWMAF(expectedLexminRepr);
EXPECT_TRUE(result.lexopt.isEqual(expectedLexmin));
}
if (expectedUnboundedDomainRepr.empty()) {
- EXPECT_TRUE(
- result.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
+ EXPECT_TRUE(result.unboundedDomain.isEmpty(SolverKind::IntegerSimplex));
} else {
PresburgerSet expectedUnboundedDomain =
parsePresburgerSet(expectedUnboundedDomainRepr);
More information about the Mlir-commits
mailing list