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
makeSetFromConstraints(unsigned ids,ArrayRef<SmallVector<int64_t,4>> ineqs,ArrayRef<SmallVector<int64_t,4>> eqs,unsigned syms=0)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
dump(ArrayRef<DynamicAPInt> vec)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.
checkSample(bool hasSample,const IntegerPolyhedron & poly,TestFunction fn=TestFunction::Sample)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.
checkPermutationsSample(bool hasSample,unsigned nDim,ArrayRef<SmallVector<int64_t,4>> ineqs,ArrayRef<SmallVector<int64_t,4>> eqs,TestFunction fn=TestFunction::Sample)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
TEST(IntegerPolyhedronTest,removeInequality)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
TEST(IntegerPolyhedronTest,removeEquality)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
TEST(IntegerPolyhedronTest,clearConstraints)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
TEST(IntegerPolyhedronTest,removeIdRange)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
TEST(IntegerPolyhedronTest,FindSampleTest)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
TEST(IntegerPolyhedronTest,IsIntegerEmptyTest)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
TEST(IntegerPolyhedronTest,removeRedundantConstraintsTest)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
TEST(IntegerPolyhedronTest,addConstantUpperBound)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
TEST(IntegerPolyhedronTest,addConstantLowerBound)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.
checkDivisionRepresentation(IntegerPolyhedron & poly,const std::vector<SmallVector<int64_t,8>> & expectedDividends,ArrayRef<int64_t> expectedDenominators)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
TEST(IntegerPolyhedronTest,computeLocalReprSimple)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
TEST(IntegerPolyhedronTest,computeLocalReprConstantFloorDiv)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
TEST(IntegerPolyhedronTest,computeLocalReprRecursive)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
TEST(IntegerPolyhedronTest,computeLocalReprTightUpperBound)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
TEST(IntegerPolyhedronTest,computeLocalReprFromEquality)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
TEST(IntegerPolyhedronTest,computeLocalReprFromEqualityAndInequality)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
TEST(IntegerPolyhedronTest,computeLocalReprNoRepr)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
TEST(IntegerPolyhedronTest,computeLocalReprNegConstNormalize)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
TEST(IntegerPolyhedronTest,simplifyLocalsTest)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
TEST(IntegerPolyhedronTest,mergeDivisionsSimple)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
TEST(IntegerPolyhedronTest,mergeDivisionsNestedDivsions)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
TEST(IntegerPolyhedronTest,mergeDivisionsConstants)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
TEST(IntegerPolyhedronTest,mergeDivisionsDuplicateInSameSet)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
TEST(IntegerPolyhedronTest,negativeDividends)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
expectRationalLexMin(const IntegerPolyhedron & poly,ArrayRef<Fraction> min)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
expectNoRationalLexMin(OptimumKind kind,const IntegerPolyhedron & poly)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
TEST(IntegerPolyhedronTest,findRationalLexMin)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
expectIntegerLexMin(const IntegerPolyhedron & poly,ArrayRef<int64_t> min)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
expectNoIntegerLexMin(OptimumKind kind,const IntegerPolyhedron & poly)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
TEST(IntegerPolyhedronTest,findIntegerLexMin)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
expectSymbolicIntegerLexMin(StringRef polyStr,ArrayRef<std::pair<StringRef,StringRef>> expectedLexminRepr,ArrayRef<StringRef> expectedUnboundedDomainRepr)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
expectSymbolicIntegerLexMin(StringRef polyStr,ArrayRef<std::pair<StringRef,StringRef>> result)1221 void expectSymbolicIntegerLexMin(
1222 StringRef polyStr, ArrayRef<std::pair<StringRef, StringRef>> result) {
1223 expectSymbolicIntegerLexMin(polyStr, result, {});
1224 }
1225
TEST(IntegerPolyhedronTest,findSymbolicIntegerLexMin)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
expectComputedVolumeIsValidOverapprox(const IntegerPolyhedron & poly,std::optional<int64_t> trueVolume,std::optional<int64_t> resultBound)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
TEST(IntegerPolyhedronTest,computeVolume)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
containsPointNoLocal(const IntegerPolyhedron & poly,ArrayRef<int64_t> point)1466 bool containsPointNoLocal(const IntegerPolyhedron &poly,
1467 ArrayRef<int64_t> point) {
1468 return poly.containsPointNoLocal(getDynamicAPIntVec(point)).has_value();
1469 }
1470
TEST(IntegerPolyhedronTest,containsPointNoLocal)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
TEST(IntegerPolyhedronTest,truncateEqualityRegressionTest)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