diff --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h b/mlir/include/mlir/Analysis/Presburger/Simplex.h --- a/mlir/include/mlir/Analysis/Presburger/Simplex.h +++ b/mlir/include/mlir/Analysis/Presburger/Simplex.h @@ -237,6 +237,16 @@ void print(raw_ostream &os) const; void dump() const; + /// Check if the specified inequality already holds in the polytope. + bool isRedundantInequality(ArrayRef coeffs); + + /// Check if the specified equality already holds in the polytope. + bool isRedundantEquality(ArrayRef coeffs); + + /// Returns true if this Simplex's polytopes is a rational subset of `fac`. + /// Otherwise, returns false. + bool isRationalSubsetOf(const FlatAffineConstraints &fac); + private: friend class GBRSimplex; diff --git a/mlir/include/mlir/Analysis/PresburgerSet.h b/mlir/include/mlir/Analysis/PresburgerSet.h --- a/mlir/include/mlir/Analysis/PresburgerSet.h +++ b/mlir/include/mlir/Analysis/PresburgerSet.h @@ -94,6 +94,12 @@ /// any of the FACs in the union are unbounded. bool findIntegerSample(SmallVectorImpl &sample); + /// Simplifies the representation of a PresburgerSet. + /// + /// In particular, removes all FACs which are subsets of other FACs in the + /// union. + PresburgerSet coalesce() const; + private: /// Construct an empty PresburgerSet. PresburgerSet(unsigned nDim = 0, unsigned nSym = 0) diff --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp --- a/mlir/lib/Analysis/Presburger/Simplex.cpp +++ b/mlir/lib/Analysis/Presburger/Simplex.cpp @@ -1246,4 +1246,38 @@ void Simplex::dump() const { print(llvm::errs()); } +bool Simplex::isRationalSubsetOf(const FlatAffineConstraints &fac) { + if (isEmpty()) + return true; + + for (unsigned i = 0, e = fac.getNumInequalities(); i < e; ++i) + if (!isRedundantInequality(fac.getInequality(i))) + return false; + + for (unsigned i = 0, e = fac.getNumEqualities(); i < e; ++i) + if (!isRedundantEquality(fac.getEquality(i))) + return false; + + return true; +} + +/// Computes the minimum value `coeffs` can take. If the value is greater +/// than zero, the polytope entirely lies in the half-space defined +/// by `coeffs`. +bool Simplex::isRedundantInequality(ArrayRef coeffs) { + Optional minimum = computeOptimum(Direction::Down, coeffs); + return minimum && *minimum >= Fraction(0, 1); +} + +/// Check whether the equality given by `coeffs == 0` is redundant given +/// the existing constraints. This is redundant when `coeffs` is already +/// always zero under the existing constraints. `coeffs` is always zero +/// when the minimum and maximum value that `coeffs` can take are both zero. +bool Simplex::isRedundantEquality(ArrayRef coeffs) { + Optional minimum = computeOptimum(Direction::Down, coeffs); + Optional maximum = computeOptimum(Direction::Up, coeffs); + return minimum && maximum && *maximum == Fraction(0, 1) && + *minimum == Fraction(0, 1); +} + } // namespace mlir diff --git a/mlir/lib/Analysis/PresburgerSet.cpp b/mlir/lib/Analysis/PresburgerSet.cpp --- a/mlir/lib/Analysis/PresburgerSet.cpp +++ b/mlir/lib/Analysis/PresburgerSet.cpp @@ -381,6 +381,42 @@ return false; } +PresburgerSet PresburgerSet::coalesce() const { + PresburgerSet newSet = PresburgerSet::getEmptySet(getNumDims(), getNumSyms()); + llvm::SmallBitVector isRedundant(getNumFACs()); + + for (unsigned i = 0, e = flatAffineConstraints.size(); i < e; ++i) { + if (isRedundant[i]) + continue; + Simplex simplex(flatAffineConstraints[i]); + + // Check whether the polytope of `simplex` is empty. If so, it is trivially + // redundant. + if (simplex.isEmpty()) { + isRedundant[i] = true; + continue; + } + + // Check whether `FlatAffineConstraints[i]` is contained in any FAC, that is + // different from itself and not yet marked as redundant. + for (unsigned j = 0, e = flatAffineConstraints.size(); j < e; ++j) { + if (j == i || isRedundant[j]) + continue; + + if (simplex.isRationalSubsetOf(flatAffineConstraints[j])) { + isRedundant[i] = true; + break; + } + } + } + + for (unsigned i = 0, e = flatAffineConstraints.size(); i < e; ++i) + if (!isRedundant[i]) + newSet.unionFACInPlace(flatAffineConstraints[i]); + + return newSet; +} + void PresburgerSet::print(raw_ostream &os) const { os << getNumFACs() << " FlatAffineConstraints:\n"; for (const FlatAffineConstraints &fac : flatAffineConstraints) { diff --git a/mlir/unittests/Analysis/Presburger/CMakeLists.txt b/mlir/unittests/Analysis/Presburger/CMakeLists.txt --- a/mlir/unittests/Analysis/Presburger/CMakeLists.txt +++ b/mlir/unittests/Analysis/Presburger/CMakeLists.txt @@ -1,8 +1,11 @@ add_mlir_unittest(MLIRPresburgerTests MatrixTest.cpp SimplexTest.cpp + ../AffineStructuresParser.cpp ) target_link_libraries(MLIRPresburgerTests - PRIVATE MLIRPresburger) - + PRIVATE MLIRPresburger + MLIRLoopAnalysis + MLIRParser + ) diff --git a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp --- a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp +++ b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp @@ -7,6 +7,7 @@ //===----------------------------------------------------------------------===// #include "mlir/Analysis/Presburger/Simplex.h" +#include "../AffineStructuresParser.h" #include #include @@ -445,4 +446,84 @@ EXPECT_EQ(simplex.getNumConstraints(), 0u); } +TEST(SimplexTest, isRedundantInequality) { + Simplex simplex(2); + simplex.addInequality({0, -1, 2}); // y <= 2. + simplex.addInequality({1, 0, 0}); // x >= 0. + simplex.addEquality({-1, 1, 0}); // y = x. + + EXPECT_TRUE(simplex.isRedundantInequality({-1, 0, 2})); // x <= 2. + EXPECT_TRUE(simplex.isRedundantInequality({0, 1, 0})); // y >= 0. + + EXPECT_FALSE(simplex.isRedundantInequality({-1, 0, -1})); // x <= -1. + EXPECT_FALSE(simplex.isRedundantInequality({0, 1, -2})); // y >= 2. + EXPECT_FALSE(simplex.isRedundantInequality({0, 1, -1})); // y >= 1. +} + +TEST(SimplexTest, isRedundantEquality) { + Simplex simplex(2); + simplex.addInequality({0, -1, 2}); // y <= 2. + simplex.addInequality({1, 0, 0}); // x >= 0. + simplex.addEquality({-1, 1, 0}); // y = x. + + EXPECT_TRUE(simplex.isRedundantEquality({-1, 1, 0})); // y = x. + EXPECT_TRUE(simplex.isRedundantEquality({1, -1, 0})); // x = y. + + EXPECT_FALSE(simplex.isRedundantEquality({0, 1, -1})); // y = 1. + + simplex.addEquality({0, -1, 2}); // y = 2. + + EXPECT_TRUE(simplex.isRedundantEquality({-1, 0, 2})); // x = 2. +} + +static FlatAffineConstraints parseFAC(StringRef str, MLIRContext *context) { + FailureOr fac = parseIntegerSetToFAC(str, context); + + EXPECT_TRUE(succeeded(fac)); + + return *fac; +} + +TEST(SimplexTest, IsRationalSubsetOf) { + + MLIRContext context; + + FlatAffineConstraints univ = FlatAffineConstraints::getUniverse(1, 0); + FlatAffineConstraints empty = + parseFAC("(x) : (x + 0 >= 0, -x - 1 >= 0)", &context); + FlatAffineConstraints s1 = parseFAC("(x) : ( x >= 0, -x + 4 >= 0)", &context); + FlatAffineConstraints s2 = + parseFAC("(x) : (x - 1 >= 0, -x + 3 >= 0)", &context); + + Simplex simUniv(univ); + Simplex simEmpty(empty); + Simplex sim1(s1); + Simplex sim2(s2); + + EXPECT_TRUE(simUniv.isRationalSubsetOf(univ)); + EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty)); + EXPECT_TRUE(sim1.isRationalSubsetOf(s1)); + EXPECT_TRUE(sim2.isRationalSubsetOf(s2)); + + EXPECT_TRUE(simEmpty.isRationalSubsetOf(univ)); + EXPECT_TRUE(simEmpty.isRationalSubsetOf(s1)); + EXPECT_TRUE(simEmpty.isRationalSubsetOf(s2)); + EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty)); + + EXPECT_TRUE(simUniv.isRationalSubsetOf(univ)); + EXPECT_FALSE(simUniv.isRationalSubsetOf(s1)); + EXPECT_FALSE(simUniv.isRationalSubsetOf(s2)); + EXPECT_FALSE(simUniv.isRationalSubsetOf(empty)); + + EXPECT_TRUE(sim1.isRationalSubsetOf(univ)); + EXPECT_TRUE(sim1.isRationalSubsetOf(s1)); + EXPECT_FALSE(sim1.isRationalSubsetOf(s2)); + EXPECT_FALSE(sim1.isRationalSubsetOf(empty)); + + EXPECT_TRUE(sim2.isRationalSubsetOf(univ)); + EXPECT_TRUE(sim2.isRationalSubsetOf(s1)); + EXPECT_TRUE(sim2.isRationalSubsetOf(s2)); + EXPECT_FALSE(sim2.isRationalSubsetOf(empty)); +} + } // namespace mlir diff --git a/mlir/unittests/Analysis/PresburgerSetTest.cpp b/mlir/unittests/Analysis/PresburgerSetTest.cpp --- a/mlir/unittests/Analysis/PresburgerSetTest.cpp +++ b/mlir/unittests/Analysis/PresburgerSetTest.cpp @@ -15,6 +15,7 @@ //===----------------------------------------------------------------------===// #include "mlir/Analysis/PresburgerSet.h" +#include "./AffineStructuresParser.h" #include #include @@ -645,4 +646,191 @@ expectEqual(multiples3.intersect(evens), multiples6); } +/// Parses a FlatAffineConstraints from a StringRef. It is expected that the +/// string represents a valid IntegerSet, otherwise it will violate a gtest +/// assertion. +static FlatAffineConstraints parseFAC(StringRef str, MLIRContext *context) { + FailureOr fac = parseIntegerSetToFAC(str, context); + + EXPECT_TRUE(succeeded(fac)); + + return *fac; +} + +/// Coalesce `set` and check that the `newSet` is equal to `set and that +/// `expectedNumFACs` matches the number of FACs in the coalesced set. +/// If one of the two +void expectCoalesce(size_t expectedNumFACs, const PresburgerSet set) { + PresburgerSet newSet = set.coalesce(); + EXPECT_TRUE(set.isEqual(newSet)); + EXPECT_TRUE(expectedNumFACs == newSet.getNumFACs()); +} + +TEST(SetTest, coalesceNoFAC) { + PresburgerSet set = makeSetFromFACs(0, {}); + expectCoalesce(0, set); +} + +TEST(SetTest, coalesceContainedOneDim) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 1, {parseFAC("(x) : (x >= 0, -x + 4 >= 0)", &context), + parseFAC("(x) : (x - 1 >= 0, -x + 2 >= 0)", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceFirstEmpty) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 1, { + parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context), + parseFAC("(x) : ( x - 1 >= 0, -x + 2 >= 0)", &context), + }); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceSecondEmpty) { + MLIRContext context; + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : (x - 1 >= 0, -x + 2 >= 0)", &context), + parseFAC("(x) : (x >= 0, -x - 1 >= 0)", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceBothEmpty) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 1, { + parseFAC("(x) : (x - 3 >= 0, -x - 1 >= 0)", &context), + parseFAC("(x) : (x >= 0, -x - 1 >= 0)", &context), + }); + expectCoalesce(0, set); +} + +TEST(SetTest, coalesceFirstUniv) { + MLIRContext context; + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : ()", &context), + parseFAC("(x) : ( x >= 0, -x + 1 >= 0)", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceSecondUniv) { + MLIRContext context; + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : ( x >= 0, -x + 1 >= 0)", &context), + parseFAC("(x) : ()", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceBothUniv) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 1, {parseFAC("(x) : ()", &context), parseFAC("(x) : ()", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceFirstUnivSecondEmpty) { + MLIRContext context; + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : ()", &context), + parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceFirstEmptySecondUniv) { + MLIRContext context; + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context), + parseFAC("(x) : ()", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceCutOneDim) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 1, {parseFAC("(x) : ( x >= 0, -x + 3 >= 0)", &context), + parseFAC("(x) : ( x - 2 >= 0, -x + 4 >= 0)", &context)}); + expectCoalesce(2, set); +} + +TEST(SetTest, coalesceSeparateOneDim) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 1, {parseFAC("(x) : ( x >= 0, -x + 2 >= 0)", &context), + parseFAC("(x) : ( x - 3 >= 0, -x + 4 >= 0)", &context)}); + expectCoalesce(2, set); +} + +TEST(SetTest, coalesceContainedTwoDim) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 2, + {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", + &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceCutTwoDim) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 2, + {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)", + &context)}); + expectCoalesce(2, set); +} + +TEST(SetTest, coalesceSeparateTwoDim) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 2, + {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", + &context)}); + expectCoalesce(2, set); +} + +TEST(SetTest, coalesceContainedEq) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)", &context), + parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceCuttingEq) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x - 1 >= 0, -x + 3 >= 0, x - y == 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)", &context)}); + expectCoalesce(2, set); +} + +TEST(SetTest, coalesceSeparateEq) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)", &context)}); + expectCoalesce(2, set); +} + +TEST(SetTest, coalesceContainedEqAsIneq) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, x - y >= 0, -x + y >= 0)", + &context), + parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)}); + expectCoalesce(1, set); +} + +TEST(SetTest, coalesceContainedEqComplex) { + MLIRContext context; + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x - 2 == 0, x - y == 0)", &context), + parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)}); + expectCoalesce(1, set); +} + } // namespace mlir