From 84d07d021333f7b5716f0444d5c09105557272e0 Mon Sep 17 00:00:00 2001 From: Groverkss Date: Thu, 15 Sep 2022 12:09:00 +0100 Subject: [PATCH] [MLIR][Presburger] Improve unittest parsing This patch adds better functions for parsing MultiAffineFunctions and PWMAFunctions in Presburger unittests. A PWMAFunction can now be parsed as: ``` PWMAFunction result = parsePWMAF({ {"(x, y) : (x >= 10, x <= 20, y >= 1)", "(x, y) -> (x + y)"}, {"(x, y) : (x >= 21)", "(x, y) -> (x + y)"}, {"(x, y) : (x <= 9)", "(x, y) -> (x - y)"}, {"(x, y) : (x >= 10, x <= 20, y <= 0)", "(x, y) -> (x - y)"}, }); ``` which is much more readable than the old format since the output can be described as an AffineMap, instead of coefficients. This patch also adds support for parsing divisions in MultiAffineFunctions and PWMAFunctions which was previously not possible. Reviewed By: arjunp Differential Revision: https://reviews.llvm.org/D133654 --- mlir/include/mlir/AsmParser/AsmParser.h | 15 +- .../Dialect/Affine/Analysis/AffineStructures.h | 8 + mlir/lib/AsmParser/AffineParser.cpp | 30 +- .../Dialect/Affine/Analysis/AffineStructures.cpp | 28 ++ mlir/unittests/Analysis/Presburger/CMakeLists.txt | 3 +- .../Analysis/Presburger/IntegerPolyhedronTest.cpp | 503 +++++++++---------- .../Analysis/Presburger/IntegerRelationTest.cpp | 27 +- .../Analysis/Presburger/PWMAFunctionTest.cpp | 542 ++++++++------------- mlir/unittests/Analysis/Presburger/Parser.h | 106 ++++ .../Presburger/ParserTest.cpp} | 81 +-- .../Analysis/Presburger/PresburgerSetTest.cpp | 476 +++++++++--------- mlir/unittests/Analysis/Presburger/SimplexTest.cpp | 13 +- mlir/unittests/Analysis/Presburger/Utils.h | 53 -- .../Affine/Analysis/AffineStructuresParser.h | 34 -- .../Dialect/Affine/Analysis/CMakeLists.txt | 10 - mlir/unittests/Dialect/Affine/CMakeLists.txt | 1 - mlir/unittests/Dialect/CMakeLists.txt | 1 - 17 files changed, 903 insertions(+), 1028 deletions(-) create mode 100644 mlir/unittests/Analysis/Presburger/Parser.h rename mlir/unittests/{Dialect/Affine/Analysis/AffineStructuresParserTest.cpp => Analysis/Presburger/ParserTest.cpp} (56%) delete mode 100644 mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.h delete mode 100644 mlir/unittests/Dialect/Affine/Analysis/CMakeLists.txt delete mode 100644 mlir/unittests/Dialect/Affine/CMakeLists.txt diff --git a/mlir/include/mlir/AsmParser/AsmParser.h b/mlir/include/mlir/AsmParser/AsmParser.h index 601e86d..60ce797 100644 --- a/mlir/include/mlir/AsmParser/AsmParser.h +++ b/mlir/include/mlir/AsmParser/AsmParser.h @@ -76,14 +76,13 @@ Type parseType(llvm::StringRef typeStr, MLIRContext *context); /// returned in `numRead`. Type parseType(llvm::StringRef typeStr, MLIRContext *context, size_t &numRead); -/// This parses a single IntegerSet to an MLIR context if it was valid. If not, -/// an error message is emitted through a new SourceMgrDiagnosticHandler -/// constructed from a new SourceMgr with a single MemoryBuffer wrapping -/// `str`. If the passed `str` has additional tokens that were not part of the -/// IntegerSet, a failure is returned. Diagnostics are printed on failure if -/// `printDiagnosticInfo` is true. -IntegerSet parseIntegerSet(llvm::StringRef str, MLIRContext *context, - bool printDiagnosticInfo = true); +/// This parses a single IntegerSet/AffineMap to an MLIR context if it was +/// valid. If not, an error message is emitted through a new +/// SourceMgrDiagnosticHandler constructed from a new SourceMgr with a single +/// MemoryBuffer wrapping `str`. If the passed `str` has additional tokens that +/// were not part of the IntegerSet/AffineMap, a failure is returned. +AffineMap parseAffineMap(llvm::StringRef str, MLIRContext *context); +IntegerSet parseIntegerSet(llvm::StringRef str, MLIRContext *context); } // namespace mlir diff --git a/mlir/include/mlir/Dialect/Affine/Analysis/AffineStructures.h b/mlir/include/mlir/Dialect/Affine/Analysis/AffineStructures.h index 3c7561e..0e78d4c 100644 --- a/mlir/include/mlir/Dialect/Affine/Analysis/AffineStructures.h +++ b/mlir/include/mlir/Dialect/Affine/Analysis/AffineStructures.h @@ -32,6 +32,10 @@ class Value; class MemRefType; struct MutableAffineMap; +namespace presburger { +class MultiAffineFunction; +} // namespace presburger + /// FlatAffineValueConstraints represents an extension of IntegerPolyhedron /// where each non-local variable can have an SSA Value attached to it. class FlatAffineValueConstraints : public presburger::IntegerPolyhedron { @@ -615,6 +619,10 @@ getFlattenedAffineExprs(IntegerSet set, std::vector> *flattenedExprs, FlatAffineValueConstraints *cst = nullptr); +LogicalResult +getMultiAffineFunctionFromMap(AffineMap map, + presburger::MultiAffineFunction &multiAff); + /// Re-indexes the dimensions and symbols of an affine map with given `operands` /// values to align with `dims` and `syms` values. /// diff --git a/mlir/lib/AsmParser/AffineParser.cpp b/mlir/lib/AsmParser/AffineParser.cpp index 0480ee4..c6af9ee 100644 --- a/mlir/lib/AsmParser/AffineParser.cpp +++ b/mlir/lib/AsmParser/AffineParser.cpp @@ -734,8 +734,8 @@ Parser::parseAffineExprOfSSAIds(AffineExpr &expr, .parseAffineExprOfSSAIds(expr); } -IntegerSet mlir::parseIntegerSet(StringRef inputStr, MLIRContext *context, - bool printDiagnosticInfo) { +static void parseAffineMapOrIntegerSet(StringRef inputStr, MLIRContext *context, + AffineMap &map, IntegerSet &set) { llvm::SourceMgr sourceMgr; auto memBuffer = llvm::MemoryBuffer::getMemBuffer( inputStr, /*BufferName=*/"", @@ -747,17 +747,31 @@ IntegerSet mlir::parseIntegerSet(StringRef inputStr, MLIRContext *context, /*codeCompleteContext=*/nullptr); Parser parser(state); - raw_ostream &os = printDiagnosticInfo ? llvm::errs() : llvm::nulls(); - SourceMgrDiagnosticHandler handler(sourceMgr, context, os); - IntegerSet set; - if (parser.parseIntegerSetReference(set)) - return IntegerSet(); + SourceMgrDiagnosticHandler handler(sourceMgr, context, llvm::errs()); + if (parser.parseAffineMapOrIntegerSetReference(map, set)) + return; Token endTok = parser.getToken(); if (endTok.isNot(Token::eof)) { parser.emitError(endTok.getLoc(), "encountered unexpected token"); - return IntegerSet(); + return; } +} + +AffineMap mlir::parseAffineMap(StringRef inputStr, MLIRContext *context) { + AffineMap map; + IntegerSet set; + parseAffineMapOrIntegerSet(inputStr, context, map, set); + assert(!set && + "expected string to represent AffineMap, but got IntegerSet instead"); + return map; +} +IntegerSet mlir::parseIntegerSet(StringRef inputStr, MLIRContext *context) { + AffineMap map; + IntegerSet set; + parseAffineMapOrIntegerSet(inputStr, context, map, set); + assert(!map && + "expected string to represent IntegerSet, but got AffineMap instead"); return set; } diff --git a/mlir/lib/Dialect/Affine/Analysis/AffineStructures.cpp b/mlir/lib/Dialect/Affine/Analysis/AffineStructures.cpp index 9e86d1e..76e9625 100644 --- a/mlir/lib/Dialect/Affine/Analysis/AffineStructures.cpp +++ b/mlir/lib/Dialect/Affine/Analysis/AffineStructures.cpp @@ -1801,3 +1801,31 @@ LogicalResult mlir::getRelationFromMap(const AffineValueMap &map, return success(); } + +LogicalResult +mlir::getMultiAffineFunctionFromMap(AffineMap map, + MultiAffineFunction &multiAff) { + FlatAffineValueConstraints cst; + std::vector> flattenedExprs; + LogicalResult result = getFlattenedAffineExprs(map, &flattenedExprs, &cst); + + if (result.failed()) + return failure(); + + DivisionRepr divs = cst.getLocalReprs(); + assert(divs.hasAllReprs() && + "AffineMap cannot produce divs without local representation"); + + // TODO: We shouldn't have to do this conversion. + Matrix mat(map.getNumResults(), map.getNumInputs() + divs.getNumDivs() + 1); + for (unsigned i = 0, e = flattenedExprs.size(); i < e; ++i) + for (unsigned j = 0, f = flattenedExprs[i].size(); j < f; ++j) + mat(i, j) = flattenedExprs[i][j]; + + multiAff = MultiAffineFunction( + PresburgerSpace::getRelationSpace(map.getNumDims(), map.getNumResults(), + map.getNumSymbols(), divs.getNumDivs()), + mat, divs); + + return success(); +} diff --git a/mlir/unittests/Analysis/Presburger/CMakeLists.txt b/mlir/unittests/Analysis/Presburger/CMakeLists.txt index c7fc5f0..5af4232 100644 --- a/mlir/unittests/Analysis/Presburger/CMakeLists.txt +++ b/mlir/unittests/Analysis/Presburger/CMakeLists.txt @@ -4,11 +4,12 @@ add_mlir_unittest(MLIRPresburgerTests LinearTransformTest.cpp MatrixTest.cpp MPIntTest.cpp + Parser.h + ParserTest.cpp PresburgerSetTest.cpp PresburgerSpaceTest.cpp PWMAFunctionTest.cpp SimplexTest.cpp - ../../Dialect/Affine/Analysis/AffineStructuresParser.cpp ) target_link_libraries(MLIRPresburgerTests diff --git a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp index e8a71ed..be8a9e2 100644 --- a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp +++ b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp @@ -6,7 +6,8 @@ // //===----------------------------------------------------------------------===// -#include "./Utils.h" +#include "Parser.h" +#include "Utils.h" #include "mlir/Analysis/Presburger/IntegerRelation.h" #include "mlir/Analysis/Presburger/PWMAFunction.h" #include "mlir/Analysis/Presburger/Simplex.h" @@ -200,46 +201,53 @@ TEST(IntegerPolyhedronTest, removeIdRange) { TEST(IntegerPolyhedronTest, FindSampleTest) { // Bounded sets with only inequalities. // 0 <= 7x <= 5 - checkSample(true, parsePoly("(x) : (7 * x >= 0, -7 * x + 5 >= 0)")); + checkSample(true, + parseIntegerPolyhedron("(x) : (7 * x >= 0, -7 * x + 5 >= 0)")); // 1 <= 5x and 5x <= 4 (no solution). - checkSample(false, parsePoly("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)")); + checkSample( + false, parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)")); // 1 <= 5x and 5x <= 9 (solution: x = 1). - checkSample(true, parsePoly("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)")); + checkSample( + true, parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)")); // Bounded sets with equalities. // x >= 8 and 40 >= y and x = y. - checkSample(true, - parsePoly("(x,y) : (x - 8 >= 0, -y + 40 >= 0, x - y == 0)")); + checkSample(true, parseIntegerPolyhedron( + "(x,y) : (x - 8 >= 0, -y + 40 >= 0, x - y == 0)")); // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z. // solution: x = y = z = 10. - checkSample(true, parsePoly("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " - "z - 10 >= 0, x + 2 * y - 3 * z == 0)")); + checkSample(true, + parseIntegerPolyhedron("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " + "z - 10 >= 0, x + 2 * y - 3 * z == 0)")); // x <= 10 and y <= 10 and 11 <= z and x + 2y = 3z. // This implies x + 2y >= 33 and x + 2y <= 30, which has no solution. - checkSample(false, parsePoly("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " - "z - 11 >= 0, x + 2 * y - 3 * z == 0)")); + checkSample(false, + parseIntegerPolyhedron("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " + "z - 11 >= 0, x + 2 * y - 3 * z == 0)")); // 0 <= r and r <= 3 and 4q + r = 7. // Solution: q = 1, r = 3. - checkSample(true, - parsePoly("(q,r) : (r >= 0, -r + 3 >= 0, 4 * q + r - 7 == 0)")); + checkSample(true, parseIntegerPolyhedron( + "(q,r) : (r >= 0, -r + 3 >= 0, 4 * q + r - 7 == 0)")); // 4q + r = 7 and r = 0. // Solution: q = 1, r = 3. - checkSample(false, parsePoly("(q,r) : (4 * q + r - 7 == 0, r == 0)")); + checkSample(false, + parseIntegerPolyhedron("(q,r) : (4 * q + r - 7 == 0, r == 0)")); // The next two sets are large sets that should take a long time to sample // with a naive branch and bound algorithm but can be sampled efficiently with // the GBR algorithm. // // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (10000, 10000). - checkSample(true, parsePoly("(x,y) : (y >= 0, " - "300000 * x - 299999 * y - 100000 >= 0, " - "-300000 * x + 299998 * y + 200000 >= 0)")); + checkSample( + true, parseIntegerPolyhedron("(x,y) : (y >= 0, " + "300000 * x - 299999 * y - 100000 >= 0, " + "-300000 * x + 299998 * y + 200000 >= 0)")); // This is a tetrahedron with vertices at // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000). @@ -257,12 +265,12 @@ TEST(IntegerPolyhedronTest, FindSampleTest) { {}); // Same thing with some spurious extra dimensions equated to constants. - checkSample( - true, - parsePoly("(a,b,c,d,e) : (b + d - e >= 0, -b + c - d + e >= 0, " - "300000 * a - 299998 * b - c - 9 * d + 21 * e - 112000 >= 0, " - "-150000 * a + 149999 * b - 15 * d + 47 * e + 68000 >= 0, " - "d - e == 0, d + e - 2000 == 0)")); + checkSample(true, + parseIntegerPolyhedron( + "(a,b,c,d,e) : (b + d - e >= 0, -b + c - d + e >= 0, " + "300000 * a - 299998 * b - c - 9 * d + 21 * e - 112000 >= 0, " + "-150000 * a + 149999 * b - 15 * d + 47 * e + 68000 >= 0, " + "d - e == 0, d + e - 2000 == 0)")); // This is a tetrahedron with vertices at // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100). @@ -279,22 +287,24 @@ TEST(IntegerPolyhedronTest, FindSampleTest) { // empty. // This is a line segment from (0, 1/3) to (100, 100 + 1/3). - checkSample( - false, - parsePoly("(x,y) : (x >= 0, -x + 100 >= 0, 3 * x - 3 * y + 1 == 0)")); + checkSample(false, + parseIntegerPolyhedron( + "(x,y) : (x >= 0, -x + 100 >= 0, 3 * x - 3 * y + 1 == 0)")); // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3. - checkSample(false, - parsePoly("(x,y) : (x >= 0, -x + 100 >= 0, " - "3 * x - 3 * y + 2 >= 0, -3 * x + 3 * y - 1 >= 0)")); + checkSample(false, parseIntegerPolyhedron( + "(x,y) : (x >= 0, -x + 100 >= 0, " + "3 * x - 3 * y + 2 >= 0, -3 * x + 3 * y - 1 >= 0)")); - checkSample(true, parsePoly("(x,y) : (2 * x >= 0, -2 * x + 99 >= 0, " - "2 * y >= 0, -2 * y + 99 >= 0)")); + checkSample(true, + parseIntegerPolyhedron("(x,y) : (2 * x >= 0, -2 * x + 99 >= 0, " + "2 * y >= 0, -2 * y + 99 >= 0)")); // 2D cone with apex at (10000, 10000) and // edges passing through (1/3, 0) and (2/3, 0). - checkSample(true, parsePoly("(x,y) : (300000 * x - 299999 * y - 100000 >= 0, " - "-300000 * x + 299998 * y + 200000 >= 0)")); + checkSample(true, parseIntegerPolyhedron( + "(x,y) : (300000 * x - 299999 * y - 100000 >= 0, " + "-300000 * x + 299998 * y + 200000 >= 0)")); // Cartesian product of a tetrahedron and a 2D cone. // The tetrahedron has vertices at @@ -407,70 +417,68 @@ TEST(IntegerPolyhedronTest, FindSampleTest) { }, {}); - checkSample(true, parsePoly("(x, y, z) : (2 * x - 1 >= 0, x - y - 1 == 0, " - "y - z == 0)")); + checkSample(true, parseIntegerPolyhedron( + "(x, y, z) : (2 * x - 1 >= 0, x - y - 1 == 0, " + "y - z == 0)")); // Test with a local id. - checkSample(true, parsePoly("(x) : (x == 5*(x floordiv 2))")); + checkSample(true, parseIntegerPolyhedron("(x) : (x == 5*(x floordiv 2))")); // Regression tests for the computation of dual coefficients. - checkSample(false, parsePoly("(x, y, z) : (" - "6*x - 4*y + 9*z + 2 >= 0," - "x + 5*y + z + 5 >= 0," - "-4*x + y + 2*z - 1 >= 0," - "-3*x - 2*y - 7*z - 1 >= 0," - "-7*x - 5*y - 9*z - 1 >= 0)")); - checkSample(true, parsePoly("(x, y, z) : (" - "3*x + 3*y + 3 >= 0," - "-4*x - 8*y - z + 4 >= 0," - "-7*x - 4*y + z + 1 >= 0," - "2*x - 7*y - 8*z - 7 >= 0," - "9*x + 8*y - 9*z - 7 >= 0)")); - - checkSample( - true, - parsePoly( - "(x) : (1152921504606846977*(x floordiv 1152921504606846977) == x, " - "1152921504606846976*(x floordiv 1152921504606846976) == x)")); + checkSample(false, parseIntegerPolyhedron("(x, y, z) : (" + "6*x - 4*y + 9*z + 2 >= 0," + "x + 5*y + z + 5 >= 0," + "-4*x + y + 2*z - 1 >= 0," + "-3*x - 2*y - 7*z - 1 >= 0," + "-7*x - 5*y - 9*z - 1 >= 0)")); + checkSample(true, parseIntegerPolyhedron("(x, y, z) : (" + "3*x + 3*y + 3 >= 0," + "-4*x - 8*y - z + 4 >= 0," + "-7*x - 4*y + z + 1 >= 0," + "2*x - 7*y - 8*z - 7 >= 0," + "9*x + 8*y - 9*z - 7 >= 0)")); } TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) { // 1 <= 5x and 5x <= 4 (no solution). - EXPECT_TRUE( - parsePoly("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)").isIntegerEmpty()); + EXPECT_TRUE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)") + .isIntegerEmpty()); // 1 <= 5x and 5x <= 9 (solution: x = 1). - EXPECT_FALSE( - parsePoly("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)").isIntegerEmpty()); + EXPECT_FALSE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)") + .isIntegerEmpty()); // Unbounded sets. - EXPECT_TRUE(parsePoly("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, " - "2 * z - 1 >= 0, 2 * x - 1 == 0)") - .isIntegerEmpty()); + EXPECT_TRUE( + parseIntegerPolyhedron("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, " + "2 * z - 1 >= 0, 2 * x - 1 == 0)") + .isIntegerEmpty()); - EXPECT_FALSE(parsePoly("(x,y,z) : (2 * x - 1 >= 0, -3 * x + 3 >= 0, " - "5 * z - 6 >= 0, -7 * z + 17 >= 0, 3 * y - 2 >= 0)") + 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()); - EXPECT_FALSE( - parsePoly("(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)") - .isIntegerEmpty()); + EXPECT_FALSE(parseIntegerPolyhedron( + "(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)") + .isIntegerEmpty()); // IntegerPolyhedron::isEmpty() 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(parsePoly("(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, " - "3 * x + 7 * y - 1 == 0)") + EXPECT_TRUE(parseIntegerPolyhedron( + "(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, " + "3 * x + 7 * y - 1 == 0)") .isIntegerEmpty()); // 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. // Since x + y = 5 cannot be equal to 6z + 2 for any z, the set is empty. - EXPECT_TRUE( - parsePoly("(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()); + 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()); // 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. @@ -478,18 +486,19 @@ TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) { // y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying // x + y = 5 mod 6, which contradicts x + y = 6q + 2, so the set is empty. EXPECT_TRUE( - parsePoly( + 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()); // Set with symbols. - EXPECT_FALSE(parsePoly("(x)[s] : (x + s >= 0, x - s == 0)").isIntegerEmpty()); + EXPECT_FALSE(parseIntegerPolyhedron("(x)[s] : (x + s >= 0, x - s == 0)") + .isIntegerEmpty()); } TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) { IntegerPolyhedron poly = - parsePoly("(x) : (x - 2 >= 0, -x + 2 >= 0, x - 2 == 0)"); + parseIntegerPolyhedron("(x) : (x - 2 >= 0, -x + 2 >= 0, x - 2 == 0)"); poly.removeRedundantConstraints(); // Both inequalities are redundant given the equality. Both have been removed. @@ -497,7 +506,7 @@ TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) { EXPECT_EQ(poly.getNumEqualities(), 1u); IntegerPolyhedron poly2 = - parsePoly("(x,y) : (x - 3 >= 0, y - 2 >= 0, x - y == 0)"); + parseIntegerPolyhedron("(x,y) : (x - 3 >= 0, y - 2 >= 0, x - y == 0)"); poly2.removeRedundantConstraints(); // The second inequality is redundant and should have been removed. The @@ -507,52 +516,52 @@ TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) { EXPECT_EQ(poly2.getNumEqualities(), 1u); IntegerPolyhedron poly3 = - parsePoly("(x,y,z) : (x - y == 0, x - z == 0, y - z == 0)"); + parseIntegerPolyhedron("(x,y,z) : (x - y == 0, x - z == 0, y - z == 0)"); poly3.removeRedundantConstraints(); // One of the three equalities can be removed. EXPECT_EQ(poly3.getNumInequalities(), 0u); EXPECT_EQ(poly3.getNumEqualities(), 2u); - IntegerPolyhedron poly4 = - parsePoly("(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) : (" - "b - 1 >= 0," - "-b + 500 >= 0," - "-16 * d + f >= 0," - "f - 1 >= 0," - "-f + 998 >= 0," - "16 * d - f + 15 >= 0," - "-16 * e + g >= 0," - "g - 1 >= 0," - "-g + 998 >= 0," - "16 * e - g + 15 >= 0," - "h >= 0," - "-h + 1 >= 0," - "j - 1 >= 0," - "-j + 500 >= 0," - "-f + 16 * l + 15 >= 0," - "f - 16 * l >= 0," - "-16 * m + o >= 0," - "o - 1 >= 0," - "-o + 998 >= 0," - "16 * m - o + 15 >= 0," - "p >= 0," - "-p + 1 >= 0," - "-g - h + 8 * q + 8 >= 0," - "-o - p + 8 * q + 8 >= 0," - "o + p - 8 * q - 1 >= 0," - "g + h - 8 * q - 1 >= 0," - "-f + n >= 0," - "f - n >= 0," - "k - 10 >= 0," - "-k + 10 >= 0," - "i - 13 >= 0," - "-i + 13 >= 0," - "c - 10 >= 0," - "-c + 10 >= 0," - "a - 13 >= 0," - "-a + 13 >= 0" - ")"); + IntegerPolyhedron poly4 = parseIntegerPolyhedron( + "(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) : (" + "b - 1 >= 0," + "-b + 500 >= 0," + "-16 * d + f >= 0," + "f - 1 >= 0," + "-f + 998 >= 0," + "16 * d - f + 15 >= 0," + "-16 * e + g >= 0," + "g - 1 >= 0," + "-g + 998 >= 0," + "16 * e - g + 15 >= 0," + "h >= 0," + "-h + 1 >= 0," + "j - 1 >= 0," + "-j + 500 >= 0," + "-f + 16 * l + 15 >= 0," + "f - 16 * l >= 0," + "-16 * m + o >= 0," + "o - 1 >= 0," + "-o + 998 >= 0," + "16 * m - o + 15 >= 0," + "p >= 0," + "-p + 1 >= 0," + "-g - h + 8 * q + 8 >= 0," + "-o - p + 8 * q + 8 >= 0," + "o + p - 8 * q - 1 >= 0," + "g + h - 8 * q - 1 >= 0," + "-f + n >= 0," + "f - n >= 0," + "k - 10 >= 0," + "-k + 10 >= 0," + "i - 13 >= 0," + "-i + 13 >= 0," + "c - 10 >= 0," + "-c + 10 >= 0," + "a - 13 >= 0," + "-a + 13 >= 0" + ")"); // The above is a large set of constraints without any redundant constraints, // as verified by the Fourier-Motzkin based removeRedundantInequalities. @@ -567,7 +576,7 @@ TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) { EXPECT_EQ(poly4.getNumInequalities(), nIneq); EXPECT_EQ(poly4.getNumEqualities(), nEq); - IntegerPolyhedron poly5 = parsePoly( + IntegerPolyhedron poly5 = parseIntegerPolyhedron( "(x,y) : (128 * x + 127 >= 0, -x + 7 >= 0, -128 * x + y >= 0, y >= 0)"); // 128x + 127 >= 0 implies that 128x >= 0, since x has to be an integer. // (This should be caught by GCDTightenInqualities().) @@ -695,7 +704,7 @@ TEST(IntegerPolyhedronTest, computeLocalReprRecursive) { TEST(IntegerPolyhedronTest, computeLocalReprTightUpperBound) { { - IntegerPolyhedron poly = parsePoly("(i) : (i mod 3 - 1 >= 0)"); + IntegerPolyhedron poly = parseIntegerPolyhedron("(i) : (i mod 3 - 1 >= 0)"); // The set formed by the poly is: // 3q - i + 2 >= 0 <-- Division lower bound @@ -715,8 +724,8 @@ TEST(IntegerPolyhedronTest, computeLocalReprTightUpperBound) { } { - IntegerPolyhedron poly = - parsePoly("(i, j, q) : (4*q - i - j + 2 >= 0, -4*q + i + j >= 0)"); + IntegerPolyhedron poly = parseIntegerPolyhedron( + "(i, j, q) : (4*q - i - j + 2 >= 0, -4*q + i + j >= 0)"); // Convert `q` to a local variable. poly.convertToLocal(VarKind::SetDim, 2, 3); @@ -730,7 +739,8 @@ TEST(IntegerPolyhedronTest, computeLocalReprTightUpperBound) { TEST(IntegerPolyhedronTest, computeLocalReprFromEquality) { { - IntegerPolyhedron poly = parsePoly("(i, j, q) : (-4*q + i + j == 0)"); + IntegerPolyhedron poly = + parseIntegerPolyhedron("(i, j, q) : (-4*q + i + j == 0)"); // Convert `q` to a local variable. poly.convertToLocal(VarKind::SetDim, 2, 3); @@ -740,7 +750,8 @@ TEST(IntegerPolyhedronTest, computeLocalReprFromEquality) { checkDivisionRepresentation(poly, divisions, denoms); } { - IntegerPolyhedron poly = parsePoly("(i, j, q) : (4*q - i - j == 0)"); + IntegerPolyhedron poly = + parseIntegerPolyhedron("(i, j, q) : (4*q - i - j == 0)"); // Convert `q` to a local variable. poly.convertToLocal(VarKind::SetDim, 2, 3); @@ -750,7 +761,8 @@ TEST(IntegerPolyhedronTest, computeLocalReprFromEquality) { checkDivisionRepresentation(poly, divisions, denoms); } { - IntegerPolyhedron poly = parsePoly("(i, j, q) : (3*q + i + j - 2 == 0)"); + IntegerPolyhedron poly = + parseIntegerPolyhedron("(i, j, q) : (3*q + i + j - 2 == 0)"); // Convert `q` to a local variable. poly.convertToLocal(VarKind::SetDim, 2, 3); @@ -764,8 +776,8 @@ TEST(IntegerPolyhedronTest, computeLocalReprFromEquality) { TEST(IntegerPolyhedronTest, computeLocalReprFromEqualityAndInequality) { { IntegerPolyhedron poly = - parsePoly("(i, j, q, k) : (-3*k + i + j == 0, 4*q - " - "i - j + 2 >= 0, -4*q + i + j >= 0)"); + parseIntegerPolyhedron("(i, j, q, k) : (-3*k + i + j == 0, 4*q - " + "i - j + 2 >= 0, -4*q + i + j >= 0)"); // Convert `q` and `k` to local variables. poly.convertToLocal(VarKind::SetDim, 2, 4); @@ -779,7 +791,7 @@ TEST(IntegerPolyhedronTest, computeLocalReprFromEqualityAndInequality) { TEST(IntegerPolyhedronTest, computeLocalReprNoRepr) { IntegerPolyhedron poly = - parsePoly("(x, q) : (x - 3 * q >= 0, -x + 3 * q + 3 >= 0)"); + parseIntegerPolyhedron("(x, q) : (x - 3 * q >= 0, -x + 3 * q + 3 >= 0)"); // Convert q to a local variable. poly.convertToLocal(VarKind::SetDim, 1, 2); @@ -791,8 +803,8 @@ TEST(IntegerPolyhedronTest, computeLocalReprNoRepr) { } TEST(IntegerPolyhedronTest, computeLocalReprNegConstNormalize) { - IntegerPolyhedron poly = - parsePoly("(x, q) : (-1 - 3*x - 6 * q >= 0, 6 + 3*x + 6*q >= 0)"); + IntegerPolyhedron poly = parseIntegerPolyhedron( + "(x, q) : (-1 - 3*x - 6 * q >= 0, 6 + 3*x + 6*q >= 0)"); // Convert q to a local variable. poly.convertToLocal(VarKind::SetDim, 1, 2); @@ -1087,32 +1099,36 @@ void expectNoRationalLexMin(OptimumKind kind, const IntegerPolyhedron &poly) { TEST(IntegerPolyhedronTest, findRationalLexMin) { expectRationalLexMin( - parsePoly("(x, y, z) : (x + 10 >= 0, y + 40 >= 0, z + 30 >= 0)"), + parseIntegerPolyhedron( + "(x, y, z) : (x + 10 >= 0, y + 40 >= 0, z + 30 >= 0)"), {{-10, 1}, {-40, 1}, {-30, 1}}); expectRationalLexMin( - parsePoly( + parseIntegerPolyhedron( "(x, y, z) : (2*x + 7 >= 0, 3*y - 5 >= 0, 8*z + 10 >= 0, 9*z >= 0)"), {{-7, 2}, {5, 3}, {0, 1}}); - expectRationalLexMin(parsePoly("(x, y) : (3*x + 2*y + 10 >= 0, -3*y + 10 >= " - "0, 4*x - 7*y - 10 >= 0)"), - {{-50, 29}, {-70, 29}}); + expectRationalLexMin( + parseIntegerPolyhedron("(x, y) : (3*x + 2*y + 10 >= 0, -3*y + 10 >= " + "0, 4*x - 7*y - 10 >= 0)"), + {{-50, 29}, {-70, 29}}); // Test with some locals. This is basically x >= 11, 0 <= x - 2e <= 1. // It'll just choose x = 11, e = 5.5 since it's rational lexmin. expectRationalLexMin( - parsePoly( + parseIntegerPolyhedron( "(x, y) : (x - 2*(x floordiv 2) == 0, y - 2*x >= 0, x - 11 >= 0)"), {{11, 1}, {22, 1}}); - expectRationalLexMin(parsePoly("(x, y) : (3*x + 2*y + 10 >= 0," - "-4*x + 7*y + 10 >= 0, -3*y + 10 >= 0)"), - {{-50, 9}, {10, 3}}); + expectRationalLexMin( + parseIntegerPolyhedron("(x, y) : (3*x + 2*y + 10 >= 0," + "-4*x + 7*y + 10 >= 0, -3*y + 10 >= 0)"), + {{-50, 9}, {10, 3}}); // Cartesian product of above with itself. expectRationalLexMin( - parsePoly("(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0," - "-3*y + 10 >= 0, 3*z + 2*w + 10 >= 0, -4*z + 7*w + 10 >= 0," - "-3*w + 10 >= 0)"), + parseIntegerPolyhedron( + "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0," + "-3*y + 10 >= 0, 3*z + 2*w + 10 >= 0, -4*z + 7*w + 10 >= 0," + "-3*w + 10 >= 0)"), {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}}); // Same as above but for the constraints on z and w, we express "10" in terms @@ -1121,7 +1137,7 @@ TEST(IntegerPolyhedronTest, findRationalLexMin) { // minimized first. Accordingly, the values -9x - 12y, -9x - 0y - 10, // and -9x - 15y + 10 are all equal to 10. expectRationalLexMin( - parsePoly( + parseIntegerPolyhedron( "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0, " "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0," "-4*z + 7*w + - 9*x - 9*y - 10 >= 0, -3*w - 9*x - 15*y + 10 >= 0)"), @@ -1130,19 +1146,22 @@ TEST(IntegerPolyhedronTest, findRationalLexMin) { // Same as above with one constraint removed, making the lexmin unbounded. expectNoRationalLexMin( OptimumKind::Unbounded, - parsePoly("(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0," - "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0," - "-4*z + 7*w + - 9*x - 9*y - 10>= 0)")); + parseIntegerPolyhedron( + "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0," + "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0," + "-4*z + 7*w + - 9*x - 9*y - 10>= 0)")); // Again, the lexmin is unbounded. expectNoRationalLexMin( OptimumKind::Unbounded, - parsePoly("(x, y, z) : (2*x + 5*y + 8*z - 10 >= 0," - "2*x + 10*y + 8*z - 10 >= 0, 2*x + 5*y + 10*z - 10 >= 0)")); + parseIntegerPolyhedron( + "(x, y, z) : (2*x + 5*y + 8*z - 10 >= 0," + "2*x + 10*y + 8*z - 10 >= 0, 2*x + 5*y + 10*z - 10 >= 0)")); // The set is empty. - expectNoRationalLexMin(OptimumKind::Empty, - parsePoly("(x) : (2*x >= 0, -x - 1 >= 0)")); + expectNoRationalLexMin( + OptimumKind::Empty, + parseIntegerPolyhedron("(x) : (2*x >= 0, -x - 1 >= 0)")); } void expectIntegerLexMin(const IntegerPolyhedron &poly, ArrayRef min) { @@ -1158,108 +1177,99 @@ void expectNoIntegerLexMin(OptimumKind kind, const IntegerPolyhedron &poly) { } TEST(IntegerPolyhedronTest, findIntegerLexMin) { - expectIntegerLexMin(parsePoly("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 >= " - "0, 11*z + 5*y - 3*x + 7 >= 0)"), - {-6, -4, 0}); + expectIntegerLexMin( + parseIntegerPolyhedron("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 >= " + "0, 11*z + 5*y - 3*x + 7 >= 0)"), + {-6, -4, 0}); // Similar to above but no lower bound on z. - expectNoIntegerLexMin(OptimumKind::Unbounded, - parsePoly("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 " - ">= 0, -11*z + 5*y - 3*x + 7 >= 0)")); + expectNoIntegerLexMin( + OptimumKind::Unbounded, + parseIntegerPolyhedron("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 " + ">= 0, -11*z + 5*y - 3*x + 7 >= 0)")); } void expectSymbolicIntegerLexMin( StringRef polyStr, - ArrayRef, 8>>> - expectedLexminRepr, + ArrayRef> expectedLexminRepr, ArrayRef expectedUnboundedDomainRepr) { - IntegerPolyhedron poly = parsePoly(polyStr); + IntegerPolyhedron poly = parseIntegerPolyhedron(polyStr); ASSERT_NE(poly.getNumDimVars(), 0u); ASSERT_NE(poly.getNumSymbolVars(), 0u); - PWMAFunction expectedLexmin = - parsePWMAF(/*numInputs=*/0, - /*numOutputs=*/poly.getNumDimVars(), expectedLexminRepr, - /*numSymbols=*/poly.getNumSymbolVars()); - - PresburgerSet expectedUnboundedDomain = parsePresburgerSetFromPolyStrings( - /*numDims=*/0, expectedUnboundedDomainRepr, poly.getNumSymbolVars()); - SymbolicLexMin result = poly.findSymbolicIntegerLexMin(); - EXPECT_TRUE(result.lexmin.isEqual(expectedLexmin)); - if (!result.lexmin.isEqual(expectedLexmin)) { - llvm::errs() << "got:\n"; - result.lexmin.dump(); - llvm::errs() << "expected:\n"; - expectedLexmin.dump(); + if (expectedLexminRepr.empty()) { + EXPECT_TRUE(result.lexmin.getDomain().isIntegerEmpty()); + } else { + PWMAFunction expectedLexmin = parsePWMAF(expectedLexminRepr); + EXPECT_TRUE(result.lexmin.isEqual(expectedLexmin)); } - EXPECT_TRUE(result.unboundedDomain.isEqual(expectedUnboundedDomain)); - if (!result.unboundedDomain.isEqual(expectedUnboundedDomain)) - result.unboundedDomain.dump(); + if (expectedUnboundedDomainRepr.empty()) { + EXPECT_TRUE(result.unboundedDomain.isIntegerEmpty()); + } else { + PresburgerSet expectedUnboundedDomain = + parsePresburgerSet(expectedUnboundedDomainRepr); + EXPECT_TRUE(result.unboundedDomain.isEqual(expectedUnboundedDomain)); + } } void expectSymbolicIntegerLexMin( - StringRef polyStr, - ArrayRef, 8>>> - result) { + StringRef polyStr, ArrayRef> result) { expectSymbolicIntegerLexMin(polyStr, result, {}); } TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) { expectSymbolicIntegerLexMin("(x)[a] : (x - a >= 0)", { - {"()[a] : ()", {{1, 0}}}, // a + {"()[a] : ()", "()[a] -> (a)"}, }); expectSymbolicIntegerLexMin( "(x)[a, b] : (x - a >= 0, x - b >= 0)", { - {"()[a, b] : (a - b >= 0)", {{1, 0, 0}}}, // a - {"()[a, b] : (b - a - 1 >= 0)", {{0, 1, 0}}}, // b + {"()[a, b] : (a - b >= 0)", "()[a, b] -> (a)"}, + {"()[a, b] : (b - a - 1 >= 0)", "()[a, b] -> (b)"}, }); expectSymbolicIntegerLexMin( "(x)[a, b, c] : (x -a >= 0, x - b >= 0, x - c >= 0)", { - {"()[a, b, c] : (a - b >= 0, a - c >= 0)", {{1, 0, 0, 0}}}, // a - {"()[a, b, c] : (b - a - 1 >= 0, b - c >= 0)", {{0, 1, 0, 0}}}, // b + {"()[a, b, c] : (a - b >= 0, a - c >= 0)", "()[a, b, c] -> (a)"}, + {"()[a, b, c] : (b - a - 1 >= 0, b - c >= 0)", "()[a, b, c] -> (b)"}, {"()[a, b, c] : (c - a - 1 >= 0, c - b - 1 >= 0)", - {{0, 0, 1, 0}}}, // c + "()[a, b, c] -> (c)"}, }); expectSymbolicIntegerLexMin("(x, y)[a] : (x - a >= 0, x + y >= 0)", { - {"()[a] : ()", {{1, 0}, {-1, 0}}}, // (a, -a) + {"()[a] : ()", "()[a] -> (a, -a)"}, }); - expectSymbolicIntegerLexMin( - "(x, y)[a] : (x - a >= 0, x + y >= 0, y >= 0)", - { - {"()[a] : (a >= 0)", {{1, 0}, {0, 0}}}, // (a, 0) - {"()[a] : (-a - 1 >= 0)", {{1, 0}, {-1, 0}}}, // (a, -a) - }); + expectSymbolicIntegerLexMin("(x, y)[a] : (x - a >= 0, x + y >= 0, y >= 0)", + { + {"()[a] : (a >= 0)", "()[a] -> (a, 0)"}, + {"()[a] : (-a - 1 >= 0)", "()[a] -> (a, -a)"}, + }); expectSymbolicIntegerLexMin( "(x, y)[a, b, c] : (x - a >= 0, y - b >= 0, c - x - y >= 0)", { - {"()[a, b, c] : (c - a - b >= 0)", - {{1, 0, 0, 0}, {0, 1, 0, 0}}}, // (a, b) + {"()[a, b, c] : (c - a - b >= 0)", "()[a, b, c] -> (a, b)"}, }); expectSymbolicIntegerLexMin( "(x, y, z)[a, b, c] : (c - z >= 0, b - y >= 0, x + y + z - a == 0)", { - {"()[a, b, c] : ()", - {{1, -1, -1, 0}, {0, 1, 0, 0}, {0, 0, 1, 0}}}, // (a - b - c, b, c) + {"()[a, b, c] : ()", "()[a, b, c] -> (a - b - c, b, c)"}, }); expectSymbolicIntegerLexMin( "(x)[a, b] : (a >= 0, b >= 0, x >= 0, a + b + x - 1 >= 0)", { - {"()[a, b] : (a >= 0, b >= 0, a + b - 1 >= 0)", {{0, 0, 0}}}, // 0 - {"()[a, b] : (a == 0, b == 0)", {{0, 0, 1}}}, // 1 + {"()[a, b] : (a >= 0, b >= 0, a + b - 1 >= 0)", "()[a, b] -> (0)"}, + {"()[a, b] : (a == 0, b == 0)", "()[a, b] -> (1)"}, }); expectSymbolicIntegerLexMin( @@ -1268,8 +1278,8 @@ TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) { { {"()[a, b] : (1 - a >= 0, a >= 0, 1 - b >= 0, b >= 0, a + b - 1 >= " "0)", - {{0, 0, 0}}}, // 0 - {"()[a, b] : (a == 0, b == 0)", {{0, 0, 1}}}, // 1 + "()[a, b] -> (0)"}, + {"()[a, b] : (a == 0, b == 0)", "()[a, b] -> (1)"}, }); expectSymbolicIntegerLexMin( @@ -1277,50 +1287,51 @@ TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) { "y + z - 1 >= 0)", { {"()[a, b] : (a >= 0, b >= 0, 1 - a - b >= 0)", - {{1, 0, 0}, {0, 1, 0}, {-1, -1, 1}}}, // (a, b, 1 - a - b) + "()[a, b] -> (a, b, 1 - a - b)"}, {"()[a, b] : (a >= 0, b >= 0, a + b - 2 >= 0)", - {{1, 0, 0}, {0, 1, 0}, {0, 0, 0}}}, // (a, b, 0) + "()[a, b] -> (a, b, 0)"}, }); - expectSymbolicIntegerLexMin("(x)[a, b] : (x - a == 0, x - b >= 0)", - { - {"()[a, b] : (a - b >= 0)", {{1, 0, 0}}}, // a - }); + expectSymbolicIntegerLexMin( + "(x)[a, b] : (x - a == 0, x - b >= 0)", + { + {"()[a, b] : (a - b >= 0)", "()[a, b] -> (a)"}, + }); expectSymbolicIntegerLexMin( "(q)[a] : (a - 1 - 3*q == 0, q >= 0)", { {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)", - {{0, 1, 0}}}, // a floordiv 3 + "()[a] -> (a floordiv 3)"}, }); expectSymbolicIntegerLexMin( "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 1 - r >= 0, r >= 0)", { {"()[a] : (a - 0 - 3*(a floordiv 3) == 0, a >= 0)", - {{0, 0, 0}, {0, 1, 0}}}, // (0, a floordiv 3) + "()[a] -> (0, a floordiv 3)"}, {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)", - {{0, 0, 1}, {0, 1, 0}}}, // (1 a floordiv 3) + "()[a] -> (1, a floordiv 3)"}, // (1 a floordiv 3) }); expectSymbolicIntegerLexMin( "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 2 - r >= 0, r - 1 >= 0)", { {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)", - {{0, 0, 1}, {0, 1, 0}}}, // (1, a floordiv 3) + "()[a] -> (1, a floordiv 3)"}, {"()[a] : (a - 2 - 3*(a floordiv 3) == 0, a >= 0)", - {{0, 0, 2}, {0, 1, 0}}}, // (2, a floordiv 3) + "()[a] -> (2, a floordiv 3)"}, }); expectSymbolicIntegerLexMin( "(r, q)[a] : (a - r - 3*q == 0, q >= 0, r >= 0)", { {"()[a] : (a - 3*(a floordiv 3) == 0, a >= 0)", - {{0, 0, 0}, {0, 1, 0}}}, // (0, a floordiv 3) + "()[a] -> (0, a floordiv 3)"}, {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)", - {{0, 0, 1}, {0, 1, 0}}}, // (1, a floordiv 3) + "()[a] -> (1, a floordiv 3)"}, {"()[a] : (a - 2 - 3*(a floordiv 3) == 0, a >= 0)", - {{0, 0, 2}, {0, 1, 0}}}, // (2, a floordiv 3) + "()[a] -> (2, a floordiv 3)"}, }); expectSymbolicIntegerLexMin( @@ -1335,12 +1346,9 @@ TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) { // What's the lexmin solution using exactly g true vars? "g - x - y - z - w == 0)", { - {"()[g] : (g - 1 == 0)", - {{0, 0}, {0, 1}, {0, 0}, {0, 0}}}, // (0, 1, 0, 0) - {"()[g] : (g - 2 == 0)", - {{0, 0}, {0, 0}, {0, 1}, {0, 1}}}, // (0, 0, 1, 1) - {"()[g] : (g - 3 == 0)", - {{0, 0}, {0, 1}, {0, 1}, {0, 1}}}, // (0, 1, 1, 1) + {"()[g] : (g - 1 == 0)", "()[g] -> (0, 1, 0, 0)"}, + {"()[g] : (g - 2 == 0)", "()[g] -> (0, 0, 1, 1)"}, + {"()[g] : (g - 3 == 0)", "()[g] -> (0, 1, 1, 1)"}, }); // Bezout's lemma: if a, b are constants, @@ -1365,7 +1373,7 @@ TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) { "(b, c)[a] : (a - 4*b + 2*c == 0, c - b >= 0)", { {"()[a] : (a - 2*(a floordiv 2) == 0)", - {{0, 1, 0}, {0, 1, 0}}}, // (a floordiv 2, a floordiv 2) + "()[a] -> (a floordiv 2, a floordiv 2)"}, }); expectSymbolicIntegerLexMin( @@ -1377,7 +1385,7 @@ TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) { {"()[a] : (255 - (a floordiv 512) >= 0, a >= 0, a - 512*(a floordiv " "512) - 1 >= 0, 512*(a floordiv 512) - a + 509 >= 0, (a floordiv " "512) + 7 - 16*((8 + (a floordiv 512)) floordiv 16) >= 0)", - {{0, 1, 0, 0}}}, // (a floordiv 2, a floordiv 2) + "()[a] -> (a floordiv 512)"}, }); expectSymbolicIntegerLexMin( @@ -1386,12 +1394,11 @@ TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) { "N >= 0, 2*N - 4 - a >= 0," "2*N - 3*K + a - b >= 0, 4*N - K + 1 - 3*b >= 0, b - N >= 0, a - x - 1 " ">= 0)", - {{ - "()[K, N, x, y] : (x + 6 - 2*N >= 0, 2*N - 5 - x >= 0, x + 1 -3*K + " - "N " - ">= 0, N + K - 2 - x >= 0, x - 4 >= 0)", - {{0, 0, 1, 0, 1}, {0, 1, 0, 0, 0}} // (1 + x, N) - }}); + { + {"()[K, N, x, y] : (x + 6 - 2*N >= 0, 2*N - 5 - x >= 0, x + 1 -3*K + " + "N >= 0, N + K - 2 - x >= 0, x - 4 >= 0)", + "()[K, N, x, y] -> (1 + x, N)"}, + }); } static void @@ -1407,29 +1414,32 @@ TEST(IntegerPolyhedronTest, computeVolume) { // i.e. 0 <= x <= 3, -5 <= y <= 2, 3 <= z <= 3 + 1/4. // So volume is 4 * 8 * 1 = 32. expectComputedVolumeIsValidOverapprox( - parsePoly("(x, y, z) : (x >= 0, -3*x + 10 >= 0, 2*y + 11 >= 0," - "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), + parseIntegerPolyhedron( + "(x, y, z) : (x >= 0, -3*x + 10 >= 0, 2*y + 11 >= 0," + "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), /*trueVolume=*/32ull, /*resultBound=*/32ull); // Same as above but y has bounds 2 + 1/5 <= y <= 2 + 3/5. So the volume is // zero. expectComputedVolumeIsValidOverapprox( - parsePoly("(x, y, z) : (x >= 0, -3*x + 10 >= 0, 5*y - 11 >= 0," - "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), + parseIntegerPolyhedron( + "(x, y, z) : (x >= 0, -3*x + 10 >= 0, 5*y - 11 >= 0," + "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), /*trueVolume=*/0ull, /*resultBound=*/0ull); // Now x is unbounded below but y still has no integer values. expectComputedVolumeIsValidOverapprox( - parsePoly("(x, y, z) : (-3*x + 10 >= 0, 5*y - 11 >= 0," - "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), + parseIntegerPolyhedron("(x, y, z) : (-3*x + 10 >= 0, 5*y - 11 >= 0," + "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), /*trueVolume=*/0ull, /*resultBound=*/0ull); // A diamond shape, 0 <= x + y <= 10, 0 <= x - y <= 10, // with vertices at (0, 0), (5, 5), (5, 5), (10, 0). // x and y can take 11 possible values so result computed is 11*11 = 121. expectComputedVolumeIsValidOverapprox( - parsePoly("(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0," - "-x + y + 10 >= 0)"), + parseIntegerPolyhedron( + "(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0," + "-x + y + 10 >= 0)"), /*trueVolume=*/61ull, /*resultBound=*/121ull); // Effectively the same diamond as above; constrain the variables to be even @@ -1438,14 +1448,15 @@ TEST(IntegerPolyhedronTest, computeVolume) { // computing that x and y can take 21 possible values so result is 21*21 = // 441. expectComputedVolumeIsValidOverapprox( - parsePoly("(x, y) : (x + y >= 0, -x - y + 20 >= 0, x - y >= 0," - " -x + y + 20 >= 0, x - 2*(x floordiv 2) == 0," - "y - 2*(y floordiv 2) == 0)"), + parseIntegerPolyhedron( + "(x, y) : (x + y >= 0, -x - y + 20 >= 0, x - y >= 0," + " -x + y + 20 >= 0, x - 2*(x floordiv 2) == 0," + "y - 2*(y floordiv 2) == 0)"), /*trueVolume=*/61ull, /*resultBound=*/441ull); // Unbounded polytope. expectComputedVolumeIsValidOverapprox( - parsePoly("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"), + parseIntegerPolyhedron("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"), /*trueVolume=*/{}, /*resultBound=*/{}); } @@ -1455,18 +1466,22 @@ bool containsPointNoLocal(const IntegerPolyhedron &poly, } TEST(IntegerPolyhedronTest, containsPointNoLocal) { - IntegerPolyhedron poly1 = parsePoly("(x) : ((x floordiv 2) - x == 0)"); - EXPECT_TRUE(containsPointNoLocal(poly1, {0})); - EXPECT_FALSE(containsPointNoLocal(poly1, {1})); + IntegerPolyhedron poly1 = + parseIntegerPolyhedron("(x) : ((x floordiv 2) - x == 0)"); + EXPECT_TRUE(poly1.containsPointNoLocal({0})); + EXPECT_FALSE(poly1.containsPointNoLocal({1})); - IntegerPolyhedron poly2 = parsePoly( + IntegerPolyhedron poly2 = parseIntegerPolyhedron( "(x) : (x - 2*(x floordiv 2) == 0, x - 4*(x floordiv 4) - 2 == 0)"); EXPECT_TRUE(containsPointNoLocal(poly2, {6})); EXPECT_FALSE(containsPointNoLocal(poly2, {4})); - IntegerPolyhedron poly3 = parsePoly("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"); - EXPECT_TRUE(containsPointNoLocal(poly3, {0, 0})); - EXPECT_FALSE(containsPointNoLocal(poly3, {1, 0})); + IntegerPolyhedron poly3 = + parseIntegerPolyhedron("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"); + + // TODO: Using 0 instead of -0 makes this call ambiguous. Fix this. + EXPECT_TRUE(poly3.containsPointNoLocal({-0, 0})); + EXPECT_FALSE(poly3.containsPointNoLocal({1, 0})); } TEST(IntegerPolyhedronTest, truncateEqualityRegressionTest) { diff --git a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp index 18efe55..1a9241b 100644 --- a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp +++ b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp @@ -7,7 +7,7 @@ //===----------------------------------------------------------------------===// #include "mlir/Analysis/Presburger/IntegerRelation.h" -#include "./Utils.h" +#include "Parser.h" #include "mlir/Analysis/Presburger/Simplex.h" #include @@ -17,7 +17,7 @@ using namespace mlir; using namespace presburger; static IntegerRelation parseRelationFromSet(StringRef set, unsigned numDomain) { - IntegerRelation rel = parsePoly(set); + IntegerRelation rel = parseIntegerPolyhedron(set); rel.convertVarKind(VarKind::SetDim, 0, numDomain, VarKind::Domain); @@ -31,14 +31,14 @@ TEST(IntegerRelationTest, getDomainAndRangeSet) { IntegerPolyhedron domainSet = rel.getDomainSet(); IntegerPolyhedron expectedDomainSet = - parsePoly("(x)[N] : (x + 10 >= 0, N - x - 10 >= 0)"); + parseIntegerPolyhedron("(x)[N] : (x + 10 >= 0, N - x - 10 >= 0)"); EXPECT_TRUE(domainSet.isEqual(expectedDomainSet)); IntegerPolyhedron rangeSet = rel.getRangeSet(); IntegerPolyhedron expectedRangeSet = - parsePoly("(x)[N] : (x >= 0, N - x >= 0)"); + parseIntegerPolyhedron("(x)[N] : (x >= 0, N - x >= 0)"); EXPECT_TRUE(rangeSet.isEqual(expectedRangeSet)); } @@ -66,7 +66,8 @@ TEST(IntegerRelationTest, intersectDomainAndRange) { 1); { - IntegerPolyhedron poly = parsePoly("(x)[N, M] : (x >= 0, M - x - 1 >= 0)"); + IntegerPolyhedron poly = + parseIntegerPolyhedron("(x)[N, M] : (x >= 0, M - x - 1 >= 0)"); IntegerRelation expectedRel = parseRelationFromSet( "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M" @@ -79,8 +80,8 @@ TEST(IntegerRelationTest, intersectDomainAndRange) { } { - IntegerPolyhedron poly = - parsePoly("(y, z)[N, M] : (y >= 0, M - y - 1 >= 0, y + z == 0)"); + IntegerPolyhedron poly = parseIntegerPolyhedron( + "(y, z)[N, M] : (y >= 0, M - y - 1 >= 0, y + z == 0)"); IntegerRelation expectedRel = parseRelationFromSet( "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M" @@ -129,14 +130,10 @@ TEST(IntegerRelationTest, symbolicLexmin) { parseRelationFromSet("(a, x)[b] : (x - a >= 0, x - b >= 0)", 1) .findSymbolicIntegerLexMin(); - PWMAFunction expectedLexmin = - parsePWMAF(/*numInputs=*/1, - /*numOutputs=*/1, - { - {"(a)[b] : (a - b >= 0)", {{1, 0, 0}}}, // a - {"(a)[b] : (b - a - 1 >= 0)", {{0, 1, 0}}}, // b - }, - /*numSymbols=*/1); + PWMAFunction expectedLexmin = parsePWMAF({ + {"(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.lexmin.isEqual(expectedLexmin)); } diff --git a/mlir/unittests/Analysis/Presburger/PWMAFunctionTest.cpp b/mlir/unittests/Analysis/Presburger/PWMAFunctionTest.cpp index 1aff2fe..cebc7fa 100644 --- a/mlir/unittests/Analysis/Presburger/PWMAFunctionTest.cpp +++ b/mlir/unittests/Analysis/Presburger/PWMAFunctionTest.cpp @@ -10,7 +10,7 @@ // //===----------------------------------------------------------------------===// -#include "./Utils.h" +#include "Parser.h" #include "mlir/Analysis/Presburger/PWMAFunction.h" #include "mlir/Analysis/Presburger/PresburgerRelation.h" @@ -27,69 +27,50 @@ using testing::ElementsAre; TEST(PWAFunctionTest, isEqual) { // The output expressions are different but it doesn't matter because they are // equal in this domain. - PWMAFunction idAtZeros = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (y == 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y). - {"(x, y) : (y - 1 >= 0, x == 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y). - {"(x, y) : (-y - 1 >= 0, x == 0)", {{1, 0, 0}, {0, 1, 0}}} // (x, y). - }); - PWMAFunction idAtZeros2 = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (y == 0)", {{1, 0, 0}, {0, 20, 0}}}, // (x, 20y). - {"(x, y) : (y - 1 >= 0, x == 0)", {{30, 0, 0}, {0, 1, 0}}}, //(30x, y) - {"(x, y) : (-y - 1 > =0, x == 0)", {{30, 0, 0}, {0, 1, 0}}} //(30x, y) - }); + PWMAFunction idAtZeros = + parsePWMAF({{"(x, y) : (y == 0)", "(x, y) -> (x, y)"}, + {"(x, y) : (y - 1 >= 0, x == 0)", "(x, y) -> (x, y)"}, + {"(x, y) : (-y - 1 >= 0, x == 0)", "(x, y) -> (x, y)"}}); + PWMAFunction idAtZeros2 = + parsePWMAF({{"(x, y) : (y == 0)", "(x, y) -> (x, 20*y)"}, + {"(x, y) : (y - 1 >= 0, x == 0)", "(x, y) -> (30*x, y)"}, + {"(x, y) : (-y - 1 > =0, x == 0)", "(x, y) -> (30*x, y)"}}); EXPECT_TRUE(idAtZeros.isEqual(idAtZeros2)); - PWMAFunction notIdAtZeros = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (y == 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y). - {"(x, y) : (y - 1 >= 0, x == 0)", {{1, 0, 0}, {0, 2, 0}}}, // (x, 2y) - {"(x, y) : (-y - 1 >= 0, x == 0)", {{1, 0, 0}, {0, 2, 0}}}, // (x, 2y) - }); + PWMAFunction notIdAtZeros = parsePWMAF({ + {"(x, y) : (y == 0)", "(x, y) -> (x, y)"}, + {"(x, y) : (y - 1 >= 0, x == 0)", "(x, y) -> (x, 2*y)"}, + {"(x, y) : (-y - 1 >= 0, x == 0)", "(x, y) -> (x, 2*y)"}, + }); EXPECT_FALSE(idAtZeros.isEqual(notIdAtZeros)); // These match at their intersection but one has a bigger domain. - PWMAFunction idNoNegNegQuadrant = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x >= 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y). - {"(x, y) : (-x - 1 >= 0, y >= 0)", {{1, 0, 0}, {0, 1, 0}}} // (x, y). - }); - PWMAFunction idOnlyPosX = - parsePWMAF(/*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x >= 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y). - }); + PWMAFunction idNoNegNegQuadrant = + parsePWMAF({{"(x, y) : (x >= 0)", "(x, y) -> (x, y)"}, + {"(x, y) : (-x - 1 >= 0, y >= 0)", "(x, y) -> (x, y)"}}); + PWMAFunction idOnlyPosX = parsePWMAF({ + {"(x, y) : (x >= 0)", "(x, y) -> (x, y)"}, + }); EXPECT_FALSE(idNoNegNegQuadrant.isEqual(idOnlyPosX)); // Different representations of the same domain. - PWMAFunction sumPlusOne = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/1, - { - {"(x, y) : (x >= 0)", {{1, 1, 1}}}, // x + y + 1. - {"(x, y) : (-x - 1 >= 0, -y - 1 >= 0)", {{1, 1, 1}}}, // x + y + 1. - {"(x, y) : (-x - 1 >= 0, y >= 0)", {{1, 1, 1}}} // x + y + 1. - }); - PWMAFunction sumPlusOne2 = - parsePWMAF(/*numInputs=*/2, /*numOutputs=*/1, - { - {"(x, y) : ()", {{1, 1, 1}}}, // x + y + 1. - }); + PWMAFunction sumPlusOne = parsePWMAF({ + {"(x, y) : (x >= 0)", "(x, y) -> (x + y + 1)"}, + {"(x, y) : (-x - 1 >= 0, -y - 1 >= 0)", "(x, y) -> (x + y + 1)"}, + {"(x, y) : (-x - 1 >= 0, y >= 0)", "(x, y) -> (x + y + 1)"}, + }); + PWMAFunction sumPlusOne2 = parsePWMAF({ + {"(x, y) : ()", "(x, y) -> (x + y + 1)"}, + }); EXPECT_TRUE(sumPlusOne.isEqual(sumPlusOne2)); // Functions with zero input dimensions. - PWMAFunction noInputs1 = parsePWMAF(/*numInputs=*/0, /*numOutputs=*/1, - { - {"() : ()", {{1}}}, // 1. - }); - PWMAFunction noInputs2 = parsePWMAF(/*numInputs=*/0, /*numOutputs=*/1, - { - {"() : ()", {{2}}}, // 1. - }); + PWMAFunction noInputs1 = parsePWMAF({ + {"() : ()", "() -> (1)"}, + }); + PWMAFunction noInputs2 = parsePWMAF({ + {"() : ()", "() -> (2)"}, + }); EXPECT_TRUE(noInputs1.isEqual(noInputs1)); EXPECT_FALSE(noInputs1.isEqual(noInputs2)); @@ -100,53 +81,41 @@ TEST(PWAFunctionTest, isEqual) { // Divisions. // Domain is only multiples of 6; x = 6k for some k. // x + 4(x/2) + 4(x/3) == 26k. - PWMAFunction mul2AndMul3 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x - 2*(x floordiv 2) == 0, x - 3*(x floordiv 3) == 0)", - {{1, 4, 4, 0}}}, // x + 4(x/2) + 4(x/3). - }); - PWMAFunction mul6 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x - 6*(x floordiv 6) == 0)", {{0, 26, 0}}}, // 26(x/6). - }); + PWMAFunction mul2AndMul3 = parsePWMAF({ + {"(x) : (x - 2*(x floordiv 2) == 0, x - 3*(x floordiv 3) == 0)", + "(x) -> (x + 4 * (x floordiv 2) + 4 * (x floordiv 3))"}, + }); + PWMAFunction mul6 = parsePWMAF({ + {"(x) : (x - 6*(x floordiv 6) == 0)", "(x) -> (26 * (x floordiv 6))"}, + }); EXPECT_TRUE(mul2AndMul3.isEqual(mul6)); - PWMAFunction mul6diff = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x - 5*(x floordiv 5) == 0)", {{0, 52, 0}}}, // 52(x/6). - }); + PWMAFunction mul6diff = parsePWMAF({ + {"(x) : (x - 5*(x floordiv 5) == 0)", "(x) -> (52 * (x floordiv 6))"}, + }); EXPECT_FALSE(mul2AndMul3.isEqual(mul6diff)); - PWMAFunction mul5 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x - 5*(x floordiv 5) == 0)", {{0, 26, 0}}}, // 26(x/5). - }); + PWMAFunction mul5 = parsePWMAF({ + {"(x) : (x - 5*(x floordiv 5) == 0)", "(x) -> (26 * (x floordiv 5))"}, + }); EXPECT_FALSE(mul2AndMul3.isEqual(mul5)); } TEST(PWMAFunction, valueAt) { PWMAFunction nonNegPWMAF = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x >= 0)", {{1, 2, 3}, {3, 4, 5}}}, // (x, y). - {"(x, y) : (y >= 0, -x - 1 >= 0)", {{-1, 2, 3}, {-3, 4, 5}}} // (x, y) - }); + {{"(x, y) : (x >= 0)", "(x, y) -> (x + 2*y + 3, 3*x + 4*y + 5)"}, + {"(x, y) : (y >= 0, -x - 1 >= 0)", + "(x, y) -> (-x + 2*y + 3, -3*x + 4*y + 5)"}}); EXPECT_THAT(*nonNegPWMAF.valueAt({2, 3}), ElementsAre(11, 23)); EXPECT_THAT(*nonNegPWMAF.valueAt({-2, 3}), ElementsAre(11, 23)); EXPECT_THAT(*nonNegPWMAF.valueAt({2, -3}), ElementsAre(-1, -1)); EXPECT_FALSE(nonNegPWMAF.valueAt({-2, -3}).has_value()); PWMAFunction divPWMAF = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x >= 0, x - 2*(x floordiv 2) == 0)", - {{0, 2, 1, 3}, {0, 4, 3, 5}}}, // (x, y). - {"(x, y) : (y >= 0, -x - 1 >= 0)", {{-1, 2, 3}, {-3, 4, 5}}} // (x, y) - }); + {{"(x, y) : (x >= 0, x - 2*(x floordiv 2) == 0)", + "(x, y) -> (2*y + (x floordiv 2) + 3, 4*y + 3*(x floordiv 2) + 5)"}, + {"(x, y) : (y >= 0, -x - 1 >= 0)", + "(x, y) -> (-x + 2*y + 3, -3*x + 4*y + 5)"}}); EXPECT_THAT(*divPWMAF.valueAt({4, 3}), ElementsAre(11, 23)); EXPECT_THAT(*divPWMAF.valueAt({4, -3}), ElementsAre(-1, -1)); EXPECT_FALSE(divPWMAF.valueAt({3, 3}).has_value()); @@ -157,53 +126,40 @@ TEST(PWMAFunction, valueAt) { } TEST(PWMAFunction, removeIdRangeRegressionTest) { - PWMAFunction pwmafA = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/1, - { - {"(x, y) : (x == 0, y == 0, x - 2*(x floordiv 2) == 0, y - 2*(y " - "floordiv 2) == 0)", - {{0, 0, 0, 0, 0}}} // (0, 0) - }); - PWMAFunction pwmafB = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/1, - { - {"(x, y) : (x - 11*y == 0, 11*x - y == 0, x - 2*(x floordiv 2) == 0, " - "y - 2*(y floordiv 2) == 0)", - {{0, 0, 0, 0, 0}}} // (0, 0) - }); + PWMAFunction pwmafA = parsePWMAF({ + {"(x, y) : (x == 0, y == 0, x - 2*(x floordiv 2) == 0, y - 2*(y floordiv " + "2) == 0)", + "(x, y) -> (0, 0)"}, + }); + PWMAFunction pwmafB = parsePWMAF({ + {"(x, y) : (x - 11*y == 0, 11*x - y == 0, x - 2*(x floordiv 2) == 0, " + "y - 2*(y floordiv 2) == 0)", + "(x, y) -> (0, 0)"}, + }); EXPECT_TRUE(pwmafA.isEqual(pwmafB)); } TEST(PWMAFunction, eliminateRedundantLocalIdRegressionTest) { - PWMAFunction pwmafA = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/1, - { - {"(x, y) : (x - 2*(x floordiv 2) == 0, x - 2*y == 0)", - {{0, 1, 0, 0}}} // (0, 0) - }); - PWMAFunction pwmafB = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/1, - { - {"(x, y) : (x - 2*(x floordiv 2) == 0, x - 2*y == 0)", - {{1, -1, 0, 0}}} // (0, 0) - }); + PWMAFunction pwmafA = parsePWMAF({ + {"(x, y) : (x - 2*(x floordiv 2) == 0, x - 2*y == 0)", "(x, y) -> (y)"}, + }); + PWMAFunction pwmafB = parsePWMAF({ + {"(x, y) : (x - 2*(x floordiv 2) == 0, x - 2*y == 0)", + "(x, y) -> (x - y)"}, + }); EXPECT_TRUE(pwmafA.isEqual(pwmafB)); } TEST(PWMAFunction, unionLexMaxSimple) { // func2 is better than func1, but func2's domain is empty. { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : ()", {{0, 1}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (1 == 0)", {{0, 2}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(x) : ()", "(x) -> (1)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x) : (1 == 0)", "(x) -> (2)"}, + }); EXPECT_TRUE(func1.unionLexMax(func2).isEqual(func1)); EXPECT_TRUE(func2.unionLexMax(func1).isEqual(func1)); @@ -211,25 +167,19 @@ TEST(PWMAFunction, unionLexMaxSimple) { // func2 is better than func1 on a subset of func1. { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : ()", {{0, 1}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x >= 0, 10 - x >= 0)", {{0, 2}}}, - }); - - PWMAFunction result = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (-1 - x >= 0)", {{0, 1}}}, - {"(x) : (x >= 0, 10 - x >= 0)", {{0, 2}}}, - {"(x) : (x - 11 >= 0)", {{0, 1}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(x) : ()", "(x) -> (1)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (2)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(x) : (-1 - x >= 0)", "(x) -> (1)"}, + {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (2)"}, + {"(x) : (x - 11 >= 0)", "(x) -> (1)"}, + }); EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result)); EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result)); @@ -237,24 +187,18 @@ TEST(PWMAFunction, unionLexMaxSimple) { // func1 and func2 are defined over the whole domain with different outputs. { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : ()", {{1, 0}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : ()", {{-1, 0}}}, - }); - - PWMAFunction result = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x >= 0)", {{1, 0}}}, - {"(x) : (-1 - x >= 0)", {{-1, 0}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(x) : ()", "(x) -> (x)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x) : ()", "(x) -> (-x)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(x) : (x >= 0)", "(x) -> (x)"}, + {"(x) : (-1 - x >= 0)", "(x) -> (-x)"}, + }); EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result)); EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result)); @@ -262,28 +206,22 @@ TEST(PWMAFunction, unionLexMaxSimple) { // func1 and func2 have disjoint domains. { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x >= 0, 10 - x >= 0)", {{0, 1}}}, - {"(x) : (x - 71 >= 0, 80 - x >= 0)", {{0, 1}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x - 20 >= 0, 41 - x >= 0)", {{0, 2}}}, - {"(x) : (x - 101 >= 0, 120 - x >= 0)", {{0, 2}}}, - }); - - PWMAFunction result = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x >= 0, 10 - x >= 0)", {{0, 1}}}, - {"(x) : (x - 71 >= 0, 80 - x >= 0)", {{0, 1}}}, - {"(x) : (x - 20 >= 0, 41 - x >= 0)", {{0, 2}}}, - {"(x) : (x - 101 >= 0, 120 - x >= 0)", {{0, 2}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (1)"}, + {"(x) : (x - 71 >= 0, 80 - x >= 0)", "(x) -> (1)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x) : (x - 20 >= 0, 41 - x >= 0)", "(x) -> (2)"}, + {"(x) : (x - 101 >= 0, 120 - x >= 0)", "(x) -> (2)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (1)"}, + {"(x) : (x - 71 >= 0, 80 - x >= 0)", "(x) -> (1)"}, + {"(x) : (x - 20 >= 0, 41 - x >= 0)", "(x) -> (2)"}, + {"(x) : (x - 101 >= 0, 120 - x >= 0)", "(x) -> (2)"}, + }); EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result)); EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result)); @@ -293,17 +231,13 @@ TEST(PWMAFunction, unionLexMaxSimple) { TEST(PWMAFunction, unionLexMinSimple) { // func2 is better than func1, but func2's domain is empty. { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : ()", {{0, -1}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (1 == 0)", {{0, -2}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(x) : ()", "(x) -> (-1)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x) : (1 == 0)", "(x) -> (-2)"}, + }); EXPECT_TRUE(func1.unionLexMin(func2).isEqual(func1)); EXPECT_TRUE(func2.unionLexMin(func1).isEqual(func1)); @@ -311,25 +245,19 @@ TEST(PWMAFunction, unionLexMinSimple) { // func2 is better than func1 on a subset of func1. { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : ()", {{0, -1}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x >= 0, 10 - x >= 0)", {{0, -2}}}, - }); - - PWMAFunction result = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (-1 - x >= 0)", {{0, -1}}}, - {"(x) : (x >= 0, 10 - x >= 0)", {{0, -2}}}, - {"(x) : (x - 11 >= 0)", {{0, -1}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(x) : ()", "(x) -> (-1)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (-2)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(x) : (-1 - x >= 0)", "(x) -> (-1)"}, + {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (-2)"}, + {"(x) : (x - 11 >= 0)", "(x) -> (-1)"}, + }); EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result)); EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result)); @@ -337,24 +265,18 @@ TEST(PWMAFunction, unionLexMinSimple) { // func1 and func2 are defined over the whole domain with different outputs. { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : ()", {{-1, 0}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : ()", {{1, 0}}}, - }); - - PWMAFunction result = parsePWMAF( - /*numInputs=*/1, /*numOutputs=*/1, - { - {"(x) : (x >= 0)", {{-1, 0}}}, - {"(x) : (-1 - x >= 0)", {{1, 0}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(x) : ()", "(x) -> (-x)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x) : ()", "(x) -> (x)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(x) : (x >= 0)", "(x) -> (-x)"}, + {"(x) : (-1 - x >= 0)", "(x) -> (x)"}, + }); EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result)); EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result)); @@ -369,35 +291,20 @@ TEST(PWMAFunction, unionLexMaxComplex) { // 10 <= x <= 20, y > 0 --> func1 (x + y > x - y for y > 0) // 10 <= x <= 20, y <= 0 --> func2 (x + y <= x - y for y <= 0) { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/1, - { - {"(x, y) : (x >= 10)", {{1, 1, 0}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/1, - { - {"(x, y) : (x <= 20)", {{1, -1, 0}}}, - }); - - PWMAFunction result = parsePWMAF(/*numInputs=*/2, /*numOutputs=*/1, - {{"(x, y) : (x >= 10, x <= 20, y >= 1)", - { - {1, 1, 0}, - }}, - {"(x, y) : (x >= 21)", - { - {1, 1, 0}, - }}, - {"(x, y) : (x <= 9)", - { - {1, -1, 0}, - }}, - {"(x, y) : (x >= 10, x <= 20, y <= 0)", - { - {1, -1, 0}, - }}}); + PWMAFunction func1 = parsePWMAF({ + {"(x, y) : (x >= 10)", "(x, y) -> (x + y)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x, y) : (x <= 20)", "(x, y) -> (x - y)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(x, y) : (x >= 10, x <= 20, y >= 1)", "(x, y) -> (x + y)"}, + {"(x, y) : (x >= 21)", "(x, y) -> (x + y)"}, + {"(x, y) : (x <= 9)", "(x, y) -> (x - y)"}, + {"(x, y) : (x >= 10, x <= 20, y <= 0)", "(x, y) -> (x - y)"}, + }); EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result)); } @@ -411,34 +318,19 @@ TEST(PWMAFunction, unionLexMaxComplex) { // second output. -2x + 4 (func1) > 2x - 2 (func2) when 0 <= x <= 1, so we // take func1 for this domain and func2 for the remaining. { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x >= 0, y >= 0)", {{1, 1, 0}, {-2, 0, 4}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x >= 0, y >= 0)", {{1, 0, 0}, {2, 0, -2}}}, - }); - - PWMAFunction result = parsePWMAF(/*numInputs=*/2, /*numOutputs=*/2, - {{"(x, y) : (x >= 0, y >= 1)", - { - {1, 1, 0}, - {-2, 0, 4}, - }}, - {"(x, y) : (x >= 0, x <= 1, y == 0)", - { - {1, 1, 0}, - {-2, 0, 4}, - }}, - {"(x, y) : (x >= 2, y == 0)", - { - {1, 0, 0}, - {2, 0, -2}, - }}}); + PWMAFunction func1 = parsePWMAF({ + {"(x, y) : (x >= 0, y >= 0)", "(x, y) -> (x + y, -2*x + 4)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x, y) : (x >= 0, y >= 0)", "(x, y) -> (x, 2*x - 2)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(x, y) : (x >= 0, y >= 1)", "(x, y) -> (x + y, -2*x + 4)"}, + {"(x, y) : (x >= 0, x <= 1, y == 0)", "(x, y) -> (x + y, -2*x + 4)"}, + {"(x, y) : (x >= 2, y == 0)", "(x, y) -> (x, 2*x - 2)"}, + }); EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result)); EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result)); @@ -451,32 +343,26 @@ TEST(PWMAFunction, unionLexMaxComplex) { // a == 0, b == 1 --> Take func1 // a == 0, b == 0, c == 1 --> Take func2 { - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/3, /*numOutputs=*/3, - { - {"(a, b, c) : (a >= 0, 1 - a >= 0, b >= 0, 1 - b >= 0, c " - ">= 0, 1 - c >= 0)", - {{0, 0, 0, 0}, {0, 1, 0, 0}, {0, 0, 0, 0}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/3, /*numOutputs=*/3, - { - {"(a, b, c) : (a >= 0, 1 - a >= 0, b >= 0, 1 - b >= 0, c >= 0, 1 - " - "c >= 0)", - {{1, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 1, 0}}}, - }); - - PWMAFunction result = parsePWMAF( - /*numInputs=*/3, /*numOutputs=*/3, - { - {"(a, b, c) : (a - 1 == 0, b >= 0, 1 - b >= 0, c >= 0, 1 - c >= 0)", - {{1, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 1, 0}}}, - {"(a, b, c) : (a == 0, b - 1 == 0, c >= 0, 1 - c >= 0)", - {{0, 0, 0, 0}, {0, 1, 0, 0}, {0, 0, 0, 0}}}, - {"(a, b, c) : (a == 0, b == 0, c >= 0, 1 - c >= 0)", - {{1, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 1, 0}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(a, b, c) : (a >= 0, 1 - a >= 0, b >= 0, 1 - b >= 0, c " + ">= 0, 1 - c >= 0)", + "(a, b, c) -> (0, b, 0)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(a, b, c) : (a >= 0, 1 - a >= 0, b >= 0, 1 - b >= 0, c >= 0, 1 - " + "c >= 0)", + "(a, b, c) -> (a, 0, c)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(a, b, c) : (a - 1 == 0, b >= 0, 1 - b >= 0, c >= 0, 1 - c >= 0)", + "(a, b, c) -> (a, 0, c)"}, + {"(a, b, c) : (a == 0, b - 1 == 0, c >= 0, 1 - c >= 0)", + "(a, b, c) -> (0, b, 0)"}, + {"(a, b, c) : (a == 0, b == 0, c >= 0, 1 - c >= 0)", + "(a, b, c) -> (a, 0, c)"}, + }); EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result)); EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result)); @@ -493,26 +379,18 @@ TEST(PWMAFunction, unionLexMinComplex) { // If x == 0, func1 and func2 both have the same first output. So we take a // look at the second output. func2 is better since in the second output, // y - 1 (func2) is < y (func1). - PWMAFunction func1 = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x >= 0, x <= 1, y >= 0, y <= 1)", - {{-1, 0, 0}, {0, 1, 0}}}, - }); - - PWMAFunction func2 = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x >= 0, x <= 1, y >= 0, y <= 1)", - {{0, 0, 0}, {0, 1, -1}}}, - }); - - PWMAFunction result = parsePWMAF( - /*numInputs=*/2, /*numOutputs=*/2, - { - {"(x, y) : (x == 1, y >= 0, y <= 1)", {{-1, 0, 0}, {0, 1, 0}}}, - {"(x, y) : (x == 0, y >= 0, y <= 1)", {{0, 0, 0}, {0, 1, -1}}}, - }); + PWMAFunction func1 = parsePWMAF({ + {"(x, y) : (x >= 0, x <= 1, y >= 0, y <= 1)", "(x, y) -> (-x, y)"}, + }); + + PWMAFunction func2 = parsePWMAF({ + {"(x, y) : (x >= 0, x <= 1, y >= 0, y <= 1)", "(x, y) -> (0, y - 1)"}, + }); + + PWMAFunction result = parsePWMAF({ + {"(x, y) : (x == 1, y >= 0, y <= 1)", "(x, y) -> (-x, y)"}, + {"(x, y) : (x == 0, y >= 0, y <= 1)", "(x, y) -> (0, y - 1)"}, + }); EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result)); EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result)); diff --git a/mlir/unittests/Analysis/Presburger/Parser.h b/mlir/unittests/Analysis/Presburger/Parser.h new file mode 100644 index 0000000..2e064e8ab --- /dev/null +++ b/mlir/unittests/Analysis/Presburger/Parser.h @@ -0,0 +1,106 @@ +//===- Parser.h - Parser for Presburger library -----------------*- C++ -*-===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// This file defines functions to parse strings into Presburger library +// constructs. +// +//===----------------------------------------------------------------------===// + +#ifndef MLIR_UNITTESTS_ANALYSIS_PRESBURGER_PARSER_H +#define MLIR_UNITTESTS_ANALYSIS_PRESBURGER_PARSER_H + +#include "mlir/Analysis/Presburger/IntegerRelation.h" +#include "mlir/Analysis/Presburger/PWMAFunction.h" +#include "mlir/Analysis/Presburger/PresburgerRelation.h" +#include "mlir/AsmParser/AsmParser.h" +#include "mlir/Dialect/Affine/Analysis/AffineStructures.h" +#include "mlir/IR/AffineExpr.h" +#include "mlir/IR/AffineMap.h" +#include "mlir/IR/IntegerSet.h" + +namespace mlir { +namespace presburger { + +/// Parses an IntegerPolyhedron from a StringRef. It is expected that the string +/// represents a valid IntegerSet. +inline IntegerPolyhedron parseIntegerPolyhedron(StringRef str) { + MLIRContext context(MLIRContext::Threading::DISABLED); + return FlatAffineValueConstraints(parseIntegerSet(str, &context)); +} + +/// Parse a list of StringRefs to IntegerRelation and combine them into a +/// PresburgerSet by using the union operation. It is expected that the strings +/// are all valid IntegerSet representation and that all of them have compatible +/// spaces. +inline PresburgerSet parsePresburgerSet(ArrayRef strs) { + assert(!strs.empty() && "strs should not be empty"); + + IntegerPolyhedron initPoly = parseIntegerPolyhedron(strs[0]); + PresburgerSet result(initPoly); + for (unsigned i = 1, e = strs.size(); i < e; ++i) + result.unionInPlace(parseIntegerPolyhedron(strs[i])); + return result; +} + +inline MultiAffineFunction parseMultiAffineFunction(StringRef str) { + MLIRContext context(MLIRContext::Threading::DISABLED); + + // TODO: Add default constructor for MultiAffineFunction. + MultiAffineFunction multiAff(PresburgerSpace::getRelationSpace(), + Matrix(0, 1)); + if (getMultiAffineFunctionFromMap(parseAffineMap(str, &context), multiAff) + .failed()) + llvm_unreachable( + "Failed to parse MultiAffineFunction because of semi-affinity"); + return multiAff; +} + +inline PWMAFunction +parsePWMAF(ArrayRef, StringRef>> pieces) { + assert(!pieces.empty() && "At least one piece should be present."); + + MLIRContext context(MLIRContext::Threading::DISABLED); + + PresburgerSet initDomain = parsePresburgerSet(pieces[0].first); + MultiAffineFunction initMultiAff = parseMultiAffineFunction(pieces[0].second); + + PWMAFunction func(PresburgerSpace::getRelationSpace( + initMultiAff.getNumDomainVars(), initMultiAff.getNumOutputs(), + initMultiAff.getNumSymbolVars())); + + func.addPiece({initDomain, initMultiAff}); + for (unsigned i = 1, e = pieces.size(); i < e; ++i) + func.addPiece({parsePresburgerSet(pieces[i].first), + parseMultiAffineFunction(pieces[i].second)}); + return func; +} + +inline PWMAFunction +parsePWMAF(ArrayRef> pieces) { + assert(!pieces.empty() && "At least one piece should be present."); + + MLIRContext context(MLIRContext::Threading::DISABLED); + + IntegerPolyhedron initDomain = parseIntegerPolyhedron(pieces[0].first); + MultiAffineFunction initMultiAff = parseMultiAffineFunction(pieces[0].second); + + PWMAFunction func(PresburgerSpace::getRelationSpace( + initMultiAff.getNumDomainVars(), initMultiAff.getNumOutputs(), + initMultiAff.getNumSymbolVars())); + + func.addPiece({PresburgerSet(initDomain), initMultiAff}); + for (unsigned i = 1, e = pieces.size(); i < e; ++i) + func.addPiece({PresburgerSet(parseIntegerPolyhedron(pieces[i].first)), + parseMultiAffineFunction(pieces[i].second)}); + return func; +} + +} // namespace presburger +} // namespace mlir + +#endif // MLIR_UNITTESTS_ANALYSIS_PRESBURGER_PARSER_H diff --git a/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParserTest.cpp b/mlir/unittests/Analysis/Presburger/ParserTest.cpp similarity index 56% rename from mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParserTest.cpp rename to mlir/unittests/Analysis/Presburger/ParserTest.cpp index 0cc41a8..4c9f54f 100644 --- a/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParserTest.cpp +++ b/mlir/unittests/Analysis/Presburger/ParserTest.cpp @@ -1,4 +1,4 @@ -//===- AffineStructuresParserTest.cpp - FAC parsing unit tests --*- C++ -*-===// +//===- PresbugerParserTest.cpp - Presburger parsing unit tests --*- C++ -*-===// // // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. // See https://llvm.org/LICENSE.txt for license information. @@ -13,8 +13,7 @@ // //===----------------------------------------------------------------------===// -#include "./AffineStructuresParser.h" -#include "mlir/Analysis/Presburger/PresburgerRelation.h" +#include "Parser.h" #include @@ -38,99 +37,53 @@ static IntegerPolyhedron makeFACFromConstraints( return fac; } -TEST(ParseFACTest, InvalidInputTest) { - MLIRContext context; - FailureOr fac; - - fac = parseIntegerSetToFAC("(x)", &context, false); - EXPECT_TRUE(failed(fac)) - << "should not accept strings with no constraint list"; - - fac = parseIntegerSetToFAC("(x)[] : ())", &context, false); - EXPECT_TRUE(failed(fac)) - << "should not accept strings that contain remaining characters"; - - fac = parseIntegerSetToFAC("(x)[] : (x - >= 0)", &context, false); - EXPECT_TRUE(failed(fac)) - << "should not accept strings that contain incomplete constraints"; - - fac = parseIntegerSetToFAC("(x)[] : (y == 0)", &context, false); - EXPECT_TRUE(failed(fac)) - << "should not accept strings that contain unknown identifiers"; - - fac = parseIntegerSetToFAC("(x, x) : (2 * x >= 0)", &context, false); - EXPECT_TRUE(failed(fac)) - << "should not accept strings that contain repeated identifier names"; - - fac = parseIntegerSetToFAC("(x)[x] : (2 * x >= 0)", &context, false); - EXPECT_TRUE(failed(fac)) - << "should not accept strings that contain repeated identifier names"; - - fac = parseIntegerSetToFAC("(x) : (2 * x + 9223372036854775808 >= 0)", - &context, false); - EXPECT_TRUE(failed(fac)) << "should not accept strings with integer literals " - "that do not fit into int64_t"; -} - /// Parses and compares the `str` to the `ex`. The equality check is performed /// by using PresburgerSet::isEqual -static bool parseAndCompare(StringRef str, const IntegerPolyhedron &ex, - MLIRContext *context) { - FailureOr fac = parseIntegerSetToFAC(str, context); - - EXPECT_TRUE(succeeded(fac)); - - return PresburgerSet(*fac).isEqual(PresburgerSet(ex)); +static bool parseAndCompare(StringRef str, const IntegerPolyhedron &ex) { + IntegerPolyhedron poly = parseIntegerPolyhedron(str); + return PresburgerSet(poly).isEqual(PresburgerSet(ex)); } TEST(ParseFACTest, ParseAndCompareTest) { - MLIRContext context; // simple ineq - EXPECT_TRUE(parseAndCompare( - "(x)[] : (x >= 0)", makeFACFromConstraints(1, 0, {{1, 0}}), &context)); + EXPECT_TRUE(parseAndCompare("(x)[] : (x >= 0)", + makeFACFromConstraints(1, 0, {{1, 0}}))); // simple eq EXPECT_TRUE(parseAndCompare("(x)[] : (x == 0)", - makeFACFromConstraints(1, 0, {}, {{1, 0}}), - &context)); + makeFACFromConstraints(1, 0, {}, {{1, 0}}))); // multiple constraints EXPECT_TRUE(parseAndCompare("(x)[] : (7 * x >= 0, -7 * x + 5 >= 0)", - makeFACFromConstraints(1, 0, {{7, 0}, {-7, 5}}), - &context)); + makeFACFromConstraints(1, 0, {{7, 0}, {-7, 5}}))); // multiple dimensions EXPECT_TRUE(parseAndCompare("(x,y,z)[] : (x + y - z >= 0)", - makeFACFromConstraints(3, 0, {{1, 1, -1, 0}}), - &context)); + makeFACFromConstraints(3, 0, {{1, 1, -1, 0}}))); // dimensions and symbols - EXPECT_TRUE(parseAndCompare( - "(x,y,z)[a,b] : (x + y - z + 2 * a - 15 * b >= 0)", - makeFACFromConstraints(3, 2, {{1, 1, -1, 2, -15, 0}}), &context)); + EXPECT_TRUE( + parseAndCompare("(x,y,z)[a,b] : (x + y - z + 2 * a - 15 * b >= 0)", + makeFACFromConstraints(3, 2, {{1, 1, -1, 2, -15, 0}}))); // only symbols EXPECT_TRUE(parseAndCompare("()[a] : (2 * a - 4 == 0)", - makeFACFromConstraints(0, 1, {}, {{2, -4}}), - &context)); + makeFACFromConstraints(0, 1, {}, {{2, -4}}))); // simple floordiv EXPECT_TRUE(parseAndCompare( "(x, y) : (y - 3 * ((x + y - 13) floordiv 3) - 42 == 0)", - makeFACFromConstraints(2, 0, {}, {{0, 1, -3, -42}}, {{{1, 1, -13}, 3}}), - &context)); + makeFACFromConstraints(2, 0, {}, {{0, 1, -3, -42}}, {{{1, 1, -13}, 3}}))); // multiple floordiv EXPECT_TRUE(parseAndCompare( "(x, y) : (y - x floordiv 3 - y floordiv 2 == 0)", makeFACFromConstraints(2, 0, {}, {{0, 1, -1, -1, 0}}, - {{{1, 0, 0}, 3}, {{0, 1, 0, 0}, 2}}), - &context)); + {{{1, 0, 0}, 3}, {{0, 1, 0, 0}, 2}}))); // nested floordiv EXPECT_TRUE(parseAndCompare( "(x, y) : (y - (x + y floordiv 2) floordiv 3 == 0)", makeFACFromConstraints(2, 0, {}, {{0, 1, 0, -1, 0}}, - {{{0, 1, 0}, 2}, {{1, 0, 1, 0}, 3}}), - &context)); + {{{0, 1, 0}, 2}, {{1, 0, 1, 0}, 3}}))); } diff --git a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp index 8e0f1c2..3e4d272 100644 --- a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp +++ b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp @@ -14,7 +14,8 @@ // //===----------------------------------------------------------------------===// -#include "./Utils.h" +#include "Parser.h" +#include "Utils.h" #include "mlir/Analysis/Presburger/PresburgerRelation.h" #include "mlir/IR/MLIRContext.h" @@ -97,8 +98,7 @@ static PresburgerSet makeSetFromPoly(unsigned numDims, } TEST(SetTest, containsPoint) { - PresburgerSet setA = parsePresburgerSetFromPolyStrings( - 1, + PresburgerSet setA = parsePresburgerSet( {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}); for (unsigned x = 0; x <= 21; ++x) { if ((2 <= x && x <= 8) || (10 <= x && x <= 20)) @@ -109,10 +109,10 @@ TEST(SetTest, containsPoint) { // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} union // a square with opposite corners (2, 2) and (10, 10). - PresburgerSet setB = parsePresburgerSetFromPolyStrings( - 2, {"(x,y) : (x + y - 4 >= 0, -x - y + 32 >= 0, " - "x - y - 2 >= 0, -x + y + 16 >= 0)", - "(x,y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"}); + PresburgerSet setB = parsePresburgerSet( + {"(x,y) : (x + y - 4 >= 0, -x - y + 32 >= 0, " + "x - y - 2 >= 0, -x + y + 16 >= 0)", + "(x,y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"}); for (unsigned x = 1; x <= 25; ++x) { for (unsigned y = -6; y <= 16; ++y) { @@ -126,13 +126,13 @@ TEST(SetTest, containsPoint) { } // The PresburgerSet has only one id, x, so we supply one value. - EXPECT_TRUE(PresburgerSet(parsePoly("(x) : (x - 2*(x floordiv 2) == 0)")) - .containsPoint({0})); + EXPECT_TRUE( + PresburgerSet(parseIntegerPolyhedron("(x) : (x - 2*(x floordiv 2) == 0)")) + .containsPoint({0})); } TEST(SetTest, Union) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, + PresburgerSet set = parsePresburgerSet( {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}); // Universe union set. @@ -160,8 +160,7 @@ TEST(SetTest, Union) { } TEST(SetTest, Intersect) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, + PresburgerSet set = parsePresburgerSet( {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}); // Universe intersection set. @@ -196,48 +195,41 @@ TEST(SetTest, Intersect) { TEST(SetTest, Subtract) { // The interval [2, 8] minus the interval [10, 20]. testSubtractAtPoints( - parsePresburgerSetFromPolyStrings(1, {"(x) : (x - 2 >= 0, -x + 8 >= 0)"}), - parsePresburgerSetFromPolyStrings(1, - {"(x) : (x - 10 >= 0, -x + 20 >= 0)"}), + parsePresburgerSet({"(x) : (x - 2 >= 0, -x + 8 >= 0)"}), + parsePresburgerSet({"(x) : (x - 10 >= 0, -x + 20 >= 0)"}), {{1}, {2}, {8}, {9}, {10}, {20}, {21}}); // Universe minus [2, 8] U [10, 20] - testSubtractAtPoints(parsePresburgerSetFromPolyStrings(1, {"(x) : ()"}), - parsePresburgerSetFromPolyStrings( - 1, {"(x) : (x - 2 >= 0, -x + 8 >= 0)", - "(x) : (x - 10 >= 0, -x + 20 >= 0)"}), - {{1}, {2}, {8}, {9}, {10}, {20}, {21}}); + testSubtractAtPoints( + parsePresburgerSet({"(x) : ()"}), + parsePresburgerSet({"(x) : (x - 2 >= 0, -x + 8 >= 0)", + "(x) : (x - 10 >= 0, -x + 20 >= 0)"}), + {{1}, {2}, {8}, {9}, {10}, {20}, {21}}); // ((-infinity, 0] U [3, 4] U [6, 7]) - ([2, 3] U [5, 6]) testSubtractAtPoints( - parsePresburgerSetFromPolyStrings(1, {"(x) : (-x >= 0)", - "(x) : (x - 3 >= 0, -x + 4 >= 0)", - "(x) : (x - 6 >= 0, -x + 7 >= 0)"}), - parsePresburgerSetFromPolyStrings(1, {"(x) : (x - 2 >= 0, -x + 3 >= 0)", - "(x) : (x - 5 >= 0, -x + 6 >= 0)"}), + parsePresburgerSet({"(x) : (-x >= 0)", "(x) : (x - 3 >= 0, -x + 4 >= 0)", + "(x) : (x - 6 >= 0, -x + 7 >= 0)"}), + parsePresburgerSet({"(x) : (x - 2 >= 0, -x + 3 >= 0)", + "(x) : (x - 5 >= 0, -x + 6 >= 0)"}), {{0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}}); // Expected result is {[x, y] : x > y}, i.e., {[x, y] : x >= y + 1}. - testSubtractAtPoints( - parsePresburgerSetFromPolyStrings(2, {"(x, y) : (x - y >= 0)"}), - parsePresburgerSetFromPolyStrings(2, {"(x, y) : (x + y >= 0)"}), - {{0, 1}, {1, 1}, {1, 0}, {1, -1}, {0, -1}}); + testSubtractAtPoints(parsePresburgerSet({"(x, y) : (x - y >= 0)"}), + parsePresburgerSet({"(x, y) : (x + y >= 0)"}), + {{0, 1}, {1, 1}, {1, 0}, {1, -1}, {0, -1}}); // A rectangle with corners at (2, 2) and (10, 10), minus // a rectangle with corners at (5, -10) and (7, 100). // This splits the former rectangle into two halves, (2, 2) to (5, 10) and // (7, 2) to (10, 10). testSubtractAtPoints( - parsePresburgerSetFromPolyStrings( - 2, - { - "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)", - }), - parsePresburgerSetFromPolyStrings( - 2, - { - "(x, y) : (x - 5 >= 0, y + 10 >= 0, -x + 7 >= 0, -y + 100 >= 0)", - }), + parsePresburgerSet({ + "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)", + }), + parsePresburgerSet({ + "(x, y) : (x - 5 >= 0, y + 10 >= 0, -x + 7 >= 0, -y + 100 >= 0)", + }), {{1, 2}, {2, 2}, {4, 2}, {5, 2}, {7, 2}, {8, 2}, {11, 2}, {1, 1}, {2, 1}, {4, 1}, {5, 1}, {7, 1}, {8, 1}, {11, 1}, {1, 10}, {2, 10}, {4, 10}, {5, 10}, {7, 10}, {8, 10}, {11, 10}, @@ -248,13 +240,11 @@ TEST(SetTest, Subtract) { // This creates a hole in the middle of the former rectangle, and the // resulting set can be represented as a union of four rectangles. testSubtractAtPoints( - parsePresburgerSetFromPolyStrings( - 2, {"(x, y) : (x - 2 >= 0, y -2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"}), - parsePresburgerSetFromPolyStrings( - 2, - { - "(x, y) : (x - 5 >= 0, y - 4 >= 0, -x + 7 >= 0, -y + 8 >= 0)", - }), + parsePresburgerSet( + {"(x, y) : (x - 2 >= 0, y -2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"}), + parsePresburgerSet({ + "(x, y) : (x - 5 >= 0, y - 4 >= 0, -x + 7 >= 0, -y + 8 >= 0)", + }), {{1, 1}, {2, 2}, {10, 10}, @@ -271,9 +261,8 @@ TEST(SetTest, Subtract) { // The second set is a superset of the first one, since on the line x + y = 0, // y <= 1 is equivalent to x >= -1. So the result is empty. testSubtractAtPoints( - parsePresburgerSetFromPolyStrings(2, {"(x, y) : (x >= 0, x + y == 0)"}), - parsePresburgerSetFromPolyStrings(2, - {"(x, y) : (-y + 1 >= 0, x + y == 0)"}), + parsePresburgerSet({"(x, y) : (x >= 0, x + y == 0)"}), + parsePresburgerSet({"(x, y) : (-y + 1 >= 0, x + y == 0)"}), {{0, 0}, {1, -1}, {2, -2}, @@ -285,10 +274,9 @@ TEST(SetTest, Subtract) { {1, -1}}); // The result should be {0} U {2}. - testSubtractAtPoints( - parsePresburgerSetFromPolyStrings(1, {"(x) : (x >= 0, -x + 2 >= 0)"}), - parsePresburgerSetFromPolyStrings(1, {"(x) : (x - 1 == 0)"}), - {{-1}, {0}, {1}, {2}, {3}}); + testSubtractAtPoints(parsePresburgerSet({"(x) : (x >= 0, -x + 2 >= 0)"}), + parsePresburgerSet({"(x) : (x - 1 == 0)"}), + {{-1}, {0}, {1}, {2}, {3}}); // Sets with lots of redundant inequalities to test the redundancy heuristic. // (the heuristic is for the subtrahend, the second set which is the one being @@ -297,16 +285,14 @@ TEST(SetTest, Subtract) { // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} minus // a triangle with vertices {(2, 2), (10, 2), (10, 10)}. testSubtractAtPoints( - parsePresburgerSetFromPolyStrings( - 2, - { - "(x, y) : (x + y - 4 >= 0, -x - y + 32 >= 0, x - y - 2 >= 0, " - "-x + y + 16 >= 0)", - }), - parsePresburgerSetFromPolyStrings( - 2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, " - "-y + 10 >= 0, x + y - 2 >= 0, -x - y + 30 >= 0, x - y >= 0, " - "-x + y + 10 >= 0)"}), + parsePresburgerSet({ + "(x, y) : (x + y - 4 >= 0, -x - y + 32 >= 0, x - y - 2 >= 0, " + "-x + y + 16 >= 0)", + }), + parsePresburgerSet( + {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, " + "-y + 10 >= 0, x + y - 2 >= 0, -x - y + 30 >= 0, x - y >= 0, " + "-x + y + 10 >= 0)"}), {{1, 2}, {2, 2}, {3, 2}, {4, 2}, {1, 1}, {2, 1}, {3, 1}, {4, 1}, {2, 0}, {3, 0}, {4, 0}, {5, 0}, {10, 2}, {11, 2}, {10, 1}, {10, 10}, {10, 11}, {10, 9}, {11, 10}, {10, -6}, {11, -6}, @@ -315,16 +301,15 @@ TEST(SetTest, Subtract) { // ((-infinity, -5] U [3, 3] U [4, 4] U [5, 5]) - ([-2, -10] U [3, 4] U [6, // 7]) testSubtractAtPoints( - parsePresburgerSetFromPolyStrings( - 1, {"(x) : (-x - 5 >= 0)", "(x) : (x - 3 == 0)", "(x) : (x - 4 == 0)", - "(x) : (x - 5 == 0)"}), - parsePresburgerSetFromPolyStrings( - 1, {"(x) : (-x - 2 >= 0, x - 10 >= 0, -x >= 0, -x + 10 >= 0, " - "x - 100 >= 0, x - 50 >= 0)", - "(x) : (x - 3 >= 0, -x + 4 >= 0, x + 1 >= 0, " - "x + 7 >= 0, -x + 10 >= 0)", - "(x) : (x - 6 >= 0, -x + 7 >= 0, x + 1 >= 0, x - 3 >= 0, " - "-x + 5 >= 0)"}), + parsePresburgerSet({"(x) : (-x - 5 >= 0)", "(x) : (x - 3 == 0)", + "(x) : (x - 4 == 0)", "(x) : (x - 5 == 0)"}), + parsePresburgerSet( + {"(x) : (-x - 2 >= 0, x - 10 >= 0, -x >= 0, -x + 10 >= 0, " + "x - 100 >= 0, x - 50 >= 0)", + "(x) : (x - 3 >= 0, -x + 4 >= 0, x + 1 >= 0, " + "x + 7 >= 0, -x + 10 >= 0)", + "(x) : (x - 6 >= 0, -x + 7 >= 0, x + 1 >= 0, x - 3 >= 0, " + "-x + 5 >= 0)"}), {{-6}, {-5}, {-4}, @@ -353,21 +338,20 @@ TEST(SetTest, Complement) { PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))), {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}}); - testComplementAtPoints( - parsePresburgerSetFromPolyStrings(2, {"(x,y) : (x - 2 >= 0, y - 2 >= 0, " - "-x + 10 >= 0, -y + 10 >= 0)"}), - {{1, 1}, - {2, 1}, - {1, 2}, - {2, 2}, - {2, 3}, - {3, 2}, - {10, 10}, - {10, 11}, - {11, 10}, - {2, 10}, - {2, 11}, - {1, 10}}); + testComplementAtPoints(parsePresburgerSet({"(x,y) : (x - 2 >= 0, y - 2 >= 0, " + "-x + 10 >= 0, -y + 10 >= 0)"}), + {{1, 1}, + {2, 1}, + {1, 2}, + {2, 2}, + {2, 3}, + {3, 2}, + {10, 10}, + {10, 11}, + {11, 10}, + {2, 10}, + {2, 11}, + {1, 10}}); } TEST(SetTest, isEqual) { @@ -376,8 +360,7 @@ TEST(SetTest, isEqual) { PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))); PresburgerSet emptySet = PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))); - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, + PresburgerSet set = parsePresburgerSet( {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}); // universe != emptySet. @@ -414,10 +397,10 @@ TEST(SetTest, isEqual) { EXPECT_FALSE(set.isEqual(set.unionSet(set.complement()))); // square is one unit taller than rect. - PresburgerSet square = parsePresburgerSetFromPolyStrings( - 2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 9 >= 0)"}); - PresburgerSet rect = parsePresburgerSetFromPolyStrings( - 2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 8 >= 0)"}); + PresburgerSet square = parsePresburgerSet( + {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 9 >= 0)"}); + PresburgerSet rect = parsePresburgerSet( + {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 8 >= 0)"}); EXPECT_FALSE(square.isEqual(rect)); PresburgerSet universeRect = square.unionSet(square.complement()); PresburgerSet universeSquare = rect.unionSet(rect.complement()); @@ -439,16 +422,20 @@ void expectEmpty(const PresburgerSet &s) { EXPECT_TRUE(s.isIntegerEmpty()); } TEST(SetTest, divisions) { // evens = {x : exists q, x = 2q}. - PresburgerSet evens{parsePoly("(x) : (x - 2 * (x floordiv 2) == 0)")}; + PresburgerSet evens{ + parseIntegerPolyhedron("(x) : (x - 2 * (x floordiv 2) == 0)")}; // odds = {x : exists q, x = 2q + 1}. - PresburgerSet odds{parsePoly("(x) : (x - 2 * (x floordiv 2) - 1 == 0)")}; + PresburgerSet odds{ + parseIntegerPolyhedron("(x) : (x - 2 * (x floordiv 2) - 1 == 0)")}; // multiples3 = {x : exists q, x = 3q}. - PresburgerSet multiples3{parsePoly("(x) : (x - 3 * (x floordiv 3) == 0)")}; + PresburgerSet multiples3{ + parseIntegerPolyhedron("(x) : (x - 3 * (x floordiv 3) == 0)")}; // multiples6 = {x : exists q, x = 6q}. - PresburgerSet multiples6{parsePoly("(x) : (x - 6 * (x floordiv 6) == 0)")}; + PresburgerSet multiples6{ + parseIntegerPolyhedron("(x) : (x - 6 * (x floordiv 6) == 0)")}; // evens /\ odds = empty. expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds))); @@ -460,8 +447,8 @@ TEST(SetTest, divisions) { // even multiples of 3 = multiples of 6. expectEqual(multiples3.intersect(evens), multiples6); - PresburgerSet setA{parsePoly("(x) : (-x >= 0)")}; - PresburgerSet setB{parsePoly("(x) : (x floordiv 2 - 4 >= 0)")}; + PresburgerSet setA{parseIntegerPolyhedron("(x) : (-x >= 0)")}; + PresburgerSet setB{parseIntegerPolyhedron("(x) : (x floordiv 2 - 4 >= 0)")}; EXPECT_TRUE(setA.subtract(setB).isEqual(setA)); } @@ -470,29 +457,29 @@ void convertSuffixDimsToLocals(IntegerPolyhedron &poly, unsigned numLocals) { poly.getNumDimVars(), VarKind::Local); } -inline IntegerPolyhedron parsePolyAndMakeLocals(StringRef str, - unsigned numLocals) { - IntegerPolyhedron poly = parsePoly(str); +inline IntegerPolyhedron +parseIntegerPolyhedronAndMakeLocals(StringRef str, unsigned numLocals) { + IntegerPolyhedron poly = parseIntegerPolyhedron(str); convertSuffixDimsToLocals(poly, numLocals); return poly; } TEST(SetTest, divisionsDefByEq) { // evens = {x : exists q, x = 2q}. - PresburgerSet evens{ - parsePolyAndMakeLocals("(x, y) : (x - 2 * y == 0)", /*numLocals=*/1)}; + PresburgerSet evens{parseIntegerPolyhedronAndMakeLocals( + "(x, y) : (x - 2 * y == 0)", /*numLocals=*/1)}; // odds = {x : exists q, x = 2q + 1}. - PresburgerSet odds{ - parsePolyAndMakeLocals("(x, y) : (x - 2 * y - 1 == 0)", /*numLocals=*/1)}; + PresburgerSet odds{parseIntegerPolyhedronAndMakeLocals( + "(x, y) : (x - 2 * y - 1 == 0)", /*numLocals=*/1)}; // multiples3 = {x : exists q, x = 3q}. - PresburgerSet multiples3{ - parsePolyAndMakeLocals("(x, y) : (x - 3 * y == 0)", /*numLocals=*/1)}; + PresburgerSet multiples3{parseIntegerPolyhedronAndMakeLocals( + "(x, y) : (x - 3 * y == 0)", /*numLocals=*/1)}; // multiples6 = {x : exists q, x = 6q}. - PresburgerSet multiples6{ - parsePolyAndMakeLocals("(x, y) : (x - 6 * y == 0)", /*numLocals=*/1)}; + PresburgerSet multiples6{parseIntegerPolyhedronAndMakeLocals( + "(x, y) : (x - 6 * y == 0)", /*numLocals=*/1)}; // evens /\ odds = empty. expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds))); @@ -505,7 +492,7 @@ TEST(SetTest, divisionsDefByEq) { expectEqual(multiples3.intersect(evens), multiples6); PresburgerSet evensDefByIneq{ - parsePoly("(x) : (x - 2 * (x floordiv 2) == 0)")}; + parseIntegerPolyhedron("(x) : (x - 2 * (x floordiv 2) == 0)")}; expectEqual(evens, PresburgerSet(evensDefByIneq)); } @@ -515,36 +502,39 @@ TEST(SetTest, divisionNonDivLocals) { // // The only integer point in this is at (1000, 1000, 1000). // We project this to the xy plane. - IntegerPolyhedron tetrahedron = - parsePolyAndMakeLocals("(x, y, z) : (y >= 0, z - y >= 0, 3000*x - 2998*y " - "- 1000 - z >= 0, -1500*x + 1499*y + 1000 >= 0)", - /*numLocals=*/1); + IntegerPolyhedron tetrahedron = parseIntegerPolyhedronAndMakeLocals( + "(x, y, z) : (y >= 0, z - y >= 0, 3000*x - 2998*y " + "- 1000 - z >= 0, -1500*x + 1499*y + 1000 >= 0)", + /*numLocals=*/1); // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (1000, 1000). // The only integer point in this is at (1000, 1000). // // It also happens to be the projection of the above onto the xy plane. - IntegerPolyhedron triangle = parsePoly("(x,y) : (y >= 0, " - "3000 * x - 2999 * y - 1000 >= 0, " - "-3000 * x + 2998 * y + 2000 >= 0)"); + IntegerPolyhedron triangle = + parseIntegerPolyhedron("(x,y) : (y >= 0, 3000 * x - 2999 * y - 1000 >= " + "0, -3000 * x + 2998 * y + 2000 >= 0)"); + EXPECT_TRUE(triangle.containsPoint({1000, 1000})); EXPECT_FALSE(triangle.containsPoint({1001, 1001})); expectEqual(triangle, tetrahedron); convertSuffixDimsToLocals(triangle, 1); - IntegerPolyhedron line = parsePoly("(x) : (x - 1000 == 0)"); + IntegerPolyhedron line = parseIntegerPolyhedron("(x) : (x - 1000 == 0)"); expectEqual(line, triangle); // Triangle with vertices (0, 0), (5, 0), (15, 5). // Projected on x, it becomes [0, 13] U {15} as it becomes too narrow towards // the apex and so does not have have any integer point at x = 14. // At x = 15, the apex is an integer point. - PresburgerSet triangle2{parsePolyAndMakeLocals("(x,y) : (y >= 0, " - "x - 3*y >= 0, " - "2*y - x + 5 >= 0)", - /*numLocals=*/1)}; - PresburgerSet zeroToThirteen{parsePoly("(x) : (13 - x >= 0, x >= 0)")}; - PresburgerSet fifteen{parsePoly("(x) : (x - 15 == 0)")}; + PresburgerSet triangle2{ + parseIntegerPolyhedronAndMakeLocals("(x,y) : (y >= 0, " + "x - 3*y >= 0, " + "2*y - x + 5 >= 0)", + /*numLocals=*/1)}; + PresburgerSet zeroToThirteen{ + parseIntegerPolyhedron("(x) : (13 - x >= 0, x >= 0)")}; + PresburgerSet fifteen{parseIntegerPolyhedron("(x) : (x - 15 == 0)")}; expectEqual(triangle2.subtract(zeroToThirteen), fifteen); } @@ -572,209 +562,193 @@ TEST(SetTest, coalesceNoPoly) { } TEST(SetTest, coalesceContainedOneDim) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : (x >= 0, -x + 4 >= 0)", "(x) : (x - 1 >= 0, -x + 2 >= 0)"}); + PresburgerSet set = parsePresburgerSet( + {"(x) : (x >= 0, -x + 4 >= 0)", "(x) : (x - 1 >= 0, -x + 2 >= 0)"}); expectCoalesce(1, set); } TEST(SetTest, coalesceFirstEmpty) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ( x - 1 >= 0, -x + 2 >= 0)"}); + PresburgerSet set = parsePresburgerSet( + {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ( x - 1 >= 0, -x + 2 >= 0)"}); expectCoalesce(1, set); } TEST(SetTest, coalesceSecondEmpty) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : (x - 1 >= 0, -x + 2 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"}); + PresburgerSet set = parsePresburgerSet( + {"(x) : (x - 1 >= 0, -x + 2 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"}); expectCoalesce(1, set); } TEST(SetTest, coalesceBothEmpty) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : (x - 3 >= 0, -x - 1 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"}); + PresburgerSet set = parsePresburgerSet( + {"(x) : (x - 3 >= 0, -x - 1 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"}); expectCoalesce(0, set); } TEST(SetTest, coalesceFirstUniv) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : ()", "(x) : ( x >= 0, -x + 1 >= 0)"}); + PresburgerSet set = + parsePresburgerSet({"(x) : ()", "(x) : ( x >= 0, -x + 1 >= 0)"}); expectCoalesce(1, set); } TEST(SetTest, coalesceSecondUniv) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : ( x >= 0, -x + 1 >= 0)", "(x) : ()"}); + PresburgerSet set = + parsePresburgerSet({"(x) : ( x >= 0, -x + 1 >= 0)", "(x) : ()"}); expectCoalesce(1, set); } TEST(SetTest, coalesceBothUniv) { - PresburgerSet set = - parsePresburgerSetFromPolyStrings(1, {"(x) : ()", "(x) : ()"}); + PresburgerSet set = parsePresburgerSet({"(x) : ()", "(x) : ()"}); expectCoalesce(1, set); } TEST(SetTest, coalesceFirstUnivSecondEmpty) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : ()", "(x) : ( x >= 0, -x - 1 >= 0)"}); + PresburgerSet set = + parsePresburgerSet({"(x) : ()", "(x) : ( x >= 0, -x - 1 >= 0)"}); expectCoalesce(1, set); } TEST(SetTest, coalesceFirstEmptySecondUniv) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ()"}); + PresburgerSet set = + parsePresburgerSet({"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ()"}); expectCoalesce(1, set); } TEST(SetTest, coalesceCutOneDim) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, { - "(x) : ( x >= 0, -x + 3 >= 0)", - "(x) : ( x - 2 >= 0, -x + 4 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x) : ( x >= 0, -x + 3 >= 0)", + "(x) : ( x - 2 >= 0, -x + 4 >= 0)", + }); expectCoalesce(1, set); } TEST(SetTest, coalesceSeparateOneDim) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : ( x >= 0, -x + 2 >= 0)", "(x) : ( x - 3 >= 0, -x + 4 >= 0)"}); + PresburgerSet set = parsePresburgerSet( + {"(x) : ( x >= 0, -x + 2 >= 0)", "(x) : ( x - 3 >= 0, -x + 4 >= 0)"}); expectCoalesce(2, set); } TEST(SetTest, coalesceAdjEq) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, {"(x) : ( x == 0)", "(x) : ( x - 1 == 0)"}); + PresburgerSet set = + parsePresburgerSet({"(x) : ( x == 0)", "(x) : ( x - 1 == 0)"}); expectCoalesce(2, set); } TEST(SetTest, coalesceContainedTwoDim) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)", - "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)", + "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", + }); expectCoalesce(1, set); } TEST(SetTest, coalesceCutTwoDim) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)", - "(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)", + "(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)", + }); expectCoalesce(1, set); } TEST(SetTest, coalesceEqStickingOut) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x >= 0, -x + 2 >= 0, y >= 0, -y + 2 >= 0)", - "(x,y) : (y - 1 == 0, x >= 0, -x + 3 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x >= 0, -x + 2 >= 0, y >= 0, -y + 2 >= 0)", + "(x,y) : (y - 1 == 0, x >= 0, -x + 3 >= 0)", + }); expectCoalesce(2, set); } TEST(SetTest, coalesceSeparateTwoDim) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)", - "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)", + "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", + }); expectCoalesce(2, set); } TEST(SetTest, coalesceContainedEq) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)", - "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)", + "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", + }); expectCoalesce(1, set); } TEST(SetTest, coalesceCuttingEq) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x + 1 >= 0, -x + 1 >= 0, x - y == 0)", - "(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x + 1 >= 0, -x + 1 >= 0, x - y == 0)", + "(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)", + }); expectCoalesce(1, set); } TEST(SetTest, coalesceSeparateEq) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)", - "(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)", + "(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)", + }); expectCoalesce(2, set); } TEST(SetTest, coalesceContainedEqAsIneq) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x >= 0, -x + 3 >= 0, x - y >= 0, -x + y >= 0)", - "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x >= 0, -x + 3 >= 0, x - y >= 0, -x + y >= 0)", + "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", + }); expectCoalesce(1, set); } TEST(SetTest, coalesceContainedEqComplex) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 2, { - "(x,y) : (x - 2 == 0, x - y == 0)", - "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x,y) : (x - 2 == 0, x - y == 0)", + "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", + }); expectCoalesce(1, set); } TEST(SetTest, coalesceThreeContained) { - PresburgerSet set = - parsePresburgerSetFromPolyStrings(1, { - "(x) : (x >= 0, -x + 1 >= 0)", - "(x) : (x >= 0, -x + 2 >= 0)", - "(x) : (x >= 0, -x + 3 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x) : (x >= 0, -x + 1 >= 0)", + "(x) : (x >= 0, -x + 2 >= 0)", + "(x) : (x >= 0, -x + 3 >= 0)", + }); expectCoalesce(1, set); } TEST(SetTest, coalesceDoubleIncrement) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, { - "(x) : (x == 0)", - "(x) : (x - 2 == 0)", - "(x) : (x + 2 == 0)", - "(x) : (x - 2 >= 0, -x + 3 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x) : (x == 0)", + "(x) : (x - 2 == 0)", + "(x) : (x + 2 == 0)", + "(x) : (x - 2 >= 0, -x + 3 >= 0)", + }); expectCoalesce(3, set); } TEST(SetTest, coalesceLastCoalesced) { - PresburgerSet set = parsePresburgerSetFromPolyStrings( - 1, { - "(x) : (x == 0)", - "(x) : (x - 1 >= 0, -x + 3 >= 0)", - "(x) : (x + 2 == 0)", - "(x) : (x - 2 >= 0, -x + 4 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x) : (x == 0)", + "(x) : (x - 1 >= 0, -x + 3 >= 0)", + "(x) : (x + 2 == 0)", + "(x) : (x - 2 >= 0, -x + 4 >= 0)", + }); expectCoalesce(3, set); } TEST(SetTest, coalesceDiv) { - PresburgerSet set = - parsePresburgerSetFromPolyStrings(1, { - "(x) : (x floordiv 2 == 0)", - "(x) : (x floordiv 2 - 1 == 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x) : (x floordiv 2 == 0)", + "(x) : (x floordiv 2 - 1 == 0)", + }); expectCoalesce(2, set); } TEST(SetTest, coalesceDivOtherContained) { - PresburgerSet set = - parsePresburgerSetFromPolyStrings(1, { - "(x) : (x floordiv 2 == 0)", - "(x) : (x == 0)", - "(x) : (x >= 0, -x + 1 >= 0)", - }); + PresburgerSet set = parsePresburgerSet({ + "(x) : (x floordiv 2 == 0)", + "(x) : (x == 0)", + "(x) : (x >= 0, -x + 1 >= 0)", + }); expectCoalesce(2, set); } @@ -788,15 +762,15 @@ expectComputedVolumeIsValidOverapprox(const PresburgerSet &set, TEST(SetTest, computeVolume) { // Diamond with vertices at (0, 0), (5, 5), (5, 5), (10, 0). - PresburgerSet diamond( - parsePoly("(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0, -x + y + " - "10 >= 0)")); + PresburgerSet diamond(parseIntegerPolyhedron( + "(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0, -x + y + " + "10 >= 0)")); expectComputedVolumeIsValidOverapprox(diamond, /*trueVolume=*/61ull, /*resultBound=*/121ull); // Diamond with vertices at (-5, 0), (0, -5), (0, 5), (5, 0). - PresburgerSet shiftedDiamond(parsePoly( + PresburgerSet shiftedDiamond(parseIntegerPolyhedron( "(x, y) : (x + y + 5 >= 0, -x - y + 5 >= 0, x - y + 5 >= 0, -x + y + " "5 >= 0)")); expectComputedVolumeIsValidOverapprox(shiftedDiamond, @@ -804,7 +778,7 @@ TEST(SetTest, computeVolume) { /*resultBound=*/121ull); // Diamond with vertices at (-5, 0), (5, -10), (5, 10), (15, 0). - PresburgerSet biggerDiamond(parsePoly( + PresburgerSet biggerDiamond(parseIntegerPolyhedron( "(x, y) : (x + y + 5 >= 0, -x - y + 15 >= 0, x - y + 5 >= 0, -x + y + " "15 >= 0)")); expectComputedVolumeIsValidOverapprox(biggerDiamond, @@ -823,7 +797,8 @@ TEST(SetTest, computeVolume) { /*resultBound=*/683ull); // Unbounded polytope. - PresburgerSet unbounded(parsePoly("(x, y) : (2*x - y >= 0, y - 3*x >= 0)")); + PresburgerSet unbounded( + parseIntegerPolyhedron("(x, y) : (2*x - y >= 0, y - 3*x >= 0)")); expectComputedVolumeIsValidOverapprox(unbounded, /*trueVolume=*/{}, /*resultBound=*/{}); @@ -860,35 +835,32 @@ void testComputeRepr(IntegerPolyhedron poly, const PresburgerSet &expected, } TEST(SetTest, computeReprWithOnlyDivLocals) { - testComputeReprAtPoints(parsePoly("(x, y) : (x - 2*y == 0)"), + testComputeReprAtPoints(parseIntegerPolyhedron("(x, y) : (x - 2*y == 0)"), {{1, 0}, {2, 1}, {3, 0}, {4, 2}, {5, 3}}, /*numToProject=*/0); - testComputeReprAtPoints(parsePoly("(x, e) : (x - 2*e == 0)"), + testComputeReprAtPoints(parseIntegerPolyhedron("(x, e) : (x - 2*e == 0)"), {{1}, {2}, {3}, {4}, {5}}, /*numToProject=*/1); // Tests to check that the space is preserved. - testComputeReprAtPoints(parsePoly("(x, y)[z, w] : ()"), {}, - /*numToProject=*/1); - testComputeReprAtPoints(parsePoly("(x, y)[z, w] : (z - (w floordiv 2) == 0)"), - {}, + testComputeReprAtPoints(parseIntegerPolyhedron("(x, y)[z, w] : ()"), {}, /*numToProject=*/1); + testComputeReprAtPoints( + parseIntegerPolyhedron("(x, y)[z, w] : (z - (w floordiv 2) == 0)"), {}, + /*numToProject=*/1); // Bezout's lemma: if a, b are constants, // the set of values that ax + by can take is all multiples of gcd(a, b). - testComputeRepr( - parsePoly("(x, e, f) : (x - 15*e - 21*f == 0)"), - PresburgerSet(parsePoly({"(x) : (x - 3*(x floordiv 3) == 0)"})), - /*numToProject=*/2); + testComputeRepr(parseIntegerPolyhedron("(x, e, f) : (x - 15*e - 21*f == 0)"), + PresburgerSet(parseIntegerPolyhedron( + {"(x) : (x - 3*(x floordiv 3) == 0)"})), + /*numToProject=*/2); } TEST(SetTest, subtractOutputSizeRegression) { - PresburgerSet set1 = - parsePresburgerSetFromPolyStrings(1, {"(i) : (i >= 0, 10 - i >= 0)"}); - PresburgerSet set2 = - parsePresburgerSetFromPolyStrings(1, {"(i) : (i - 5 >= 0)"}); + PresburgerSet set1 = parsePresburgerSet({"(i) : (i >= 0, 10 - i >= 0)"}); + PresburgerSet set2 = parsePresburgerSet({"(i) : (i - 5 >= 0)"}); - PresburgerSet set3 = - parsePresburgerSetFromPolyStrings(1, {"(i) : (i >= 0, 4 - i >= 0)"}); + PresburgerSet set3 = parsePresburgerSet({"(i) : (i >= 0, 4 - i >= 0)"}); PresburgerSet result = set1.subtract(set2); diff --git a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp index f1a41e0..8ff6d75b 100644 --- a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp +++ b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp @@ -6,7 +6,8 @@ // //===----------------------------------------------------------------------===// -#include "./Utils.h" +#include "Parser.h" +#include "Utils.h" #include "mlir/Analysis/Presburger/Simplex.h" #include "mlir/IR/MLIRContext.h" @@ -527,10 +528,12 @@ TEST(SimplexTest, isRedundantEquality) { } TEST(SimplexTest, IsRationalSubsetOf) { - IntegerPolyhedron univ = parsePoly("(x) : ()"); - IntegerPolyhedron empty = parsePoly("(x) : (x + 0 >= 0, -x - 1 >= 0)"); - IntegerPolyhedron s1 = parsePoly("(x) : ( x >= 0, -x + 4 >= 0)"); - IntegerPolyhedron s2 = parsePoly("(x) : (x - 1 >= 0, -x + 3 >= 0)"); + IntegerPolyhedron univ = parseIntegerPolyhedron("(x) : ()"); + IntegerPolyhedron empty = + parseIntegerPolyhedron("(x) : (x + 0 >= 0, -x - 1 >= 0)"); + IntegerPolyhedron s1 = parseIntegerPolyhedron("(x) : ( x >= 0, -x + 4 >= 0)"); + IntegerPolyhedron s2 = + parseIntegerPolyhedron("(x) : (x - 1 >= 0, -x + 3 >= 0)"); Simplex simUniv(univ); Simplex simEmpty(empty); diff --git a/mlir/unittests/Analysis/Presburger/Utils.h b/mlir/unittests/Analysis/Presburger/Utils.h index b839b62..b100771 100644 --- a/mlir/unittests/Analysis/Presburger/Utils.h +++ b/mlir/unittests/Analysis/Presburger/Utils.h @@ -13,7 +13,6 @@ #ifndef MLIR_UNITTESTS_ANALYSIS_PRESBURGER_UTILS_H #define MLIR_UNITTESTS_ANALYSIS_PRESBURGER_UTILS_H -#include "../../Dialect/Affine/Analysis/AffineStructuresParser.h" #include "mlir/Analysis/Presburger/IntegerRelation.h" #include "mlir/Analysis/Presburger/PWMAFunction.h" #include "mlir/Analysis/Presburger/PresburgerRelation.h" @@ -26,30 +25,6 @@ namespace mlir { namespace presburger { -/// Parses a IntegerPolyhedron from a StringRef. It is expected that the -/// string represents a valid IntegerSet, otherwise it will violate a gtest -/// assertion. -inline IntegerPolyhedron parsePoly(StringRef str) { - MLIRContext context(MLIRContext::Threading::DISABLED); - FailureOr poly = parseIntegerSetToFAC(str, &context); - EXPECT_TRUE(succeeded(poly)); - return *poly; -} - -/// Parse a list of StringRefs to IntegerRelation and combine them into a -/// PresburgerSet be using the union operation. It is expected that the strings -/// are all valid IntegerSet representation and that all of them have the same -/// number of dimensions as is specified by the numDims argument. -inline PresburgerSet -parsePresburgerSetFromPolyStrings(unsigned numDims, ArrayRef strs, - unsigned numSymbols = 0) { - PresburgerSet set = PresburgerSet::getEmpty( - PresburgerSpace::getSetSpace(numDims, numSymbols)); - for (StringRef str : strs) - set.unionInPlace(parsePoly(str)); - return set; -} - inline Matrix makeMatrix(unsigned numRow, unsigned numColumns, ArrayRef> matrix) { Matrix results(numRow, numColumns); @@ -63,34 +38,6 @@ inline Matrix makeMatrix(unsigned numRow, unsigned numColumns, return results; } -/// Construct a PWMAFunction given the dimensionalities and an array describing -/// the list of pieces. Each piece is given by a string describing the domain -/// and a 2D array that represents the output. -inline PWMAFunction parsePWMAF( - unsigned numInputs, unsigned numOutputs, - ArrayRef, 8>>> - data, - unsigned numSymbols = 0) { - static MLIRContext context; - - PWMAFunction result( - PresburgerSpace::getRelationSpace(numInputs, numOutputs, numSymbols)); - for (const auto &pair : data) { - IntegerPolyhedron domain = parsePoly(pair.first); - - PresburgerSpace funcSpace = result.getSpace(); - funcSpace.insertVar(VarKind::Local, 0, domain.getNumLocalVars()); - - result.addPiece( - {PresburgerSet(domain), - MultiAffineFunction( - funcSpace, - makeMatrix(numOutputs, domain.getNumVars() + 1, pair.second), - domain.getLocalReprs())}); - } - return result; -} - /// lhs and rhs represent non-negative integers or positive infinity. The /// infinity case corresponds to when the Optional is empty. inline bool infinityOrUInt64LE(Optional lhs, Optional rhs) { diff --git a/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.h b/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.h deleted file mode 100644 index 773d2ac..0000000 --- a/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.h +++ /dev/null @@ -1,34 +0,0 @@ -//===- AffineStructuresParser.h - Parser for AffineStructures ---*- C++ -*-===// -// -// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. -// See https://llvm.org/LICENSE.txt for license information. -// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -// -//===----------------------------------------------------------------------===// -// -// This file defines helper functions to parse AffineStructures from -// StringRefs. -// -//===----------------------------------------------------------------------===// - -#ifndef MLIR_UNITTEST_ANALYSIS_AFFINESTRUCTURESPARSER_H -#define MLIR_UNITTEST_ANALYSIS_AFFINESTRUCTURESPARSER_H - -#include "mlir/Dialect/Affine/Analysis/AffineStructures.h" -#include "mlir/Support/LogicalResult.h" - -namespace mlir { - -/// This parses a single IntegerSet to an MLIR context and transforms it to -/// IntegerPolyhedron if it was valid. If not, a failure is returned. If the -/// passed `str` has additional tokens that were not part of the IntegerSet, a -/// failure is returned. Diagnostics are printed on failure if -/// `printDiagnosticInfo` is true. - -FailureOr -parseIntegerSetToFAC(llvm::StringRef, MLIRContext *context, - bool printDiagnosticInfo = true); - -} // namespace mlir - -#endif // MLIR_UNITTEST_ANALYSIS_AFFINESTRUCTURESPARSER_H diff --git a/mlir/unittests/Dialect/Affine/Analysis/CMakeLists.txt b/mlir/unittests/Dialect/Affine/Analysis/CMakeLists.txt deleted file mode 100644 index b5f81b4..0000000 --- a/mlir/unittests/Dialect/Affine/Analysis/CMakeLists.txt +++ /dev/null @@ -1,10 +0,0 @@ -add_mlir_unittest(MLIRAffineAnalysisTests - AffineStructuresParser.cpp - AffineStructuresParserTest.cpp -) - -target_link_libraries(MLIRAffineAnalysisTests - PRIVATE - MLIRAffineAnalysis - MLIRParser - ) diff --git a/mlir/unittests/Dialect/Affine/CMakeLists.txt b/mlir/unittests/Dialect/Affine/CMakeLists.txt deleted file mode 100644 index fc6ef10..0000000 --- a/mlir/unittests/Dialect/Affine/CMakeLists.txt +++ /dev/null @@ -1 +0,0 @@ -add_subdirectory(Analysis) diff --git a/mlir/unittests/Dialect/CMakeLists.txt b/mlir/unittests/Dialect/CMakeLists.txt index befbffc..522aeca 100644 --- a/mlir/unittests/Dialect/CMakeLists.txt +++ b/mlir/unittests/Dialect/CMakeLists.txt @@ -6,7 +6,6 @@ target_link_libraries(MLIRDialectTests MLIRIR MLIRDialect) -add_subdirectory(Affine) add_subdirectory(LLVMIR) add_subdirectory(MemRef) add_subdirectory(SparseTensor) -- 2.7.4