1 //===- IntegerPolyhedron.cpp - Tests for IntegerPolyhedron class ----------===// 2 // 3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4 // See https://llvm.org/LICENSE.txt for license information. 5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6 // 7 //===----------------------------------------------------------------------===// 8 9 #include "./Utils.h" 10 #include "mlir/Analysis/Presburger/IntegerRelation.h" 11 #include "mlir/Analysis/Presburger/PWMAFunction.h" 12 #include "mlir/Analysis/Presburger/Simplex.h" 13 14 #include <gmock/gmock.h> 15 #include <gtest/gtest.h> 16 17 #include <numeric> 18 19 using namespace mlir; 20 using namespace presburger; 21 22 using testing::ElementsAre; 23 24 enum class TestFunction { Sample, Empty }; 25 26 /// Construct a IntegerPolyhedron from a set of inequality and 27 /// equality constraints. 28 static IntegerPolyhedron 29 makeSetFromConstraints(unsigned ids, ArrayRef<SmallVector<int64_t, 4>> ineqs, 30 ArrayRef<SmallVector<int64_t, 4>> eqs, 31 unsigned syms = 0) { 32 IntegerPolyhedron set( 33 ineqs.size(), eqs.size(), ids + 1, 34 PresburgerSpace::getSetSpace(ids - syms, syms, /*numLocals=*/0)); 35 for (const auto &eq : eqs) 36 set.addEquality(eq); 37 for (const auto &ineq : ineqs) 38 set.addInequality(ineq); 39 return set; 40 } 41 42 static void dump(ArrayRef<int64_t> vec) { 43 for (int64_t x : vec) 44 llvm::errs() << x << ' '; 45 llvm::errs() << '\n'; 46 } 47 48 /// If fn is TestFunction::Sample (default): 49 /// 50 /// If hasSample is true, check that findIntegerSample returns a valid sample 51 /// for the IntegerPolyhedron poly. Also check that getIntegerLexmin finds a 52 /// non-empty lexmin. 53 /// 54 /// If hasSample is false, check that findIntegerSample returns None and 55 /// findIntegerLexMin returns Empty. 56 /// 57 /// If fn is TestFunction::Empty, check that isIntegerEmpty returns the 58 /// opposite of hasSample. 59 static void checkSample(bool hasSample, const IntegerPolyhedron &poly, 60 TestFunction fn = TestFunction::Sample) { 61 Optional<SmallVector<int64_t, 8>> maybeSample; 62 MaybeOptimum<SmallVector<int64_t, 8>> maybeLexMin; 63 switch (fn) { 64 case TestFunction::Sample: 65 maybeSample = poly.findIntegerSample(); 66 maybeLexMin = poly.findIntegerLexMin(); 67 68 if (!hasSample) { 69 EXPECT_FALSE(maybeSample.hasValue()); 70 if (maybeSample.hasValue()) { 71 llvm::errs() << "findIntegerSample gave sample: "; 72 dump(*maybeSample); 73 } 74 75 EXPECT_TRUE(maybeLexMin.isEmpty()); 76 if (maybeLexMin.isBounded()) { 77 llvm::errs() << "findIntegerLexMin gave sample: "; 78 dump(*maybeLexMin); 79 } 80 } else { 81 ASSERT_TRUE(maybeSample.hasValue()); 82 EXPECT_TRUE(poly.containsPoint(*maybeSample)); 83 84 ASSERT_FALSE(maybeLexMin.isEmpty()); 85 if (maybeLexMin.isUnbounded()) { 86 EXPECT_TRUE(Simplex(poly).isUnbounded()); 87 } 88 if (maybeLexMin.isBounded()) { 89 EXPECT_TRUE(poly.containsPoint(*maybeLexMin)); 90 } 91 } 92 break; 93 case TestFunction::Empty: 94 EXPECT_EQ(!hasSample, poly.isIntegerEmpty()); 95 break; 96 } 97 } 98 99 /// Check sampling for all the permutations of the dimensions for the given 100 /// constraint set. Since the GBR algorithm progresses dimension-wise, different 101 /// orderings may cause the algorithm to proceed differently. At least some of 102 ///.these permutations should make it past the heuristics and test the 103 /// implementation of the GBR algorithm itself. 104 /// Use TestFunction fn to test. 105 static void checkPermutationsSample(bool hasSample, unsigned nDim, 106 ArrayRef<SmallVector<int64_t, 4>> ineqs, 107 ArrayRef<SmallVector<int64_t, 4>> eqs, 108 TestFunction fn = TestFunction::Sample) { 109 SmallVector<unsigned, 4> perm(nDim); 110 std::iota(perm.begin(), perm.end(), 0); 111 auto permute = [&perm](ArrayRef<int64_t> coeffs) { 112 SmallVector<int64_t, 4> permuted; 113 for (unsigned id : perm) 114 permuted.push_back(coeffs[id]); 115 permuted.push_back(coeffs.back()); 116 return permuted; 117 }; 118 do { 119 SmallVector<SmallVector<int64_t, 4>, 4> permutedIneqs, permutedEqs; 120 for (const auto &ineq : ineqs) 121 permutedIneqs.push_back(permute(ineq)); 122 for (const auto &eq : eqs) 123 permutedEqs.push_back(permute(eq)); 124 125 checkSample(hasSample, 126 makeSetFromConstraints(nDim, permutedIneqs, permutedEqs), fn); 127 } while (std::next_permutation(perm.begin(), perm.end())); 128 } 129 130 TEST(IntegerPolyhedronTest, removeInequality) { 131 IntegerPolyhedron set = 132 makeSetFromConstraints(1, {{0, 0}, {1, 1}, {2, 2}, {3, 3}, {4, 4}}, {}); 133 134 set.removeInequalityRange(0, 0); 135 EXPECT_EQ(set.getNumInequalities(), 5u); 136 137 set.removeInequalityRange(1, 3); 138 EXPECT_EQ(set.getNumInequalities(), 3u); 139 EXPECT_THAT(set.getInequality(0), ElementsAre(0, 0)); 140 EXPECT_THAT(set.getInequality(1), ElementsAre(3, 3)); 141 EXPECT_THAT(set.getInequality(2), ElementsAre(4, 4)); 142 143 set.removeInequality(1); 144 EXPECT_EQ(set.getNumInequalities(), 2u); 145 EXPECT_THAT(set.getInequality(0), ElementsAre(0, 0)); 146 EXPECT_THAT(set.getInequality(1), ElementsAre(4, 4)); 147 } 148 149 TEST(IntegerPolyhedronTest, removeEquality) { 150 IntegerPolyhedron set = 151 makeSetFromConstraints(1, {}, {{0, 0}, {1, 1}, {2, 2}, {3, 3}, {4, 4}}); 152 153 set.removeEqualityRange(0, 0); 154 EXPECT_EQ(set.getNumEqualities(), 5u); 155 156 set.removeEqualityRange(1, 3); 157 EXPECT_EQ(set.getNumEqualities(), 3u); 158 EXPECT_THAT(set.getEquality(0), ElementsAre(0, 0)); 159 EXPECT_THAT(set.getEquality(1), ElementsAre(3, 3)); 160 EXPECT_THAT(set.getEquality(2), ElementsAre(4, 4)); 161 162 set.removeEquality(1); 163 EXPECT_EQ(set.getNumEqualities(), 2u); 164 EXPECT_THAT(set.getEquality(0), ElementsAre(0, 0)); 165 EXPECT_THAT(set.getEquality(1), ElementsAre(4, 4)); 166 } 167 168 TEST(IntegerPolyhedronTest, clearConstraints) { 169 IntegerPolyhedron set = makeSetFromConstraints(1, {}, {}); 170 171 set.addInequality({1, 0}); 172 EXPECT_EQ(set.atIneq(0, 0), 1); 173 EXPECT_EQ(set.atIneq(0, 1), 0); 174 175 set.clearConstraints(); 176 177 set.addInequality({1, 0}); 178 EXPECT_EQ(set.atIneq(0, 0), 1); 179 EXPECT_EQ(set.atIneq(0, 1), 0); 180 } 181 182 TEST(IntegerPolyhedronTest, removeIdRange) { 183 IntegerPolyhedron set(PresburgerSpace::getSetSpace(3, 2, 1)); 184 185 set.addInequality({10, 11, 12, 20, 21, 30, 40}); 186 set.removeId(IdKind::Symbol, 1); 187 EXPECT_THAT(set.getInequality(0), 188 testing::ElementsAre(10, 11, 12, 20, 30, 40)); 189 190 set.removeIdRange(IdKind::SetDim, 0, 2); 191 EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 30, 40)); 192 193 set.removeIdRange(IdKind::Local, 1, 1); 194 EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 30, 40)); 195 196 set.removeIdRange(IdKind::Local, 0, 1); 197 EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 40)); 198 } 199 200 TEST(IntegerPolyhedronTest, FindSampleTest) { 201 // Bounded sets with only inequalities. 202 // 0 <= 7x <= 5 203 checkSample(true, parsePoly("(x) : (7 * x >= 0, -7 * x + 5 >= 0)")); 204 205 // 1 <= 5x and 5x <= 4 (no solution). 206 checkSample(false, parsePoly("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)")); 207 208 // 1 <= 5x and 5x <= 9 (solution: x = 1). 209 checkSample(true, parsePoly("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)")); 210 211 // Bounded sets with equalities. 212 // x >= 8 and 40 >= y and x = y. 213 checkSample(true, 214 parsePoly("(x,y) : (x - 8 >= 0, -y + 40 >= 0, x - y == 0)")); 215 216 // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z. 217 // solution: x = y = z = 10. 218 checkSample(true, parsePoly("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " 219 "z - 10 >= 0, x + 2 * y - 3 * z == 0)")); 220 221 // x <= 10 and y <= 10 and 11 <= z and x + 2y = 3z. 222 // This implies x + 2y >= 33 and x + 2y <= 30, which has no solution. 223 checkSample(false, parsePoly("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, " 224 "z - 11 >= 0, x + 2 * y - 3 * z == 0)")); 225 226 // 0 <= r and r <= 3 and 4q + r = 7. 227 // Solution: q = 1, r = 3. 228 checkSample(true, 229 parsePoly("(q,r) : (r >= 0, -r + 3 >= 0, 4 * q + r - 7 == 0)")); 230 231 // 4q + r = 7 and r = 0. 232 // Solution: q = 1, r = 3. 233 checkSample(false, parsePoly("(q,r) : (4 * q + r - 7 == 0, r == 0)")); 234 235 // The next two sets are large sets that should take a long time to sample 236 // with a naive branch and bound algorithm but can be sampled efficiently with 237 // the GBR algorithm. 238 // 239 // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (10000, 10000). 240 checkSample(true, parsePoly("(x,y) : (y >= 0, " 241 "300000 * x - 299999 * y - 100000 >= 0, " 242 "-300000 * x + 299998 * y + 200000 >= 0)")); 243 244 // This is a tetrahedron with vertices at 245 // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000). 246 // The first three points form a triangular base on the xz plane with the 247 // apex at the fourth point, which is the only integer point. 248 checkPermutationsSample( 249 true, 3, 250 { 251 {0, 1, 0, 0}, // y >= 0 252 {0, -1, 1, 0}, // z >= y 253 {300000, -299998, -1, 254 -100000}, // -300000x + 299998y + 100000 + z <= 0. 255 {-150000, 149999, 0, 100000}, // -150000x + 149999y + 100000 >= 0. 256 }, 257 {}); 258 259 // Same thing with some spurious extra dimensions equated to constants. 260 checkSample( 261 true, 262 parsePoly("(a,b,c,d,e) : (b + d - e >= 0, -b + c - d + e >= 0, " 263 "300000 * a - 299998 * b - c - 9 * d + 21 * e - 112000 >= 0, " 264 "-150000 * a + 149999 * b - 15 * d + 47 * e + 68000 >= 0, " 265 "d - e == 0, d + e - 2000 == 0)")); 266 267 // This is a tetrahedron with vertices at 268 // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100). 269 checkPermutationsSample(false, 3, 270 { 271 {0, 1, 0, 0}, 272 {0, -300, 299, 0}, 273 {300 * 299, -89400, -299, -100 * 299}, 274 {-897, 894, 0, 598}, 275 }, 276 {}); 277 278 // Two tests involving equalities that are integer empty but not rational 279 // empty. 280 281 // This is a line segment from (0, 1/3) to (100, 100 + 1/3). 282 checkSample( 283 false, 284 parsePoly("(x,y) : (x >= 0, -x + 100 >= 0, 3 * x - 3 * y + 1 == 0)")); 285 286 // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3. 287 checkSample(false, 288 parsePoly("(x,y) : (x >= 0, -x + 100 >= 0, " 289 "3 * x - 3 * y + 2 >= 0, -3 * x + 3 * y - 1 >= 0)")); 290 291 checkSample(true, parsePoly("(x,y) : (2 * x >= 0, -2 * x + 99 >= 0, " 292 "2 * y >= 0, -2 * y + 99 >= 0)")); 293 294 // 2D cone with apex at (10000, 10000) and 295 // edges passing through (1/3, 0) and (2/3, 0). 296 checkSample(true, parsePoly("(x,y) : (300000 * x - 299999 * y - 100000 >= 0, " 297 "-300000 * x + 299998 * y + 200000 >= 0)")); 298 299 // Cartesian product of a tetrahedron and a 2D cone. 300 // The tetrahedron has vertices at 301 // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000). 302 // The first three points form a triangular base on the xz plane with the 303 // apex at the fourth point, which is the only integer point. 304 // The cone has apex at (10000, 10000) and 305 // edges passing through (1/3, 0) and (2/3, 0). 306 checkPermutationsSample( 307 true /* not empty */, 5, 308 { 309 // Tetrahedron contraints: 310 {0, 1, 0, 0, 0, 0}, // y >= 0 311 {0, -1, 1, 0, 0, 0}, // z >= y 312 // -300000x + 299998y + 100000 + z <= 0. 313 {300000, -299998, -1, 0, 0, -100000}, 314 // -150000x + 149999y + 100000 >= 0. 315 {-150000, 149999, 0, 0, 0, 100000}, 316 317 // Triangle constraints: 318 // 300000p - 299999q >= 100000 319 {0, 0, 0, 300000, -299999, -100000}, 320 // -300000p + 299998q + 200000 >= 0 321 {0, 0, 0, -300000, 299998, 200000}, 322 }, 323 {}); 324 325 // Cartesian product of same tetrahedron as above and {(p, q) : 1/3 <= p <= 326 // 2/3}. Since the second set is empty, the whole set is too. 327 checkPermutationsSample( 328 false /* empty */, 5, 329 { 330 // Tetrahedron contraints: 331 {0, 1, 0, 0, 0, 0}, // y >= 0 332 {0, -1, 1, 0, 0, 0}, // z >= y 333 // -300000x + 299998y + 100000 + z <= 0. 334 {300000, -299998, -1, 0, 0, -100000}, 335 // -150000x + 149999y + 100000 >= 0. 336 {-150000, 149999, 0, 0, 0, 100000}, 337 338 // Second set constraints: 339 // 3p >= 1 340 {0, 0, 0, 3, 0, -1}, 341 // 3p <= 2 342 {0, 0, 0, -3, 0, 2}, 343 }, 344 {}); 345 346 // Cartesian product of same tetrahedron as above and 347 // {(p, q, r) : 1 <= p <= 2 and p = 3q + 3r}. 348 // Since the second set is empty, the whole set is too. 349 checkPermutationsSample( 350 false /* empty */, 5, 351 { 352 // Tetrahedron contraints: 353 {0, 1, 0, 0, 0, 0, 0}, // y >= 0 354 {0, -1, 1, 0, 0, 0, 0}, // z >= y 355 // -300000x + 299998y + 100000 + z <= 0. 356 {300000, -299998, -1, 0, 0, 0, -100000}, 357 // -150000x + 149999y + 100000 >= 0. 358 {-150000, 149999, 0, 0, 0, 0, 100000}, 359 360 // Second set constraints: 361 // p >= 1 362 {0, 0, 0, 1, 0, 0, -1}, 363 // p <= 2 364 {0, 0, 0, -1, 0, 0, 2}, 365 }, 366 { 367 {0, 0, 0, 1, -3, -3, 0}, // p = 3q + 3r 368 }); 369 370 // Cartesian product of a tetrahedron and a 2D cone. 371 // The tetrahedron is empty and has vertices at 372 // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), and (100, 100 - 1/3, 100). 373 // The cone has apex at (10000, 10000) and 374 // edges passing through (1/3, 0) and (2/3, 0). 375 // Since the tetrahedron is empty, the Cartesian product is too. 376 checkPermutationsSample(false /* empty */, 5, 377 { 378 // Tetrahedron contraints: 379 {0, 1, 0, 0, 0, 0}, 380 {0, -300, 299, 0, 0, 0}, 381 {300 * 299, -89400, -299, 0, 0, -100 * 299}, 382 {-897, 894, 0, 0, 0, 598}, 383 384 // Triangle constraints: 385 // 300000p - 299999q >= 100000 386 {0, 0, 0, 300000, -299999, -100000}, 387 // -300000p + 299998q + 200000 >= 0 388 {0, 0, 0, -300000, 299998, 200000}, 389 }, 390 {}); 391 392 // Cartesian product of same tetrahedron as above and 393 // {(p, q) : 1/3 <= p <= 2/3}. 394 checkPermutationsSample(false /* empty */, 5, 395 { 396 // Tetrahedron contraints: 397 {0, 1, 0, 0, 0, 0}, 398 {0, -300, 299, 0, 0, 0}, 399 {300 * 299, -89400, -299, 0, 0, -100 * 299}, 400 {-897, 894, 0, 0, 0, 598}, 401 402 // Second set constraints: 403 // 3p >= 1 404 {0, 0, 0, 3, 0, -1}, 405 // 3p <= 2 406 {0, 0, 0, -3, 0, 2}, 407 }, 408 {}); 409 410 checkSample(true, parsePoly("(x, y, z) : (2 * x - 1 >= 0, x - y - 1 == 0, " 411 "y - z == 0)")); 412 413 // Regression tests for the computation of dual coefficients. 414 checkSample(false, parsePoly("(x, y, z) : (" 415 "6*x - 4*y + 9*z + 2 >= 0," 416 "x + 5*y + z + 5 >= 0," 417 "-4*x + y + 2*z - 1 >= 0," 418 "-3*x - 2*y - 7*z - 1 >= 0," 419 "-7*x - 5*y - 9*z - 1 >= 0)")); 420 checkSample(true, parsePoly("(x, y, z) : (" 421 "3*x + 3*y + 3 >= 0," 422 "-4*x - 8*y - z + 4 >= 0," 423 "-7*x - 4*y + z + 1 >= 0," 424 "2*x - 7*y - 8*z - 7 >= 0," 425 "9*x + 8*y - 9*z - 7 >= 0)")); 426 } 427 428 TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) { 429 // 1 <= 5x and 5x <= 4 (no solution). 430 EXPECT_TRUE( 431 parsePoly("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)").isIntegerEmpty()); 432 // 1 <= 5x and 5x <= 9 (solution: x = 1). 433 EXPECT_FALSE( 434 parsePoly("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)").isIntegerEmpty()); 435 436 // Unbounded sets. 437 EXPECT_TRUE(parsePoly("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, " 438 "2 * z - 1 >= 0, 2 * x - 1 == 0)") 439 .isIntegerEmpty()); 440 441 EXPECT_FALSE(parsePoly("(x,y,z) : (2 * x - 1 >= 0, -3 * x + 3 >= 0, " 442 "5 * z - 6 >= 0, -7 * z + 17 >= 0, 3 * y - 2 >= 0)") 443 .isIntegerEmpty()); 444 445 EXPECT_FALSE( 446 parsePoly("(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)") 447 .isIntegerEmpty()); 448 449 // IntegerPolyhedron::isEmpty() does not detect the following sets to be 450 // empty. 451 452 // 3x + 7y = 1 and 0 <= x, y <= 10. 453 // Since x and y are non-negative, 3x + 7y can never be 1. 454 EXPECT_TRUE(parsePoly("(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, " 455 "3 * x + 7 * y - 1 == 0)") 456 .isIntegerEmpty()); 457 458 // 2x = 3y and y = x - 1 and x + y = 6z + 2 and 0 <= x, y <= 100. 459 // Substituting y = x - 1 in 3y = 2x, we obtain x = 3 and hence y = 2. 460 // Since x + y = 5 cannot be equal to 6z + 2 for any z, the set is empty. 461 EXPECT_TRUE( 462 parsePoly("(x,y,z) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, " 463 "2 * x - 3 * y == 0, x - y - 1 == 0, x + y - 6 * z - 2 == 0)") 464 .isIntegerEmpty()); 465 466 // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100. 467 // 2x = 3y implies x is a multiple of 3 and y is even. 468 // Now y = x - 1 + 6z implies y = 2 mod 3. In fact, since y is even, we have 469 // y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying 470 // x + y = 5 mod 6, which contradicts x + y = 6q + 2, so the set is empty. 471 EXPECT_TRUE( 472 parsePoly( 473 "(x,y,z,q) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, " 474 "2 * x - 3 * y == 0, x - y + 6 * z - 1 == 0, x + y - 6 * q - 2 == 0)") 475 .isIntegerEmpty()); 476 477 // Set with symbols. 478 EXPECT_FALSE(parsePoly("(x)[s] : (x + s >= 0, x - s == 0)").isIntegerEmpty()); 479 } 480 481 TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) { 482 IntegerPolyhedron poly = 483 parsePoly("(x) : (x - 2 >= 0, -x + 2 >= 0, x - 2 == 0)"); 484 poly.removeRedundantConstraints(); 485 486 // Both inequalities are redundant given the equality. Both have been removed. 487 EXPECT_EQ(poly.getNumInequalities(), 0u); 488 EXPECT_EQ(poly.getNumEqualities(), 1u); 489 490 IntegerPolyhedron poly2 = 491 parsePoly("(x,y) : (x - 3 >= 0, y - 2 >= 0, x - y == 0)"); 492 poly2.removeRedundantConstraints(); 493 494 // The second inequality is redundant and should have been removed. The 495 // remaining inequality should be the first one. 496 EXPECT_EQ(poly2.getNumInequalities(), 1u); 497 EXPECT_THAT(poly2.getInequality(0), ElementsAre(1, 0, -3)); 498 EXPECT_EQ(poly2.getNumEqualities(), 1u); 499 500 IntegerPolyhedron poly3 = 501 parsePoly("(x,y,z) : (x - y == 0, x - z == 0, y - z == 0)"); 502 poly3.removeRedundantConstraints(); 503 504 // One of the three equalities can be removed. 505 EXPECT_EQ(poly3.getNumInequalities(), 0u); 506 EXPECT_EQ(poly3.getNumEqualities(), 2u); 507 508 IntegerPolyhedron poly4 = 509 parsePoly("(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) : (" 510 "b - 1 >= 0," 511 "-b + 500 >= 0," 512 "-16 * d + f >= 0," 513 "f - 1 >= 0," 514 "-f + 998 >= 0," 515 "16 * d - f + 15 >= 0," 516 "-16 * e + g >= 0," 517 "g - 1 >= 0," 518 "-g + 998 >= 0," 519 "16 * e - g + 15 >= 0," 520 "h >= 0," 521 "-h + 1 >= 0," 522 "j - 1 >= 0," 523 "-j + 500 >= 0," 524 "-f + 16 * l + 15 >= 0," 525 "f - 16 * l >= 0," 526 "-16 * m + o >= 0," 527 "o - 1 >= 0," 528 "-o + 998 >= 0," 529 "16 * m - o + 15 >= 0," 530 "p >= 0," 531 "-p + 1 >= 0," 532 "-g - h + 8 * q + 8 >= 0," 533 "-o - p + 8 * q + 8 >= 0," 534 "o + p - 8 * q - 1 >= 0," 535 "g + h - 8 * q - 1 >= 0," 536 "-f + n >= 0," 537 "f - n >= 0," 538 "k - 10 >= 0," 539 "-k + 10 >= 0," 540 "i - 13 >= 0," 541 "-i + 13 >= 0," 542 "c - 10 >= 0," 543 "-c + 10 >= 0," 544 "a - 13 >= 0," 545 "-a + 13 >= 0" 546 ")"); 547 548 // The above is a large set of constraints without any redundant constraints, 549 // as verified by the Fourier-Motzkin based removeRedundantInequalities. 550 unsigned nIneq = poly4.getNumInequalities(); 551 unsigned nEq = poly4.getNumEqualities(); 552 poly4.removeRedundantInequalities(); 553 ASSERT_EQ(poly4.getNumInequalities(), nIneq); 554 ASSERT_EQ(poly4.getNumEqualities(), nEq); 555 // Now we test that removeRedundantConstraints does not find any constraints 556 // to be redundant either. 557 poly4.removeRedundantConstraints(); 558 EXPECT_EQ(poly4.getNumInequalities(), nIneq); 559 EXPECT_EQ(poly4.getNumEqualities(), nEq); 560 561 IntegerPolyhedron poly5 = parsePoly( 562 "(x,y) : (128 * x + 127 >= 0, -x + 7 >= 0, -128 * x + y >= 0, y >= 0)"); 563 // 128x + 127 >= 0 implies that 128x >= 0, since x has to be an integer. 564 // (This should be caught by GCDTightenInqualities().) 565 // So -128x + y >= 0 and 128x + 127 >= 0 imply y >= 0 since we have 566 // y >= 128x >= 0. 567 poly5.removeRedundantConstraints(); 568 EXPECT_EQ(poly5.getNumInequalities(), 3u); 569 SmallVector<int64_t, 8> redundantConstraint = {0, 1, 0}; 570 for (unsigned i = 0; i < 3; ++i) { 571 // Ensure that the removed constraint was the redundant constraint [3]. 572 EXPECT_NE(poly5.getInequality(i), ArrayRef<int64_t>(redundantConstraint)); 573 } 574 } 575 576 TEST(IntegerPolyhedronTest, addConstantUpperBound) { 577 IntegerPolyhedron poly(PresburgerSpace::getSetSpace(2)); 578 poly.addBound(IntegerPolyhedron::UB, 0, 1); 579 EXPECT_EQ(poly.atIneq(0, 0), -1); 580 EXPECT_EQ(poly.atIneq(0, 1), 0); 581 EXPECT_EQ(poly.atIneq(0, 2), 1); 582 583 poly.addBound(IntegerPolyhedron::UB, {1, 2, 3}, 1); 584 EXPECT_EQ(poly.atIneq(1, 0), -1); 585 EXPECT_EQ(poly.atIneq(1, 1), -2); 586 EXPECT_EQ(poly.atIneq(1, 2), -2); 587 } 588 589 TEST(IntegerPolyhedronTest, addConstantLowerBound) { 590 IntegerPolyhedron poly(PresburgerSpace::getSetSpace(2)); 591 poly.addBound(IntegerPolyhedron::LB, 0, 1); 592 EXPECT_EQ(poly.atIneq(0, 0), 1); 593 EXPECT_EQ(poly.atIneq(0, 1), 0); 594 EXPECT_EQ(poly.atIneq(0, 2), -1); 595 596 poly.addBound(IntegerPolyhedron::LB, {1, 2, 3}, 1); 597 EXPECT_EQ(poly.atIneq(1, 0), 1); 598 EXPECT_EQ(poly.atIneq(1, 1), 2); 599 EXPECT_EQ(poly.atIneq(1, 2), 2); 600 } 601 602 /// Check if the expected division representation of local variables matches the 603 /// computed representation. The expected division representation is given as 604 /// a vector of expressions set in `expectedDividends` and the corressponding 605 /// denominator in `expectedDenominators`. The `denominators` and `dividends` 606 /// obtained through `getLocalRepr` function is verified against the 607 /// `expectedDenominators` and `expectedDividends` respectively. 608 static void checkDivisionRepresentation( 609 IntegerPolyhedron &poly, 610 const std::vector<SmallVector<int64_t, 8>> &expectedDividends, 611 const SmallVectorImpl<unsigned> &expectedDenominators) { 612 std::vector<SmallVector<int64_t, 8>> dividends; 613 SmallVector<unsigned, 4> denominators; 614 615 poly.getLocalReprs(dividends, denominators); 616 617 // Check that the `denominators` and `expectedDenominators` match. 618 EXPECT_TRUE(expectedDenominators == denominators); 619 620 // Check that the `dividends` and `expectedDividends` match. If the 621 // denominator for a division is zero, we ignore its dividend. 622 EXPECT_TRUE(dividends.size() == expectedDividends.size()); 623 for (unsigned i = 0, e = dividends.size(); i < e; ++i) { 624 if (denominators[i] != 0) { 625 EXPECT_TRUE(expectedDividends[i] == dividends[i]); 626 } 627 } 628 } 629 630 TEST(IntegerPolyhedronTest, computeLocalReprSimple) { 631 IntegerPolyhedron poly(PresburgerSpace::getSetSpace(1)); 632 633 poly.addLocalFloorDiv({1, 4}, 10); 634 poly.addLocalFloorDiv({1, 0, 100}, 10); 635 636 std::vector<SmallVector<int64_t, 8>> divisions = {{1, 0, 0, 4}, 637 {1, 0, 0, 100}}; 638 SmallVector<unsigned, 8> denoms = {10, 10}; 639 640 // Check if floordivs can be computed when no other inequalities exist 641 // and floor divs do not depend on each other. 642 checkDivisionRepresentation(poly, divisions, denoms); 643 } 644 645 TEST(IntegerPolyhedronTest, computeLocalReprConstantFloorDiv) { 646 IntegerPolyhedron poly(PresburgerSpace::getSetSpace(4)); 647 648 poly.addInequality({1, 0, 3, 1, 2}); 649 poly.addInequality({1, 2, -8, 1, 10}); 650 poly.addEquality({1, 2, -4, 1, 10}); 651 652 poly.addLocalFloorDiv({0, 0, 0, 0, 100}, 30); 653 poly.addLocalFloorDiv({0, 0, 0, 0, 0, 206}, 101); 654 655 std::vector<SmallVector<int64_t, 8>> divisions = {{0, 0, 0, 0, 0, 0, 3}, 656 {0, 0, 0, 0, 0, 0, 2}}; 657 SmallVector<unsigned, 8> denoms = {1, 1}; 658 659 // Check if floordivs with constant numerator can be computed. 660 checkDivisionRepresentation(poly, divisions, denoms); 661 } 662 663 TEST(IntegerPolyhedronTest, computeLocalReprRecursive) { 664 IntegerPolyhedron poly(PresburgerSpace::getSetSpace(4)); 665 poly.addInequality({1, 0, 3, 1, 2}); 666 poly.addInequality({1, 2, -8, 1, 10}); 667 poly.addEquality({1, 2, -4, 1, 10}); 668 669 poly.addLocalFloorDiv({0, -2, 7, 2, 10}, 3); 670 poly.addLocalFloorDiv({3, 0, 9, 2, 2, 10}, 5); 671 poly.addLocalFloorDiv({0, 1, -123, 2, 0, -4, 10}, 3); 672 673 poly.addInequality({1, 2, -2, 1, -5, 0, 6, 100}); 674 poly.addInequality({1, 2, -8, 1, 3, 7, 0, -9}); 675 676 std::vector<SmallVector<int64_t, 8>> divisions = { 677 {0, -2, 7, 2, 0, 0, 0, 10}, 678 {3, 0, 9, 2, 2, 0, 0, 10}, 679 {0, 1, -123, 2, 0, -4, 0, 10}}; 680 681 SmallVector<unsigned, 8> denoms = {3, 5, 3}; 682 683 // Check if floordivs which may depend on other floordivs can be computed. 684 checkDivisionRepresentation(poly, divisions, denoms); 685 } 686 687 TEST(IntegerPolyhedronTest, computeLocalReprTightUpperBound) { 688 { 689 IntegerPolyhedron poly = parsePoly("(i) : (i mod 3 - 1 >= 0)"); 690 691 // The set formed by the poly is: 692 // 3q - i + 2 >= 0 <-- Division lower bound 693 // -3q + i - 1 >= 0 694 // -3q + i >= 0 <-- Division upper bound 695 // We remove redundant constraints to get the set: 696 // 3q - i + 2 >= 0 <-- Division lower bound 697 // -3q + i - 1 >= 0 <-- Tighter division upper bound 698 // thus, making the upper bound tighter. 699 poly.removeRedundantConstraints(); 700 701 std::vector<SmallVector<int64_t, 8>> divisions = {{1, 0, 0}}; 702 SmallVector<unsigned, 8> denoms = {3}; 703 704 // Check if the divisions can be computed even with a tighter upper bound. 705 checkDivisionRepresentation(poly, divisions, denoms); 706 } 707 708 { 709 IntegerPolyhedron poly = 710 parsePoly("(i, j, q) : (4*q - i - j + 2 >= 0, -4*q + i + j >= 0)"); 711 // Convert `q` to a local variable. 712 poly.convertToLocal(IdKind::SetDim, 2, 3); 713 714 std::vector<SmallVector<int64_t, 8>> divisions = {{1, 1, 0, 1}}; 715 SmallVector<unsigned, 8> denoms = {4}; 716 717 // Check if the divisions can be computed even with a tighter upper bound. 718 checkDivisionRepresentation(poly, divisions, denoms); 719 } 720 } 721 722 TEST(IntegerPolyhedronTest, computeLocalReprFromEquality) { 723 { 724 IntegerPolyhedron poly = parsePoly("(i, j, q) : (-4*q + i + j == 0)"); 725 // Convert `q` to a local variable. 726 poly.convertToLocal(IdKind::SetDim, 2, 3); 727 728 std::vector<SmallVector<int64_t, 8>> divisions = {{1, 1, 0, 0}}; 729 SmallVector<unsigned, 8> denoms = {4}; 730 731 checkDivisionRepresentation(poly, divisions, denoms); 732 } 733 { 734 IntegerPolyhedron poly = parsePoly("(i, j, q) : (4*q - i - j == 0)"); 735 // Convert `q` to a local variable. 736 poly.convertToLocal(IdKind::SetDim, 2, 3); 737 738 std::vector<SmallVector<int64_t, 8>> divisions = {{1, 1, 0, 0}}; 739 SmallVector<unsigned, 8> denoms = {4}; 740 741 checkDivisionRepresentation(poly, divisions, denoms); 742 } 743 { 744 IntegerPolyhedron poly = parsePoly("(i, j, q) : (3*q + i + j - 2 == 0)"); 745 // Convert `q` to a local variable. 746 poly.convertToLocal(IdKind::SetDim, 2, 3); 747 748 std::vector<SmallVector<int64_t, 8>> divisions = {{-1, -1, 0, 2}}; 749 SmallVector<unsigned, 8> denoms = {3}; 750 751 checkDivisionRepresentation(poly, divisions, denoms); 752 } 753 } 754 755 TEST(IntegerPolyhedronTest, computeLocalReprFromEqualityAndInequality) { 756 { 757 IntegerPolyhedron poly = 758 parsePoly("(i, j, q, k) : (-3*k + i + j == 0, 4*q - " 759 "i - j + 2 >= 0, -4*q + i + j >= 0)"); 760 // Convert `q` and `k` to local variables. 761 poly.convertToLocal(IdKind::SetDim, 2, 4); 762 763 std::vector<SmallVector<int64_t, 8>> divisions = {{1, 1, 0, 0, 1}, 764 {1, 1, 0, 0, 0}}; 765 SmallVector<unsigned, 8> denoms = {4, 3}; 766 767 checkDivisionRepresentation(poly, divisions, denoms); 768 } 769 } 770 771 TEST(IntegerPolyhedronTest, computeLocalReprNoRepr) { 772 IntegerPolyhedron poly = 773 parsePoly("(x, q) : (x - 3 * q >= 0, -x + 3 * q + 3 >= 0)"); 774 // Convert q to a local variable. 775 poly.convertToLocal(IdKind::SetDim, 1, 2); 776 777 std::vector<SmallVector<int64_t, 8>> divisions = {{0, 0, 0}}; 778 SmallVector<unsigned, 8> denoms = {0}; 779 780 // Check that no division is computed. 781 checkDivisionRepresentation(poly, divisions, denoms); 782 } 783 784 TEST(IntegerPolyhedronTest, computeLocalReprNegConstNormalize) { 785 IntegerPolyhedron poly = 786 parsePoly("(x, q) : (-1 - 3*x - 6 * q >= 0, 6 + 3*x + 6*q >= 0)"); 787 // Convert q to a local variable. 788 poly.convertToLocal(IdKind::SetDim, 1, 2); 789 790 // q = floor((-1/3 - x)/2) 791 // = floor((1/3) + (-1 - x)/2) 792 // = floor((-1 - x)/2). 793 std::vector<SmallVector<int64_t, 8>> divisions = {{-1, 0, -1}}; 794 SmallVector<unsigned, 8> denoms = {2}; 795 checkDivisionRepresentation(poly, divisions, denoms); 796 } 797 798 TEST(IntegerPolyhedronTest, simplifyLocalsTest) { 799 // (x) : (exists y: 2x + y = 1 and y = 2). 800 IntegerPolyhedron poly(PresburgerSpace::getSetSpace(1, 0, 1)); 801 poly.addEquality({2, 1, -1}); 802 poly.addEquality({0, 1, -2}); 803 804 EXPECT_TRUE(poly.isEmpty()); 805 806 // (x) : (exists y, z, w: 3x + y = 1 and 2y = z and 3y = w and z = w). 807 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1, 0, 3)); 808 poly2.addEquality({3, 1, 0, 0, -1}); 809 poly2.addEquality({0, 2, -1, 0, 0}); 810 poly2.addEquality({0, 3, 0, -1, 0}); 811 poly2.addEquality({0, 0, 1, -1, 0}); 812 813 EXPECT_TRUE(poly2.isEmpty()); 814 815 // (x) : (exists y: x >= y + 1 and 2x + y = 0 and y >= -1). 816 IntegerPolyhedron poly3(PresburgerSpace::getSetSpace(1, 0, 1)); 817 poly3.addInequality({1, -1, -1}); 818 poly3.addInequality({0, 1, 1}); 819 poly3.addEquality({2, 1, 0}); 820 821 EXPECT_TRUE(poly3.isEmpty()); 822 } 823 824 TEST(IntegerPolyhedronTest, mergeDivisionsSimple) { 825 { 826 // (x) : (exists z, y = [x / 2] : x = 3y and x + z + 1 >= 0). 827 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1, 0, 1)); 828 poly1.addLocalFloorDiv({1, 0, 0}, 2); // y = [x / 2]. 829 poly1.addEquality({1, 0, -3, 0}); // x = 3y. 830 poly1.addInequality({1, 1, 0, 1}); // x + z + 1 >= 0. 831 832 // (x) : (exists y = [x / 2], z : x = 5y). 833 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 834 poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2]. 835 poly2.addEquality({1, -5, 0}); // x = 5y. 836 poly2.appendId(IdKind::Local); // Add local id z. 837 838 poly1.mergeLocalIds(poly2); 839 840 // Local space should be same. 841 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 842 843 // 1 division should be matched + 2 unmatched local ids. 844 EXPECT_EQ(poly1.getNumLocalIds(), 3u); 845 EXPECT_EQ(poly2.getNumLocalIds(), 3u); 846 } 847 848 { 849 // (x) : (exists z = [x / 5], y = [x / 2] : x = 3y). 850 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1)); 851 poly1.addLocalFloorDiv({1, 0}, 5); // z = [x / 5]. 852 poly1.addLocalFloorDiv({1, 0, 0}, 2); // y = [x / 2]. 853 poly1.addEquality({1, 0, -3, 0}); // x = 3y. 854 855 // (x) : (exists y = [x / 2], z = [x / 5]: x = 5z). 856 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 857 poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2]. 858 poly2.addLocalFloorDiv({1, 0, 0}, 5); // z = [x / 5]. 859 poly2.addEquality({1, 0, -5, 0}); // x = 5z. 860 861 poly1.mergeLocalIds(poly2); 862 863 // Local space should be same. 864 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 865 866 // 2 divisions should be matched. 867 EXPECT_EQ(poly1.getNumLocalIds(), 2u); 868 EXPECT_EQ(poly2.getNumLocalIds(), 2u); 869 } 870 871 { 872 // Division Normalization test. 873 // (x) : (exists z, y = [x / 2] : x = 3y and x + z + 1 >= 0). 874 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1, 0, 1)); 875 // This division would be normalized. 876 poly1.addLocalFloorDiv({3, 0, 0}, 6); // y = [3x / 6] -> [x/2]. 877 poly1.addEquality({1, 0, -3, 0}); // x = 3z. 878 poly1.addInequality({1, 1, 0, 1}); // x + y + 1 >= 0. 879 880 // (x) : (exists y = [x / 2], z : x = 5y). 881 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 882 poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2]. 883 poly2.addEquality({1, -5, 0}); // x = 5y. 884 poly2.appendId(IdKind::Local); // Add local id z. 885 886 poly1.mergeLocalIds(poly2); 887 888 // Local space should be same. 889 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 890 891 // One division should be matched + 2 unmatched local ids. 892 EXPECT_EQ(poly1.getNumLocalIds(), 3u); 893 EXPECT_EQ(poly2.getNumLocalIds(), 3u); 894 } 895 } 896 897 TEST(IntegerPolyhedronTest, mergeDivisionsNestedDivsions) { 898 { 899 // (x) : (exists y = [x / 2], z = [x + y / 3]: y + z >= x). 900 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1)); 901 poly1.addLocalFloorDiv({1, 0}, 2); // y = [x / 2]. 902 poly1.addLocalFloorDiv({1, 1, 0}, 3); // z = [x + y / 3]. 903 poly1.addInequality({-1, 1, 1, 0}); // y + z >= x. 904 905 // (x) : (exists y = [x / 2], z = [x + y / 3]: y + z <= x). 906 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 907 poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2]. 908 poly2.addLocalFloorDiv({1, 1, 0}, 3); // z = [x + y / 3]. 909 poly2.addInequality({1, -1, -1, 0}); // y + z <= x. 910 911 poly1.mergeLocalIds(poly2); 912 913 // Local space should be same. 914 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 915 916 // 2 divisions should be matched. 917 EXPECT_EQ(poly1.getNumLocalIds(), 2u); 918 EXPECT_EQ(poly2.getNumLocalIds(), 2u); 919 } 920 921 { 922 // (x) : (exists y = [x / 2], z = [x + y / 3], w = [z + 1 / 5]: y + z >= x). 923 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1)); 924 poly1.addLocalFloorDiv({1, 0}, 2); // y = [x / 2]. 925 poly1.addLocalFloorDiv({1, 1, 0}, 3); // z = [x + y / 3]. 926 poly1.addLocalFloorDiv({0, 0, 1, 1}, 5); // w = [z + 1 / 5]. 927 poly1.addInequality({-1, 1, 1, 0, 0}); // y + z >= x. 928 929 // (x) : (exists y = [x / 2], z = [x + y / 3], w = [z + 1 / 5]: y + z <= x). 930 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 931 poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2]. 932 poly2.addLocalFloorDiv({1, 1, 0}, 3); // z = [x + y / 3]. 933 poly2.addLocalFloorDiv({0, 0, 1, 1}, 5); // w = [z + 1 / 5]. 934 poly2.addInequality({1, -1, -1, 0, 0}); // y + z <= x. 935 936 poly1.mergeLocalIds(poly2); 937 938 // Local space should be same. 939 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 940 941 // 3 divisions should be matched. 942 EXPECT_EQ(poly1.getNumLocalIds(), 3u); 943 EXPECT_EQ(poly2.getNumLocalIds(), 3u); 944 } 945 { 946 // (x) : (exists y = [x / 2], z = [x + y / 3]: y + z >= x). 947 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1)); 948 poly1.addLocalFloorDiv({2, 0}, 4); // y = [2x / 4] -> [x / 2]. 949 poly1.addLocalFloorDiv({1, 1, 0}, 3); // z = [x + y / 3]. 950 poly1.addInequality({-1, 1, 1, 0}); // y + z >= x. 951 952 // (x) : (exists y = [x / 2], z = [x + y / 3]: y + z <= x). 953 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 954 poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2]. 955 // This division would be normalized. 956 poly2.addLocalFloorDiv({3, 3, 0}, 9); // z = [3x + 3y / 9] -> [x + y / 3]. 957 poly2.addInequality({1, -1, -1, 0}); // y + z <= x. 958 959 poly1.mergeLocalIds(poly2); 960 961 // Local space should be same. 962 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 963 964 // 2 divisions should be matched. 965 EXPECT_EQ(poly1.getNumLocalIds(), 2u); 966 EXPECT_EQ(poly2.getNumLocalIds(), 2u); 967 } 968 } 969 970 TEST(IntegerPolyhedronTest, mergeDivisionsConstants) { 971 { 972 // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z >= x). 973 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1)); 974 poly1.addLocalFloorDiv({1, 1}, 2); // y = [x + 1 / 2]. 975 poly1.addLocalFloorDiv({1, 0, 2}, 3); // z = [x + 2 / 3]. 976 poly1.addInequality({-1, 1, 1, 0}); // y + z >= x. 977 978 // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x). 979 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 980 poly2.addLocalFloorDiv({1, 1}, 2); // y = [x + 1 / 2]. 981 poly2.addLocalFloorDiv({1, 0, 2}, 3); // z = [x + 2 / 3]. 982 poly2.addInequality({1, -1, -1, 0}); // y + z <= x. 983 984 poly1.mergeLocalIds(poly2); 985 986 // Local space should be same. 987 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 988 989 // 2 divisions should be matched. 990 EXPECT_EQ(poly1.getNumLocalIds(), 2u); 991 EXPECT_EQ(poly2.getNumLocalIds(), 2u); 992 } 993 { 994 // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z >= x). 995 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1)); 996 poly1.addLocalFloorDiv({1, 1}, 2); // y = [x + 1 / 2]. 997 // Normalization test. 998 poly1.addLocalFloorDiv({3, 0, 6}, 9); // z = [3x + 6 / 9] -> [x + 2 / 3]. 999 poly1.addInequality({-1, 1, 1, 0}); // y + z >= x. 1000 1001 // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x). 1002 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 1003 // Normalization test. 1004 poly2.addLocalFloorDiv({2, 2}, 4); // y = [2x + 2 / 4] -> [x + 1 / 2]. 1005 poly2.addLocalFloorDiv({1, 0, 2}, 3); // z = [x + 2 / 3]. 1006 poly2.addInequality({1, -1, -1, 0}); // y + z <= x. 1007 1008 poly1.mergeLocalIds(poly2); 1009 1010 // Local space should be same. 1011 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 1012 1013 // 2 divisions should be matched. 1014 EXPECT_EQ(poly1.getNumLocalIds(), 2u); 1015 EXPECT_EQ(poly2.getNumLocalIds(), 2u); 1016 } 1017 } 1018 1019 TEST(IntegerPolyhedronTest, mergeDivisionsDuplicateInSameSet) { 1020 // (x) : (exists y = [x + 1 / 3], z = [x + 1 / 3]: y + z >= x). 1021 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1)); 1022 poly1.addLocalFloorDiv({1, 1}, 3); // y = [x + 1 / 2]. 1023 poly1.addLocalFloorDiv({1, 0, 1}, 3); // z = [x + 1 / 3]. 1024 poly1.addInequality({-1, 1, 1, 0}); // y + z >= x. 1025 1026 // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x). 1027 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 1028 poly2.addLocalFloorDiv({1, 1}, 3); // y = [x + 1 / 3]. 1029 poly2.addLocalFloorDiv({1, 0, 2}, 3); // z = [x + 2 / 3]. 1030 poly2.addInequality({1, -1, -1, 0}); // y + z <= x. 1031 1032 poly1.mergeLocalIds(poly2); 1033 1034 // Local space should be same. 1035 EXPECT_EQ(poly1.getNumLocalIds(), poly2.getNumLocalIds()); 1036 1037 // 1 divisions should be matched. 1038 EXPECT_EQ(poly1.getNumLocalIds(), 3u); 1039 EXPECT_EQ(poly2.getNumLocalIds(), 3u); 1040 } 1041 1042 TEST(IntegerPolyhedronTest, negativeDividends) { 1043 // (x) : (exists y = [-x + 1 / 2], z = [-x - 2 / 3]: y + z >= x). 1044 IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1)); 1045 poly1.addLocalFloorDiv({-1, 1}, 2); // y = [x + 1 / 2]. 1046 // Normalization test with negative dividends 1047 poly1.addLocalFloorDiv({-3, 0, -6}, 9); // z = [3x + 6 / 9] -> [x + 2 / 3]. 1048 poly1.addInequality({-1, 1, 1, 0}); // y + z >= x. 1049 1050 // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x). 1051 IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1)); 1052 // Normalization test. 1053 poly2.addLocalFloorDiv({-2, 2}, 4); // y = [-2x + 2 / 4] -> [-x + 1 / 2]. 1054 poly2.addLocalFloorDiv({-1, 0, -2}, 3); // z = [-x - 2 / 3]. 1055 poly2.addInequality({1, -1, -1, 0}); // y + z <= x. 1056 1057 poly1.mergeLocalIds(poly2); 1058 1059 // Merging triggers normalization. 1060 std::vector<SmallVector<int64_t, 8>> divisions = {{-1, 0, 0, 1}, 1061 {-1, 0, 0, -2}}; 1062 SmallVector<unsigned, 8> denoms = {2, 3}; 1063 checkDivisionRepresentation(poly1, divisions, denoms); 1064 } 1065 1066 void expectRationalLexMin(const IntegerPolyhedron &poly, 1067 ArrayRef<Fraction> min) { 1068 auto lexMin = poly.findRationalLexMin(); 1069 ASSERT_TRUE(lexMin.isBounded()); 1070 EXPECT_EQ(ArrayRef<Fraction>(*lexMin), min); 1071 } 1072 1073 void expectNoRationalLexMin(OptimumKind kind, const IntegerPolyhedron &poly) { 1074 ASSERT_NE(kind, OptimumKind::Bounded) 1075 << "Use expectRationalLexMin for bounded min"; 1076 EXPECT_EQ(poly.findRationalLexMin().getKind(), kind); 1077 } 1078 1079 TEST(IntegerPolyhedronTest, findRationalLexMin) { 1080 expectRationalLexMin( 1081 parsePoly("(x, y, z) : (x + 10 >= 0, y + 40 >= 0, z + 30 >= 0)"), 1082 {{-10, 1}, {-40, 1}, {-30, 1}}); 1083 expectRationalLexMin( 1084 parsePoly( 1085 "(x, y, z) : (2*x + 7 >= 0, 3*y - 5 >= 0, 8*z + 10 >= 0, 9*z >= 0)"), 1086 {{-7, 2}, {5, 3}, {0, 1}}); 1087 expectRationalLexMin(parsePoly("(x, y) : (3*x + 2*y + 10 >= 0, -3*y + 10 >= " 1088 "0, 4*x - 7*y - 10 >= 0)"), 1089 {{-50, 29}, {-70, 29}}); 1090 1091 // Test with some locals. This is basically x >= 11, 0 <= x - 2e <= 1. 1092 // It'll just choose x = 11, e = 5.5 since it's rational lexmin. 1093 expectRationalLexMin( 1094 parsePoly( 1095 "(x, y) : (x - 2*(x floordiv 2) == 0, y - 2*x >= 0, x - 11 >= 0)"), 1096 {{11, 1}, {22, 1}}); 1097 1098 expectRationalLexMin(parsePoly("(x, y) : (3*x + 2*y + 10 >= 0," 1099 "-4*x + 7*y + 10 >= 0, -3*y + 10 >= 0)"), 1100 {{-50, 9}, {10, 3}}); 1101 1102 // Cartesian product of above with itself. 1103 expectRationalLexMin( 1104 parsePoly("(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0," 1105 "-3*y + 10 >= 0, 3*z + 2*w + 10 >= 0, -4*z + 7*w + 10 >= 0," 1106 "-3*w + 10 >= 0)"), 1107 {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}}); 1108 1109 // Same as above but for the constraints on z and w, we express "10" in terms 1110 // of x and y. We know that x and y still have to take the values 1111 // -50/9 and 10/3 since their constraints are the same and their values are 1112 // minimized first. Accordingly, the values -9x - 12y, -9x - 0y - 10, 1113 // and -9x - 15y + 10 are all equal to 10. 1114 expectRationalLexMin( 1115 parsePoly( 1116 "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0, " 1117 "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0," 1118 "-4*z + 7*w + - 9*x - 9*y - 10 >= 0, -3*w - 9*x - 15*y + 10 >= 0)"), 1119 {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}}); 1120 1121 // Same as above with one constraint removed, making the lexmin unbounded. 1122 expectNoRationalLexMin( 1123 OptimumKind::Unbounded, 1124 parsePoly("(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0," 1125 "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0," 1126 "-4*z + 7*w + - 9*x - 9*y - 10>= 0)")); 1127 1128 // Again, the lexmin is unbounded. 1129 expectNoRationalLexMin( 1130 OptimumKind::Unbounded, 1131 parsePoly("(x, y, z) : (2*x + 5*y + 8*z - 10 >= 0," 1132 "2*x + 10*y + 8*z - 10 >= 0, 2*x + 5*y + 10*z - 10 >= 0)")); 1133 1134 // The set is empty. 1135 expectNoRationalLexMin(OptimumKind::Empty, 1136 parsePoly("(x) : (2*x >= 0, -x - 1 >= 0)")); 1137 } 1138 1139 void expectIntegerLexMin(const IntegerPolyhedron &poly, ArrayRef<int64_t> min) { 1140 auto lexMin = poly.findIntegerLexMin(); 1141 ASSERT_TRUE(lexMin.isBounded()); 1142 EXPECT_EQ(ArrayRef<int64_t>(*lexMin), min); 1143 } 1144 1145 void expectNoIntegerLexMin(OptimumKind kind, const IntegerPolyhedron &poly) { 1146 ASSERT_NE(kind, OptimumKind::Bounded) 1147 << "Use expectRationalLexMin for bounded min"; 1148 EXPECT_EQ(poly.findRationalLexMin().getKind(), kind); 1149 } 1150 1151 TEST(IntegerPolyhedronTest, findIntegerLexMin) { 1152 expectIntegerLexMin(parsePoly("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 >= " 1153 "0, 11*z + 5*y - 3*x + 7 >= 0)"), 1154 {-6, -4, 0}); 1155 // Similar to above but no lower bound on z. 1156 expectNoIntegerLexMin(OptimumKind::Unbounded, 1157 parsePoly("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 " 1158 ">= 0, -11*z + 5*y - 3*x + 7 >= 0)")); 1159 } 1160 1161 void expectSymbolicIntegerLexMin( 1162 StringRef polyStr, 1163 ArrayRef<std::pair<StringRef, SmallVector<SmallVector<int64_t, 8>, 8>>> 1164 expectedLexminRepr, 1165 ArrayRef<StringRef> expectedUnboundedDomainRepr) { 1166 IntegerPolyhedron poly = parsePoly(polyStr); 1167 1168 ASSERT_NE(poly.getNumDimIds(), 0u); 1169 ASSERT_NE(poly.getNumSymbolIds(), 0u); 1170 1171 PWMAFunction expectedLexmin = 1172 parsePWMAF(/*numInputs=*/poly.getNumSymbolIds(), 1173 /*numOutputs=*/poly.getNumDimIds(), expectedLexminRepr); 1174 1175 PresburgerSet expectedUnboundedDomain = parsePresburgerSetFromPolyStrings( 1176 poly.getNumSymbolIds(), expectedUnboundedDomainRepr); 1177 1178 SymbolicLexMin result = poly.findSymbolicIntegerLexMin(); 1179 1180 EXPECT_TRUE(result.lexmin.isEqual(expectedLexmin)); 1181 if (!result.lexmin.isEqual(expectedLexmin)) { 1182 llvm::errs() << "got:\n"; 1183 result.lexmin.dump(); 1184 llvm::errs() << "expected:\n"; 1185 expectedLexmin.dump(); 1186 } 1187 1188 EXPECT_TRUE(result.unboundedDomain.isEqual(expectedUnboundedDomain)); 1189 if (!result.unboundedDomain.isEqual(expectedUnboundedDomain)) 1190 result.unboundedDomain.dump(); 1191 } 1192 1193 void expectSymbolicIntegerLexMin( 1194 StringRef polyStr, 1195 ArrayRef<std::pair<StringRef, SmallVector<SmallVector<int64_t, 8>, 8>>> 1196 result) { 1197 expectSymbolicIntegerLexMin(polyStr, result, {}); 1198 } 1199 1200 TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) { 1201 expectSymbolicIntegerLexMin("(x)[a] : (x - a >= 0)", 1202 { 1203 {"(a) : ()", {{1, 0}}}, // a 1204 }); 1205 1206 expectSymbolicIntegerLexMin( 1207 "(x)[a, b] : (x - a >= 0, x - b >= 0)", 1208 { 1209 {"(a, b) : (a - b >= 0)", {{1, 0, 0}}}, // a 1210 {"(a, b) : (b - a - 1 >= 0)", {{0, 1, 0}}}, // b 1211 }); 1212 1213 expectSymbolicIntegerLexMin( 1214 "(x)[a, b, c] : (x -a >= 0, x - b >= 0, x - c >= 0)", 1215 { 1216 {"(a, b, c) : (a - b >= 0, a - c >= 0)", {{1, 0, 0, 0}}}, // a 1217 {"(a, b, c) : (b - a - 1 >= 0, b - c >= 0)", {{0, 1, 0, 0}}}, // b 1218 {"(a, b, c) : (c - a - 1 >= 0, c - b - 1 >= 0)", {{0, 0, 1, 0}}}, // c 1219 }); 1220 1221 expectSymbolicIntegerLexMin("(x, y)[a] : (x - a >= 0, x + y >= 0)", 1222 { 1223 {"(a) : ()", {{1, 0}, {-1, 0}}}, // (a, -a) 1224 }); 1225 1226 expectSymbolicIntegerLexMin( 1227 "(x, y)[a] : (x - a >= 0, x + y >= 0, y >= 0)", 1228 { 1229 {"(a) : (a >= 0)", {{1, 0}, {0, 0}}}, // (a, 0) 1230 {"(a) : (-a - 1 >= 0)", {{1, 0}, {-1, 0}}}, // (a, -a) 1231 }); 1232 1233 expectSymbolicIntegerLexMin( 1234 "(x, y)[a, b, c] : (x - a >= 0, y - b >= 0, c - x - y >= 0)", 1235 { 1236 {"(a, b, c) : (c - a - b >= 0)", 1237 {{1, 0, 0, 0}, {0, 1, 0, 0}}}, // (a, b) 1238 }); 1239 1240 expectSymbolicIntegerLexMin( 1241 "(x, y, z)[a, b, c] : (c - z >= 0, b - y >= 0, x + y + z - a == 0)", 1242 { 1243 {"(a, b, c) : ()", 1244 {{1, -1, -1, 0}, {0, 1, 0, 0}, {0, 0, 1, 0}}}, // (a - b - c, b, c) 1245 }); 1246 1247 expectSymbolicIntegerLexMin( 1248 "(x)[a, b] : (a >= 0, b >= 0, x >= 0, a + b + x - 1 >= 0)", 1249 { 1250 {"(a, b) : (a >= 0, b >= 0, a + b - 1 >= 0)", {{0, 0, 0}}}, // 0 1251 {"(a, b) : (a == 0, b == 0)", {{0, 0, 1}}}, // 1 1252 }); 1253 1254 expectSymbolicIntegerLexMin( 1255 "(x)[a, b] : (1 - a >= 0, a >= 0, 1 - b >= 0, b >= 0, 1 - x >= 0, x >= " 1256 "0, a + b + x - 1 >= 0)", 1257 { 1258 {"(a, b) : (1 - a >= 0, a >= 0, 1 - b >= 0, b >= 0, a + b - 1 >= 0)", 1259 {{0, 0, 0}}}, // 0 1260 {"(a, b) : (a == 0, b == 0)", {{0, 0, 1}}}, // 1 1261 }); 1262 1263 expectSymbolicIntegerLexMin( 1264 "(x, y, z)[a, b] : (x - a == 0, y - b == 0, x >= 0, y >= 0, z >= 0, x + " 1265 "y + z - 1 >= 0)", 1266 { 1267 {"(a, b) : (a >= 0, b >= 0, 1 - a - b >= 0)", 1268 {{1, 0, 0}, {0, 1, 0}, {-1, -1, 1}}}, // (a, b, 1 - a - b) 1269 {"(a, b) : (a >= 0, b >= 0, a + b - 2 >= 0)", 1270 {{1, 0, 0}, {0, 1, 0}, {0, 0, 0}}}, // (a, b, 0) 1271 }); 1272 1273 expectSymbolicIntegerLexMin("(x)[a, b] : (x - a == 0, x - b >= 0)", 1274 { 1275 {"(a, b) : (a - b >= 0)", {{1, 0, 0}}}, // a 1276 }); 1277 1278 expectSymbolicIntegerLexMin( 1279 "(q)[a] : (a - 1 - 3*q == 0, q >= 0)", 1280 { 1281 {"(a) : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)", 1282 {{0, 1, 0}}}, // a floordiv 3 1283 }); 1284 1285 expectSymbolicIntegerLexMin( 1286 "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 1 - r >= 0, r >= 0)", 1287 { 1288 {"(a) : (a - 0 - 3*(a floordiv 3) == 0, a >= 0)", 1289 {{0, 0, 0}, {0, 1, 0}}}, // (0, a floordiv 3) 1290 {"(a) : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)", 1291 {{0, 0, 1}, {0, 1, 0}}}, // (1 a floordiv 3) 1292 }); 1293 1294 expectSymbolicIntegerLexMin( 1295 "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 2 - r >= 0, r - 1 >= 0)", 1296 { 1297 {"(a) : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)", 1298 {{0, 0, 1}, {0, 1, 0}}}, // (1, a floordiv 3) 1299 {"(a) : (a - 2 - 3*(a floordiv 3) == 0, a >= 0)", 1300 {{0, 0, 2}, {0, 1, 0}}}, // (2, a floordiv 3) 1301 }); 1302 1303 expectSymbolicIntegerLexMin( 1304 "(r, q)[a] : (a - r - 3*q == 0, q >= 0, r >= 0)", 1305 { 1306 {"(a) : (a - 3*(a floordiv 3) == 0, a >= 0)", 1307 {{0, 0, 0}, {0, 1, 0}}}, // (0, a floordiv 3) 1308 {"(a) : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)", 1309 {{0, 0, 1}, {0, 1, 0}}}, // (1, a floordiv 3) 1310 {"(a) : (a - 2 - 3*(a floordiv 3) == 0, a >= 0)", 1311 {{0, 0, 2}, {0, 1, 0}}}, // (2, a floordiv 3) 1312 }); 1313 1314 expectSymbolicIntegerLexMin( 1315 "(x, y, z, w)[g] : (" 1316 // x, y, z, w are boolean variables. 1317 "1 - x >= 0, x >= 0, 1 - y >= 0, y >= 0," 1318 "1 - z >= 0, z >= 0, 1 - w >= 0, w >= 0," 1319 // We have some constraints on them: 1320 "x + y + z - 1 >= 0," // x or y or z 1321 "x + y + w - 1 >= 0," // x or y or w 1322 "1 - x + 1 - y + 1 - w - 1 >= 0," // ~x or ~y or ~w 1323 // What's the lexmin solution using exactly g true vars? 1324 "g - x - y - z - w == 0)", 1325 { 1326 {"(g) : (g - 1 == 0)", 1327 {{0, 0}, {0, 1}, {0, 0}, {0, 0}}}, // (0, 1, 0, 0) 1328 {"(g) : (g - 2 == 0)", 1329 {{0, 0}, {0, 0}, {0, 1}, {0, 1}}}, // (0, 0, 1, 1) 1330 {"(g) : (g - 3 == 0)", 1331 {{0, 0}, {0, 1}, {0, 1}, {0, 1}}}, // (0, 1, 1, 1) 1332 }); 1333 1334 // Bezout's lemma: if a, b are constants, 1335 // the set of values that ax + by can take is all multiples of gcd(a, b). 1336 expectSymbolicIntegerLexMin( 1337 // If (x, y) is a solution for a given [a, r], then so is (x - 5, y + 2). 1338 // So the lexmin is unbounded if it exists. 1339 "(x, y)[a, r] : (a >= 0, r - a + 14*x + 35*y == 0)", {}, 1340 // According to Bezout's lemma, 14x + 35y can take on all multiples 1341 // of 7 and no other values. So the solution exists iff r - a is a 1342 // multiple of 7. 1343 {"(a, r) : (a >= 0, r - a - 7*((r - a) floordiv 7) == 0)"}); 1344 1345 // The lexmins are unbounded. 1346 expectSymbolicIntegerLexMin("(x, y)[a] : (9*x - 4*y - 2*a >= 0)", {}, 1347 {"(a) : ()"}); 1348 1349 // Test cases adapted from isl. 1350 expectSymbolicIntegerLexMin( 1351 // a = 2b - 2(c - b), c - b >= 0. 1352 // So b is minimized when c = b. 1353 "(b, c)[a] : (a - 4*b + 2*c == 0, c - b >= 0)", 1354 { 1355 {"(a) : (a - 2*(a floordiv 2) == 0)", 1356 {{0, 1, 0}, {0, 1, 0}}}, // (a floordiv 2, a floordiv 2) 1357 }); 1358 1359 expectSymbolicIntegerLexMin( 1360 // 0 <= b <= 255, 1 <= a - 512b <= 509, 1361 // b + 8 >= 1 + 16*(b + 8 floordiv 16) // i.e. b % 16 != 8 1362 "(b)[a] : (255 - b >= 0, b >= 0, a - 512*b - 1 >= 0, 512*b -a + 509 >= " 1363 "0, b + 7 - 16*((8 + b) floordiv 16) >= 0)", 1364 { 1365 {"(a) : (255 - (a floordiv 512) >= 0, a >= 0, a - 512*(a floordiv " 1366 "512) - 1 >= 0, 512*(a floordiv 512) - a + 509 >= 0, (a floordiv " 1367 "512) + 7 - 16*((8 + (a floordiv 512)) floordiv 16) >= 0)", 1368 {{0, 1, 0, 0}}}, // (a floordiv 2, a floordiv 2) 1369 }); 1370 1371 expectSymbolicIntegerLexMin( 1372 "(a, b)[K, N, x, y] : (N - K - 2 >= 0, K + 4 - N >= 0, x - 4 >= 0, x + 6 " 1373 "- 2*N >= 0, K+N - x - 1 >= 0, a - N + 1 >= 0, K+N-1-a >= 0,a + 6 - b - " 1374 "N >= 0, 2*N - 4 - a >= 0," 1375 "2*N - 3*K + a - b >= 0, 4*N - K + 1 - 3*b >= 0, b - N >= 0, a - x - 1 " 1376 ">= 0)", 1377 {{ 1378 "(K, N, x, y) : (x + 6 - 2*N >= 0, 2*N - 5 - x >= 0, x + 1 -3*K + N " 1379 ">= 0, N + K - 2 - x >= 0, x - 4 >= 0)", 1380 {{0, 0, 1, 0, 1}, {0, 1, 0, 0, 0}} // (1 + x, N) 1381 }}); 1382 } 1383 1384 static void 1385 expectComputedVolumeIsValidOverapprox(const IntegerPolyhedron &poly, 1386 Optional<uint64_t> trueVolume, 1387 Optional<uint64_t> resultBound) { 1388 expectComputedVolumeIsValidOverapprox(poly.computeVolume(), trueVolume, 1389 resultBound); 1390 } 1391 1392 TEST(IntegerPolyhedronTest, computeVolume) { 1393 // 0 <= x <= 3 + 1/3, -5.5 <= y <= 2 + 3/5, 3 <= z <= 1.75. 1394 // i.e. 0 <= x <= 3, -5 <= y <= 2, 3 <= z <= 3 + 1/4. 1395 // So volume is 4 * 8 * 1 = 32. 1396 expectComputedVolumeIsValidOverapprox( 1397 parsePoly("(x, y, z) : (x >= 0, -3*x + 10 >= 0, 2*y + 11 >= 0," 1398 "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), 1399 /*trueVolume=*/32ull, /*resultBound=*/32ull); 1400 1401 // Same as above but y has bounds 2 + 1/5 <= y <= 2 + 3/5. So the volume is 1402 // zero. 1403 expectComputedVolumeIsValidOverapprox( 1404 parsePoly("(x, y, z) : (x >= 0, -3*x + 10 >= 0, 5*y - 11 >= 0," 1405 "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), 1406 /*trueVolume=*/0ull, /*resultBound=*/0ull); 1407 1408 // Now x is unbounded below but y still has no integer values. 1409 expectComputedVolumeIsValidOverapprox( 1410 parsePoly("(x, y, z) : (-3*x + 10 >= 0, 5*y - 11 >= 0," 1411 "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"), 1412 /*trueVolume=*/0ull, /*resultBound=*/0ull); 1413 1414 // A diamond shape, 0 <= x + y <= 10, 0 <= x - y <= 10, 1415 // with vertices at (0, 0), (5, 5), (5, 5), (10, 0). 1416 // x and y can take 11 possible values so result computed is 11*11 = 121. 1417 expectComputedVolumeIsValidOverapprox( 1418 parsePoly("(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0," 1419 "-x + y + 10 >= 0)"), 1420 /*trueVolume=*/61ull, /*resultBound=*/121ull); 1421 1422 // Effectively the same diamond as above; constrain the variables to be even 1423 // and double the constant terms of the constraints. The algorithm can't 1424 // eliminate locals exactly, so the result is an overapproximation by 1425 // computing that x and y can take 21 possible values so result is 21*21 = 1426 // 441. 1427 expectComputedVolumeIsValidOverapprox( 1428 parsePoly("(x, y) : (x + y >= 0, -x - y + 20 >= 0, x - y >= 0," 1429 " -x + y + 20 >= 0, x - 2*(x floordiv 2) == 0," 1430 "y - 2*(y floordiv 2) == 0)"), 1431 /*trueVolume=*/61ull, /*resultBound=*/441ull); 1432 1433 // Unbounded polytope. 1434 expectComputedVolumeIsValidOverapprox( 1435 parsePoly("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"), 1436 /*trueVolume=*/{}, /*resultBound=*/{}); 1437 } 1438 1439 TEST(IntegerPolyhedronTest, containsPointNoLocal) { 1440 IntegerPolyhedron poly1 = parsePoly("(x) : ((x floordiv 2) - x == 0)"); 1441 EXPECT_TRUE(poly1.containsPointNoLocal({0})); 1442 EXPECT_FALSE(poly1.containsPointNoLocal({1})); 1443 1444 IntegerPolyhedron poly2 = parsePoly( 1445 "(x) : (x - 2*(x floordiv 2) == 0, x - 4*(x floordiv 4) - 2 == 0)"); 1446 EXPECT_TRUE(poly2.containsPointNoLocal({6})); 1447 EXPECT_FALSE(poly2.containsPointNoLocal({4})); 1448 1449 IntegerPolyhedron poly3 = parsePoly("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"); 1450 EXPECT_TRUE(poly3.containsPointNoLocal({0, 0})); 1451 EXPECT_FALSE(poly3.containsPointNoLocal({1, 0})); 1452 } 1453 1454 TEST(IntegerPolyhedronTest, truncateEqualityRegressionTest) { 1455 // IntegerRelation::truncate was truncating inequalities to the number of 1456 // equalities. 1457 IntegerRelation set(PresburgerSpace::getSetSpace(1)); 1458 IntegerRelation::CountsSnapshot snapshot = set.getCounts(); 1459 set.addEquality({1, 0}); 1460 set.truncate(snapshot); 1461 EXPECT_EQ(set.getNumEqualities(), 0u); 1462 } 1463