forked from OSchip/llvm-project
Revert "[MLIR] rewrite AffineStructures and Presburger tests to use the parser"
This reverts commit b0e8667b1d.
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<llvm::mapped_iterator<mlir::Fraction *, long (*)(mlir::Fraction), long>, long *> include/c++/v1/__memory/uninitialized_algorithms.h:36:62
#4 0x7f63ace8587e in uninitialized_copy<llvm::mapped_iterator<mlir::Fraction *, long (*)(mlir::Fraction), long>, long *> llvm-project/llvm/include/llvm/ADT/SmallVector.h:490:5
#5 0x7f63ace8587e in append<llvm::mapped_iterator<mlir::Fraction *, long (*)(mlir::Fraction), long>, void> llvm-project/llvm/include/llvm/ADT/SmallVector.h:662:5
#6 0x7f63ace8587e in SmallVector<llvm::mapped_iterator<mlir::Fraction *, long (*)(mlir::Fraction), long> > 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
This commit is contained in:
Mehdi Amini
parent
7f9e9c7fc3
commit
6963be1276
|
|
@ -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<int64_t, 8> 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});
|
||||
|
|
|
|||
|
|
@ -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<StringRef> 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<SmallVector<int64_t, 4>> ineqs,
|
||||
ArrayRef<SmallVector<int64_t, 4>> eqs,
|
||||
unsigned numLocals = 0) {
|
||||
FlatAffineConstraints fac(/*numReservedInequalities=*/ineqs.size(),
|
||||
/*numReservedEqualities=*/eqs.size(),
|
||||
/*numReservedCols=*/numIds + 1,
|
||||
/*numDims=*/numIds - numLocals,
|
||||
/*numSymbols=*/0, numLocals);
|
||||
for (const SmallVector<int64_t, 4> &eq : eqs)
|
||||
fac.addEquality(eq);
|
||||
for (const SmallVector<int64_t, 4> &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<SmallVector<int64_t, 4>> 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(
|
||||
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 - 5 >= 0)", "(x) : (x - 3 == 0)", "(x) : (x - 4 == 0)",
|
||||
"(x) : (x - 5 == 0)"},
|
||||
&context),
|
||||
parsePresburgerSetFromFACStrings(
|
||||
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);
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue