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

source code of mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp