[Mlir-commits] [mlir] 8c867f7 - [MLIR][Presburger] Improve unittest parsing
llvmlistbot at llvm.org
llvmlistbot at llvm.org
Thu Sep 15 11:29:40 PDT 2022
Author: Groverkss
Date: 2022-09-15T19:28:49+01:00
New Revision: 8c867f7827f618e2a3164235ef91725199dd76f1
URL: https://github.com/llvm/llvm-project/commit/8c867f7827f618e2a3164235ef91725199dd76f1
DIFF: https://github.com/llvm/llvm-project/commit/8c867f7827f618e2a3164235ef91725199dd76f1.diff
LOG: [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
Added:
mlir/unittests/Analysis/Presburger/Parser.h
mlir/unittests/Analysis/Presburger/ParserTest.cpp
Modified:
mlir/include/mlir/AsmParser/AsmParser.h
mlir/include/mlir/Dialect/Affine/Analysis/AffineStructures.h
mlir/lib/AsmParser/AffineParser.cpp
mlir/lib/Dialect/Affine/Analysis/AffineStructures.cpp
mlir/unittests/Analysis/Presburger/CMakeLists.txt
mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp
mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
mlir/unittests/Analysis/Presburger/PWMAFunctionTest.cpp
mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
mlir/unittests/Analysis/Presburger/SimplexTest.cpp
mlir/unittests/Analysis/Presburger/Utils.h
mlir/unittests/Dialect/CMakeLists.txt
utils/bazel/llvm-project-overlay/mlir/unittests/BUILD.bazel
Removed:
mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.cpp
mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.h
mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParserTest.cpp
mlir/unittests/Dialect/Affine/Analysis/CMakeLists.txt
mlir/unittests/Dialect/Affine/CMakeLists.txt
################################################################################
diff --git a/mlir/include/mlir/AsmParser/AsmParser.h b/mlir/include/mlir/AsmParser/AsmParser.h
index 601e86dd36b50..60ce797f01589 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 3c7561ef40d72..0e78d4c4cc28c 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<SmallVector<int64_t, 8>> *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 0480ee48ec7d4..c6af9ee50db15 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=*/"<mlir_parser_buffer>",
@@ -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 9e86d1ea58c63..76e9625fd34ff 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<SmallVector<int64_t, 8>> 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 c7fc5f0c9b161..5af423295c0b6 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 82be6f02eeb58..1be5a3f04bf59 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<int64_t> 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<std::pair<StringRef, SmallVector<SmallVector<int64_t, 8>, 8>>>
- expectedLexminRepr,
+ ArrayRef<std::pair<StringRef, StringRef>> expectedLexminRepr,
ArrayRef<StringRef> 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<std::pair<StringRef, SmallVector<SmallVector<int64_t, 8>, 8>>>
- result) {
+ StringRef polyStr, ArrayRef<std::pair<StringRef, StringRef>> 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,16 +1466,18 @@ 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)");
+ IntegerPolyhedron poly3 =
+ parseIntegerPolyhedron("(x, y) : (2*x - y >= 0, y - 3*x >= 0)");
// -0 instead of 0 to prevent unwanted conversion to pointer types,
// which would lead to ambiguity in overload resolution.
diff --git a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
index 18efe55c2479a..1a9241bfe3ffc 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 <gmock/gmock.h>
@@ -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 1aff2fe80a69a..cebc7fa2ec6e6 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
diff erent 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 mul6
diff = parsePWMAF(
- /*numInputs=*/1, /*numOutputs=*/1,
- {
- {"(x) : (x - 5*(x floordiv 5) == 0)", {{0, 52, 0}}}, // 52(x/6).
- });
+ PWMAFunction mul6
diff = parsePWMAF({
+ {"(x) : (x - 5*(x floordiv 5) == 0)", "(x) -> (52 * (x floordiv 6))"},
+ });
EXPECT_FALSE(mul2AndMul3.isEqual(mul6
diff ));
- 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
diff erent 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
diff erent 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 0000000000000..e80267c5adae2
--- /dev/null
+++ b/mlir/unittests/Analysis/Presburger/Parser.h
@@ -0,0 +1,86 @@
+//===- 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<StringRef> 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<std::pair<StringRef, StringRef>> 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 0cc41a8b6afaf..4c9f54f97d246 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 <gtest/gtest.h>
@@ -38,99 +37,53 @@ static IntegerPolyhedron makeFACFromConstraints(
return fac;
}
-TEST(ParseFACTest, InvalidInputTest) {
- MLIRContext context;
- FailureOr<IntegerPolyhedron> 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<IntegerPolyhedron> 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 8e0f1c2217f28..3e4d272ca11f7 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 f1a41e0fd0fca..8ff6d75b3499a 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 b839b628173a8..b100771021814 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<IntegerPolyhedron> 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<StringRef> 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<SmallVector<int64_t, 8>> 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<std::pair<StringRef, SmallVector<SmallVector<int64_t, 8>, 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<MPInt> lhs, Optional<MPInt> rhs) {
diff --git a/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.cpp b/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.cpp
deleted file mode 100644
index 4bd15e49824a3..0000000000000
--- a/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.cpp
+++ /dev/null
@@ -1,25 +0,0 @@
-//===- AffineStructuresParser.cpp - 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
-//
-//===----------------------------------------------------------------------===//
-
-#include "./AffineStructuresParser.h"
-#include "mlir/AsmParser/AsmParser.h"
-#include "mlir/IR/IntegerSet.h"
-
-using namespace mlir;
-using namespace presburger;
-
-FailureOr<IntegerPolyhedron>
-mlir::parseIntegerSetToFAC(llvm::StringRef str, MLIRContext *context,
- bool printDiagnosticInfo) {
- IntegerSet set = parseIntegerSet(str, context, printDiagnosticInfo);
-
- if (!set)
- return failure();
-
- return FlatAffineValueConstraints(set);
-}
diff --git a/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.h b/mlir/unittests/Dialect/Affine/Analysis/AffineStructuresParser.h
deleted file mode 100644
index 773d2acaae4b8..0000000000000
--- 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<presburger::IntegerPolyhedron>
-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 b5f81b4a50287..0000000000000
--- 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 fc6ef10fab1f5..0000000000000
--- 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 befbffcf07561..522aeca29146d 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)
diff --git a/utils/bazel/llvm-project-overlay/mlir/unittests/BUILD.bazel b/utils/bazel/llvm-project-overlay/mlir/unittests/BUILD.bazel
index 91a03f2643b73..4ca24969667b9 100644
--- a/utils/bazel/llvm-project-overlay/mlir/unittests/BUILD.bazel
+++ b/utils/bazel/llvm-project-overlay/mlir/unittests/BUILD.bazel
@@ -293,7 +293,6 @@ cc_test(
"Analysis/*.h",
"Analysis/*/*.cpp",
"Analysis/*/*.h",
- "Dialect/Affine/Analysis/AffineStructuresParser.*",
]),
deps = [
"//llvm:TestingSupport",
More information about the Mlir-commits
mailing list