From 6963be12761f9d78a49c6d43e7ac13862a8f7270 Mon Sep 17 00:00:00 2001 From: Mehdi Amini Date: Mon, 20 Dec 2021 07:20:31 +0000 Subject: [PATCH] Revert "[MLIR] rewrite AffineStructures and Presburger tests to use the parser" This reverts commit b0e8667b1dbdb45bdc2738e4bec1c69fe3790a27. ASAN/UBSAN bot is broken with this trace: [ RUN ] FlatAffineConstraintsTest.FindSampleTest llvm-project/mlir/include/mlir/Support/MathExtras.h:27:15: runtime error: signed integer overflow: 1229996100002 * 809999700000 cannot be represented in type 'long' #0 0x7f63ace960e4 in mlir::ceilDiv(long, long) llvm-project/mlir/include/mlir/Support/MathExtras.h:27:15 #1 0x7f63ace8587e in ceil llvm-project/mlir/include/mlir/Analysis/Presburger/Fraction.h:57:42 #2 0x7f63ace8587e in operator* llvm-project/llvm/include/llvm/ADT/STLExtras.h:347:42 #3 0x7f63ace8587e in uninitialized_copy, long *> include/c++/v1/__memory/uninitialized_algorithms.h:36:62 #4 0x7f63ace8587e in uninitialized_copy, long *> llvm-project/llvm/include/llvm/ADT/SmallVector.h:490:5 #5 0x7f63ace8587e in append, void> llvm-project/llvm/include/llvm/ADT/SmallVector.h:662:5 #6 0x7f63ace8587e in SmallVector > llvm-project/llvm/include/llvm/ADT/SmallVector.h:1204:11 #7 0x7f63ace8587e in mlir::FlatAffineConstraints::findIntegerSample() const llvm-project/mlir/lib/Analysis/AffineStructures.cpp:1171:27 #8 0x7f63ae95a84d in mlir::checkSample(bool, mlir::FlatAffineConstraints const&, mlir::TestFunction) llvm-project/mlir/unittests/Analysis/AffineStructuresTest.cpp:37:23 #9 0x7f63ae957545 in mlir::FlatAffineConstraintsTest_FindSampleTest_Test::TestBody() llvm-project/mlir/unittests/Analysis/AffineStructuresTest.cpp:222:3 --- .../Analysis/AffineStructuresTest.cpp | 336 ++++++---- mlir/unittests/Analysis/PresburgerSetTest.cpp | 607 +++++++++++------- 2 files changed, 571 insertions(+), 372 deletions(-) diff --git a/mlir/unittests/Analysis/AffineStructuresTest.cpp b/mlir/unittests/Analysis/AffineStructuresTest.cpp index e51752aef25f..d459d08a322f 100644 --- a/mlir/unittests/Analysis/AffineStructuresTest.cpp +++ b/mlir/unittests/Analysis/AffineStructuresTest.cpp @@ -119,50 +119,47 @@ TEST(FlatAffineConstraintsTest, FindSampleTest) { checkSample(true, parseFAC("(x) : (7 * x >= 0, -7 * x + 5 >= 0)", &context)); // 1 <= 5x and 5x <= 4 (no solution). - checkSample(false, - parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)", &context)); + checkSample(false, makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {})); // 1 <= 5x and 5x <= 9 (solution: x = 1). - checkSample(true, - parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)", &context)); + checkSample(true, makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {})); // Bounded sets with equalities. // x >= 8 and 40 >= y and x = y. - checkSample(true, parseFAC("(x,y) : (x - 8 >= 0, -y + 40 >= 0, x - y == 0)", - &context)); + checkSample( + true, makeFACFromConstraints(2, {{1, 0, -8}, {0, -1, 40}}, {{1, -1, 0}})); // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z. // solution: x = y = z = 10. - checkSample(true, parseFAC("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " - "z - 10 >= 0, x + 2 * y - 3 * z == 0)", - &context)); + checkSample(true, makeFACFromConstraints( + 3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -10}}, + {{1, 2, -3, 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, parseFAC("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " - "z - 11 >= 0, x + 2 * y - 3 * z == 0)", - &context)); + checkSample(false, makeFACFromConstraints( + 3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -11}}, + {{1, 2, -3, 0}})); // 0 <= r and r <= 3 and 4q + r = 7. // Solution: q = 1, r = 3. - checkSample( - true, - parseFAC("(q,r) : (r >= 0, -r + 3 >= 0, 4 * q + r - 7 == 0)", &context)); + checkSample(true, + makeFACFromConstraints(2, {{0, 1, 0}, {0, -1, 3}}, {{4, 1, -7}})); // 4q + r = 7 and r = 0. // Solution: q = 1, r = 3. - checkSample(false, - parseFAC("(q,r) : (4 * q + r - 7 == 0, r == 0)", &context)); + checkSample(false, makeFACFromConstraints(2, {}, {{4, 1, -7}, {0, 1, 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, parseFAC("(x,y) : (y >= 0, " - "300000 * x - 299999 * y - 100000 >= 0, " - "-300000 * x + 299998 * y + 200000 >= 0)", - &context)); + checkSample( + true, + makeFACFromConstraints( + 2, {{0, 1, 0}, {300000, -299999, -100000}, {-300000, 299998, 200000}}, + {})); // This is a tetrahedron with vertices at // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000). @@ -180,13 +177,17 @@ TEST(FlatAffineConstraintsTest, FindSampleTest) { {}); // Same thing with some spurious extra dimensions equated to constants. - checkSample( - true, - parseFAC("(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)", - &context)); + checkSample(true, + makeFACFromConstraints( + 5, + { + {0, 1, 0, 1, -1, 0}, + {0, -1, 1, -1, 1, 0}, + {300000, -299998, -1, -9, 21, -112000}, + {-150000, 149999, 0, -15, 47, 68000}, + }, + {{0, 0, 0, 1, -1, 0}, // p = q. + {0, 0, 0, 1, 1, -2000}})); // p + q = 20000 => p = q = 10000. // This is a tetrahedron with vertices at // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100). @@ -203,25 +204,40 @@ TEST(FlatAffineConstraintsTest, FindSampleTest) { // empty. // This is a line segment from (0, 1/3) to (100, 100 + 1/3). - checkSample( - false, parseFAC("(x,y) : (x >= 0, -x + 100 >= 0, 3 * x - 3 * y + 1 == 0)", - &context)); + checkSample(false, makeFACFromConstraints( + 2, + { + {1, 0, 0}, // x >= 0. + {-1, 0, 100} // -x + 100 >= 0, i.e., x <= 100. + }, + { + {3, -3, 1} // 3x - 3y + 1 = 0, i.e., y = x + 1/3. + })); // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3. - checkSample(false, - parseFAC("(x,y) : (x >= 0, -x + 100 >= 0, " - "3 * x - 3 * y + 2 >= 0, -3 * x + 3 * y - 1 >= 0)", - &context)); - - checkSample(true, parseFAC("(x,y) : (2 * x >= 0, -2 * x + 99 >= 0, " - "2 * y >= 0, -2 * y + 99 >= 0)", - &context)); - + checkSample(false, makeFACFromConstraints(2, + { + {1, 0, 0}, // x >= 0. + {-1, 0, 100}, // x <= 100. + {3, -3, 2}, // 3x - 3y >= -2. + {-3, 3, -1}, // 3x - 3y <= -1. + }, + {})); + + checkSample(true, makeFACFromConstraints(2, + { + {2, 0, 0}, // 2x >= 1. + {-2, 0, 99}, // 2x <= 99. + {0, 2, 0}, // 2y >= 0. + {0, -2, 99}, // 2y <= 99. + }, + {})); // 2D cone with apex at (10000, 10000) and // edges passing through (1/3, 0) and (2/3, 0). - checkSample(true, parseFAC("(x,y) : (300000 * x - 299999 * y - 100000 >= 0, " - "-300000 * x + 2999998 * y + 200000 >= 0)", - &context)); + checkSample( + true, + makeFACFromConstraints( + 2, {{300000, -299999, -100000}, {-300000, 299998, 200000}}, {})); // Cartesian product of a tetrahedron and a 2D cone. // The tetrahedron has vertices at @@ -334,9 +350,14 @@ TEST(FlatAffineConstraintsTest, FindSampleTest) { }, {}); - checkSample(true, parseFAC("(x, y, z) : (2 * x - 1 >= 0, x - y - 1 == 0, " - "y - z == 0)", - &context)); + checkSample(true, makeFACFromConstraints(3, + { + {2, 0, 0, -1}, // 2x >= 1 + }, + {{ + {1, -1, 0, -1}, // y = x - 1 + {0, 1, -1, 0}, // z = y + }})); // Regression tests for the computation of dual coefficients. checkSample(false, parseFAC("(x, y, z) : (" @@ -356,49 +377,67 @@ TEST(FlatAffineConstraintsTest, FindSampleTest) { } TEST(FlatAffineConstraintsTest, IsIntegerEmptyTest) { - - MLIRContext context; - // 1 <= 5x and 5x <= 4 (no solution). - EXPECT_TRUE(parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)", &context) - .isIntegerEmpty()); + EXPECT_TRUE( + makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}).isIntegerEmpty()); // 1 <= 5x and 5x <= 9 (solution: x = 1). - EXPECT_FALSE(parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)", &context) - .isIntegerEmpty()); + EXPECT_FALSE( + makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}).isIntegerEmpty()); // Unbounded sets. - EXPECT_TRUE(parseFAC("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, " - "2 * z - 1 >= 0, 2 * x - 1 == 0)", - &context) + EXPECT_TRUE(makeFACFromConstraints(3, + { + {0, 2, 0, -1}, // 2y >= 1 + {0, -2, 0, 1}, // 2y <= 1 + {0, 0, 2, -1}, // 2z >= 1 + }, + {{2, 0, 0, -1}} // 2x = 1 + ) .isIntegerEmpty()); - EXPECT_FALSE(parseFAC("(x,y,z) : (2 * x - 1 >= 0, -3 * x + 3 >= 0, " - "5 * z - 6 >= 0, -7 * z + 17 >= 0, 3 * y - 2 >= 0)", - &context) + EXPECT_FALSE(makeFACFromConstraints(3, + { + {2, 0, 0, -1}, // 2x >= 1 + {-3, 0, 0, 3}, // 3x <= 3 + {0, 0, 5, -6}, // 5z >= 6 + {0, 0, -7, 17}, // 7z <= 17 + {0, 3, 0, -2}, // 3y >= 2 + }, + {}) .isIntegerEmpty()); - EXPECT_FALSE( - parseFAC("(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)", - &context) - .isIntegerEmpty()); + EXPECT_FALSE(makeFACFromConstraints(3, + { + {2, 0, 0, -1}, // 2x >= 1 + }, + {{ + {1, -1, 0, -1}, // y = x - 1 + {0, 1, -1, 0}, // z = y + }}) + .isIntegerEmpty()); // FlatAffineConstraints::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(parseFAC("(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, " - "3 * x + 7 * y - 1 == 0)", - &context) - .isIntegerEmpty()); + EXPECT_TRUE( + makeFACFromConstraints( + 2, {{1, 0, 0}, {-1, 0, 10}, {0, 1, 0}, {0, -1, 10}}, {{3, 7, -1}}) + .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( - parseFAC("(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)", - &context) + makeFACFromConstraints(3, + { + {1, 0, 0, 0}, + {-1, 0, 0, 100}, + {0, 1, 0, 0}, + {0, -1, 0, 100}, + }, + {{2, -3, 0, 0}, {1, -1, 0, -1}, {1, 1, -6, -2}}) .isIntegerEmpty()); // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100. @@ -406,23 +445,36 @@ TEST(FlatAffineConstraintsTest, IsIntegerEmptyTest) { // Now y = x - 1 + 6z implies y = 2 mod 3. In fact, since y is even, we have // 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( - parseFAC( - "(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)", - &context) - .isIntegerEmpty()); + EXPECT_TRUE(makeFACFromConstraints( + 4, + { + {1, 0, 0, 0, 0}, + {-1, 0, 0, 0, 100}, + {0, 1, 0, 0, 0}, + {0, -1, 0, 0, 100}, + }, + {{2, -3, 0, 0, 0}, {1, -1, 6, 0, -1}, {1, 1, 0, -6, -2}}) + .isIntegerEmpty()); // Set with symbols. - EXPECT_FALSE( - parseFAC("(x)[s] : (x + s >= 0, x - s == 0)", &context).isIntegerEmpty()); + FlatAffineConstraints fac6 = makeFACFromConstraints(2, + { + {1, 1, 0}, + }, + { + {1, -1, 0}, + }, + 1); + EXPECT_FALSE(fac6.isIntegerEmpty()); } TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) { - MLIRContext context; - - FlatAffineConstraints fac = - parseFAC("(x) : (x - 2 >= 0, -x + 2 >= 0, x - 2 == 0)", &context); + FlatAffineConstraints fac = makeFACFromConstraints(1, + { + {1, -2}, // x >= 2. + {-1, 2} // x <= 2. + }, + {{1, -2}}); // x == 2. fac.removeRedundantConstraints(); // Both inequalities are redundant given the equality. Both have been removed. @@ -430,7 +482,12 @@ TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) { EXPECT_EQ(fac.getNumEqualities(), 1u); FlatAffineConstraints fac2 = - parseFAC("(x,y) : (x - 3 >= 0, y - 2 >= 0, x - y == 0)", &context); + makeFACFromConstraints(2, + { + {1, 0, -3}, // x >= 3. + {0, 1, -2} // y >= 2 (redundant). + }, + {{1, -1, 0}}); // x == y. fac2.removeRedundantConstraints(); // The second inequality is redundant and should have been removed. The @@ -440,53 +497,55 @@ TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) { EXPECT_EQ(fac2.getNumEqualities(), 1u); FlatAffineConstraints fac3 = - parseFAC("(x,y,z) : (x - y == 0, x - z == 0, y - z == 0)", &context); + makeFACFromConstraints(3, {}, + {{1, -1, 0, 0}, // x == y. + {1, 0, -1, 0}, // x == z. + {0, 1, -1, 0}}); // y == z. fac3.removeRedundantConstraints(); // One of the three equalities can be removed. EXPECT_EQ(fac3.getNumInequalities(), 0u); EXPECT_EQ(fac3.getNumEqualities(), 2u); - FlatAffineConstraints fac4 = - parseFAC("(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" - ")", - &context); + FlatAffineConstraints fac4 = makeFACFromConstraints( + 17, + {{0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1}, + {0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 500}, + {0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, + {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1}, + {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998}, + {0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15}, + {0, 0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, + {0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1}, + {0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998}, + {0, 0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15}, + {0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, + {0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 500}, + {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 16, 0, 0, 0, 0, 0, 15}, + {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -16, 0, 0, 0, 0, 0, 0}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -16, 0, 1, 0, 0, 0}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 998}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16, 0, -1, 0, 0, 15}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 1}, + {0, 0, 0, 0, 0, 0, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, 8, 8}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, -8, -1}, + {0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, -8, -1}, + {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0}, + {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, -10}, + {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 10}, + {0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, -13}, + {0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 13}, + {0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -10}, + {0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10}, + {1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -13}, + {-1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 13}}, + {}); // The above is a large set of constraints without any redundant constraints, // as verified by the Fourier-Motzkin based removeRedundantInequalities. @@ -501,13 +560,18 @@ TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) { EXPECT_EQ(fac4.getNumInequalities(), nIneq); EXPECT_EQ(fac4.getNumEqualities(), nEq); - FlatAffineConstraints fac5 = parseFAC( - "(x,y) : (128 * x + 127 >= 0, -x + 7 >= 0, -128 * x + y >= 0, y >= 0)", - &context); - // 128x + 127 >= 0 implies that 128x >= 0, since x has to be an integer. - // (This should be caught by GCDTightenInqualities().) - // So -128x + y >= 0 and 128x + 127 >= 0 imply y >= 0 since we have - // y >= 128x >= 0. + FlatAffineConstraints fac5 = + makeFACFromConstraints(2, + { + {128, 0, 127}, // [0]: 128x >= -127. + {-1, 0, 7}, // [1]: x <= 7. + {-128, 1, 0}, // [2]: y >= 128x. + {0, 1, 0} // [3]: y >= 0. + }, + {}); + // [0] implies that 128x >= 0, since x has to be an integer. (This should be + // caught by GCDTightenInqualities().) + // So [2] and [0] imply [3] since we have y >= 128x >= 0. fac5.removeRedundantConstraints(); EXPECT_EQ(fac5.getNumInequalities(), 3u); SmallVector redundantConstraint = {0, 1, 0}; @@ -518,7 +582,7 @@ TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) { } TEST(FlatAffineConstraintsTest, addConstantUpperBound) { - FlatAffineConstraints fac(2); + FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {}); fac.addBound(FlatAffineConstraints::UB, 0, 1); EXPECT_EQ(fac.atIneq(0, 0), -1); EXPECT_EQ(fac.atIneq(0, 1), 0); @@ -531,7 +595,7 @@ TEST(FlatAffineConstraintsTest, addConstantUpperBound) { } TEST(FlatAffineConstraintsTest, addConstantLowerBound) { - FlatAffineConstraints fac(2); + FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {}); fac.addBound(FlatAffineConstraints::LB, 0, 1); EXPECT_EQ(fac.atIneq(0, 0), 1); EXPECT_EQ(fac.atIneq(0, 1), 0); @@ -571,7 +635,7 @@ static void checkDivisionRepresentation( } TEST(FlatAffineConstraintsTest, computeLocalReprSimple) { - FlatAffineConstraints fac(1); + FlatAffineConstraints fac = makeFACFromConstraints(1, {}, {}); fac.addLocalFloorDiv({1, 4}, 10); fac.addLocalFloorDiv({1, 0, 100}, 10); @@ -586,7 +650,7 @@ TEST(FlatAffineConstraintsTest, computeLocalReprSimple) { } TEST(FlatAffineConstraintsTest, computeLocalReprConstantFloorDiv) { - FlatAffineConstraints fac(4); + FlatAffineConstraints fac = makeFACFromConstraints(4, {}, {}); fac.addInequality({1, 0, 3, 1, 2}); fac.addInequality({1, 2, -8, 1, 10}); @@ -604,7 +668,7 @@ TEST(FlatAffineConstraintsTest, computeLocalReprConstantFloorDiv) { } TEST(FlatAffineConstraintsTest, computeLocalReprRecursive) { - FlatAffineConstraints fac(4); + FlatAffineConstraints fac = makeFACFromConstraints(4, {}, {}); fac.addInequality({1, 0, 3, 1, 2}); fac.addInequality({1, 2, -8, 1, 10}); fac.addEquality({1, 2, -4, 1, 10}); diff --git a/mlir/unittests/Analysis/PresburgerSetTest.cpp b/mlir/unittests/Analysis/PresburgerSetTest.cpp index c7c3c0db4f5f..5a44b8db9d8c 100644 --- a/mlir/unittests/Analysis/PresburgerSetTest.cpp +++ b/mlir/unittests/Analysis/PresburgerSetTest.cpp @@ -33,19 +33,6 @@ static FlatAffineConstraints parseFAC(StringRef str, MLIRContext *context) { return *fac; } -/// Parse a list of StringRefs to FlatAffineConstraints 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. -static PresburgerSet parsePresburgerSetFromFACStrings(unsigned numDims, - ArrayRef strs, - MLIRContext *context) { - PresburgerSet set = PresburgerSet::getEmptySet(numDims); - for (StringRef str : strs) - set.unionFACInPlace(parseFAC(str, context)); - return set; -} - /// Compute the union of s and t, and check that each of the given points /// belongs to the union iff it belongs to at least one of s and t. static void testUnionAtPoints(PresburgerSet s, PresburgerSet t, @@ -104,6 +91,34 @@ static void testComplementAtPoints(PresburgerSet s, } } +/// Construct a FlatAffineConstraints from a set of inequality and +/// equality constraints. `numIds` is the total number of ids, of which +/// `numLocals` is the number of local ids. +static FlatAffineConstraints +makeFACFromConstraints(unsigned numIds, ArrayRef> ineqs, + ArrayRef> eqs, + unsigned numLocals = 0) { + FlatAffineConstraints fac(/*numReservedInequalities=*/ineqs.size(), + /*numReservedEqualities=*/eqs.size(), + /*numReservedCols=*/numIds + 1, + /*numDims=*/numIds - numLocals, + /*numSymbols=*/0, numLocals); + for (const SmallVector &eq : eqs) + fac.addEquality(eq); + for (const SmallVector &ineq : ineqs) + fac.addInequality(ineq); + return fac; +} + +/// Construct a FlatAffineConstraints having `numDims` dimensions from the given +/// set of inequality constraints. This is a convenience function to be used +/// when the FAC to be constructed does not have any local ids and does not have +/// equalties. +static FlatAffineConstraints +makeFACFromIneqs(unsigned numDims, ArrayRef> ineqs) { + return makeFACFromConstraints(numDims, ineqs, /*eqs=*/{}); +} + /// Construct a PresburgerSet having `numDims` dimensions and no symbols from /// the given list of FlatAffineConstraints. Each FAC in `facs` should also have /// `numDims` dimensions and no symbols, although it can have any number of @@ -117,12 +132,13 @@ static PresburgerSet makeSetFromFACs(unsigned numDims, } TEST(SetTest, containsPoint) { - MLIRContext context; - - PresburgerSet setA = parsePresburgerSetFromFACStrings( - 1, - {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}, - &context); + PresburgerSet setA = + makeSetFromFACs(1, { + makeFACFromIneqs(1, {{1, -2}, // x >= 2. + {-1, 8}}), // x <= 8. + makeFACFromIneqs(1, {{1, -10}, // x >= 10. + {-1, 20}}), // x <= 20. + }); for (unsigned x = 0; x <= 21; ++x) { if ((2 <= x && x <= 8) || (10 <= x && x <= 20)) EXPECT_TRUE(setA.containsPoint({x})); @@ -132,12 +148,20 @@ 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 = parsePresburgerSetFromFACStrings( - 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)"}, - &context); + PresburgerSet setB = + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 1, -2}, // x + y >= 4. + {-1, -1, 30}, // x + y <= 32. + {1, -1, 0}, // x - y >= 2. + {-1, 1, 10}, // x - y <= 16. + }), + makeFACFromIneqs(2, { + {1, 0, -2}, // x >= 2. + {0, 1, -2}, // y >= 2. + {-1, 0, 10}, // x <= 10. + {0, -1, 10} // y <= 10. + })}); for (unsigned x = 1; x <= 25; ++x) { for (unsigned y = -6; y <= 16; ++y) { @@ -152,12 +176,13 @@ TEST(SetTest, containsPoint) { } TEST(SetTest, Union) { - MLIRContext context; - - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, - {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}, - &context); + PresburgerSet set = + makeSetFromFACs(1, { + makeFACFromIneqs(1, {{1, -2}, // x >= 2. + {-1, 8}}), // x <= 8. + makeFACFromIneqs(1, {{1, -10}, // x >= 10. + {-1, 20}}), // x <= 20. + }); // Universe union set. testUnionAtPoints(PresburgerSet::getUniverse(1), set, @@ -181,12 +206,13 @@ TEST(SetTest, Union) { } TEST(SetTest, Intersect) { - MLIRContext context; - - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, - {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}, - &context); + PresburgerSet set = + makeSetFromFACs(1, { + makeFACFromIneqs(1, {{1, -2}, // x >= 2. + {-1, 8}}), // x <= 8. + makeFACFromIneqs(1, {{1, -10}, // x >= 10. + {-1, 20}}), // x <= 20. + }); // Universe intersection set. testIntersectAtPoints(PresburgerSet::getUniverse(1), set, @@ -210,40 +236,67 @@ TEST(SetTest, Intersect) { } TEST(SetTest, Subtract) { - MLIRContext context; // The interval [2, 8] minus the interval [10, 20]. - testSubtractAtPoints(parsePresburgerSetFromFACStrings( - 1, {"(x) : (x - 2 >= 0, -x + 8 >= 0)"}, &context), - parsePresburgerSetFromFACStrings( - 1, {"(x) : (x - 10 >= 0, -x + 20 >= 0)"}, &context), - {{1}, {2}, {8}, {9}, {10}, {20}, {21}}); + testSubtractAtPoints( + makeSetFromFACs(1, {makeFACFromIneqs(1, {{1, -2}, // x >= 2. + {-1, 8}})}), // x <= 8. + makeSetFromFACs(1, {makeFACFromIneqs(1, {{1, -10}, // x >= 10. + {-1, 20}})}), // x <= 20. + {{1}, {2}, {8}, {9}, {10}, {20}, {21}}); // Universe minus [2, 8] U [10, 20] testSubtractAtPoints( - parsePresburgerSetFromFACStrings(1, {"(x) : ()"}, &context), - parsePresburgerSetFromFACStrings(1, - {"(x) : (x - 2 >= 0, -x + 8 >= 0)", - "(x) : (x - 10 >= 0, -x + 20 >= 0)"}, - &context), + makeSetFromFACs(1, {makeFACFromIneqs(1, {})}), + makeSetFromFACs(1, + { + makeFACFromIneqs(1, {{1, -2}, // x >= 2. + {-1, 8}}), // x <= 8. + makeFACFromIneqs(1, {{1, -10}, // x >= 10. + {-1, 20}}), // x <= 20. + }), {{1}, {2}, {8}, {9}, {10}, {20}, {21}}); // ((-infinity, 0] U [3, 4] U [6, 7]) - ([2, 3] U [5, 6]) testSubtractAtPoints( - parsePresburgerSetFromFACStrings(1, - {"(x) : (-x >= 0)", - "(x) : (x - 3 >= 0, -x + 4 >= 0)", - "(x) : (x - 6 >= 0, -x + 7 >= 0)"}, - &context), - parsePresburgerSetFromFACStrings(1, - {"(x) : (x - 2 >= 0, -x + 3 >= 0)", - "(x) : (x - 5 >= 0, -x + 6 >= 0)"}, - &context), + makeSetFromFACs(1, + { + makeFACFromIneqs(1, + { + {-1, 0} // x <= 0. + }), + makeFACFromIneqs(1, + { + {1, -3}, // x >= 3. + {-1, 4} // x <= 4. + }), + makeFACFromIneqs(1, + { + {1, -6}, // x >= 6. + {-1, 7} // x <= 7. + }), + }), + makeSetFromFACs(1, {makeFACFromIneqs(1, + { + {1, -2}, // x >= 2. + {-1, 3}, // x <= 3. + }), + makeFACFromIneqs(1, + { + {1, -5}, // x >= 5. + {-1, 6} // x <= 6. + })}), {{0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}}); // Expected result is {[x, y] : x > y}, i.e., {[x, y] : x >= y + 1}. testSubtractAtPoints( - parsePresburgerSetFromFACStrings(2, {"(x, y) : (x - y >= 0)"}, &context), - parsePresburgerSetFromFACStrings(2, {"(x, y) : (x + y >= 0)"}, &context), + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, -1, 0} // x >= y. + })}), + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 1, 0} // x >= -y. + })}), {{0, 1}, {1, 1}, {1, 0}, {1, -1}, {0, -1}}); // A rectangle with corners at (2, 2) and (10, 10), minus @@ -251,18 +304,20 @@ TEST(SetTest, Subtract) { // This splits the former rectangle into two halves, (2, 2) to (5, 10) and // (7, 2) to (10, 10). testSubtractAtPoints( - parsePresburgerSetFromFACStrings( - 2, - { - "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)", - }, - &context), - parsePresburgerSetFromFACStrings( - 2, - { - "(x, y) : (x - 5 >= 0, y + 10 >= 0, -x + 7 >= 0, -y + 100 >= 0)", - }, - &context), + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 0, -2}, // x >= 2. + {0, 1, -2}, // y >= 2. + {-1, 0, 10}, // x <= 10. + {0, -1, 10} // y <= 10. + })}), + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 0, -5}, // x >= 5. + {0, 1, 10}, // y >= -10. + {-1, 0, 7}, // x <= 7. + {0, -1, 100}, // y <= 100. + })}), {{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}, @@ -273,15 +328,20 @@ 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( - parsePresburgerSetFromFACStrings( - 2, {"(x, y) : (x - 2 >= 0, y -2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"}, - &context), - parsePresburgerSetFromFACStrings( - 2, - { - "(x, y) : (x - 5 >= 0, y - 4 >= 0, -x + 7 >= 0, -y + 8 >= 0)", - }, - &context), + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 0, -2}, // x >= 2. + {0, 1, -2}, // y >= 2. + {-1, 0, 10}, // x <= 10. + {0, -1, 10} // y <= 10. + })}), + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 0, -5}, // x >= 5. + {0, 1, -4}, // y >= 4. + {-1, 0, 7}, // x <= 7. + {0, -1, 8}, // y <= 8. + })}), {{1, 1}, {2, 2}, {10, 10}, @@ -297,25 +357,45 @@ 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(parsePresburgerSetFromFACStrings( - 2, {"(x, y) : (x >= 0, x + y == 0)"}, &context), - parsePresburgerSetFromFACStrings( - 2, {"(x, y) : (-y + 1 >= 0, x + y == 0)"}, &context), - {{0, 0}, - {1, -1}, - {2, -2}, - {-1, 1}, - {-2, 2}, - {1, 1}, - {-1, -1}, - {-1, 1}, - {1, -1}}); + testSubtractAtPoints( + makeSetFromFACs(2, {makeFACFromConstraints(2, + { + {1, 0, 0} // x >= 0. + }, + { + {1, 1, 0} // x + y = 0. + })}), + makeSetFromFACs(2, {makeFACFromConstraints(2, + { + {0, -1, 1} // y <= 1. + }, + { + {1, 1, 0} // x + y = 0. + })}), + {{0, 0}, + {1, -1}, + {2, -2}, + {-1, 1}, + {-2, 2}, + {1, 1}, + {-1, -1}, + {-1, 1}, + {1, -1}}); // The result should be {0} U {2}. testSubtractAtPoints( - parsePresburgerSetFromFACStrings(1, {"(x) : (x >= 0, -x + 2 >= 0)"}, - &context), - parsePresburgerSetFromFACStrings(1, {"(x) : (x - 1 == 0)"}, &context), + makeSetFromFACs(1, + { + makeFACFromIneqs(1, {{1, 0}, // x >= 0. + {-1, 2}}), // x <= 2. + }), + makeSetFromFACs(1, + { + makeFACFromConstraints(1, {}, + { + {1, -1} // x = 1. + }), + }), {{-1}, {0}, {1}, {2}, {3}}); // Sets with lots of redundant inequalities to test the redundancy heuristic. @@ -325,19 +405,50 @@ 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( - parsePresburgerSetFromFACStrings( - 2, - { - "(x, y) : (x + y - 4 >= 0, -x - y + 32 >= 0, x - y - 2 >= 0, " - "-x + y + 16 >= 0)", - }, - &context), - parsePresburgerSetFromFACStrings( - 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)"}, - &context), + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 1, -2}, // x + y >= 4. + {-1, -1, 30}, // x + y <= 32. + {1, -1, 0}, // x - y >= 2. + {-1, 1, 10}, // x - y <= 16. + })}), + makeSetFromFACs( + 2, {makeFACFromIneqs(2, + { + {1, 0, -2}, // x >= 2. [redundant] + {0, 1, -2}, // y >= 2. + {-1, 0, 10}, // x <= 10. + {0, -1, 10}, // y <= 10. [redundant] + {1, 1, -2}, // x + y >= 2. [redundant] + {-1, -1, 30}, // x + y <= 30. [redundant] + {1, -1, 0}, // x - y >= 0. + {-1, 1, 10}, // x - y <= 10. + })}), + {{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}, + {24, 8}, {24, 7}, {17, 15}, {16, 15}}); + + testSubtractAtPoints( + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 1, -2}, // x + y >= 4. + {-1, -1, 30}, // x + y <= 32. + {1, -1, 0}, // x - y >= 2. + {-1, 1, 10}, // x - y <= 16. + })}), + makeSetFromFACs( + 2, {makeFACFromIneqs(2, + { + {1, 0, -2}, // x >= 2. [redundant] + {0, 1, -2}, // y >= 2. + {-1, 0, 10}, // x <= 10. + {0, -1, 10}, // y <= 10. [redundant] + {1, 1, -2}, // x + y >= 2. [redundant] + {-1, -1, 30}, // x + y <= 30. [redundant] + {1, -1, 0}, // x - y >= 0. + {-1, 1, 10}, // x - y <= 10. + })}), {{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}, @@ -346,20 +457,54 @@ TEST(SetTest, Subtract) { // ((-infinity, -5] U [3, 3] U [4, 4] U [5, 5]) - ([-2, -10] U [3, 4] U [6, // 7]) testSubtractAtPoints( - parsePresburgerSetFromFACStrings( - 1, - {"(x) : (-x - 5 >= 0)", "(x) : (x - 3 == 0)", "(x) : (x - 4 == 0)", - "(x) : (x - 5 == 0)"}, - &context), - parsePresburgerSetFromFACStrings( + makeSetFromFACs(1, + { + makeFACFromIneqs(1, + { + {-1, -5}, // x <= -5. + }), + makeFACFromConstraints(1, {}, + { + {1, -3} // x = 3. + }), + makeFACFromConstraints(1, {}, + { + {1, -4} // x = 4. + }), + makeFACFromConstraints(1, {}, + { + {1, -5} // x = 5. + }), + }), + makeSetFromFACs( 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)"}, - &context), + { + makeFACFromIneqs(1, + { + {-1, -2}, // x <= -2. + {1, -10}, // x >= -10. + {-1, 0}, // x <= 0. [redundant] + {-1, 10}, // x <= 10. [redundant] + {1, -100}, // x >= -100. [redundant] + {1, -50} // x >= -50. [redundant] + }), + makeFACFromIneqs(1, + { + {1, -3}, // x >= 3. + {-1, 4}, // x <= 4. + {1, 1}, // x >= -1. [redundant] + {1, 7}, // x >= -7. [redundant] + {-1, 10} // x <= 10. [redundant] + }), + makeFACFromIneqs(1, + { + {1, -6}, // x >= 6. + {-1, 7}, // x <= 7. + {1, 1}, // x >= -1. [redundant] + {1, -3}, // x >= -3. [redundant] + {-1, 5} // x <= 5. [redundant] + }), + }), {{-6}, {-5}, {-4}, @@ -378,8 +523,6 @@ TEST(SetTest, Subtract) { } TEST(SetTest, Complement) { - - MLIRContext context; // Complement of universe. testComplementAtPoints( PresburgerSet::getUniverse(1), @@ -391,10 +534,13 @@ TEST(SetTest, Complement) { {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}}); testComplementAtPoints( - parsePresburgerSetFromFACStrings(2, - {"(x,y) : (x - 2 >= 0, y - 2 >= 0, " - "-x + 10 >= 0, -y + 10 >= 0)"}, - &context), + makeSetFromFACs(2, {makeFACFromIneqs(2, + { + {1, 0, -2}, // x >= 2. + {0, 1, -2}, // y >= 2. + {-1, 0, 10}, // x <= 10. + {0, -1, 10} // y <= 10. + })}), {{1, 1}, {2, 1}, {1, 2}, @@ -410,15 +556,16 @@ TEST(SetTest, Complement) { } TEST(SetTest, isEqual) { - - MLIRContext context; // set = [2, 8] U [10, 20]. PresburgerSet universe = PresburgerSet::getUniverse(1); PresburgerSet emptySet = PresburgerSet::getEmptySet(1); - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, - {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}, - &context); + PresburgerSet set = + makeSetFromFACs(1, { + makeFACFromIneqs(1, {{1, -2}, // x >= 2. + {-1, 8}}), // x <= 8. + makeFACFromIneqs(1, {{1, -10}, // x >= 10. + {-1, 20}}), // x <= 20. + }); // universe != emptySet. EXPECT_FALSE(universe.isEqual(emptySet)); @@ -454,12 +601,20 @@ TEST(SetTest, isEqual) { EXPECT_FALSE(set.isEqual(set.unionSet(set.complement()))); // square is one unit taller than rect. - PresburgerSet square = parsePresburgerSetFromFACStrings( - 2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 9 >= 0)"}, - &context); - PresburgerSet rect = parsePresburgerSetFromFACStrings( - 2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 8 >= 0)"}, - &context); + PresburgerSet square = + makeSetFromFACs(2, {makeFACFromIneqs(2, { + {1, 0, -2}, // x >= 2. + {0, 1, -2}, // y >= 2. + {-1, 0, 9}, // x <= 9. + {0, -1, 9} // y <= 9. + })}); + PresburgerSet rect = + makeSetFromFACs(2, {makeFACFromIneqs(2, { + {1, 0, -2}, // x >= 2. + {0, 1, -2}, // y >= 2. + {-1, 0, 9}, // x <= 9. + {0, -1, 8} // y <= 8. + })}); EXPECT_FALSE(square.isEqual(rect)); PresburgerSet universeRect = square.unionSet(square.complement()); PresburgerSet universeSquare = rect.unionSet(rect.complement()); @@ -477,22 +632,21 @@ void expectEmpty(PresburgerSet s) { EXPECT_TRUE(s.isIntegerEmpty()); } TEST(SetTest, divisions) { MLIRContext context; + // Note: we currently need to add the equalities as inequalities to the FAC + // since detecting divisions based on equalities is not yet supported. // evens = {x : exists q, x = 2q}. PresburgerSet evens{ - parseFAC("(x) : (x - 2 * (x floordiv 2) == 0)", &context)}; - - // odds = {x : exists q, x = 2q + 1}. + makeFACFromConstraints(2, {{1, -2, 0}, {-1, 2, 1}}, {{1, -2, 0}}, 1)}; + // odds = {x : exists q, x = 2q + 1}. PresburgerSet odds{ - parseFAC("(x) : (x - 2 * (x floordiv 2) - 1 == 0)", &context)}; - - // multiples3 = {x : exists q, x = 3q}. + makeFACFromConstraints(2, {{1, -2, 0}, {-1, 2, 1}}, {{1, -2, -1}}, 1)}; + // multiples6 = {x : exists q, x = 6q}. PresburgerSet multiples3{ - parseFAC("(x) : (x - 3 * (x floordiv 3) == 0)", &context)}; - + makeFACFromConstraints(2, {{1, -3, 0}, {-1, 3, 2}}, {{1, -3, 0}}, 1)}; // multiples6 = {x : exists q, x = 6q}. PresburgerSet multiples6{ - parseFAC("(x) : (x - 6 * (x floordiv 6) == 0)", &context)}; + makeFACFromConstraints(2, {{1, -6, 0}, {-1, 6, 5}}, {{1, -6, 0}}, 1)}; // evens /\ odds = empty. expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds))); @@ -503,8 +657,10 @@ TEST(SetTest, divisions) { // even multiples of 3 = multiples of 6. expectEqual(multiples3.intersect(evens), multiples6); - PresburgerSet setA{parseFAC("(x) : (-x >= 0)", &context)}; - PresburgerSet setB{parseFAC("(x) : (x floordiv 2 - 4 >= 0)", &context)}; + PresburgerSet setA = + makeSetFromFACs(1, {parseFAC("(x) : (-x >= 0)", &context)}); + PresburgerSet setB = + makeSetFromFACs(1, {parseFAC("(x) : (x floordiv 2 - 4 >= 0)", &context)}); EXPECT_TRUE(setA.subtract(setB).isEqual(setA)); } @@ -524,184 +680,163 @@ TEST(SetTest, coalesceNoFAC) { TEST(SetTest, coalesceContainedOneDim) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : (x >= 0, -x + 4 >= 0)", "(x) : (x - 1 >= 0, -x + 2 >= 0)"}, - &context); + PresburgerSet set = makeSetFromFACs( + 1, {parseFAC("(x) : (x >= 0, -x + 4 >= 0)", &context), + parseFAC("(x) : (x - 1 >= 0, -x + 2 >= 0)", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceFirstEmpty) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ( x - 1 >= 0, -x + 2 >= 0)"}, - &context); + PresburgerSet set = makeSetFromFACs( + 1, { + parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context), + parseFAC("(x) : ( x - 1 >= 0, -x + 2 >= 0)", &context), + }); expectCoalesce(1, set); } TEST(SetTest, coalesceSecondEmpty) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : (x - 1 >= 0, -x + 2 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"}, - &context); + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : (x - 1 >= 0, -x + 2 >= 0)", &context), + parseFAC("(x) : (x >= 0, -x - 1 >= 0)", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceBothEmpty) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : (x - 3 >= 0, -x - 1 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"}, - &context); + PresburgerSet set = makeSetFromFACs( + 1, { + parseFAC("(x) : (x - 3 >= 0, -x - 1 >= 0)", &context), + parseFAC("(x) : (x >= 0, -x - 1 >= 0)", &context), + }); expectCoalesce(0, set); } TEST(SetTest, coalesceFirstUniv) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : ()", "(x) : ( x >= 0, -x + 1 >= 0)"}, &context); + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : ()", &context), + parseFAC("(x) : ( x >= 0, -x + 1 >= 0)", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceSecondUniv) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : ( x >= 0, -x + 1 >= 0)", "(x) : ()"}, &context); + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : ( x >= 0, -x + 1 >= 0)", &context), + parseFAC("(x) : ()", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceBothUniv) { MLIRContext context; - PresburgerSet set = - parsePresburgerSetFromFACStrings(1, {"(x) : ()", "(x) : ()"}, &context); + PresburgerSet set = makeSetFromFACs( + 1, {parseFAC("(x) : ()", &context), parseFAC("(x) : ()", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceFirstUnivSecondEmpty) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : ()", "(x) : ( x >= 0, -x - 1 >= 0)"}, &context); + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : ()", &context), + parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceFirstEmptySecondUniv) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ()"}, &context); + PresburgerSet set = + makeSetFromFACs(1, {parseFAC("(x) : ( x >= 0, -x - 1 >= 0)", &context), + parseFAC("(x) : ()", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceCutOneDim) { MLIRContext context; - PresburgerSet set = - parsePresburgerSetFromFACStrings(1, - { - "(x) : ( x >= 0, -x + 3 >= 0)", - "(x) : ( x - 2 >= 0, -x + 4 >= 0)", - }, - &context); + PresburgerSet set = makeSetFromFACs( + 1, {parseFAC("(x) : ( x >= 0, -x + 3 >= 0)", &context), + parseFAC("(x) : ( x - 2 >= 0, -x + 4 >= 0)", &context)}); expectCoalesce(2, set); } TEST(SetTest, coalesceSeparateOneDim) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 1, {"(x) : ( x >= 0, -x + 2 >= 0)", "(x) : ( x - 3 >= 0, -x + 4 >= 0)"}, - &context); + PresburgerSet set = makeSetFromFACs( + 1, {parseFAC("(x) : ( x >= 0, -x + 2 >= 0)", &context), + parseFAC("(x) : ( x - 3 >= 0, -x + 4 >= 0)", &context)}); expectCoalesce(2, set); } TEST(SetTest, coalesceContainedTwoDim) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = makeSetFromFACs( 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)", - }, - &context); + {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", + &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceCutTwoDim) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = makeSetFromFACs( 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)", - }, - &context); + {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)", + &context)}); expectCoalesce(2, set); } TEST(SetTest, coalesceSeparateTwoDim) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = makeSetFromFACs( 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)", - }, - &context); + {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", + &context)}); expectCoalesce(2, set); } TEST(SetTest, coalesceContainedEq) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 2, - { - "(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)", - "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", - }, - &context); + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)", &context), + parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceCuttingEq) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 2, - { - "(x,y) : (x - 1 >= 0, -x + 3 >= 0, x - y == 0)", - "(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)", - }, - &context); + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x - 1 >= 0, -x + 3 >= 0, x - y == 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)", &context)}); expectCoalesce(2, set); } TEST(SetTest, coalesceSeparateEq) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 2, - { - "(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)", - "(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)", - }, - &context); + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)", &context), + parseFAC("(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)", &context)}); expectCoalesce(2, set); } TEST(SetTest, coalesceContainedEqAsIneq) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 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)", - }, - &context); + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x >= 0, -x + 3 >= 0, x - y >= 0, -x + y >= 0)", + &context), + parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)}); expectCoalesce(1, set); } TEST(SetTest, coalesceContainedEqComplex) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( - 2, - { - "(x,y) : (x - 2 == 0, x - y == 0)", - "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", - }, - &context); + PresburgerSet set = makeSetFromFACs( + 2, {parseFAC("(x,y) : (x - 2 == 0, x - y == 0)", &context), + parseFAC("(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", &context)}); expectCoalesce(1, set); }