1 //===- IntegerRelationTest.cpp - Tests for IntegerRelation class ----------===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8
9 #include "mlir/Analysis/Presburger/IntegerRelation.h"
10 #include "Parser.h"
11 #include "mlir/Analysis/Presburger/PresburgerSpace.h"
12 #include "mlir/Analysis/Presburger/Simplex.h"
13
14 #include <gmock/gmock.h>
15 #include <gtest/gtest.h>
16
17 using namespace mlir;
18 using namespace presburger;
19
TEST(IntegerRelationTest,getDomainAndRangeSet)20 TEST(IntegerRelationTest, getDomainAndRangeSet) {
21 IntegerRelation rel = parseRelationFromSet(
22 "(x, xr)[N] : (xr - x - 10 == 0, xr >= 0, N - xr >= 0)", 1);
23
24 IntegerPolyhedron domainSet = rel.getDomainSet();
25
26 IntegerPolyhedron expectedDomainSet =
27 parseIntegerPolyhedron("(x)[N] : (x + 10 >= 0, N - x - 10 >= 0)");
28
29 EXPECT_TRUE(domainSet.isEqual(expectedDomainSet));
30
31 IntegerPolyhedron rangeSet = rel.getRangeSet();
32
33 IntegerPolyhedron expectedRangeSet =
34 parseIntegerPolyhedron("(x)[N] : (x >= 0, N - x >= 0)");
35
36 EXPECT_TRUE(rangeSet.isEqual(expectedRangeSet));
37 }
38
TEST(IntegerRelationTest,inverse)39 TEST(IntegerRelationTest, inverse) {
40 IntegerRelation rel =
41 parseRelationFromSet("(x, y, z)[N, M] : (z - x - y == 0, x >= 0, N - x "
42 ">= 0, y >= 0, M - y >= 0)",
43 2);
44
45 IntegerRelation inverseRel =
46 parseRelationFromSet("(z, x, y)[N, M] : (x >= 0, N - x >= 0, y >= 0, M "
47 "- y >= 0, x + y - z == 0)",
48 1);
49
50 rel.inverse();
51
52 EXPECT_TRUE(rel.isEqual(inverseRel));
53 }
54
TEST(IntegerRelationTest,intersectDomainAndRange)55 TEST(IntegerRelationTest, intersectDomainAndRange) {
56 IntegerRelation rel = parseRelationFromSet(
57 "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
58 ">= 0, x + y + z floordiv 7 == 0)",
59 1);
60
61 {
62 IntegerPolyhedron poly =
63 parseIntegerPolyhedron("(x)[N, M] : (x >= 0, M - x - 1 >= 0)");
64
65 IntegerRelation expectedRel = parseRelationFromSet(
66 "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
67 ">= 0, x + y + z floordiv 7 == 0, x >= 0, M - x - 1 >= 0)",
68 1);
69
70 IntegerRelation copyRel = rel;
71 copyRel.intersectDomain(poly);
72 EXPECT_TRUE(copyRel.isEqual(expectedRel));
73 }
74
75 {
76 IntegerPolyhedron poly = parseIntegerPolyhedron(
77 "(y, z)[N, M] : (y >= 0, M - y - 1 >= 0, y + z == 0)");
78
79 IntegerRelation expectedRel = parseRelationFromSet(
80 "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
81 ">= 0, x + y + z floordiv 7 == 0, y >= 0, M - y - 1 >= 0, y + z == 0)",
82 1);
83
84 IntegerRelation copyRel = rel;
85 copyRel.intersectRange(poly);
86 EXPECT_TRUE(copyRel.isEqual(expectedRel));
87 }
88 }
89
TEST(IntegerRelationTest,applyDomainAndRange)90 TEST(IntegerRelationTest, applyDomainAndRange) {
91
92 {
93 IntegerRelation map1 = parseRelationFromSet(
94 "(x, y, a, b)[N] : (a - x - N == 0, b - y + N == 0)", 2);
95 IntegerRelation map2 =
96 parseRelationFromSet("(x, y, a)[N] : (a - x - y == 0)", 2);
97
98 map1.applyRange(map2);
99
100 IntegerRelation map3 =
101 parseRelationFromSet("(x, y, a)[N] : (a - x - y == 0)", 2);
102
103 EXPECT_TRUE(map1.isEqual(map3));
104 }
105
106 {
107 IntegerRelation map1 = parseRelationFromSet(
108 "(x, y, a, b)[N] : (a - x + N == 0, b - y - N == 0)", 2);
109 IntegerRelation map2 =
110 parseRelationFromSet("(x, y, a, b)[N] : (a - N == 0, b - N == 0)", 2);
111
112 IntegerRelation map3 =
113 parseRelationFromSet("(x, y, a, b)[N] : (x - N == 0, y - N == 0)", 2);
114
115 map1.applyDomain(map2);
116
117 EXPECT_TRUE(map1.isEqual(map3));
118 }
119 }
120
TEST(IntegerRelationTest,symbolicLexmin)121 TEST(IntegerRelationTest, symbolicLexmin) {
122 SymbolicLexOpt lexmin =
123 parseRelationFromSet("(a, x)[b] : (x - a >= 0, x - b >= 0)", 1)
124 .findSymbolicIntegerLexMin();
125
126 PWMAFunction expectedLexmin = parsePWMAF({
127 {"(a)[b] : (a - b >= 0)", "(a)[b] -> (a)"}, // a
128 {"(a)[b] : (b - a - 1 >= 0)", "(a)[b] -> (b)"}, // b
129 });
130 EXPECT_TRUE(lexmin.unboundedDomain.isIntegerEmpty());
131 EXPECT_TRUE(lexmin.lexopt.isEqual(expectedLexmin));
132 }
133
TEST(IntegerRelationTest,symbolicLexmax)134 TEST(IntegerRelationTest, symbolicLexmax) {
135 SymbolicLexOpt lexmax1 =
136 parseRelationFromSet("(a, x)[b] : (a - x >= 0, b - x >= 0)", 1)
137 .findSymbolicIntegerLexMax();
138
139 PWMAFunction expectedLexmax1 = parsePWMAF({
140 {"(a)[b] : (a - b >= 0)", "(a)[b] -> (b)"},
141 {"(a)[b] : (b - a - 1 >= 0)", "(a)[b] -> (a)"},
142 });
143
144 SymbolicLexOpt lexmax2 =
145 parseRelationFromSet("(i, j)[N] : (i >= 0, j >= 0, N - i - j >= 0)", 1)
146 .findSymbolicIntegerLexMax();
147
148 PWMAFunction expectedLexmax2 = parsePWMAF({
149 {"(i)[N] : (i >= 0, N - i >= 0)", "(i)[N] -> (N - i)"},
150 });
151
152 SymbolicLexOpt lexmax3 =
153 parseRelationFromSet("(x, y)[N] : (x >= 0, 2 * N - x >= 0, y >= 0, x - y "
154 "+ 2 * N >= 0, 4 * N - x - y >= 0)",
155 1)
156 .findSymbolicIntegerLexMax();
157
158 PWMAFunction expectedLexmax3 =
159 parsePWMAF({{"(x)[N] : (x >= 0, 2 * N - x >= 0, x - N - 1 >= 0)",
160 "(x)[N] -> (4 * N - x)"},
161 {"(x)[N] : (x >= 0, 2 * N - x >= 0, -x + N >= 0)",
162 "(x)[N] -> (x + 2 * N)"}});
163
164 EXPECT_TRUE(lexmax1.unboundedDomain.isIntegerEmpty());
165 EXPECT_TRUE(lexmax1.lexopt.isEqual(expectedLexmax1));
166 EXPECT_TRUE(lexmax2.unboundedDomain.isIntegerEmpty());
167 EXPECT_TRUE(lexmax2.lexopt.isEqual(expectedLexmax2));
168 EXPECT_TRUE(lexmax3.unboundedDomain.isIntegerEmpty());
169 EXPECT_TRUE(lexmax3.lexopt.isEqual(expectedLexmax3));
170 }
171
TEST(IntegerRelationTest,swapVar)172 TEST(IntegerRelationTest, swapVar) {
173 PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 2, 0);
174
175 int identifiers[6] = {0, 1, 2, 3, 4};
176
177 // Attach identifiers to domain identifiers.
178 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
179 space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
180
181 // Attach identifiers to range identifiers.
182 space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
183
184 // Attach identifiers to symbol identifiers.
185 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
186 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
187
188 IntegerRelation rel =
189 parseRelationFromSet("(x, y, z)[N, M] : (z - x - y == 0, x >= 0, N - x "
190 ">= 0, y >= 0, M - y >= 0)",
191 2);
192 rel.setSpace(space);
193 // Swap (Domain 0, Range 0)
194 rel.swapVar(0, 2);
195 // Swap (Domain 1, Symbol 1)
196 rel.swapVar(1, 4);
197
198 PresburgerSpace swappedSpace = rel.getSpace();
199
200 EXPECT_TRUE(swappedSpace.getId(VarKind::Domain, 0)
201 .isEqual(space.getId(VarKind::Range, 0)));
202 EXPECT_TRUE(swappedSpace.getId(VarKind::Domain, 1)
203 .isEqual(space.getId(VarKind::Symbol, 1)));
204 EXPECT_TRUE(swappedSpace.getId(VarKind::Range, 0)
205 .isEqual(space.getId(VarKind::Domain, 0)));
206 EXPECT_TRUE(swappedSpace.getId(VarKind::Symbol, 1)
207 .isEqual(space.getId(VarKind::Domain, 1)));
208 }
209
TEST(IntegerRelationTest,mergeAndAlignSymbols)210 TEST(IntegerRelationTest, mergeAndAlignSymbols) {
211 IntegerRelation rel =
212 parseRelationFromSet("(x, y, z, a, b, c)[N, Q] : (a - x - y == 0, "
213 "x >= 0, N - b >= 0, y >= 0, Q - y >= 0)",
214 3);
215 IntegerRelation otherRel = parseRelationFromSet(
216 "(x, y, z, a, b)[N, M, P] : (z - x - y == 0, x >= 0, N - x "
217 ">= 0, y >= 0, M - y >= 0, 2 * P - 3 * a + 2 * b == 0)",
218 3);
219 PresburgerSpace space = PresburgerSpace::getRelationSpace(3, 3, 2, 0);
220
221 PresburgerSpace otherSpace = PresburgerSpace::getRelationSpace(3, 2, 3, 0);
222
223 // Attach identifiers.
224 int identifiers[7] = {0, 1, 2, 3, 4, 5, 6};
225 int otherIdentifiers[8] = {10, 11, 12, 13, 14, 15, 16, 17};
226
227 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
228 space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
229 // Note the common identifier.
230 space.setId(VarKind::Domain, 2, Identifier(&otherIdentifiers[2]));
231 space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
232 space.setId(VarKind::Range, 1, Identifier(&identifiers[3]));
233 space.setId(VarKind::Range, 2, Identifier(&identifiers[4]));
234 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[5]));
235 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[6]));
236
237 otherSpace.setId(VarKind::Domain, 0, Identifier(&otherIdentifiers[0]));
238 otherSpace.setId(VarKind::Domain, 1, Identifier(&otherIdentifiers[1]));
239 otherSpace.setId(VarKind::Domain, 2, Identifier(&otherIdentifiers[2]));
240 otherSpace.setId(VarKind::Range, 0, Identifier(&otherIdentifiers[3]));
241 otherSpace.setId(VarKind::Range, 1, Identifier(&otherIdentifiers[4]));
242 // Note the common identifier.
243 otherSpace.setId(VarKind::Symbol, 0, Identifier(&identifiers[6]));
244 otherSpace.setId(VarKind::Symbol, 1, Identifier(&otherIdentifiers[5]));
245 otherSpace.setId(VarKind::Symbol, 2, Identifier(&otherIdentifiers[7]));
246
247 rel.setSpace(space);
248 otherRel.setSpace(otherSpace);
249 rel.mergeAndAlignSymbols(otherRel);
250
251 space = rel.getSpace();
252 otherSpace = otherRel.getSpace();
253
254 // Check if merge and align is successful.
255 // Check symbol var identifiers.
256 EXPECT_EQ(4u, space.getNumSymbolVars());
257 EXPECT_EQ(4u, otherSpace.getNumSymbolVars());
258 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[5]));
259 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[6]));
260 EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&otherIdentifiers[5]));
261 EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&otherIdentifiers[7]));
262 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 0), Identifier(&identifiers[5]));
263 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 1), Identifier(&identifiers[6]));
264 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 2),
265 Identifier(&otherIdentifiers[5]));
266 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 3),
267 Identifier(&otherIdentifiers[7]));
268 // Check that domain and range var identifiers are not affected.
269 EXPECT_EQ(3u, space.getNumDomainVars());
270 EXPECT_EQ(3u, space.getNumRangeVars());
271 EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
272 EXPECT_EQ(space.getId(VarKind::Domain, 1), Identifier(&identifiers[1]));
273 EXPECT_EQ(space.getId(VarKind::Domain, 2), Identifier(&otherIdentifiers[2]));
274 EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
275 EXPECT_EQ(space.getId(VarKind::Range, 1), Identifier(&identifiers[3]));
276 EXPECT_EQ(space.getId(VarKind::Range, 2), Identifier(&identifiers[4]));
277 EXPECT_EQ(3u, otherSpace.getNumDomainVars());
278 EXPECT_EQ(2u, otherSpace.getNumRangeVars());
279 EXPECT_EQ(otherSpace.getId(VarKind::Domain, 0),
280 Identifier(&otherIdentifiers[0]));
281 EXPECT_EQ(otherSpace.getId(VarKind::Domain, 1),
282 Identifier(&otherIdentifiers[1]));
283 EXPECT_EQ(otherSpace.getId(VarKind::Domain, 2),
284 Identifier(&otherIdentifiers[2]));
285 EXPECT_EQ(otherSpace.getId(VarKind::Range, 0),
286 Identifier(&otherIdentifiers[3]));
287 EXPECT_EQ(otherSpace.getId(VarKind::Range, 1),
288 Identifier(&otherIdentifiers[4]));
289 }
290
291 // Check that mergeAndAlignSymbols unions symbol variables when they are
292 // disjoint.
TEST(IntegerRelationTest,mergeAndAlignDisjointSymbols)293 TEST(IntegerRelationTest, mergeAndAlignDisjointSymbols) {
294 IntegerRelation rel = parseRelationFromSet(
295 "(x, y, z)[A, B, C, D] : (x + A - C - y + D - z >= 0)", 2);
296 IntegerRelation otherRel = parseRelationFromSet(
297 "(u, v, a, b)[E, F, G, H] : (E - u + v == 0, v - G - H >= 0)", 2);
298 PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 4, 0);
299
300 PresburgerSpace otherSpace = PresburgerSpace::getRelationSpace(2, 2, 4, 0);
301
302 // Attach identifiers.
303 int identifiers[7] = {'x', 'y', 'z', 'A', 'B', 'C', 'D'};
304 int otherIdentifiers[8] = {'u', 'v', 'a', 'b', 'E', 'F', 'G', 'H'};
305
306 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
307 space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
308 space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
309 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
310 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
311 space.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
312 space.setId(VarKind::Symbol, 3, Identifier(&identifiers[6]));
313
314 otherSpace.setId(VarKind::Domain, 0, Identifier(&otherIdentifiers[0]));
315 otherSpace.setId(VarKind::Domain, 1, Identifier(&otherIdentifiers[1]));
316 otherSpace.setId(VarKind::Range, 0, Identifier(&otherIdentifiers[2]));
317 otherSpace.setId(VarKind::Range, 1, Identifier(&otherIdentifiers[3]));
318 otherSpace.setId(VarKind::Symbol, 0, Identifier(&otherIdentifiers[4]));
319 otherSpace.setId(VarKind::Symbol, 1, Identifier(&otherIdentifiers[5]));
320 otherSpace.setId(VarKind::Symbol, 2, Identifier(&otherIdentifiers[6]));
321 otherSpace.setId(VarKind::Symbol, 3, Identifier(&otherIdentifiers[7]));
322
323 rel.setSpace(space);
324 otherRel.setSpace(otherSpace);
325 rel.mergeAndAlignSymbols(otherRel);
326
327 space = rel.getSpace();
328 otherSpace = otherRel.getSpace();
329
330 // Check if merge and align is successful.
331 // Check symbol var identifiers.
332 EXPECT_EQ(8u, space.getNumSymbolVars());
333 EXPECT_EQ(8u, otherSpace.getNumSymbolVars());
334 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
335 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
336 EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&identifiers[5]));
337 EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
338 EXPECT_EQ(space.getId(VarKind::Symbol, 4), Identifier(&otherIdentifiers[4]));
339 EXPECT_EQ(space.getId(VarKind::Symbol, 5), Identifier(&otherIdentifiers[5]));
340 EXPECT_EQ(space.getId(VarKind::Symbol, 6), Identifier(&otherIdentifiers[6]));
341 EXPECT_EQ(space.getId(VarKind::Symbol, 7), Identifier(&otherIdentifiers[7]));
342 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
343 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
344 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 2), Identifier(&identifiers[5]));
345 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
346 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 4),
347 Identifier(&otherIdentifiers[4]));
348 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 5),
349 Identifier(&otherIdentifiers[5]));
350 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 6),
351 Identifier(&otherIdentifiers[6]));
352 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 7),
353 Identifier(&otherIdentifiers[7]));
354 // Check that domain and range var identifiers are not affected.
355 EXPECT_EQ(2u, space.getNumDomainVars());
356 EXPECT_EQ(1u, space.getNumRangeVars());
357 EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
358 EXPECT_EQ(space.getId(VarKind::Domain, 1), Identifier(&identifiers[1]));
359 EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
360 EXPECT_EQ(2u, otherSpace.getNumDomainVars());
361 EXPECT_EQ(2u, otherSpace.getNumRangeVars());
362 EXPECT_EQ(otherSpace.getId(VarKind::Domain, 0),
363 Identifier(&otherIdentifiers[0]));
364 EXPECT_EQ(otherSpace.getId(VarKind::Domain, 1),
365 Identifier(&otherIdentifiers[1]));
366 EXPECT_EQ(otherSpace.getId(VarKind::Range, 0),
367 Identifier(&otherIdentifiers[2]));
368 EXPECT_EQ(otherSpace.getId(VarKind::Range, 1),
369 Identifier(&otherIdentifiers[3]));
370 }
371
372 // Check that mergeAndAlignSymbols is correct when a suffix of identifiers is
373 // shared; i.e. identifiers are [A, B, C, D] and [E, F, C, D].
TEST(IntegerRelationTest,mergeAndAlignCommonSuffixSymbols)374 TEST(IntegerRelationTest, mergeAndAlignCommonSuffixSymbols) {
375 IntegerRelation rel = parseRelationFromSet(
376 "(x, y, z)[A, B, C, D] : (x + A - C - y + D - z >= 0)", 2);
377 IntegerRelation otherRel = parseRelationFromSet(
378 "(u, v, a, b)[E, F, C, D] : (E - u + v == 0, v - C - D >= 0)", 2);
379 PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 4, 0);
380
381 PresburgerSpace otherSpace = PresburgerSpace::getRelationSpace(2, 2, 4, 0);
382
383 // Attach identifiers.
384 int identifiers[7] = {'x', 'y', 'z', 'A', 'B', 'C', 'D'};
385 int otherIdentifiers[6] = {'u', 'v', 'a', 'b', 'E', 'F'};
386
387 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
388 space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
389 space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
390 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
391 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
392 space.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
393 space.setId(VarKind::Symbol, 3, Identifier(&identifiers[6]));
394
395 otherSpace.setId(VarKind::Domain, 0, Identifier(&otherIdentifiers[0]));
396 otherSpace.setId(VarKind::Domain, 1, Identifier(&otherIdentifiers[1]));
397 otherSpace.setId(VarKind::Range, 0, Identifier(&otherIdentifiers[2]));
398 otherSpace.setId(VarKind::Range, 1, Identifier(&otherIdentifiers[3]));
399 otherSpace.setId(VarKind::Symbol, 0, Identifier(&otherIdentifiers[4]));
400 otherSpace.setId(VarKind::Symbol, 1, Identifier(&otherIdentifiers[5]));
401 // Note common identifiers
402 otherSpace.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
403 otherSpace.setId(VarKind::Symbol, 3, Identifier(&identifiers[6]));
404
405 rel.setSpace(space);
406 otherRel.setSpace(otherSpace);
407 rel.mergeAndAlignSymbols(otherRel);
408
409 space = rel.getSpace();
410 otherSpace = otherRel.getSpace();
411
412 // Check if merge and align is successful.
413 // Check symbol var identifiers.
414 EXPECT_EQ(6u, space.getNumSymbolVars());
415 EXPECT_EQ(6u, otherSpace.getNumSymbolVars());
416 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
417 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
418 EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&identifiers[5]));
419 EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
420 EXPECT_EQ(space.getId(VarKind::Symbol, 4), Identifier(&otherIdentifiers[4]));
421 EXPECT_EQ(space.getId(VarKind::Symbol, 5), Identifier(&otherIdentifiers[5]));
422 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
423 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
424 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 2), Identifier(&identifiers[5]));
425 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
426 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 4),
427 Identifier(&otherIdentifiers[4]));
428 EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 5),
429 Identifier(&otherIdentifiers[5]));
430 // Check that domain and range var identifiers are not affected.
431 EXPECT_EQ(2u, space.getNumDomainVars());
432 EXPECT_EQ(1u, space.getNumRangeVars());
433 EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
434 EXPECT_EQ(space.getId(VarKind::Domain, 1), Identifier(&identifiers[1]));
435 EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
436 EXPECT_EQ(2u, otherSpace.getNumDomainVars());
437 EXPECT_EQ(2u, otherSpace.getNumRangeVars());
438 EXPECT_EQ(otherSpace.getId(VarKind::Domain, 0),
439 Identifier(&otherIdentifiers[0]));
440 EXPECT_EQ(otherSpace.getId(VarKind::Domain, 1),
441 Identifier(&otherIdentifiers[1]));
442 EXPECT_EQ(otherSpace.getId(VarKind::Range, 0),
443 Identifier(&otherIdentifiers[2]));
444 EXPECT_EQ(otherSpace.getId(VarKind::Range, 1),
445 Identifier(&otherIdentifiers[3]));
446 }
447
TEST(IntegerRelationTest,setId)448 TEST(IntegerRelationTest, setId) {
449 IntegerRelation rel = parseRelationFromSet(
450 "(x, y, z)[A, B, C, D] : (x + A - C - y + D - z >= 0)", 2);
451 PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 4, 0);
452
453 // Attach identifiers.
454 int identifiers[7] = {'x', 'y', 'z', 'A', 'B', 'C', 'D'};
455 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
456 space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
457 space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
458 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
459 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
460 space.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
461 space.setId(VarKind::Symbol, 3, Identifier(&identifiers[6]));
462 rel.setSpace(space);
463
464 int newIdentifiers[3] = {1, 2, 3};
465 rel.setId(VarKind::Domain, 1, Identifier(&newIdentifiers[0]));
466 rel.setId(VarKind::Range, 0, Identifier(&newIdentifiers[1]));
467 rel.setId(VarKind::Symbol, 2, Identifier(&newIdentifiers[2]));
468
469 space = rel.getSpace();
470 // Check that new identifiers are set correctly.
471 EXPECT_EQ(space.getId(VarKind::Domain, 1), Identifier(&newIdentifiers[0]));
472 EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&newIdentifiers[1]));
473 EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&newIdentifiers[2]));
474 // Check that old identifier are not changed.
475 EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
476 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
477 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
478 EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
479 }
480
TEST(IntegerRelationTest,convertVarKind)481 TEST(IntegerRelationTest, convertVarKind) {
482 PresburgerSpace space = PresburgerSpace::getSetSpace(3, 3, 0);
483
484 // Attach identifiers.
485 int identifiers[6] = {0, 1, 2, 3, 4, 5};
486 space.setId(VarKind::SetDim, 0, Identifier(&identifiers[0]));
487 space.setId(VarKind::SetDim, 1, Identifier(&identifiers[1]));
488 space.setId(VarKind::SetDim, 2, Identifier(&identifiers[2]));
489 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
490 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
491 space.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
492
493 // Cannot call parseIntegerRelation to test convertVarKind as
494 // parseIntegerRelation uses convertVarKind.
495 IntegerRelation rel = parseIntegerPolyhedron(
496 // 0 1 2 3 4 5
497 "(x, y, a)[U, V, W] : (x - U == 0, y + a - W == 0, U - V >= 0,"
498 "y - a >= 0)");
499 rel.setSpace(space);
500
501 // Make a few kind conversions.
502 rel.convertVarKind(VarKind::Symbol, 1, 2, VarKind::Domain, 0);
503 rel.convertVarKind(VarKind::Range, 2, 3, VarKind::Domain, 0);
504 rel.convertVarKind(VarKind::Range, 0, 2, VarKind::Symbol, 1);
505 rel.convertVarKind(VarKind::Domain, 1, 2, VarKind::Range, 0);
506 rel.convertVarKind(VarKind::Domain, 0, 1, VarKind::Range, 1);
507
508 space = rel.getSpace();
509
510 // Expected rel.
511 IntegerRelation expectedRel = parseIntegerPolyhedron(
512 "(V, a)[U, x, y, W] : (x - U == 0, y + a - W == 0, U - V >= 0,"
513 "y - a >= 0)");
514 expectedRel.setSpace(space);
515
516 EXPECT_TRUE(rel.isEqual(expectedRel));
517
518 EXPECT_EQ(space.getId(VarKind::SetDim, 0), Identifier(&identifiers[4]));
519 EXPECT_EQ(space.getId(VarKind::SetDim, 1), Identifier(&identifiers[2]));
520 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
521 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[0]));
522 EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&identifiers[1]));
523 EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&identifiers[5]));
524 }
525
TEST(IntegerRelationTest,convertVarKindToLocal)526 TEST(IntegerRelationTest, convertVarKindToLocal) {
527 // Convert all range variables to local variables.
528 IntegerRelation rel = parseRelationFromSet(
529 "(x, y, z)[N, M] : (x - y >= 0, y - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)",
530 1);
531 PresburgerSpace space = rel.getSpace();
532 // Attach identifiers.
533 char identifiers[5] = {'x', 'y', 'z', 'N', 'M'};
534 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
535 space.setId(VarKind::Range, 0, Identifier(&identifiers[1]));
536 space.setId(VarKind::Range, 1, Identifier(&identifiers[2]));
537 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
538 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
539 rel.setSpace(space);
540 rel.convertToLocal(VarKind::Range, 0, rel.getNumRangeVars());
541 IntegerRelation expectedRel =
542 parseRelationFromSet("(x)[N, M] : (x - N >= 0, 2 * M - 5 >= 0)", 1);
543 EXPECT_TRUE(rel.isEqual(expectedRel));
544 space = rel.getSpace();
545 EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
546 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
547 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
548
549 // Convert all domain variables to local variables.
550 IntegerRelation rel2 = parseRelationFromSet(
551 "(x, y, z)[N, M] : (x - y >= 0, y - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)",
552 2);
553 space = rel2.getSpace();
554 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
555 space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
556 space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
557 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
558 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
559 rel2.setSpace(space);
560 rel2.convertToLocal(VarKind::Domain, 0, rel2.getNumDomainVars());
561 expectedRel =
562 parseIntegerPolyhedron("(z)[N, M] : (3 - z >= 0, 2 * M - 5 >= 0)");
563 EXPECT_TRUE(rel2.isEqual(expectedRel));
564 space = rel2.getSpace();
565 EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
566 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
567 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
568
569 // Convert a prefix of range variables to local variables.
570 IntegerRelation rel3 = parseRelationFromSet(
571 "(x, y, z)[N, M] : (x - y >= 0, y - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)",
572 1);
573 space = rel3.getSpace();
574 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
575 space.setId(VarKind::Range, 0, Identifier(&identifiers[1]));
576 space.setId(VarKind::Range, 1, Identifier(&identifiers[2]));
577 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
578 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
579 rel3.setSpace(space);
580 rel3.convertToLocal(VarKind::Range, 0, 1);
581 expectedRel = parseRelationFromSet(
582 "(x, z)[N, M] : (x - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)", 1);
583 EXPECT_TRUE(rel3.isEqual(expectedRel));
584 space = rel3.getSpace();
585 EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
586 EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
587 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
588 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
589
590 // Convert a suffix of domain variables to local variables.
591 IntegerRelation rel4 = parseRelationFromSet(
592 "(x, y, z)[N, M] : (x - y >= 0, y - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)",
593 2);
594 space = rel4.getSpace();
595 space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
596 space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
597 space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
598 space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
599 space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
600 rel4.setSpace(space);
601 rel4.convertToLocal(VarKind::Domain, rel4.getNumDomainVars() - 1,
602 rel4.getNumDomainVars());
603 // expectedRel same as before.
604 EXPECT_TRUE(rel4.isEqual(expectedRel));
605 space = rel4.getSpace();
606 EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
607 EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
608 EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
609 EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
610 }
611