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. 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. 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. 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. 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. 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 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 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 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 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 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 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 430 void expectEqual(const PresburgerSet &s, const PresburgerSet &t) { 431 EXPECT_TRUE(s.isEqual(t)); 432 } 433 434 void expectEqual(const IntegerPolyhedron &s, const IntegerPolyhedron &t) { 435 EXPECT_TRUE(s.isEqual(t)); 436 } 437 438 void expectEmpty(const PresburgerSet &s) { EXPECT_TRUE(s.isIntegerEmpty()); } 439 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 468 void convertSuffixDimsToLocals(IntegerPolyhedron &poly, unsigned numLocals) { 469 poly.convertVarKind(VarKind::SetDim, poly.getNumDimVars() - numLocals, 470 poly.getNumDimVars(), VarKind::Local); 471 } 472 473 inline IntegerPolyhedron parsePolyAndMakeLocals(StringRef str, 474 unsigned numLocals) { 475 IntegerPolyhedron poly = parsePoly(str); 476 convertSuffixDimsToLocals(poly, numLocals); 477 return poly; 478 } 479 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 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 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. 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 569 TEST(SetTest, coalesceNoPoly) { 570 PresburgerSet set = makeSetFromPoly(0, {}); 571 expectCoalesce(0, set); 572 } 573 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 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 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 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 598 TEST(SetTest, coalesceFirstUniv) { 599 PresburgerSet set = parsePresburgerSetFromPolyStrings( 600 1, {"(x) : ()", "(x) : ( x >= 0, -x + 1 >= 0)"}); 601 expectCoalesce(1, set); 602 } 603 604 TEST(SetTest, coalesceSecondUniv) { 605 PresburgerSet set = parsePresburgerSetFromPolyStrings( 606 1, {"(x) : ( x >= 0, -x + 1 >= 0)", "(x) : ()"}); 607 expectCoalesce(1, set); 608 } 609 610 TEST(SetTest, coalesceBothUniv) { 611 PresburgerSet set = 612 parsePresburgerSetFromPolyStrings(1, {"(x) : ()", "(x) : ()"}); 613 expectCoalesce(1, set); 614 } 615 616 TEST(SetTest, coalesceFirstUnivSecondEmpty) { 617 PresburgerSet set = parsePresburgerSetFromPolyStrings( 618 1, {"(x) : ()", "(x) : ( x >= 0, -x - 1 >= 0)"}); 619 expectCoalesce(1, set); 620 } 621 622 TEST(SetTest, coalesceFirstEmptySecondUniv) { 623 PresburgerSet set = parsePresburgerSetFromPolyStrings( 624 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ()"}); 625 expectCoalesce(1, set); 626 } 627 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 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 643 TEST(SetTest, coalesceAdjEq) { 644 PresburgerSet set = parsePresburgerSetFromPolyStrings( 645 1, {"(x) : ( x == 0)", "(x) : ( x - 1 == 0)"}); 646 expectCoalesce(2, set); 647 } 648 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 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 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 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 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 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 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 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 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 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 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 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 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 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 782 expectComputedVolumeIsValidOverapprox(const PresburgerSet &set, 783 Optional<uint64_t> trueVolume, 784 Optional<uint64_t> resultBound) { 785 expectComputedVolumeIsValidOverapprox(set.computeVolume(), trueVolume, 786 resultBound); 787 } 788 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. 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 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 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 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