1 //===- SetTest.cpp - Tests for PresburgerSet ------------------------------===//
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 // This file contains tests for PresburgerSet. The tests for union,
10 // intersection, subtract, and complement work by computing the operation on
11 // two sets and checking, for a set of points, that the resulting set contains
12 // the point iff the result is supposed to contain it. The test for isEqual just
13 // checks if the result for two sets matches the expected result.
14 //
15 //===----------------------------------------------------------------------===//
16
17 #include "./Utils.h"
18 #include "mlir/Analysis/Presburger/PresburgerRelation.h"
19 #include "mlir/IR/MLIRContext.h"
20
21 #include <gmock/gmock.h>
22 #include <gtest/gtest.h>
23
24 using namespace mlir;
25 using namespace presburger;
26
27 /// Compute the union of s and t, and check that each of the given points
28 /// belongs to the union iff it belongs to at least one of s and t.
testUnionAtPoints(const PresburgerSet & s,const PresburgerSet & t,ArrayRef<SmallVector<int64_t,4>> points)29 static void testUnionAtPoints(const PresburgerSet &s, const PresburgerSet &t,
30 ArrayRef<SmallVector<int64_t, 4>> points) {
31 PresburgerSet unionSet = s.unionSet(t);
32 for (const SmallVector<int64_t, 4> &point : points) {
33 bool inS = s.containsPoint(point);
34 bool inT = t.containsPoint(point);
35 bool inUnion = unionSet.containsPoint(point);
36 EXPECT_EQ(inUnion, inS || inT);
37 }
38 }
39
40 /// Compute the intersection of s and t, and check that each of the given points
41 /// belongs to the intersection iff it belongs to both s and t.
testIntersectAtPoints(const PresburgerSet & s,const PresburgerSet & t,ArrayRef<SmallVector<int64_t,4>> points)42 static void testIntersectAtPoints(const PresburgerSet &s,
43 const PresburgerSet &t,
44 ArrayRef<SmallVector<int64_t, 4>> points) {
45 PresburgerSet intersection = s.intersect(t);
46 for (const SmallVector<int64_t, 4> &point : points) {
47 bool inS = s.containsPoint(point);
48 bool inT = t.containsPoint(point);
49 bool inIntersection = intersection.containsPoint(point);
50 EXPECT_EQ(inIntersection, inS && inT);
51 }
52 }
53
54 /// Compute the set difference s \ t, and check that each of the given points
55 /// belongs to the difference iff it belongs to s and does not belong to t.
testSubtractAtPoints(const PresburgerSet & s,const PresburgerSet & t,ArrayRef<SmallVector<int64_t,4>> points)56 static void testSubtractAtPoints(const PresburgerSet &s, const PresburgerSet &t,
57 ArrayRef<SmallVector<int64_t, 4>> points) {
58 PresburgerSet diff = s.subtract(t);
59 for (const SmallVector<int64_t, 4> &point : points) {
60 bool inS = s.containsPoint(point);
61 bool inT = t.containsPoint(point);
62 bool inDiff = diff.containsPoint(point);
63 if (inT)
64 EXPECT_FALSE(inDiff);
65 else
66 EXPECT_EQ(inDiff, inS);
67 }
68 }
69
70 /// Compute the complement of s, and check that each of the given points
71 /// belongs to the complement iff it does not belong to s.
testComplementAtPoints(const PresburgerSet & s,ArrayRef<SmallVector<int64_t,4>> points)72 static void testComplementAtPoints(const PresburgerSet &s,
73 ArrayRef<SmallVector<int64_t, 4>> points) {
74 PresburgerSet complement = s.complement();
75 complement.complement();
76 for (const SmallVector<int64_t, 4> &point : points) {
77 bool inS = s.containsPoint(point);
78 bool inComplement = complement.containsPoint(point);
79 if (inS)
80 EXPECT_FALSE(inComplement);
81 else
82 EXPECT_TRUE(inComplement);
83 }
84 }
85
86 /// Construct a PresburgerSet having `numDims` dimensions and no symbols from
87 /// the given list of IntegerPolyhedron. Each Poly in `polys` should also have
88 /// `numDims` dimensions and no symbols, although it can have any number of
89 /// local ids.
makeSetFromPoly(unsigned numDims,ArrayRef<IntegerPolyhedron> polys)90 static PresburgerSet makeSetFromPoly(unsigned numDims,
91 ArrayRef<IntegerPolyhedron> polys) {
92 PresburgerSet set =
93 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace(numDims));
94 for (const IntegerPolyhedron &poly : polys)
95 set.unionInPlace(poly);
96 return set;
97 }
98
TEST(SetTest,containsPoint)99 TEST(SetTest, containsPoint) {
100 PresburgerSet setA = parsePresburgerSetFromPolyStrings(
101 1,
102 {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"});
103 for (unsigned x = 0; x <= 21; ++x) {
104 if ((2 <= x && x <= 8) || (10 <= x && x <= 20))
105 EXPECT_TRUE(setA.containsPoint({x}));
106 else
107 EXPECT_FALSE(setA.containsPoint({x}));
108 }
109
110 // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} union
111 // a square with opposite corners (2, 2) and (10, 10).
112 PresburgerSet setB = parsePresburgerSetFromPolyStrings(
113 2, {"(x,y) : (x + y - 4 >= 0, -x - y + 32 >= 0, "
114 "x - y - 2 >= 0, -x + y + 16 >= 0)",
115 "(x,y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"});
116
117 for (unsigned x = 1; x <= 25; ++x) {
118 for (unsigned y = -6; y <= 16; ++y) {
119 if (4 <= x + y && x + y <= 32 && 2 <= x - y && x - y <= 16)
120 EXPECT_TRUE(setB.containsPoint({x, y}));
121 else if (2 <= x && x <= 10 && 2 <= y && y <= 10)
122 EXPECT_TRUE(setB.containsPoint({x, y}));
123 else
124 EXPECT_FALSE(setB.containsPoint({x, y}));
125 }
126 }
127
128 // The PresburgerSet has only one id, x, so we supply one value.
129 EXPECT_TRUE(PresburgerSet(parsePoly("(x) : (x - 2*(x floordiv 2) == 0)"))
130 .containsPoint({0}));
131 }
132
TEST(SetTest,Union)133 TEST(SetTest, Union) {
134 PresburgerSet set = parsePresburgerSetFromPolyStrings(
135 1,
136 {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"});
137
138 // Universe union set.
139 testUnionAtPoints(PresburgerSet::getUniverse(PresburgerSpace::getSetSpace(1)),
140 set, {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
141
142 // empty set union set.
143 testUnionAtPoints(PresburgerSet::getEmpty(PresburgerSpace::getSetSpace(1)),
144 set, {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
145
146 // empty set union Universe.
147 testUnionAtPoints(PresburgerSet::getEmpty(PresburgerSpace::getSetSpace(1)),
148 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace(1)),
149 {{1}, {2}, {0}, {-1}});
150
151 // Universe union empty set.
152 testUnionAtPoints(PresburgerSet::getUniverse(PresburgerSpace::getSetSpace(1)),
153 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace(1)),
154 {{1}, {2}, {0}, {-1}});
155
156 // empty set union empty set.
157 testUnionAtPoints(PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))),
158 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))),
159 {{1}, {2}, {0}, {-1}});
160 }
161
TEST(SetTest,Intersect)162 TEST(SetTest, Intersect) {
163 PresburgerSet set = parsePresburgerSetFromPolyStrings(
164 1,
165 {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"});
166
167 // Universe intersection set.
168 testIntersectAtPoints(
169 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))), set,
170 {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
171
172 // empty set intersection set.
173 testIntersectAtPoints(
174 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))), set,
175 {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
176
177 // empty set intersection Universe.
178 testIntersectAtPoints(
179 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))),
180 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))),
181 {{1}, {2}, {0}, {-1}});
182
183 // Universe intersection empty set.
184 testIntersectAtPoints(
185 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))),
186 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))),
187 {{1}, {2}, {0}, {-1}});
188
189 // Universe intersection Universe.
190 testIntersectAtPoints(
191 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))),
192 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))),
193 {{1}, {2}, {0}, {-1}});
194 }
195
TEST(SetTest,Subtract)196 TEST(SetTest, Subtract) {
197 // The interval [2, 8] minus the interval [10, 20].
198 testSubtractAtPoints(
199 parsePresburgerSetFromPolyStrings(1, {"(x) : (x - 2 >= 0, -x + 8 >= 0)"}),
200 parsePresburgerSetFromPolyStrings(1,
201 {"(x) : (x - 10 >= 0, -x + 20 >= 0)"}),
202 {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
203
204 // Universe minus [2, 8] U [10, 20]
205 testSubtractAtPoints(parsePresburgerSetFromPolyStrings(1, {"(x) : ()"}),
206 parsePresburgerSetFromPolyStrings(
207 1, {"(x) : (x - 2 >= 0, -x + 8 >= 0)",
208 "(x) : (x - 10 >= 0, -x + 20 >= 0)"}),
209 {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
210
211 // ((-infinity, 0] U [3, 4] U [6, 7]) - ([2, 3] U [5, 6])
212 testSubtractAtPoints(
213 parsePresburgerSetFromPolyStrings(1, {"(x) : (-x >= 0)",
214 "(x) : (x - 3 >= 0, -x + 4 >= 0)",
215 "(x) : (x - 6 >= 0, -x + 7 >= 0)"}),
216 parsePresburgerSetFromPolyStrings(1, {"(x) : (x - 2 >= 0, -x + 3 >= 0)",
217 "(x) : (x - 5 >= 0, -x + 6 >= 0)"}),
218 {{0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}});
219
220 // Expected result is {[x, y] : x > y}, i.e., {[x, y] : x >= y + 1}.
221 testSubtractAtPoints(
222 parsePresburgerSetFromPolyStrings(2, {"(x, y) : (x - y >= 0)"}),
223 parsePresburgerSetFromPolyStrings(2, {"(x, y) : (x + y >= 0)"}),
224 {{0, 1}, {1, 1}, {1, 0}, {1, -1}, {0, -1}});
225
226 // A rectangle with corners at (2, 2) and (10, 10), minus
227 // a rectangle with corners at (5, -10) and (7, 100).
228 // This splits the former rectangle into two halves, (2, 2) to (5, 10) and
229 // (7, 2) to (10, 10).
230 testSubtractAtPoints(
231 parsePresburgerSetFromPolyStrings(
232 2,
233 {
234 "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)",
235 }),
236 parsePresburgerSetFromPolyStrings(
237 2,
238 {
239 "(x, y) : (x - 5 >= 0, y + 10 >= 0, -x + 7 >= 0, -y + 100 >= 0)",
240 }),
241 {{1, 2}, {2, 2}, {4, 2}, {5, 2}, {7, 2}, {8, 2}, {11, 2},
242 {1, 1}, {2, 1}, {4, 1}, {5, 1}, {7, 1}, {8, 1}, {11, 1},
243 {1, 10}, {2, 10}, {4, 10}, {5, 10}, {7, 10}, {8, 10}, {11, 10},
244 {1, 11}, {2, 11}, {4, 11}, {5, 11}, {7, 11}, {8, 11}, {11, 11}});
245
246 // A rectangle with corners at (2, 2) and (10, 10), minus
247 // a rectangle with corners at (5, 4) and (7, 8).
248 // This creates a hole in the middle of the former rectangle, and the
249 // resulting set can be represented as a union of four rectangles.
250 testSubtractAtPoints(
251 parsePresburgerSetFromPolyStrings(
252 2, {"(x, y) : (x - 2 >= 0, y -2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"}),
253 parsePresburgerSetFromPolyStrings(
254 2,
255 {
256 "(x, y) : (x - 5 >= 0, y - 4 >= 0, -x + 7 >= 0, -y + 8 >= 0)",
257 }),
258 {{1, 1},
259 {2, 2},
260 {10, 10},
261 {11, 11},
262 {5, 4},
263 {7, 4},
264 {5, 8},
265 {7, 8},
266 {4, 4},
267 {8, 4},
268 {4, 8},
269 {8, 8}});
270
271 // The second set is a superset of the first one, since on the line x + y = 0,
272 // y <= 1 is equivalent to x >= -1. So the result is empty.
273 testSubtractAtPoints(
274 parsePresburgerSetFromPolyStrings(2, {"(x, y) : (x >= 0, x + y == 0)"}),
275 parsePresburgerSetFromPolyStrings(2,
276 {"(x, y) : (-y + 1 >= 0, x + y == 0)"}),
277 {{0, 0},
278 {1, -1},
279 {2, -2},
280 {-1, 1},
281 {-2, 2},
282 {1, 1},
283 {-1, -1},
284 {-1, 1},
285 {1, -1}});
286
287 // The result should be {0} U {2}.
288 testSubtractAtPoints(
289 parsePresburgerSetFromPolyStrings(1, {"(x) : (x >= 0, -x + 2 >= 0)"}),
290 parsePresburgerSetFromPolyStrings(1, {"(x) : (x - 1 == 0)"}),
291 {{-1}, {0}, {1}, {2}, {3}});
292
293 // Sets with lots of redundant inequalities to test the redundancy heuristic.
294 // (the heuristic is for the subtrahend, the second set which is the one being
295 // subtracted)
296
297 // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} minus
298 // a triangle with vertices {(2, 2), (10, 2), (10, 10)}.
299 testSubtractAtPoints(
300 parsePresburgerSetFromPolyStrings(
301 2,
302 {
303 "(x, y) : (x + y - 4 >= 0, -x - y + 32 >= 0, x - y - 2 >= 0, "
304 "-x + y + 16 >= 0)",
305 }),
306 parsePresburgerSetFromPolyStrings(
307 2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, "
308 "-y + 10 >= 0, x + y - 2 >= 0, -x - y + 30 >= 0, x - y >= 0, "
309 "-x + y + 10 >= 0)"}),
310 {{1, 2}, {2, 2}, {3, 2}, {4, 2}, {1, 1}, {2, 1}, {3, 1},
311 {4, 1}, {2, 0}, {3, 0}, {4, 0}, {5, 0}, {10, 2}, {11, 2},
312 {10, 1}, {10, 10}, {10, 11}, {10, 9}, {11, 10}, {10, -6}, {11, -6},
313 {24, 8}, {24, 7}, {17, 15}, {16, 15}});
314
315 // ((-infinity, -5] U [3, 3] U [4, 4] U [5, 5]) - ([-2, -10] U [3, 4] U [6,
316 // 7])
317 testSubtractAtPoints(
318 parsePresburgerSetFromPolyStrings(
319 1, {"(x) : (-x - 5 >= 0)", "(x) : (x - 3 == 0)", "(x) : (x - 4 == 0)",
320 "(x) : (x - 5 == 0)"}),
321 parsePresburgerSetFromPolyStrings(
322 1, {"(x) : (-x - 2 >= 0, x - 10 >= 0, -x >= 0, -x + 10 >= 0, "
323 "x - 100 >= 0, x - 50 >= 0)",
324 "(x) : (x - 3 >= 0, -x + 4 >= 0, x + 1 >= 0, "
325 "x + 7 >= 0, -x + 10 >= 0)",
326 "(x) : (x - 6 >= 0, -x + 7 >= 0, x + 1 >= 0, x - 3 >= 0, "
327 "-x + 5 >= 0)"}),
328 {{-6},
329 {-5},
330 {-4},
331 {-9},
332 {-10},
333 {-11},
334 {0},
335 {1},
336 {2},
337 {3},
338 {4},
339 {5},
340 {6},
341 {7},
342 {8}});
343 }
344
TEST(SetTest,Complement)345 TEST(SetTest, Complement) {
346 // Complement of universe.
347 testComplementAtPoints(
348 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))),
349 {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}});
350
351 // Complement of empty set.
352 testComplementAtPoints(
353 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))),
354 {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}});
355
356 testComplementAtPoints(
357 parsePresburgerSetFromPolyStrings(2, {"(x,y) : (x - 2 >= 0, y - 2 >= 0, "
358 "-x + 10 >= 0, -y + 10 >= 0)"}),
359 {{1, 1},
360 {2, 1},
361 {1, 2},
362 {2, 2},
363 {2, 3},
364 {3, 2},
365 {10, 10},
366 {10, 11},
367 {11, 10},
368 {2, 10},
369 {2, 11},
370 {1, 10}});
371 }
372
TEST(SetTest,isEqual)373 TEST(SetTest, isEqual) {
374 // set = [2, 8] U [10, 20].
375 PresburgerSet universe =
376 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1)));
377 PresburgerSet emptySet =
378 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1)));
379 PresburgerSet set = parsePresburgerSetFromPolyStrings(
380 1,
381 {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"});
382
383 // universe != emptySet.
384 EXPECT_FALSE(universe.isEqual(emptySet));
385 // emptySet != universe.
386 EXPECT_FALSE(emptySet.isEqual(universe));
387 // emptySet == emptySet.
388 EXPECT_TRUE(emptySet.isEqual(emptySet));
389 // universe == universe.
390 EXPECT_TRUE(universe.isEqual(universe));
391
392 // universe U emptySet == universe.
393 EXPECT_TRUE(universe.unionSet(emptySet).isEqual(universe));
394 // universe U universe == universe.
395 EXPECT_TRUE(universe.unionSet(universe).isEqual(universe));
396 // emptySet U emptySet == emptySet.
397 EXPECT_TRUE(emptySet.unionSet(emptySet).isEqual(emptySet));
398 // universe U emptySet != emptySet.
399 EXPECT_FALSE(universe.unionSet(emptySet).isEqual(emptySet));
400 // universe U universe != emptySet.
401 EXPECT_FALSE(universe.unionSet(universe).isEqual(emptySet));
402 // emptySet U emptySet != universe.
403 EXPECT_FALSE(emptySet.unionSet(emptySet).isEqual(universe));
404
405 // set \ set == emptySet.
406 EXPECT_TRUE(set.subtract(set).isEqual(emptySet));
407 // set == set.
408 EXPECT_TRUE(set.isEqual(set));
409 // set U (universe \ set) == universe.
410 EXPECT_TRUE(set.unionSet(set.complement()).isEqual(universe));
411 // set U (universe \ set) != set.
412 EXPECT_FALSE(set.unionSet(set.complement()).isEqual(set));
413 // set != set U (universe \ set).
414 EXPECT_FALSE(set.isEqual(set.unionSet(set.complement())));
415
416 // square is one unit taller than rect.
417 PresburgerSet square = parsePresburgerSetFromPolyStrings(
418 2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 9 >= 0)"});
419 PresburgerSet rect = parsePresburgerSetFromPolyStrings(
420 2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 8 >= 0)"});
421 EXPECT_FALSE(square.isEqual(rect));
422 PresburgerSet universeRect = square.unionSet(square.complement());
423 PresburgerSet universeSquare = rect.unionSet(rect.complement());
424 EXPECT_TRUE(universeRect.isEqual(universeSquare));
425 EXPECT_FALSE(universeRect.isEqual(rect));
426 EXPECT_FALSE(universeSquare.isEqual(square));
427 EXPECT_FALSE(rect.complement().isEqual(square.complement()));
428 }
429
expectEqual(const PresburgerSet & s,const PresburgerSet & t)430 void expectEqual(const PresburgerSet &s, const PresburgerSet &t) {
431 EXPECT_TRUE(s.isEqual(t));
432 }
433
expectEqual(const IntegerPolyhedron & s,const IntegerPolyhedron & t)434 void expectEqual(const IntegerPolyhedron &s, const IntegerPolyhedron &t) {
435 EXPECT_TRUE(s.isEqual(t));
436 }
437
expectEmpty(const PresburgerSet & s)438 void expectEmpty(const PresburgerSet &s) { EXPECT_TRUE(s.isIntegerEmpty()); }
439
TEST(SetTest,divisions)440 TEST(SetTest, divisions) {
441 // evens = {x : exists q, x = 2q}.
442 PresburgerSet evens{parsePoly("(x) : (x - 2 * (x floordiv 2) == 0)")};
443
444 // odds = {x : exists q, x = 2q + 1}.
445 PresburgerSet odds{parsePoly("(x) : (x - 2 * (x floordiv 2) - 1 == 0)")};
446
447 // multiples3 = {x : exists q, x = 3q}.
448 PresburgerSet multiples3{parsePoly("(x) : (x - 3 * (x floordiv 3) == 0)")};
449
450 // multiples6 = {x : exists q, x = 6q}.
451 PresburgerSet multiples6{parsePoly("(x) : (x - 6 * (x floordiv 6) == 0)")};
452
453 // evens /\ odds = empty.
454 expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds)));
455 // evens U odds = universe.
456 expectEqual(evens.unionSet(odds),
457 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))));
458 expectEqual(evens.complement(), odds);
459 expectEqual(odds.complement(), evens);
460 // even multiples of 3 = multiples of 6.
461 expectEqual(multiples3.intersect(evens), multiples6);
462
463 PresburgerSet setA{parsePoly("(x) : (-x >= 0)")};
464 PresburgerSet setB{parsePoly("(x) : (x floordiv 2 - 4 >= 0)")};
465 EXPECT_TRUE(setA.subtract(setB).isEqual(setA));
466 }
467
convertSuffixDimsToLocals(IntegerPolyhedron & poly,unsigned numLocals)468 void convertSuffixDimsToLocals(IntegerPolyhedron &poly, unsigned numLocals) {
469 poly.convertVarKind(VarKind::SetDim, poly.getNumDimVars() - numLocals,
470 poly.getNumDimVars(), VarKind::Local);
471 }
472
parsePolyAndMakeLocals(StringRef str,unsigned numLocals)473 inline IntegerPolyhedron parsePolyAndMakeLocals(StringRef str,
474 unsigned numLocals) {
475 IntegerPolyhedron poly = parsePoly(str);
476 convertSuffixDimsToLocals(poly, numLocals);
477 return poly;
478 }
479
TEST(SetTest,divisionsDefByEq)480 TEST(SetTest, divisionsDefByEq) {
481 // evens = {x : exists q, x = 2q}.
482 PresburgerSet evens{
483 parsePolyAndMakeLocals("(x, y) : (x - 2 * y == 0)", /*numLocals=*/1)};
484
485 // odds = {x : exists q, x = 2q + 1}.
486 PresburgerSet odds{
487 parsePolyAndMakeLocals("(x, y) : (x - 2 * y - 1 == 0)", /*numLocals=*/1)};
488
489 // multiples3 = {x : exists q, x = 3q}.
490 PresburgerSet multiples3{
491 parsePolyAndMakeLocals("(x, y) : (x - 3 * y == 0)", /*numLocals=*/1)};
492
493 // multiples6 = {x : exists q, x = 6q}.
494 PresburgerSet multiples6{
495 parsePolyAndMakeLocals("(x, y) : (x - 6 * y == 0)", /*numLocals=*/1)};
496
497 // evens /\ odds = empty.
498 expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds)));
499 // evens U odds = universe.
500 expectEqual(evens.unionSet(odds),
501 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))));
502 expectEqual(evens.complement(), odds);
503 expectEqual(odds.complement(), evens);
504 // even multiples of 3 = multiples of 6.
505 expectEqual(multiples3.intersect(evens), multiples6);
506
507 PresburgerSet evensDefByIneq{
508 parsePoly("(x) : (x - 2 * (x floordiv 2) == 0)")};
509 expectEqual(evens, PresburgerSet(evensDefByIneq));
510 }
511
TEST(SetTest,divisionNonDivLocals)512 TEST(SetTest, divisionNonDivLocals) {
513 // This is a tetrahedron with vertices at
514 // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 1000), and (1000, 1000, 1000).
515 //
516 // The only integer point in this is at (1000, 1000, 1000).
517 // We project this to the xy plane.
518 IntegerPolyhedron tetrahedron =
519 parsePolyAndMakeLocals("(x, y, z) : (y >= 0, z - y >= 0, 3000*x - 2998*y "
520 "- 1000 - z >= 0, -1500*x + 1499*y + 1000 >= 0)",
521 /*numLocals=*/1);
522
523 // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (1000, 1000).
524 // The only integer point in this is at (1000, 1000).
525 //
526 // It also happens to be the projection of the above onto the xy plane.
527 IntegerPolyhedron triangle = parsePoly("(x,y) : (y >= 0, "
528 "3000 * x - 2999 * y - 1000 >= 0, "
529 "-3000 * x + 2998 * y + 2000 >= 0)");
530 EXPECT_TRUE(triangle.containsPoint({1000, 1000}));
531 EXPECT_FALSE(triangle.containsPoint({1001, 1001}));
532 expectEqual(triangle, tetrahedron);
533
534 convertSuffixDimsToLocals(triangle, 1);
535 IntegerPolyhedron line = parsePoly("(x) : (x - 1000 == 0)");
536 expectEqual(line, triangle);
537
538 // Triangle with vertices (0, 0), (5, 0), (15, 5).
539 // Projected on x, it becomes [0, 13] U {15} as it becomes too narrow towards
540 // the apex and so does not have have any integer point at x = 14.
541 // At x = 15, the apex is an integer point.
542 PresburgerSet triangle2{parsePolyAndMakeLocals("(x,y) : (y >= 0, "
543 "x - 3*y >= 0, "
544 "2*y - x + 5 >= 0)",
545 /*numLocals=*/1)};
546 PresburgerSet zeroToThirteen{parsePoly("(x) : (13 - x >= 0, x >= 0)")};
547 PresburgerSet fifteen{parsePoly("(x) : (x - 15 == 0)")};
548 expectEqual(triangle2.subtract(zeroToThirteen), fifteen);
549 }
550
TEST(SetTest,subtractDuplicateDivsRegression)551 TEST(SetTest, subtractDuplicateDivsRegression) {
552 // Previously, subtracting sets with duplicate divs might result in crashes
553 // due to existing divs being removed when merging local ids, due to being
554 // identified as being duplicates for the first time.
555 IntegerPolyhedron setA(PresburgerSpace::getSetSpace(1));
556 setA.addLocalFloorDiv({1, 0}, 2);
557 setA.addLocalFloorDiv({1, 0, 0}, 2);
558 EXPECT_TRUE(setA.isEqual(setA));
559 }
560
561 /// Coalesce `set` and check that the `newSet` is equal to `set` and that
562 /// `expectedNumPoly` matches the number of Poly in the coalesced set.
expectCoalesce(size_t expectedNumPoly,const PresburgerSet & set)563 void expectCoalesce(size_t expectedNumPoly, const PresburgerSet &set) {
564 PresburgerSet newSet = set.coalesce();
565 EXPECT_TRUE(set.isEqual(newSet));
566 EXPECT_TRUE(expectedNumPoly == newSet.getNumDisjuncts());
567 }
568
TEST(SetTest,coalesceNoPoly)569 TEST(SetTest, coalesceNoPoly) {
570 PresburgerSet set = makeSetFromPoly(0, {});
571 expectCoalesce(0, set);
572 }
573
TEST(SetTest,coalesceContainedOneDim)574 TEST(SetTest, coalesceContainedOneDim) {
575 PresburgerSet set = parsePresburgerSetFromPolyStrings(
576 1, {"(x) : (x >= 0, -x + 4 >= 0)", "(x) : (x - 1 >= 0, -x + 2 >= 0)"});
577 expectCoalesce(1, set);
578 }
579
TEST(SetTest,coalesceFirstEmpty)580 TEST(SetTest, coalesceFirstEmpty) {
581 PresburgerSet set = parsePresburgerSetFromPolyStrings(
582 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ( x - 1 >= 0, -x + 2 >= 0)"});
583 expectCoalesce(1, set);
584 }
585
TEST(SetTest,coalesceSecondEmpty)586 TEST(SetTest, coalesceSecondEmpty) {
587 PresburgerSet set = parsePresburgerSetFromPolyStrings(
588 1, {"(x) : (x - 1 >= 0, -x + 2 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"});
589 expectCoalesce(1, set);
590 }
591
TEST(SetTest,coalesceBothEmpty)592 TEST(SetTest, coalesceBothEmpty) {
593 PresburgerSet set = parsePresburgerSetFromPolyStrings(
594 1, {"(x) : (x - 3 >= 0, -x - 1 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"});
595 expectCoalesce(0, set);
596 }
597
TEST(SetTest,coalesceFirstUniv)598 TEST(SetTest, coalesceFirstUniv) {
599 PresburgerSet set = parsePresburgerSetFromPolyStrings(
600 1, {"(x) : ()", "(x) : ( x >= 0, -x + 1 >= 0)"});
601 expectCoalesce(1, set);
602 }
603
TEST(SetTest,coalesceSecondUniv)604 TEST(SetTest, coalesceSecondUniv) {
605 PresburgerSet set = parsePresburgerSetFromPolyStrings(
606 1, {"(x) : ( x >= 0, -x + 1 >= 0)", "(x) : ()"});
607 expectCoalesce(1, set);
608 }
609
TEST(SetTest,coalesceBothUniv)610 TEST(SetTest, coalesceBothUniv) {
611 PresburgerSet set =
612 parsePresburgerSetFromPolyStrings(1, {"(x) : ()", "(x) : ()"});
613 expectCoalesce(1, set);
614 }
615
TEST(SetTest,coalesceFirstUnivSecondEmpty)616 TEST(SetTest, coalesceFirstUnivSecondEmpty) {
617 PresburgerSet set = parsePresburgerSetFromPolyStrings(
618 1, {"(x) : ()", "(x) : ( x >= 0, -x - 1 >= 0)"});
619 expectCoalesce(1, set);
620 }
621
TEST(SetTest,coalesceFirstEmptySecondUniv)622 TEST(SetTest, coalesceFirstEmptySecondUniv) {
623 PresburgerSet set = parsePresburgerSetFromPolyStrings(
624 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ()"});
625 expectCoalesce(1, set);
626 }
627
TEST(SetTest,coalesceCutOneDim)628 TEST(SetTest, coalesceCutOneDim) {
629 PresburgerSet set = parsePresburgerSetFromPolyStrings(
630 1, {
631 "(x) : ( x >= 0, -x + 3 >= 0)",
632 "(x) : ( x - 2 >= 0, -x + 4 >= 0)",
633 });
634 expectCoalesce(1, set);
635 }
636
TEST(SetTest,coalesceSeparateOneDim)637 TEST(SetTest, coalesceSeparateOneDim) {
638 PresburgerSet set = parsePresburgerSetFromPolyStrings(
639 1, {"(x) : ( x >= 0, -x + 2 >= 0)", "(x) : ( x - 3 >= 0, -x + 4 >= 0)"});
640 expectCoalesce(2, set);
641 }
642
TEST(SetTest,coalesceAdjEq)643 TEST(SetTest, coalesceAdjEq) {
644 PresburgerSet set = parsePresburgerSetFromPolyStrings(
645 1, {"(x) : ( x == 0)", "(x) : ( x - 1 == 0)"});
646 expectCoalesce(2, set);
647 }
648
TEST(SetTest,coalesceContainedTwoDim)649 TEST(SetTest, coalesceContainedTwoDim) {
650 PresburgerSet set = parsePresburgerSetFromPolyStrings(
651 2, {
652 "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)",
653 "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)",
654 });
655 expectCoalesce(1, set);
656 }
657
TEST(SetTest,coalesceCutTwoDim)658 TEST(SetTest, coalesceCutTwoDim) {
659 PresburgerSet set = parsePresburgerSetFromPolyStrings(
660 2, {
661 "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)",
662 "(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)",
663 });
664 expectCoalesce(1, set);
665 }
666
TEST(SetTest,coalesceEqStickingOut)667 TEST(SetTest, coalesceEqStickingOut) {
668 PresburgerSet set = parsePresburgerSetFromPolyStrings(
669 2, {
670 "(x,y) : (x >= 0, -x + 2 >= 0, y >= 0, -y + 2 >= 0)",
671 "(x,y) : (y - 1 == 0, x >= 0, -x + 3 >= 0)",
672 });
673 expectCoalesce(2, set);
674 }
675
TEST(SetTest,coalesceSeparateTwoDim)676 TEST(SetTest, coalesceSeparateTwoDim) {
677 PresburgerSet set = parsePresburgerSetFromPolyStrings(
678 2, {
679 "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)",
680 "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)",
681 });
682 expectCoalesce(2, set);
683 }
684
TEST(SetTest,coalesceContainedEq)685 TEST(SetTest, coalesceContainedEq) {
686 PresburgerSet set = parsePresburgerSetFromPolyStrings(
687 2, {
688 "(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)",
689 "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)",
690 });
691 expectCoalesce(1, set);
692 }
693
TEST(SetTest,coalesceCuttingEq)694 TEST(SetTest, coalesceCuttingEq) {
695 PresburgerSet set = parsePresburgerSetFromPolyStrings(
696 2, {
697 "(x,y) : (x + 1 >= 0, -x + 1 >= 0, x - y == 0)",
698 "(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)",
699 });
700 expectCoalesce(1, set);
701 }
702
TEST(SetTest,coalesceSeparateEq)703 TEST(SetTest, coalesceSeparateEq) {
704 PresburgerSet set = parsePresburgerSetFromPolyStrings(
705 2, {
706 "(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)",
707 "(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)",
708 });
709 expectCoalesce(2, set);
710 }
711
TEST(SetTest,coalesceContainedEqAsIneq)712 TEST(SetTest, coalesceContainedEqAsIneq) {
713 PresburgerSet set = parsePresburgerSetFromPolyStrings(
714 2, {
715 "(x,y) : (x >= 0, -x + 3 >= 0, x - y >= 0, -x + y >= 0)",
716 "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)",
717 });
718 expectCoalesce(1, set);
719 }
720
TEST(SetTest,coalesceContainedEqComplex)721 TEST(SetTest, coalesceContainedEqComplex) {
722 PresburgerSet set = parsePresburgerSetFromPolyStrings(
723 2, {
724 "(x,y) : (x - 2 == 0, x - y == 0)",
725 "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)",
726 });
727 expectCoalesce(1, set);
728 }
729
TEST(SetTest,coalesceThreeContained)730 TEST(SetTest, coalesceThreeContained) {
731 PresburgerSet set =
732 parsePresburgerSetFromPolyStrings(1, {
733 "(x) : (x >= 0, -x + 1 >= 0)",
734 "(x) : (x >= 0, -x + 2 >= 0)",
735 "(x) : (x >= 0, -x + 3 >= 0)",
736 });
737 expectCoalesce(1, set);
738 }
739
TEST(SetTest,coalesceDoubleIncrement)740 TEST(SetTest, coalesceDoubleIncrement) {
741 PresburgerSet set = parsePresburgerSetFromPolyStrings(
742 1, {
743 "(x) : (x == 0)",
744 "(x) : (x - 2 == 0)",
745 "(x) : (x + 2 == 0)",
746 "(x) : (x - 2 >= 0, -x + 3 >= 0)",
747 });
748 expectCoalesce(3, set);
749 }
750
TEST(SetTest,coalesceLastCoalesced)751 TEST(SetTest, coalesceLastCoalesced) {
752 PresburgerSet set = parsePresburgerSetFromPolyStrings(
753 1, {
754 "(x) : (x == 0)",
755 "(x) : (x - 1 >= 0, -x + 3 >= 0)",
756 "(x) : (x + 2 == 0)",
757 "(x) : (x - 2 >= 0, -x + 4 >= 0)",
758 });
759 expectCoalesce(3, set);
760 }
761
TEST(SetTest,coalesceDiv)762 TEST(SetTest, coalesceDiv) {
763 PresburgerSet set =
764 parsePresburgerSetFromPolyStrings(1, {
765 "(x) : (x floordiv 2 == 0)",
766 "(x) : (x floordiv 2 - 1 == 0)",
767 });
768 expectCoalesce(2, set);
769 }
770
TEST(SetTest,coalesceDivOtherContained)771 TEST(SetTest, coalesceDivOtherContained) {
772 PresburgerSet set =
773 parsePresburgerSetFromPolyStrings(1, {
774 "(x) : (x floordiv 2 == 0)",
775 "(x) : (x == 0)",
776 "(x) : (x >= 0, -x + 1 >= 0)",
777 });
778 expectCoalesce(2, set);
779 }
780
781 static void
expectComputedVolumeIsValidOverapprox(const PresburgerSet & set,Optional<uint64_t> trueVolume,Optional<uint64_t> resultBound)782 expectComputedVolumeIsValidOverapprox(const PresburgerSet &set,
783 Optional<uint64_t> trueVolume,
784 Optional<uint64_t> resultBound) {
785 expectComputedVolumeIsValidOverapprox(set.computeVolume(), trueVolume,
786 resultBound);
787 }
788
TEST(SetTest,computeVolume)789 TEST(SetTest, computeVolume) {
790 // Diamond with vertices at (0, 0), (5, 5), (5, 5), (10, 0).
791 PresburgerSet diamond(
792 parsePoly("(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0, -x + y + "
793 "10 >= 0)"));
794 expectComputedVolumeIsValidOverapprox(diamond,
795 /*trueVolume=*/61ull,
796 /*resultBound=*/121ull);
797
798 // Diamond with vertices at (-5, 0), (0, -5), (0, 5), (5, 0).
799 PresburgerSet shiftedDiamond(parsePoly(
800 "(x, y) : (x + y + 5 >= 0, -x - y + 5 >= 0, x - y + 5 >= 0, -x + y + "
801 "5 >= 0)"));
802 expectComputedVolumeIsValidOverapprox(shiftedDiamond,
803 /*trueVolume=*/61ull,
804 /*resultBound=*/121ull);
805
806 // Diamond with vertices at (-5, 0), (5, -10), (5, 10), (15, 0).
807 PresburgerSet biggerDiamond(parsePoly(
808 "(x, y) : (x + y + 5 >= 0, -x - y + 15 >= 0, x - y + 5 >= 0, -x + y + "
809 "15 >= 0)"));
810 expectComputedVolumeIsValidOverapprox(biggerDiamond,
811 /*trueVolume=*/221ull,
812 /*resultBound=*/441ull);
813
814 // There is some overlap between diamond and shiftedDiamond.
815 expectComputedVolumeIsValidOverapprox(diamond.unionSet(shiftedDiamond),
816 /*trueVolume=*/104ull,
817 /*resultBound=*/242ull);
818
819 // biggerDiamond subsumes both the small ones.
820 expectComputedVolumeIsValidOverapprox(
821 diamond.unionSet(shiftedDiamond).unionSet(biggerDiamond),
822 /*trueVolume=*/221ull,
823 /*resultBound=*/683ull);
824
825 // Unbounded polytope.
826 PresburgerSet unbounded(parsePoly("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"));
827 expectComputedVolumeIsValidOverapprox(unbounded, /*trueVolume=*/{},
828 /*resultBound=*/{});
829
830 // Union of unbounded with bounded is unbounded.
831 expectComputedVolumeIsValidOverapprox(unbounded.unionSet(diamond),
832 /*trueVolume=*/{},
833 /*resultBound=*/{});
834 }
835
836 // The last `numToProject` dims will be projected out, i.e., converted to
837 // locals.
testComputeReprAtPoints(IntegerPolyhedron poly,ArrayRef<SmallVector<int64_t,4>> points,unsigned numToProject)838 void testComputeReprAtPoints(IntegerPolyhedron poly,
839 ArrayRef<SmallVector<int64_t, 4>> points,
840 unsigned numToProject) {
841 poly.convertVarKind(VarKind::SetDim, poly.getNumDimVars() - numToProject,
842 poly.getNumDimVars(), VarKind::Local);
843 PresburgerRelation repr = poly.computeReprWithOnlyDivLocals();
844 EXPECT_TRUE(repr.hasOnlyDivLocals());
845 EXPECT_TRUE(repr.getSpace().isCompatible(poly.getSpace()));
846 for (const SmallVector<int64_t, 4> &point : points) {
847 EXPECT_EQ(poly.containsPointNoLocal(point).has_value(),
848 repr.containsPoint(point));
849 }
850 }
851
testComputeRepr(IntegerPolyhedron poly,const PresburgerSet & expected,unsigned numToProject)852 void testComputeRepr(IntegerPolyhedron poly, const PresburgerSet &expected,
853 unsigned numToProject) {
854 poly.convertVarKind(VarKind::SetDim, poly.getNumDimVars() - numToProject,
855 poly.getNumDimVars(), VarKind::Local);
856 PresburgerRelation repr = poly.computeReprWithOnlyDivLocals();
857 EXPECT_TRUE(repr.hasOnlyDivLocals());
858 EXPECT_TRUE(repr.getSpace().isCompatible(poly.getSpace()));
859 EXPECT_TRUE(repr.isEqual(expected));
860 }
861
TEST(SetTest,computeReprWithOnlyDivLocals)862 TEST(SetTest, computeReprWithOnlyDivLocals) {
863 testComputeReprAtPoints(parsePoly("(x, y) : (x - 2*y == 0)"),
864 {{1, 0}, {2, 1}, {3, 0}, {4, 2}, {5, 3}},
865 /*numToProject=*/0);
866 testComputeReprAtPoints(parsePoly("(x, e) : (x - 2*e == 0)"),
867 {{1}, {2}, {3}, {4}, {5}}, /*numToProject=*/1);
868
869 // Tests to check that the space is preserved.
870 testComputeReprAtPoints(parsePoly("(x, y)[z, w] : ()"), {},
871 /*numToProject=*/1);
872 testComputeReprAtPoints(parsePoly("(x, y)[z, w] : (z - (w floordiv 2) == 0)"),
873 {},
874 /*numToProject=*/1);
875
876 // Bezout's lemma: if a, b are constants,
877 // the set of values that ax + by can take is all multiples of gcd(a, b).
878 testComputeRepr(
879 parsePoly("(x, e, f) : (x - 15*e - 21*f == 0)"),
880 PresburgerSet(parsePoly({"(x) : (x - 3*(x floordiv 3) == 0)"})),
881 /*numToProject=*/2);
882 }
883
TEST(SetTest,subtractOutputSizeRegression)884 TEST(SetTest, subtractOutputSizeRegression) {
885 PresburgerSet set1 =
886 parsePresburgerSetFromPolyStrings(1, {"(i) : (i >= 0, 10 - i >= 0)"});
887 PresburgerSet set2 =
888 parsePresburgerSetFromPolyStrings(1, {"(i) : (i - 5 >= 0)"});
889
890 PresburgerSet set3 =
891 parsePresburgerSetFromPolyStrings(1, {"(i) : (i >= 0, 4 - i >= 0)"});
892
893 PresburgerSet result = set1.subtract(set2);
894
895 EXPECT_TRUE(result.isEqual(set3));
896
897 // Previously, the subtraction result was producing an extra empty set, which
898 // is correct, but bad for output size.
899 EXPECT_EQ(result.getNumDisjuncts(), 1u);
900
901 PresburgerSet subtractSelf = set1.subtract(set1);
902 EXPECT_TRUE(subtractSelf.isIntegerEmpty());
903 // Previously, the subtraction result was producing several unnecessary empty
904 // sets, which is correct, but bad for output size.
905 EXPECT_EQ(subtractSelf.getNumDisjuncts(), 0u);
906 }
907