diff --git a/mlir/unittests/Analysis/AffineStructuresTest.cpp b/mlir/unittests/Analysis/AffineStructuresTest.cpp --- a/mlir/unittests/Analysis/AffineStructuresTest.cpp +++ b/mlir/unittests/Analysis/AffineStructuresTest.cpp @@ -119,47 +119,50 @@ checkSample(true, parseFAC("(x) : (7 * x >= 0, -7 * x + 5 >= 0)", &context)); // 1 <= 5x and 5x <= 4 (no solution). - checkSample(false, makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {})); + checkSample(false, + parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)", &context)); // 1 <= 5x and 5x <= 9 (solution: x = 1). - checkSample(true, makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {})); + checkSample(true, + parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)", &context)); // Bounded sets with equalities. // x >= 8 and 40 >= y and x = y. - checkSample( - true, makeFACFromConstraints(2, {{1, 0, -8}, {0, -1, 40}}, {{1, -1, 0}})); + checkSample(true, parseFAC("(x,y) : (x - 8 >= 0, -y + 40 >= 0, x - y == 0)", + &context)); // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z. // solution: x = y = z = 10. - checkSample(true, makeFACFromConstraints( - 3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -10}}, - {{1, 2, -3, 0}})); + checkSample(true, parseFAC("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " + "z - 10 >= 0, x + 2 * y - 3 * z == 0)", + &context)); // 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, makeFACFromConstraints( - 3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -11}}, - {{1, 2, -3, 0}})); + checkSample(false, parseFAC("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " + "z - 11 >= 0, x + 2 * y - 3 * z == 0)", + &context)); // 0 <= r and r <= 3 and 4q + r = 7. // Solution: q = 1, r = 3. - checkSample(true, - makeFACFromConstraints(2, {{0, 1, 0}, {0, -1, 3}}, {{4, 1, -7}})); + checkSample( + true, + parseFAC("(q,r) : (r >= 0, -r + 3 >= 0, 4 * q + r - 7 == 0)", &context)); // 4q + r = 7 and r = 0. // Solution: q = 1, r = 3. - checkSample(false, makeFACFromConstraints(2, {}, {{4, 1, -7}, {0, 1, 0}})); + checkSample(false, + parseFAC("(q,r) : (4 * q + r - 7 == 0, r == 0)", &context)); // 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, - makeFACFromConstraints( - 2, {{0, 1, 0}, {300000, -299999, -100000}, {-300000, 299998, 200000}}, - {})); + checkSample(true, parseFAC("(x,y) : (y >= 0, " + "300000 * x - 299999 * y - 100000 >= 0, " + "-300000 * x + 299998 * y + 200000 >= 0)", + &context)); // This is a tetrahedron with vertices at // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000). @@ -176,18 +179,13 @@ }, {}); - // Same thing with some spurious extra dimensions equated to constants. - 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. + 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)); // This is a tetrahedron with vertices at // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100). @@ -204,40 +202,25 @@ // empty. // This is a line segment from (0, 1/3) to (100, 100 + 1/3). - 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. - })); + checkSample( + false, parseFAC("(x,y) : (x >= 0, -x + 100 >= 0, 3 * x - 3 * y + 1 == 0)", + &context)); // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3. - 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. - }, - {})); + 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)); + // 2D cone with apex at (10000, 10000) and // edges passing through (1/3, 0) and (2/3, 0). - checkSample( - true, - makeFACFromConstraints( - 2, {{300000, -299999, -100000}, {-300000, 299998, 200000}}, {})); + checkSample(true, parseFAC("(x,y) : (300000 * x - 299999 * y - 100000 >= 0, " + "-300000 * x + 2999998 * y + 200000 >= 0)", + &context)); // Cartesian product of a tetrahedron and a 2D cone. // The tetrahedron has vertices at @@ -350,14 +333,9 @@ }, {}); - checkSample(true, makeFACFromConstraints(3, - { - {2, 0, 0, -1}, // 2x >= 1 - }, - {{ - {1, -1, 0, -1}, // y = x - 1 - {0, 1, -1, 0}, // z = y - }})); + checkSample(true, parseFAC("(x, y, z) : (2 * x - 1 >= 0, x - y - 1 == 0, " + "y - z == 0)", + &context)); // Regression tests for the computation of dual coefficients. checkSample(false, parseFAC("(x, y, z) : (" @@ -377,67 +355,49 @@ } TEST(FlatAffineConstraintsTest, IsIntegerEmptyTest) { + + MLIRContext context; + // 1 <= 5x and 5x <= 4 (no solution). - EXPECT_TRUE( - makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}).isIntegerEmpty()); + EXPECT_TRUE(parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)", &context) + .isIntegerEmpty()); // 1 <= 5x and 5x <= 9 (solution: x = 1). - EXPECT_FALSE( - makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}).isIntegerEmpty()); + EXPECT_FALSE(parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)", &context) + .isIntegerEmpty()); // Unbounded sets. - 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 - ) + EXPECT_TRUE(parseFAC("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, " + "2 * z - 1 >= 0, 2 * x - 1 == 0)", + &context) .isIntegerEmpty()); - 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 - }, - {}) + 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) .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()); + EXPECT_FALSE( + parseFAC("(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)", + &context) + .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( - makeFACFromConstraints( - 2, {{1, 0, 0}, {-1, 0, 10}, {0, 1, 0}, {0, -1, 10}}, {{3, 7, -1}}) - .isIntegerEmpty()); + EXPECT_TRUE(parseFAC("(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, " + "3 * x + 7 * y - 1 == 0)", + &context) + .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( - 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}}) + 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) .isIntegerEmpty()); // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100. @@ -445,36 +405,23 @@ // 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(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()); + 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()); // Set with symbols. - FlatAffineConstraints fac6 = makeFACFromConstraints(2, - { - {1, 1, 0}, - }, - { - {1, -1, 0}, - }, - 1); - EXPECT_FALSE(fac6.isIntegerEmpty()); + EXPECT_FALSE( + parseFAC("(x)[s] : (x + s >= 0, x - s == 0)", &context).isIntegerEmpty()); } TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) { - FlatAffineConstraints fac = makeFACFromConstraints(1, - { - {1, -2}, // x >= 2. - {-1, 2} // x <= 2. - }, - {{1, -2}}); // x == 2. + MLIRContext context; + + FlatAffineConstraints fac = + parseFAC("(x) : (x - 2 >= 0, -x + 2 >= 0, x - 2 == 0)", &context); fac.removeRedundantConstraints(); // Both inequalities are redundant given the equality. Both have been removed. @@ -482,12 +429,7 @@ EXPECT_EQ(fac.getNumEqualities(), 1u); FlatAffineConstraints fac2 = - makeFACFromConstraints(2, - { - {1, 0, -3}, // x >= 3. - {0, 1, -2} // y >= 2 (redundant). - }, - {{1, -1, 0}}); // x == y. + parseFAC("(x,y) : (x - 3 >= 0, y - 2 >= 0, x - y == 0)", &context); fac2.removeRedundantConstraints(); // The second inequality is redundant and should have been removed. The @@ -497,55 +439,53 @@ EXPECT_EQ(fac2.getNumEqualities(), 1u); FlatAffineConstraints fac3 = - makeFACFromConstraints(3, {}, - {{1, -1, 0, 0}, // x == y. - {1, 0, -1, 0}, // x == z. - {0, 1, -1, 0}}); // y == z. + parseFAC("(x,y,z) : (x - y == 0, x - z == 0, y - z == 0)", &context); fac3.removeRedundantConstraints(); // One of the three equalities can be removed. EXPECT_EQ(fac3.getNumInequalities(), 0u); EXPECT_EQ(fac3.getNumEqualities(), 2u); - 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}}, - {}); + 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); // The above is a large set of constraints without any redundant constraints, // as verified by the Fourier-Motzkin based removeRedundantInequalities. @@ -560,15 +500,9 @@ EXPECT_EQ(fac4.getNumInequalities(), nIneq); EXPECT_EQ(fac4.getNumEqualities(), nEq); - 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. - }, - {}); + FlatAffineConstraints fac5 = parseFAC( + "(x,y) : (128 * x + 127 >= 0, -x + 7 >= 0, -128 * x + y >= 0, y >= 0)", + &context); // [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. @@ -582,7 +516,7 @@ } TEST(FlatAffineConstraintsTest, addConstantUpperBound) { - FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {}); + FlatAffineConstraints fac(2); fac.addBound(FlatAffineConstraints::UB, 0, 1); EXPECT_EQ(fac.atIneq(0, 0), -1); EXPECT_EQ(fac.atIneq(0, 1), 0); @@ -595,7 +529,7 @@ } TEST(FlatAffineConstraintsTest, addConstantLowerBound) { - FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {}); + FlatAffineConstraints fac(2); fac.addBound(FlatAffineConstraints::LB, 0, 1); EXPECT_EQ(fac.atIneq(0, 0), 1); EXPECT_EQ(fac.atIneq(0, 1), 0); @@ -635,8 +569,9 @@ } TEST(FlatAffineConstraintsTest, computeLocalReprSimple) { - FlatAffineConstraints fac = makeFACFromConstraints(1, {}, {}); + FlatAffineConstraints fac(1); + // TODO do this with the parser fac.addLocalFloorDiv({1, 4}, 10); fac.addLocalFloorDiv({1, 0, 100}, 10); @@ -650,7 +585,7 @@ } TEST(FlatAffineConstraintsTest, computeLocalReprConstantFloorDiv) { - FlatAffineConstraints fac = makeFACFromConstraints(4, {}, {}); + FlatAffineConstraints fac(4); fac.addInequality({1, 0, 3, 1, 2}); fac.addInequality({1, 2, -8, 1, 10}); @@ -668,7 +603,7 @@ } TEST(FlatAffineConstraintsTest, computeLocalReprRecursive) { - FlatAffineConstraints fac = makeFACFromConstraints(4, {}, {}); + FlatAffineConstraints fac(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 --- a/mlir/unittests/Analysis/PresburgerSetTest.cpp +++ b/mlir/unittests/Analysis/PresburgerSetTest.cpp @@ -33,6 +33,15 @@ return *fac; } +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, @@ -91,34 +100,6 @@ } } -/// 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 @@ -132,13 +113,12 @@ } TEST(SetTest, containsPoint) { - PresburgerSet setA = - makeSetFromFACs(1, { - makeFACFromIneqs(1, {{1, -2}, // x >= 2. - {-1, 8}}), // x <= 8. - makeFACFromIneqs(1, {{1, -10}, // x >= 10. - {-1, 20}}), // x <= 20. - }); + MLIRContext context; + + PresburgerSet setA = parsePresburgerSetFromFACStrings( + 1, + {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"}, + &context); for (unsigned x = 0; x <= 21; ++x) { if ((2 <= x && x <= 8) || (10 <= x && x <= 20)) EXPECT_TRUE(setA.containsPoint({x})); @@ -148,20 +128,11 @@ // 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 = - 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. - })}); + 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); for (unsigned x = 1; x <= 25; ++x) { for (unsigned y = -6; y <= 16; ++y) { @@ -176,13 +147,13 @@ } TEST(SetTest, Union) { - PresburgerSet set = - makeSetFromFACs(1, { - makeFACFromIneqs(1, {{1, -2}, // x >= 2. - {-1, 8}}), // x <= 8. - makeFACFromIneqs(1, {{1, -10}, // x >= 10. - {-1, 20}}), // x <= 20. - }); + MLIRContext context; + + PresburgerSet set = makeSetFromFACs( + 1, { + parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context), + parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context), + }); // Universe union set. testUnionAtPoints(PresburgerSet::getUniverse(1), set, @@ -206,13 +177,13 @@ } TEST(SetTest, Intersect) { - PresburgerSet set = - makeSetFromFACs(1, { - makeFACFromIneqs(1, {{1, -2}, // x >= 2. - {-1, 8}}), // x <= 8. - makeFACFromIneqs(1, {{1, -10}, // x >= 10. - {-1, 20}}), // x <= 20. - }); + MLIRContext context; + + PresburgerSet set = makeSetFromFACs( + 1, { + parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context), + parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context), + }); // Universe intersection set. testIntersectAtPoints(PresburgerSet::getUniverse(1), set, @@ -236,67 +207,51 @@ } TEST(SetTest, Subtract) { + MLIRContext context; // The interval [2, 8] minus the interval [10, 20]. 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. + makeSetFromFACs(1, + {parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context)}), + makeSetFromFACs( + 1, {parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context)}), {{1}, {2}, {8}, {9}, {10}, {20}, {21}}); // Universe minus [2, 8] U [10, 20] testSubtractAtPoints( - 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. - }), + makeSetFromFACs(1, {parseFAC("(x) : ()", &context)}), + makeSetFromFACs( + 1, + { + parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context), + parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context), + }), {{1}, {2}, {8}, {9}, {10}, {20}, {21}}); // ((-infinity, 0] U [3, 4] U [6, 7]) - ([2, 3] U [5, 6]) testSubtractAtPoints( 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. - }), + parseFAC("(x) : (-x >= 0)", &context), + parseFAC("(x) : (x - 3 >= 0, -x + 4 >= 0)", &context), + parseFAC("(x) : (x - 6 >= 0, -x + 7 >= 0)", &context), + }), + makeSetFromFACs(1, + { + parseFAC("(x) : (x - 2 >= 0, -x + 3 >= 0)", &context), + parseFAC("(x) : (x - 5 >= 0, -x + 6 >= 0)", &context), }), - 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( - makeSetFromFACs(2, {makeFACFromIneqs(2, - { - {1, -1, 0} // x >= y. - })}), - makeSetFromFACs(2, {makeFACFromIneqs(2, - { - {1, 1, 0} // x >= -y. - })}), + makeSetFromFACs(2, + { + parseFAC("(x, y) : (x - y >= 0)", &context), + }), + makeSetFromFACs(2, + { + parseFAC("(x, y) : (x + y >= 0)", &context), + }), {{0, 1}, {1, 1}, {1, 0}, {1, -1}, {0, -1}}); // A rectangle with corners at (2, 2) and (10, 10), minus @@ -304,20 +259,18 @@ // This splits the former rectangle into two halves, (2, 2) to (5, 10) and // (7, 2) to (10, 10). testSubtractAtPoints( - 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. - })}), + makeSetFromFACs(2, + { + parseFAC("(x, y) : (x - 2 >= 0, y - 2 >= 0, " + "-x + 10 >= 0, -y + 10 >= 0)", + &context), + }), + makeSetFromFACs(2, + { + parseFAC("(x, y) : (x - 5 >= 0, y + 10 >= 0, " + "-x + 7 >= 0, -y + 100 >= 0)", + &context), + }), {{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}, @@ -328,20 +281,18 @@ // 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( - 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. - })}), + makeSetFromFACs(2, + { + parseFAC("(x, y) : (x - 2 >= 0, y -2 >= 0, " + "-x + 10 >= 0, -y + 10 >= 0)", + &context), + }), + makeSetFromFACs(2, + { + parseFAC("(x, y) : (x - 5 >= 0, y - 4 >= 0, " + "-x + 7 >= 0, -y + 8 >= 0)", + &context), + }), {{1, 1}, {2, 2}, {10, 10}, @@ -358,20 +309,15 @@ // 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( - 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. - })}), + makeSetFromFACs(2, + { + parseFAC("(x, y) : (x >= 0, x + y == 0)", &context), + }), + makeSetFromFACs( + 2, + { + parseFAC("(x, y) : (-y + 1 >= 0, x + y == 0)", &context), + }), {{0, 0}, {1, -1}, {2, -2}, @@ -386,15 +332,11 @@ testSubtractAtPoints( makeSetFromFACs(1, { - makeFACFromIneqs(1, {{1, 0}, // x >= 0. - {-1, 2}}), // x <= 2. + parseFAC("(x) : (x >= 0, -x + 2 >= 0)", &context), }), makeSetFromFACs(1, { - makeFACFromConstraints(1, {}, - { - {1, -1} // x = 1. - }), + parseFAC("(x) : (x - 1 == 0)", &context), }), {{-1}, {0}, {1}, {2}, {3}}); @@ -405,50 +347,22 @@ // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} minus // a triangle with vertices {(2, 2), (10, 2), (10, 10)}. 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}, - {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. - })}), + 2, + { + parseFAC("(x, y) : (x + y - 4 >= 0, " + "-x - y + 32 >= 0, x - y - 2 >= 0, -x + y + 16 >= 0)", + &context), + }), 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. - })}), + 2, + { + parseFAC( + "(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), + }), {{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}, @@ -459,51 +373,25 @@ testSubtractAtPoints( 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. - }), + parseFAC("(x) : (-x - 5 >= 0)", &context), + parseFAC("(x) : (x - 3 == 0)", &context), + parseFAC("(x) : (x - 4 == 0)", &context), + parseFAC("(x) : (x - 5 == 0)", &context), }), makeSetFromFACs( 1, { - 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] - }), + parseFAC( + "(x) : (-x - 2 >= 0, x - 10 >= 0, -x >= 0, -x + 10 >= 0, " + "x - 100 >= 0, x - 50 >= 0)", + &context), + parseFAC("(x) : (x - 3 >= 0, -x + 4 >= 0, x + 1 >= 0, " + "x + 7 >= 0, -x + 10 >= 0)", + &context), + parseFAC( + "(x) : (x - 6 >= 0, -x + 7 >= 0, x + 1 >= 0, x - 3 >= 0, " + "-x + 5 >= 0)", + &context), }), {{-6}, {-5}, @@ -523,6 +411,8 @@ } TEST(SetTest, Complement) { + + MLIRContext context; // Complement of universe. testComplementAtPoints( PresburgerSet::getUniverse(1), @@ -534,13 +424,12 @@ {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}}); testComplementAtPoints( - 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, + { + parseFAC("(x,y) : (x - 2 >= 0, y - 2 >= 0, " + "-x + 10 >= 0, -y + 10 >= 0)", + &context), + }), {{1, 1}, {2, 1}, {1, 2}, @@ -556,16 +445,16 @@ } TEST(SetTest, isEqual) { + + MLIRContext context; // set = [2, 8] U [10, 20]. PresburgerSet universe = PresburgerSet::getUniverse(1); PresburgerSet emptySet = PresburgerSet::getEmptySet(1); - PresburgerSet set = - makeSetFromFACs(1, { - makeFACFromIneqs(1, {{1, -2}, // x >= 2. - {-1, 8}}), // x <= 8. - makeFACFromIneqs(1, {{1, -10}, // x >= 10. - {-1, 20}}), // x <= 20. - }); + PresburgerSet set = makeSetFromFACs( + 1, { + parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context), + parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context), + }); // universe != emptySet. EXPECT_FALSE(universe.isEqual(emptySet)); @@ -601,20 +490,18 @@ EXPECT_FALSE(set.isEqual(set.unionSet(set.complement()))); // square is one unit taller than rect. - 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. - })}); + PresburgerSet square = makeSetFromFACs( + 2, { + parseFAC( + "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 9 >= 0)", + &context), + }); + PresburgerSet rect = makeSetFromFACs( + 2, { + parseFAC( + "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 8 >= 0)", + &context), + }); EXPECT_FALSE(square.isEqual(rect)); PresburgerSet universeRect = square.unionSet(square.complement()); PresburgerSet universeSquare = rect.unionSet(rect.complement()); @@ -637,16 +524,19 @@ // evens = {x : exists q, x = 2q}. PresburgerSet evens{ - makeFACFromConstraints(2, {{1, -2, 0}, {-1, 2, 1}}, {{1, -2, 0}}, 1)}; - // odds = {x : exists q, x = 2q + 1}. + parseFAC("(x) : (x - 2 * (x floordiv 2) == 0)", &context)}; + + // odds = {x : exists q, x = 2q + 1}. PresburgerSet odds{ - makeFACFromConstraints(2, {{1, -2, 0}, {-1, 2, 1}}, {{1, -2, -1}}, 1)}; - // multiples6 = {x : exists q, x = 6q}. + parseFAC("(x) : (x - 2 * (x floordiv 2) - 1 == 0)", &context)}; + + // multiples3 = {x : exists q, x = 3q}. PresburgerSet multiples3{ - makeFACFromConstraints(2, {{1, -3, 0}, {-1, 3, 2}}, {{1, -3, 0}}, 1)}; + parseFAC("(x) : (x - 3 * (x floordiv 3) == 0)", &context)}; + // multiples6 = {x : exists q, x = 6q}. PresburgerSet multiples6{ - makeFACFromConstraints(2, {{1, -6, 0}, {-1, 6, 5}}, {{1, -6, 0}}, 1)}; + parseFAC("(x) : (x - 6 * (x floordiv 6) == 0)", &context)}; // evens /\ odds = empty. expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds)));