1502 lines · cpp
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-exception6//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 21using namespace mlir;22using namespace presburger;23 24using testing::ElementsAre;25 26enum class TestFunction { Sample, Empty };27 28/// Construct a IntegerPolyhedron from a set of inequality and29/// equality constraints.30static IntegerPolyhedron31makeSetFromConstraints(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 44static 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 sample53/// for the IntegerPolyhedron poly. Also check that getIntegerLexmin finds a54/// non-empty lexmin.55///56/// If hasSample is false, check that findIntegerSample returns std::nullopt57/// and findIntegerLexMin returns Empty.58///59/// If fn is TestFunction::Empty, check that isIntegerEmpty returns the60/// opposite of hasSample.61static 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 given102/// constraint set. Since the GBR algorithm progresses dimension-wise, different103/// orderings may cause the algorithm to proceed differently. At least some of104///.these permutations should make it past the heuristics and test the105/// implementation of the GBR algorithm itself.106/// Use TestFunction fn to test.107static 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 132TEST(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 151TEST(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 170TEST(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 184TEST(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 202TEST(IntegerPolyhedronTest, FindSampleTest) {203 // Bounded sets with only inequalities.204 // 0 <= 7x <= 5205 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 sample244 // with a naive branch and bound algorithm but can be sampled efficiently with245 // 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 at254 // (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 the256 // apex at the fourth point, which is the only integer point.257 checkPermutationsSample(258 true, 3,259 {260 {0, 1, 0, 0}, // y >= 0261 {0, -1, 1, 0}, // z >= y262 {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 at277 // (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 rational288 // 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) and305 // 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 at312 // (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 the314 // apex at the fourth point, which is the only integer point.315 // The cone has apex at (10000, 10000) and316 // 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 >= 0322 {0, -1, 1, 0, 0, 0}, // z >= y323 // -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 >= 100000330 {0, 0, 0, 300000, -299999, -100000},331 // -300000p + 299998q + 200000 >= 0332 {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 >= 0343 {0, -1, 1, 0, 0, 0}, // z >= y344 // -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 >= 1351 {0, 0, 0, 3, 0, -1},352 // 3p <= 2353 {0, 0, 0, -3, 0, 2},354 },355 {});356 357 // Cartesian product of same tetrahedron as above and358 // {(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 >= 0365 {0, -1, 1, 0, 0, 0, 0}, // z >= y366 // -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 >= 1373 {0, 0, 0, 1, 0, 0, -1},374 // p <= 2375 {0, 0, 0, -1, 0, 0, 2},376 },377 {378 {0, 0, 0, 1, -3, -3, 0}, // p = 3q + 3r379 });380 381 // Cartesian product of a tetrahedron and a 2D cone.382 // The tetrahedron is empty and has vertices at383 // (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) and385 // 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 >= 100000397 {0, 0, 0, 300000, -299999, -100000},398 // -300000p + 299998q + 200000 >= 0399 {0, 0, 0, -300000, 299998, 200000},400 },401 {});402 403 // Cartesian product of same tetrahedron as above and404 // {(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 >= 1415 {0, 0, 0, 3, 0, -1},416 // 3p <= 2417 {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 443TEST(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 be467 // 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 have487 // y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying488 // 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 500TEST(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. The514 // 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 constraints575 // 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 have585 // 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 597TEST(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 610TEST(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 the624/// computed representation. The expected division representation is given as625/// a vector of expressions set in `expectedDividends` and the corressponding626/// denominator in `expectedDenominators`. The `denominators` and `dividends`627/// obtained through `getLocalRepr` function is verified against the628/// `expectedDenominators` and `expectedDividends` respectively.629static 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 the640 // 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 651TEST(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 exist662 // and floor divs do not depend on each other.663 checkDivisionRepresentation(poly, divisions, denoms);664}665 666TEST(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 684TEST(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 708TEST(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 bound714 // -3q + i - 1 >= 0715 // -3q + i >= 0 <-- Division upper bound716 // We remove redundant constraints to get the set:717 // 3q - i + 2 >= 0 <-- Division lower bound718 // -3q + i - 1 >= 0 <-- Tighter division upper bound719 // 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 743TEST(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 779TEST(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 795TEST(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 808TEST(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 822TEST(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 848TEST(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 921TEST(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 994TEST(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 1043TEST(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 1066TEST(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 dividends1071 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 1090static 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 1097static void expectNoRationalLexMin(OptimumKind kind,1098 const IntegerPolyhedron &poly) {1099 ASSERT_NE(kind, OptimumKind::Bounded)1100 << "Use expectRationalLexMin for bounded min";1101 EXPECT_EQ(poly.findRationalLexMin().getKind(), kind);1102}1103 1104TEST(IntegerPolyhedronTest, findRationalLexMin) {1105 expectRationalLexMin(1106 parseIntegerPolyhedron(1107 "(x, y, z) : (x + 10 >= 0, y + 40 >= 0, z + 30 >= 0)"),1108 {{-10, 1}, {-40, 1}, {-30, 1}});1109 expectRationalLexMin(1110 parseIntegerPolyhedron(1111 "(x, y, z) : (2*x + 7 >= 0, 3*y - 5 >= 0, 8*z + 10 >= 0, 9*z >= 0)"),1112 {{-7, 2}, {5, 3}, {0, 1}});1113 expectRationalLexMin(1114 parseIntegerPolyhedron("(x, y) : (3*x + 2*y + 10 >= 0, -3*y + 10 >= "1115 "0, 4*x - 7*y - 10 >= 0)"),1116 {{-50, 29}, {-70, 29}});1117 1118 // Test with some locals. This is basically x >= 11, 0 <= x - 2e <= 1.1119 // It'll just choose x = 11, e = 5.5 since it's rational lexmin.1120 expectRationalLexMin(1121 parseIntegerPolyhedron(1122 "(x, y) : (x - 2*(x floordiv 2) == 0, y - 2*x >= 0, x - 11 >= 0)"),1123 {{11, 1}, {22, 1}});1124 1125 expectRationalLexMin(1126 parseIntegerPolyhedron("(x, y) : (3*x + 2*y + 10 >= 0,"1127 "-4*x + 7*y + 10 >= 0, -3*y + 10 >= 0)"),1128 {{-50, 9}, {10, 3}});1129 1130 // Cartesian product of above with itself.1131 expectRationalLexMin(1132 parseIntegerPolyhedron(1133 "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0,"1134 "-3*y + 10 >= 0, 3*z + 2*w + 10 >= 0, -4*z + 7*w + 10 >= 0,"1135 "-3*w + 10 >= 0)"),1136 {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}});1137 1138 // Same as above but for the constraints on z and w, we express "10" in terms1139 // of x and y. We know that x and y still have to take the values1140 // -50/9 and 10/3 since their constraints are the same and their values are1141 // minimized first. Accordingly, the values -9x - 12y, -9x - 0y - 10,1142 // and -9x - 15y + 10 are all equal to 10.1143 expectRationalLexMin(1144 parseIntegerPolyhedron(1145 "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0, "1146 "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0,"1147 "-4*z + 7*w + - 9*x - 9*y - 10 >= 0, -3*w - 9*x - 15*y + 10 >= 0)"),1148 {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}});1149 1150 // Same as above with one constraint removed, making the lexmin unbounded.1151 expectNoRationalLexMin(1152 OptimumKind::Unbounded,1153 parseIntegerPolyhedron(1154 "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0,"1155 "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0,"1156 "-4*z + 7*w + - 9*x - 9*y - 10>= 0)"));1157 1158 // Again, the lexmin is unbounded.1159 expectNoRationalLexMin(1160 OptimumKind::Unbounded,1161 parseIntegerPolyhedron(1162 "(x, y, z) : (2*x + 5*y + 8*z - 10 >= 0,"1163 "2*x + 10*y + 8*z - 10 >= 0, 2*x + 5*y + 10*z - 10 >= 0)"));1164 1165 // The set is empty.1166 expectNoRationalLexMin(1167 OptimumKind::Empty,1168 parseIntegerPolyhedron("(x) : (2*x >= 0, -x - 1 >= 0)"));1169}1170 1171static void expectIntegerLexMin(const IntegerPolyhedron &poly,1172 ArrayRef<int64_t> min) {1173 MaybeOptimum<SmallVector<DynamicAPInt, 8>> lexMin = poly.findIntegerLexMin();1174 ASSERT_TRUE(lexMin.isBounded());1175 EXPECT_EQ(*lexMin, getDynamicAPIntVec(min));1176}1177 1178static void expectNoIntegerLexMin(OptimumKind kind,1179 const IntegerPolyhedron &poly) {1180 ASSERT_NE(kind, OptimumKind::Bounded)1181 << "Use expectRationalLexMin for bounded min";1182 EXPECT_EQ(poly.findRationalLexMin().getKind(), kind);1183}1184 1185TEST(IntegerPolyhedronTest, findIntegerLexMin) {1186 expectIntegerLexMin(1187 parseIntegerPolyhedron("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 >= "1188 "0, 11*z + 5*y - 3*x + 7 >= 0)"),1189 {-6, -4, 0});1190 // Similar to above but no lower bound on z.1191 expectNoIntegerLexMin(1192 OptimumKind::Unbounded,1193 parseIntegerPolyhedron("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 "1194 ">= 0, -11*z + 5*y - 3*x + 7 >= 0)"));1195}1196 1197static void expectSymbolicIntegerLexMin(1198 StringRef polyStr,1199 ArrayRef<std::pair<StringRef, StringRef>> expectedLexminRepr,1200 ArrayRef<StringRef> expectedUnboundedDomainRepr) {1201 IntegerPolyhedron poly = parseIntegerPolyhedron(polyStr);1202 1203 ASSERT_NE(poly.getNumDimVars(), 0u);1204 ASSERT_NE(poly.getNumSymbolVars(), 0u);1205 1206 SymbolicLexOpt result = poly.findSymbolicIntegerLexMin();1207 1208 if (expectedLexminRepr.empty()) {1209 EXPECT_TRUE(result.lexopt.getDomain().isIntegerEmpty());1210 } else {1211 PWMAFunction expectedLexmin = parsePWMAF(expectedLexminRepr);1212 EXPECT_TRUE(result.lexopt.isEqual(expectedLexmin));1213 }1214 1215 if (expectedUnboundedDomainRepr.empty()) {1216 EXPECT_TRUE(result.unboundedDomain.isIntegerEmpty());1217 } else {1218 PresburgerSet expectedUnboundedDomain =1219 parsePresburgerSet(expectedUnboundedDomainRepr);1220 EXPECT_TRUE(result.unboundedDomain.isEqual(expectedUnboundedDomain));1221 }1222}1223 1224static void1225expectSymbolicIntegerLexMin(StringRef polyStr,1226 ArrayRef<std::pair<StringRef, StringRef>> result) {1227 expectSymbolicIntegerLexMin(polyStr, result, {});1228}1229 1230TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) {1231 expectSymbolicIntegerLexMin("(x)[a] : (x - a >= 0)",1232 {1233 {"()[a] : ()", "()[a] -> (a)"},1234 });1235 1236 expectSymbolicIntegerLexMin(1237 "(x)[a, b] : (x - a >= 0, x - b >= 0)",1238 {1239 {"()[a, b] : (a - b >= 0)", "()[a, b] -> (a)"},1240 {"()[a, b] : (b - a - 1 >= 0)", "()[a, b] -> (b)"},1241 });1242 1243 expectSymbolicIntegerLexMin(1244 "(x)[a, b, c] : (x -a >= 0, x - b >= 0, x - c >= 0)",1245 {1246 {"()[a, b, c] : (a - b >= 0, a - c >= 0)", "()[a, b, c] -> (a)"},1247 {"()[a, b, c] : (b - a - 1 >= 0, b - c >= 0)", "()[a, b, c] -> (b)"},1248 {"()[a, b, c] : (c - a - 1 >= 0, c - b - 1 >= 0)",1249 "()[a, b, c] -> (c)"},1250 });1251 1252 expectSymbolicIntegerLexMin("(x, y)[a] : (x - a >= 0, x + y >= 0)",1253 {1254 {"()[a] : ()", "()[a] -> (a, -a)"},1255 });1256 1257 expectSymbolicIntegerLexMin("(x, y)[a] : (x - a >= 0, x + y >= 0, y >= 0)",1258 {1259 {"()[a] : (a >= 0)", "()[a] -> (a, 0)"},1260 {"()[a] : (-a - 1 >= 0)", "()[a] -> (a, -a)"},1261 });1262 1263 expectSymbolicIntegerLexMin(1264 "(x, y)[a, b, c] : (x - a >= 0, y - b >= 0, c - x - y >= 0)",1265 {1266 {"()[a, b, c] : (c - a - b >= 0)", "()[a, b, c] -> (a, b)"},1267 });1268 1269 expectSymbolicIntegerLexMin(1270 "(x, y, z)[a, b, c] : (c - z >= 0, b - y >= 0, x + y + z - a == 0)",1271 {1272 {"()[a, b, c] : ()", "()[a, b, c] -> (a - b - c, b, c)"},1273 });1274 1275 expectSymbolicIntegerLexMin(1276 "(x)[a, b] : (a >= 0, b >= 0, x >= 0, a + b + x - 1 >= 0)",1277 {1278 {"()[a, b] : (a >= 0, b >= 0, a + b - 1 >= 0)", "()[a, b] -> (0)"},1279 {"()[a, b] : (a == 0, b == 0)", "()[a, b] -> (1)"},1280 });1281 1282 expectSymbolicIntegerLexMin(1283 "(x)[a, b] : (1 - a >= 0, a >= 0, 1 - b >= 0, b >= 0, 1 - x >= 0, x >= "1284 "0, a + b + x - 1 >= 0)",1285 {1286 {"()[a, b] : (1 - a >= 0, a >= 0, 1 - b >= 0, b >= 0, a + b - 1 >= "1287 "0)",1288 "()[a, b] -> (0)"},1289 {"()[a, b] : (a == 0, b == 0)", "()[a, b] -> (1)"},1290 });1291 1292 expectSymbolicIntegerLexMin(1293 "(x, y, z)[a, b] : (x - a == 0, y - b == 0, x >= 0, y >= 0, z >= 0, x + "1294 "y + z - 1 >= 0)",1295 {1296 {"()[a, b] : (a >= 0, b >= 0, 1 - a - b >= 0)",1297 "()[a, b] -> (a, b, 1 - a - b)"},1298 {"()[a, b] : (a >= 0, b >= 0, a + b - 2 >= 0)",1299 "()[a, b] -> (a, b, 0)"},1300 });1301 1302 expectSymbolicIntegerLexMin(1303 "(x)[a, b] : (x - a == 0, x - b >= 0)",1304 {1305 {"()[a, b] : (a - b >= 0)", "()[a, b] -> (a)"},1306 });1307 1308 expectSymbolicIntegerLexMin(1309 "(q)[a] : (a - 1 - 3*q == 0, q >= 0)",1310 {1311 {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",1312 "()[a] -> (a floordiv 3)"},1313 });1314 1315 expectSymbolicIntegerLexMin(1316 "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 1 - r >= 0, r >= 0)",1317 {1318 {"()[a] : (a - 0 - 3*(a floordiv 3) == 0, a >= 0)",1319 "()[a] -> (0, a floordiv 3)"},1320 {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",1321 "()[a] -> (1, a floordiv 3)"}, // (1 a floordiv 3)1322 });1323 1324 expectSymbolicIntegerLexMin(1325 "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 2 - r >= 0, r - 1 >= 0)",1326 {1327 {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",1328 "()[a] -> (1, a floordiv 3)"},1329 {"()[a] : (a - 2 - 3*(a floordiv 3) == 0, a >= 0)",1330 "()[a] -> (2, a floordiv 3)"},1331 });1332 1333 expectSymbolicIntegerLexMin(1334 "(r, q)[a] : (a - r - 3*q == 0, q >= 0, r >= 0)",1335 {1336 {"()[a] : (a - 3*(a floordiv 3) == 0, a >= 0)",1337 "()[a] -> (0, a floordiv 3)"},1338 {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",1339 "()[a] -> (1, a floordiv 3)"},1340 {"()[a] : (a - 2 - 3*(a floordiv 3) == 0, a >= 0)",1341 "()[a] -> (2, a floordiv 3)"},1342 });1343 1344 expectSymbolicIntegerLexMin(1345 "(x, y, z, w)[g] : ("1346 // x, y, z, w are boolean variables.1347 "1 - x >= 0, x >= 0, 1 - y >= 0, y >= 0,"1348 "1 - z >= 0, z >= 0, 1 - w >= 0, w >= 0,"1349 // We have some constraints on them:1350 "x + y + z - 1 >= 0," // x or y or z1351 "x + y + w - 1 >= 0," // x or y or w1352 "1 - x + 1 - y + 1 - w - 1 >= 0," // ~x or ~y or ~w1353 // What's the lexmin solution using exactly g true vars?1354 "g - x - y - z - w == 0)",1355 {1356 {"()[g] : (g - 1 == 0)", "()[g] -> (0, 1, 0, 0)"},1357 {"()[g] : (g - 2 == 0)", "()[g] -> (0, 0, 1, 1)"},1358 {"()[g] : (g - 3 == 0)", "()[g] -> (0, 1, 1, 1)"},1359 });1360 1361 // Bezout's lemma: if a, b are constants,1362 // the set of values that ax + by can take is all multiples of gcd(a, b).1363 expectSymbolicIntegerLexMin(1364 // If (x, y) is a solution for a given [a, r], then so is (x - 5, y + 2).1365 // So the lexmin is unbounded if it exists.1366 "(x, y)[a, r] : (a >= 0, r - a + 14*x + 35*y == 0)", {},1367 // According to Bezout's lemma, 14x + 35y can take on all multiples1368 // of 7 and no other values. So the solution exists iff r - a is a1369 // multiple of 7.1370 {"()[a, r] : (a >= 0, r - a - 7*((r - a) floordiv 7) == 0)"});1371 1372 // The lexmins are unbounded.1373 expectSymbolicIntegerLexMin("(x, y)[a] : (9*x - 4*y - 2*a >= 0)", {},1374 {"()[a] : ()"});1375 1376 // Test cases adapted from isl.1377 expectSymbolicIntegerLexMin(1378 // a = 2b - 2(c - b), c - b >= 0.1379 // So b is minimized when c = b.1380 "(b, c)[a] : (a - 4*b + 2*c == 0, c - b >= 0)",1381 {1382 {"()[a] : (a - 2*(a floordiv 2) == 0)",1383 "()[a] -> (a floordiv 2, a floordiv 2)"},1384 });1385 1386 expectSymbolicIntegerLexMin(1387 // 0 <= b <= 255, 1 <= a - 512b <= 509,1388 // b + 8 >= 1 + 16*(b + 8 floordiv 16) // i.e. b % 16 != 81389 "(b)[a] : (255 - b >= 0, b >= 0, a - 512*b - 1 >= 0, 512*b -a + 509 >= "1390 "0, b + 7 - 16*((8 + b) floordiv 16) >= 0)",1391 {1392 {"()[a] : (255 - (a floordiv 512) >= 0, a >= 0, a - 512*(a floordiv "1393 "512) - 1 >= 0, 512*(a floordiv 512) - a + 509 >= 0, (a floordiv "1394 "512) + 7 - 16*((8 + (a floordiv 512)) floordiv 16) >= 0)",1395 "()[a] -> (a floordiv 512)"},1396 });1397 1398 expectSymbolicIntegerLexMin(1399 "(a, b)[K, N, x, y] : (N - K - 2 >= 0, K + 4 - N >= 0, x - 4 >= 0, x + 6 "1400 "- 2*N >= 0, K+N - x - 1 >= 0, a - N + 1 >= 0, K+N-1-a >= 0,a + 6 - b - "1401 "N >= 0, 2*N - 4 - a >= 0,"1402 "2*N - 3*K + a - b >= 0, 4*N - K + 1 - 3*b >= 0, b - N >= 0, a - x - 1 "1403 ">= 0)",1404 {1405 {"()[K, N, x, y] : (x + 6 - 2*N >= 0, 2*N - 5 - x >= 0, x + 1 -3*K + "1406 "N >= 0, N + K - 2 - x >= 0, x - 4 >= 0)",1407 "()[K, N, x, y] -> (1 + x, N)"},1408 });1409}1410 1411static void1412expectComputedVolumeIsValidOverapprox(const IntegerPolyhedron &poly,1413 std::optional<int64_t> trueVolume,1414 std::optional<int64_t> resultBound) {1415 expectComputedVolumeIsValidOverapprox(poly.computeVolume(), trueVolume,1416 resultBound);1417}1418 1419TEST(IntegerPolyhedronTest, computeVolume) {1420 // 0 <= x <= 3 + 1/3, -5.5 <= y <= 2 + 3/5, 3 <= z <= 1.75.1421 // i.e. 0 <= x <= 3, -5 <= y <= 2, 3 <= z <= 3 + 1/4.1422 // So volume is 4 * 8 * 1 = 32.1423 expectComputedVolumeIsValidOverapprox(1424 parseIntegerPolyhedron(1425 "(x, y, z) : (x >= 0, -3*x + 10 >= 0, 2*y + 11 >= 0,"1426 "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"),1427 /*trueVolume=*/32ull, /*resultBound=*/32ull);1428 1429 // Same as above but y has bounds 2 + 1/5 <= y <= 2 + 3/5. So the volume is1430 // zero.1431 expectComputedVolumeIsValidOverapprox(1432 parseIntegerPolyhedron(1433 "(x, y, z) : (x >= 0, -3*x + 10 >= 0, 5*y - 11 >= 0,"1434 "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"),1435 /*trueVolume=*/0ull, /*resultBound=*/0ull);1436 1437 // Now x is unbounded below but y still has no integer values.1438 expectComputedVolumeIsValidOverapprox(1439 parseIntegerPolyhedron("(x, y, z) : (-3*x + 10 >= 0, 5*y - 11 >= 0,"1440 "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"),1441 /*trueVolume=*/0ull, /*resultBound=*/0ull);1442 1443 // A diamond shape, 0 <= x + y <= 10, 0 <= x - y <= 10,1444 // with vertices at (0, 0), (5, 5), (5, 5), (10, 0).1445 // x and y can take 11 possible values so result computed is 11*11 = 121.1446 expectComputedVolumeIsValidOverapprox(1447 parseIntegerPolyhedron(1448 "(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0,"1449 "-x + y + 10 >= 0)"),1450 /*trueVolume=*/61ull, /*resultBound=*/121ull);1451 1452 // Effectively the same diamond as above; constrain the variables to be even1453 // and double the constant terms of the constraints. The algorithm can't1454 // eliminate locals exactly, so the result is an overapproximation by1455 // computing that x and y can take 21 possible values so result is 21*21 =1456 // 441.1457 expectComputedVolumeIsValidOverapprox(1458 parseIntegerPolyhedron(1459 "(x, y) : (x + y >= 0, -x - y + 20 >= 0, x - y >= 0,"1460 " -x + y + 20 >= 0, x - 2*(x floordiv 2) == 0,"1461 "y - 2*(y floordiv 2) == 0)"),1462 /*trueVolume=*/61ull, /*resultBound=*/441ull);1463 1464 // Unbounded polytope.1465 expectComputedVolumeIsValidOverapprox(1466 parseIntegerPolyhedron("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"),1467 /*trueVolume=*/{}, /*resultBound=*/{});1468}1469 1470static bool containsPointNoLocal(const IntegerPolyhedron &poly,1471 ArrayRef<int64_t> point) {1472 return poly.containsPointNoLocal(getDynamicAPIntVec(point)).has_value();1473}1474 1475TEST(IntegerPolyhedronTest, containsPointNoLocal) {1476 IntegerPolyhedron poly1 =1477 parseIntegerPolyhedron("(x) : ((x floordiv 2) - x == 0)");1478 EXPECT_TRUE(poly1.containsPointNoLocal({0}));1479 EXPECT_FALSE(poly1.containsPointNoLocal({1}));1480 1481 IntegerPolyhedron poly2 = parseIntegerPolyhedron(1482 "(x) : (x - 2*(x floordiv 2) == 0, x - 4*(x floordiv 4) - 2 == 0)");1483 EXPECT_TRUE(containsPointNoLocal(poly2, {6}));1484 EXPECT_FALSE(containsPointNoLocal(poly2, {4}));1485 1486 IntegerPolyhedron poly3 =1487 parseIntegerPolyhedron("(x, y) : (2*x - y >= 0, y - 3*x >= 0)");1488 1489 EXPECT_TRUE(poly3.containsPointNoLocal(ArrayRef<int64_t>({0, 0})));1490 EXPECT_FALSE(poly3.containsPointNoLocal({1, 0}));1491}1492 1493TEST(IntegerPolyhedronTest, truncateEqualityRegressionTest) {1494 // IntegerRelation::truncate was truncating inequalities to the number of1495 // equalities.1496 IntegerRelation set(PresburgerSpace::getSetSpace(1));1497 IntegerRelation::CountsSnapshot snapshot = set.getCounts();1498 set.addEquality({1, 0});1499 set.truncate(snapshot);1500 EXPECT_EQ(set.getNumEqualities(), 0u);1501}1502