[Mlir-commits] [mlir] 6963be1 - Revert "[MLIR] rewrite AffineStructures and Presburger tests to use the parser"
Mehdi Amini
llvmlistbot at llvm.org
Sun Dec 19 23:22:06 PST 2021
Author: Mehdi Amini
Date: 2021-12-20T07:20:31Z
New Revision: 6963be12761f9d78a49c6d43e7ac13862a8f7270
URL: https://github.com/llvm/llvm-project/commit/6963be12761f9d78a49c6d43e7ac13862a8f7270
DIFF: https://github.com/llvm/llvm-project/commit/6963be12761f9d78a49c6d43e7ac13862a8f7270.diff
LOG: 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<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
Added:
Modified:
mlir/unittests/Analysis/AffineStructuresTest.cpp
mlir/unittests/Analysis/PresburgerSetTest.cpp
Removed:
################################################################################
diff --git a/mlir/unittests/Analysis/AffineStructuresTest.cpp b/mlir/unittests/Analysis/AffineStructuresTest.cpp
index e51752aef25ff..d459d08a322fd 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<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});
diff --git a/mlir/unittests/Analysis/PresburgerSetTest.cpp b/mlir/unittests/Analysis/PresburgerSetTest.cpp
index c7c3c0db4f5fe..5a44b8db9d8cd 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<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(
- 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);
}
More information about the Mlir-commits
mailing list