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