@@ -33,16 +33,16 @@ parsePresburgerRelationFromPresburgerSet(ArrayRef<StringRef> strs,
33
33
}
34
34
35
35
TEST (PresburgerRelationTest, intersectDomainAndRange) {
36
- PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet (
37
- {// (x, y) -> (x + N, y - N)
38
- " (x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)" ,
39
- // (x, y) -> (x + y, x - y)
40
- " (x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0)" ,
41
- // (x, y) -> (x - y, y - x)}
42
- " (x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0)" },
43
- 2 );
44
-
45
36
{
37
+ PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet (
38
+ {// (x, y) -> (x + N, y - N)
39
+ " (x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)" ,
40
+ // (x, y) -> (x + y, x - y)
41
+ " (x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0)" ,
42
+ // (x, y) -> (x - y, y - x)}
43
+ " (x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0)" },
44
+ 2 );
45
+
46
46
PresburgerSet set =
47
47
parsePresburgerSet ({// (2x, x)
48
48
" (a, b)[N] : (a - 2 * b == 0)" ,
@@ -71,6 +71,15 @@ TEST(PresburgerRelationTest, intersectDomainAndRange) {
71
71
}
72
72
73
73
{
74
+ PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet (
75
+ {// (x)[N] -> (x + N, x - N)
76
+ " (x, a, b)[N] : (a - x - N == 0, b - x + N == 0)" ,
77
+ // (x)[N] -> (x, -x)
78
+ " (x, a, b)[N] : (a - x == 0, b + x == 0)" ,
79
+ // (x)[N] -> (N - x, 2 * x)}
80
+ " (x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0)" },
81
+ 1 );
82
+
74
83
PresburgerSet set =
75
84
parsePresburgerSet ({// (2x, x)
76
85
" (a, b)[N] : (a - 2 * b == 0)" ,
@@ -80,19 +89,19 @@ TEST(PresburgerRelationTest, intersectDomainAndRange) {
80
89
" (a, b)[N] : (a - N == 0, b - N == 0)" });
81
90
82
91
PresburgerRelation expectedRel = parsePresburgerRelationFromPresburgerSet (
83
- {" (x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, a - 2 * b == 0)" ,
84
- " (x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, a + b == 0)" ,
85
- " (x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, a - N == 0, b - N "
92
+ {" (x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a - 2 * b == 0)" ,
93
+ " (x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a + b == 0)" ,
94
+ " (x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a - N == 0, b - N "
86
95
" == 0)" ,
87
- " (x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, a - 2 * b == 0)" ,
88
- " (x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, a + b == 0)" ,
89
- " (x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, a - N == 0, b - N "
96
+ " (x, a, b)[N] : (a - x == 0, b + x == 0, a - 2 * b == 0)" ,
97
+ " (x, a, b)[N] : (a - x == 0, b + x == 0, a + b == 0)" ,
98
+ " (x, a, b)[N] : (a - x == 0, b + x == 0, a - N == 0, b - N "
90
99
" == 0)" ,
91
- " (x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, a - 2 * b == 0)" ,
92
- " (x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, a + b == 0)" ,
93
- " (x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, a - N == 0, b - N "
100
+ " (x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a - 2 * b == 0)" ,
101
+ " (x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a + b == 0)" ,
102
+ " (x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a - N == 0, b - N "
94
103
" == 0)" },
95
- 2 );
104
+ 1 );
96
105
97
106
PresburgerRelation computedRel = rel.intersectRange (set);
98
107
EXPECT_TRUE (computedRel.isEqual (expectedRel));
0 commit comments