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 expectEmpty(const PresburgerSet &s) { EXPECT_TRUE(s.isIntegerEmpty()); } 435 436 TEST(SetTest, divisions) { 437 // evens = {x : exists q, x = 2q}. 438 PresburgerSet evens{parsePoly("(x) : (x - 2 * (x floordiv 2) == 0)")}; 439 440 // odds = {x : exists q, x = 2q + 1}. 441 PresburgerSet odds{parsePoly("(x) : (x - 2 * (x floordiv 2) - 1 == 0)")}; 442 443 // multiples3 = {x : exists q, x = 3q}. 444 PresburgerSet multiples3{parsePoly("(x) : (x - 3 * (x floordiv 3) == 0)")}; 445 446 // multiples6 = {x : exists q, x = 6q}. 447 PresburgerSet multiples6{parsePoly("(x) : (x - 6 * (x floordiv 6) == 0)")}; 448 449 // evens /\ odds = empty. 450 expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds))); 451 // evens U odds = universe. 452 expectEqual(evens.unionSet(odds), 453 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1)))); 454 expectEqual(evens.complement(), odds); 455 expectEqual(odds.complement(), evens); 456 // even multiples of 3 = multiples of 6. 457 expectEqual(multiples3.intersect(evens), multiples6); 458 459 PresburgerSet setA{parsePoly("(x) : (-x >= 0)")}; 460 PresburgerSet setB{parsePoly("(x) : (x floordiv 2 - 4 >= 0)")}; 461 EXPECT_TRUE(setA.subtract(setB).isEqual(setA)); 462 463 IntegerPolyhedron evensDefByEquality(PresburgerSpace::getSetSpace( 464 /*numDims=*/1, /*numSymbols=*/0, /*numLocals=*/1)); 465 evensDefByEquality.addEquality({1, -2, 0}); 466 expectEqual(evens, PresburgerSet(evensDefByEquality)); 467 } 468 469 TEST(SetTest, subtractDuplicateDivsRegression) { 470 // Previously, subtracting sets with duplicate divs might result in crashes 471 // due to existing divs being removed when merging local ids, due to being 472 // identified as being duplicates for the first time. 473 IntegerPolyhedron setA(PresburgerSpace::getSetSpace(1)); 474 setA.addLocalFloorDiv({1, 0}, 2); 475 setA.addLocalFloorDiv({1, 0, 0}, 2); 476 EXPECT_TRUE(setA.isEqual(setA)); 477 } 478 479 /// Coalesce `set` and check that the `newSet` is equal to `set` and that 480 /// `expectedNumPoly` matches the number of Poly in the coalesced set. 481 void expectCoalesce(size_t expectedNumPoly, const PresburgerSet &set) { 482 PresburgerSet newSet = set.coalesce(); 483 EXPECT_TRUE(set.isEqual(newSet)); 484 EXPECT_TRUE(expectedNumPoly == newSet.getNumDisjuncts()); 485 } 486 487 TEST(SetTest, coalesceNoPoly) { 488 PresburgerSet set = makeSetFromPoly(0, {}); 489 expectCoalesce(0, set); 490 } 491 492 TEST(SetTest, coalesceContainedOneDim) { 493 PresburgerSet set = parsePresburgerSetFromPolyStrings( 494 1, {"(x) : (x >= 0, -x + 4 >= 0)", "(x) : (x - 1 >= 0, -x + 2 >= 0)"}); 495 expectCoalesce(1, set); 496 } 497 498 TEST(SetTest, coalesceFirstEmpty) { 499 PresburgerSet set = parsePresburgerSetFromPolyStrings( 500 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ( x - 1 >= 0, -x + 2 >= 0)"}); 501 expectCoalesce(1, set); 502 } 503 504 TEST(SetTest, coalesceSecondEmpty) { 505 PresburgerSet set = parsePresburgerSetFromPolyStrings( 506 1, {"(x) : (x - 1 >= 0, -x + 2 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"}); 507 expectCoalesce(1, set); 508 } 509 510 TEST(SetTest, coalesceBothEmpty) { 511 PresburgerSet set = parsePresburgerSetFromPolyStrings( 512 1, {"(x) : (x - 3 >= 0, -x - 1 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"}); 513 expectCoalesce(0, set); 514 } 515 516 TEST(SetTest, coalesceFirstUniv) { 517 PresburgerSet set = parsePresburgerSetFromPolyStrings( 518 1, {"(x) : ()", "(x) : ( x >= 0, -x + 1 >= 0)"}); 519 expectCoalesce(1, set); 520 } 521 522 TEST(SetTest, coalesceSecondUniv) { 523 PresburgerSet set = parsePresburgerSetFromPolyStrings( 524 1, {"(x) : ( x >= 0, -x + 1 >= 0)", "(x) : ()"}); 525 expectCoalesce(1, set); 526 } 527 528 TEST(SetTest, coalesceBothUniv) { 529 PresburgerSet set = 530 parsePresburgerSetFromPolyStrings(1, {"(x) : ()", "(x) : ()"}); 531 expectCoalesce(1, set); 532 } 533 534 TEST(SetTest, coalesceFirstUnivSecondEmpty) { 535 PresburgerSet set = parsePresburgerSetFromPolyStrings( 536 1, {"(x) : ()", "(x) : ( x >= 0, -x - 1 >= 0)"}); 537 expectCoalesce(1, set); 538 } 539 540 TEST(SetTest, coalesceFirstEmptySecondUniv) { 541 PresburgerSet set = parsePresburgerSetFromPolyStrings( 542 1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ()"}); 543 expectCoalesce(1, set); 544 } 545 546 TEST(SetTest, coalesceCutOneDim) { 547 PresburgerSet set = parsePresburgerSetFromPolyStrings( 548 1, { 549 "(x) : ( x >= 0, -x + 3 >= 0)", 550 "(x) : ( x - 2 >= 0, -x + 4 >= 0)", 551 }); 552 expectCoalesce(1, set); 553 } 554 555 TEST(SetTest, coalesceSeparateOneDim) { 556 PresburgerSet set = parsePresburgerSetFromPolyStrings( 557 1, {"(x) : ( x >= 0, -x + 2 >= 0)", "(x) : ( x - 3 >= 0, -x + 4 >= 0)"}); 558 expectCoalesce(2, set); 559 } 560 561 TEST(SetTest, coalesceAdjEq) { 562 PresburgerSet set = parsePresburgerSetFromPolyStrings( 563 1, {"(x) : ( x == 0)", "(x) : ( x - 1 == 0)"}); 564 expectCoalesce(2, set); 565 } 566 567 TEST(SetTest, coalesceContainedTwoDim) { 568 PresburgerSet set = parsePresburgerSetFromPolyStrings( 569 2, { 570 "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)", 571 "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", 572 }); 573 expectCoalesce(1, set); 574 } 575 576 TEST(SetTest, coalesceCutTwoDim) { 577 PresburgerSet set = parsePresburgerSetFromPolyStrings( 578 2, { 579 "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)", 580 "(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)", 581 }); 582 expectCoalesce(1, set); 583 } 584 585 TEST(SetTest, coalesceEqStickingOut) { 586 PresburgerSet set = parsePresburgerSetFromPolyStrings( 587 2, { 588 "(x,y) : (x >= 0, -x + 2 >= 0, y >= 0, -y + 2 >= 0)", 589 "(x,y) : (y - 1 == 0, x >= 0, -x + 3 >= 0)", 590 }); 591 expectCoalesce(2, set); 592 } 593 594 TEST(SetTest, coalesceSeparateTwoDim) { 595 PresburgerSet set = parsePresburgerSetFromPolyStrings( 596 2, { 597 "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)", 598 "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)", 599 }); 600 expectCoalesce(2, set); 601 } 602 603 TEST(SetTest, coalesceContainedEq) { 604 PresburgerSet set = parsePresburgerSetFromPolyStrings( 605 2, { 606 "(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)", 607 "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", 608 }); 609 expectCoalesce(1, set); 610 } 611 612 TEST(SetTest, coalesceCuttingEq) { 613 PresburgerSet set = parsePresburgerSetFromPolyStrings( 614 2, { 615 "(x,y) : (x + 1 >= 0, -x + 1 >= 0, x - y == 0)", 616 "(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)", 617 }); 618 expectCoalesce(1, set); 619 } 620 621 TEST(SetTest, coalesceSeparateEq) { 622 PresburgerSet set = parsePresburgerSetFromPolyStrings( 623 2, { 624 "(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)", 625 "(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)", 626 }); 627 expectCoalesce(2, set); 628 } 629 630 TEST(SetTest, coalesceContainedEqAsIneq) { 631 PresburgerSet set = parsePresburgerSetFromPolyStrings( 632 2, { 633 "(x,y) : (x >= 0, -x + 3 >= 0, x - y >= 0, -x + y >= 0)", 634 "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", 635 }); 636 expectCoalesce(1, set); 637 } 638 639 TEST(SetTest, coalesceContainedEqComplex) { 640 PresburgerSet set = parsePresburgerSetFromPolyStrings( 641 2, { 642 "(x,y) : (x - 2 == 0, x - y == 0)", 643 "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)", 644 }); 645 expectCoalesce(1, set); 646 } 647 648 TEST(SetTest, coalesceThreeContained) { 649 PresburgerSet set = 650 parsePresburgerSetFromPolyStrings(1, { 651 "(x) : (x >= 0, -x + 1 >= 0)", 652 "(x) : (x >= 0, -x + 2 >= 0)", 653 "(x) : (x >= 0, -x + 3 >= 0)", 654 }); 655 expectCoalesce(1, set); 656 } 657 658 TEST(SetTest, coalesceDoubleIncrement) { 659 PresburgerSet set = parsePresburgerSetFromPolyStrings( 660 1, { 661 "(x) : (x == 0)", 662 "(x) : (x - 2 == 0)", 663 "(x) : (x + 2 == 0)", 664 "(x) : (x - 2 >= 0, -x + 3 >= 0)", 665 }); 666 expectCoalesce(3, set); 667 } 668 669 TEST(SetTest, coalesceLastCoalesced) { 670 PresburgerSet set = parsePresburgerSetFromPolyStrings( 671 1, { 672 "(x) : (x == 0)", 673 "(x) : (x - 1 >= 0, -x + 3 >= 0)", 674 "(x) : (x + 2 == 0)", 675 "(x) : (x - 2 >= 0, -x + 4 >= 0)", 676 }); 677 expectCoalesce(3, set); 678 } 679 680 TEST(SetTest, coalesceDiv) { 681 PresburgerSet set = 682 parsePresburgerSetFromPolyStrings(1, { 683 "(x) : (x floordiv 2 == 0)", 684 "(x) : (x floordiv 2 - 1 == 0)", 685 }); 686 expectCoalesce(2, set); 687 } 688 689 TEST(SetTest, coalesceDivOtherContained) { 690 PresburgerSet set = 691 parsePresburgerSetFromPolyStrings(1, { 692 "(x) : (x floordiv 2 == 0)", 693 "(x) : (x == 0)", 694 "(x) : (x >= 0, -x + 1 >= 0)", 695 }); 696 expectCoalesce(2, set); 697 } 698 699 static void 700 expectComputedVolumeIsValidOverapprox(const PresburgerSet &set, 701 Optional<uint64_t> trueVolume, 702 Optional<uint64_t> resultBound) { 703 expectComputedVolumeIsValidOverapprox(set.computeVolume(), trueVolume, 704 resultBound); 705 } 706 707 TEST(SetTest, computeVolume) { 708 // Diamond with vertices at (0, 0), (5, 5), (5, 5), (10, 0). 709 PresburgerSet diamond( 710 parsePoly("(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0, -x + y + " 711 "10 >= 0)")); 712 expectComputedVolumeIsValidOverapprox(diamond, 713 /*trueVolume=*/61ull, 714 /*resultBound=*/121ull); 715 716 // Diamond with vertices at (-5, 0), (0, -5), (0, 5), (5, 0). 717 PresburgerSet shiftedDiamond(parsePoly( 718 "(x, y) : (x + y + 5 >= 0, -x - y + 5 >= 0, x - y + 5 >= 0, -x + y + " 719 "5 >= 0)")); 720 expectComputedVolumeIsValidOverapprox(shiftedDiamond, 721 /*trueVolume=*/61ull, 722 /*resultBound=*/121ull); 723 724 // Diamond with vertices at (-5, 0), (5, -10), (5, 10), (15, 0). 725 PresburgerSet biggerDiamond(parsePoly( 726 "(x, y) : (x + y + 5 >= 0, -x - y + 15 >= 0, x - y + 5 >= 0, -x + y + " 727 "15 >= 0)")); 728 expectComputedVolumeIsValidOverapprox(biggerDiamond, 729 /*trueVolume=*/221ull, 730 /*resultBound=*/441ull); 731 732 // There is some overlap between diamond and shiftedDiamond. 733 expectComputedVolumeIsValidOverapprox(diamond.unionSet(shiftedDiamond), 734 /*trueVolume=*/104ull, 735 /*resultBound=*/242ull); 736 737 // biggerDiamond subsumes both the small ones. 738 expectComputedVolumeIsValidOverapprox( 739 diamond.unionSet(shiftedDiamond).unionSet(biggerDiamond), 740 /*trueVolume=*/221ull, 741 /*resultBound=*/683ull); 742 743 // Unbounded polytope. 744 PresburgerSet unbounded(parsePoly("(x, y) : (2*x - y >= 0, y - 3*x >= 0)")); 745 expectComputedVolumeIsValidOverapprox(unbounded, /*trueVolume=*/{}, 746 /*resultBound=*/{}); 747 748 // Union of unbounded with bounded is unbounded. 749 expectComputedVolumeIsValidOverapprox(unbounded.unionSet(diamond), 750 /*trueVolume=*/{}, 751 /*resultBound=*/{}); 752 } 753 754 TEST(SetTest, subtractOutputSizeRegression) { 755 PresburgerSet set1 = 756 parsePresburgerSetFromPolyStrings(1, {"(i) : (i >= 0, 10 - i >= 0)"}); 757 PresburgerSet set2 = 758 parsePresburgerSetFromPolyStrings(1, {"(i) : (i - 5 >= 0)"}); 759 760 PresburgerSet set3 = 761 parsePresburgerSetFromPolyStrings(1, {"(i) : (i >= 0, 4 - i >= 0)"}); 762 763 PresburgerSet result = set1.subtract(set2); 764 765 EXPECT_TRUE(result.isEqual(set3)); 766 767 // Previously, the subtraction result was producing an extra empty set, which 768 // is correct, but bad for output size. 769 EXPECT_EQ(result.getNumDisjuncts(), 1u); 770 771 PresburgerSet subtractSelf = set1.subtract(set1); 772 EXPECT_TRUE(subtractSelf.isIntegerEmpty()); 773 // Previously, the subtraction result was producing several unnecessary empty 774 // sets, which is correct, but bad for output size. 775 EXPECT_EQ(subtractSelf.getNumDisjuncts(), 0u); 776 } 777