1	//===- IntegerPolyhedron.cpp - Tests for IntegerPolyhedron class ----------===//
2	//
3	// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4	// See https://llvm.org/LICENSE.txt for license information.
5	// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6	//
7	//===----------------------------------------------------------------------===//
8
9	#include "Parser.h"
10	#include "Utils.h"
11	#include "mlir/Analysis/Presburger/IntegerRelation.h"
12	#include "mlir/Analysis/Presburger/PWMAFunction.h"
13	#include "mlir/Analysis/Presburger/Simplex.h"
14
15	#include <gmock/gmock.h>
16	#include <gtest/gtest.h>
17
18	#include <numeric>
19	#include <optional>
20
21	using namespace mlir;
22	using namespace presburger;
23
24	using testing::ElementsAre;
25
26	enum class TestFunction { Sample, Empty };
27
28	/// Construct a IntegerPolyhedron from a set of inequality and
29	/// equality constraints.
30	static IntegerPolyhedron
31	makeSetFromConstraints(unsigned ids, ArrayRef<SmallVector<int64_t, 4>> ineqs,
32	ArrayRef<SmallVector<int64_t, 4>> eqs,
33	unsigned syms = 0) {
34	IntegerPolyhedron set(
35	ineqs.size(), eqs.size(), ids + 1,
36	PresburgerSpace::getSetSpace(numDims: ids - syms, numSymbols: syms, /*numLocals=*/0));
37	for (const auto &eq : eqs)
38	set.addEquality(eq);
39	for (const auto &ineq : ineqs)
40	set.addInequality(inEq: ineq);
41	return set;
42	}
43
44	static void dump(ArrayRef<DynamicAPInt> vec) {
45	for (const DynamicAPInt &x : vec)
46	llvm::errs() << x << ' ';
47	llvm::errs() << '\n';
48	}
49
50	/// If fn is TestFunction::Sample (default):
51	///
52	/// If hasSample is true, check that findIntegerSample returns a valid sample
53	/// for the IntegerPolyhedron poly. Also check that getIntegerLexmin finds a
54	/// non-empty lexmin.
55	///
56	/// If hasSample is false, check that findIntegerSample returns std::nullopt
57	/// and findIntegerLexMin returns Empty.
58	///
59	/// If fn is TestFunction::Empty, check that isIntegerEmpty returns the
60	/// opposite of hasSample.
61	static void checkSample(bool hasSample, const IntegerPolyhedron &poly,
62	TestFunction fn = TestFunction::Sample) {
63	std::optional<SmallVector<DynamicAPInt, 8>> maybeSample;
64	MaybeOptimum<SmallVector<DynamicAPInt, 8>> maybeLexMin;
65	switch (fn) {
66	case TestFunction::Sample:
67	maybeSample = poly.findIntegerSample();
68	maybeLexMin = poly.findIntegerLexMin();
69
70	if (!hasSample) {
71	EXPECT_FALSE(maybeSample.has_value());
72	if (maybeSample.has_value()) {
73	llvm::errs() << "findIntegerSample gave sample: ";
74	dump(vec: *maybeSample);
75	}
76
77	EXPECT_TRUE(maybeLexMin.isEmpty());
78	if (maybeLexMin.isBounded()) {
79	llvm::errs() << "findIntegerLexMin gave sample: ";
80	dump(vec: *maybeLexMin);
81	}
82	} else {
83	ASSERT_TRUE(maybeSample.has_value());
84	EXPECT_TRUE(poly.containsPoint(*maybeSample));
85
86	ASSERT_FALSE(maybeLexMin.isEmpty());
87	if (maybeLexMin.isUnbounded()) {
88	EXPECT_TRUE(Simplex(poly).isUnbounded());
89	}
90	if (maybeLexMin.isBounded()) {
91	EXPECT_TRUE(poly.containsPointNoLocal(*maybeLexMin));
92	}
93	}
94	break;
95	case TestFunction::Empty:
96	EXPECT_EQ(!hasSample, poly.isIntegerEmpty());
97	break;
98	}
99	}
100
101	/// Check sampling for all the permutations of the dimensions for the given
102	/// constraint set. Since the GBR algorithm progresses dimension-wise, different
103	/// orderings may cause the algorithm to proceed differently. At least some of
104	///.these permutations should make it past the heuristics and test the
105	/// implementation of the GBR algorithm itself.
106	/// Use TestFunction fn to test.
107	static void checkPermutationsSample(bool hasSample, unsigned nDim,
108	ArrayRef<SmallVector<int64_t, 4>> ineqs,
109	ArrayRef<SmallVector<int64_t, 4>> eqs,
110	TestFunction fn = TestFunction::Sample) {
111	SmallVector<unsigned, 4> perm(nDim);
112	std::iota(first: perm.begin(), last: perm.end(), value: 0);
113	auto permute = [&perm](ArrayRef<int64_t> coeffs) {
114	SmallVector<int64_t, 4> permuted;
115	for (unsigned id : perm)
116	permuted.push_back(Elt: coeffs[id]);
117	permuted.push_back(Elt: 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(Elt: permute(ineq));
124	for (const auto &eq : eqs)
125	permutedEqs.push_back(Elt: permute(eq));
126
127	checkSample(hasSample,
128	poly: makeSetFromConstraints(ids: nDim, ineqs: permutedIneqs, eqs: permutedEqs), fn);
129	} while (std::next_permutation(first: perm.begin(), last: perm.end()));
130	}
131
132	TEST(IntegerPolyhedronTest, removeInequality) {
133	IntegerPolyhedron set =
134	makeSetFromConstraints(ids: 1, ineqs: {{0, 0}, {1, 1}, {2, 2}, {3, 3}, {4, 4}}, eqs: {});
135
136	set.removeInequalityRange(start: 0, end: 0);
137	EXPECT_EQ(set.getNumInequalities(), 5u);
138
139	set.removeInequalityRange(start: 1, end: 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(pos: 1);
146	EXPECT_EQ(set.getNumInequalities(), 2u);
147	EXPECT_THAT(set.getInequality(0), ElementsAre(0, 0));
148	EXPECT_THAT(set.getInequality(1), ElementsAre(4, 4));
149	}
150
151	TEST(IntegerPolyhedronTest, removeEquality) {
152	IntegerPolyhedron set =
153	makeSetFromConstraints(ids: 1, ineqs: {}, eqs: {{0, 0}, {1, 1}, {2, 2}, {3, 3}, {4, 4}});
154
155	set.removeEqualityRange(start: 0, end: 0);
156	EXPECT_EQ(set.getNumEqualities(), 5u);
157
158	set.removeEqualityRange(start: 1, end: 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(pos: 1);
165	EXPECT_EQ(set.getNumEqualities(), 2u);
166	EXPECT_THAT(set.getEquality(0), ElementsAre(0, 0));
167	EXPECT_THAT(set.getEquality(1), ElementsAre(4, 4));
168	}
169
170	TEST(IntegerPolyhedronTest, clearConstraints) {
171	IntegerPolyhedron set = makeSetFromConstraints(ids: 1, ineqs: {}, eqs: {});
172
173	set.addInequality(inEq: {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(inEq: {1, 0});
180	EXPECT_EQ(set.atIneq(0, 0), 1);
181	EXPECT_EQ(set.atIneq(0, 1), 0);
182	}
183
184	TEST(IntegerPolyhedronTest, removeIdRange) {
185	IntegerPolyhedron set(PresburgerSpace::getSetSpace(numDims: 3, numSymbols: 2, numLocals: 1));
186
187	set.addInequality(inEq: {10, 11, 12, 20, 21, 30, 40});
188	set.removeVar(kind: VarKind::Symbol, pos: 1);
189	EXPECT_THAT(set.getInequality(0),
190	testing::ElementsAre(10, 11, 12, 20, 30, 40));
191
192	set.removeVarRange(kind: VarKind::SetDim, varStart: 0, varLimit: 2);
193	EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 30, 40));
194
195	set.removeVarRange(kind: VarKind::Local, varStart: 1, varLimit: 1);
196	EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 30, 40));
197
198	set.removeVarRange(kind: VarKind::Local, varStart: 0, varLimit: 1);
199	EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 40));
200	}
201
202	TEST(IntegerPolyhedronTest, FindSampleTest) {
203	// Bounded sets with only inequalities.
204	// 0 <= 7x <= 5
205	checkSample(hasSample: true,
206	poly: parseIntegerPolyhedron(str: "(x) : (7 * x >= 0, -7 * x + 5 >= 0)"));
207
208	// 1 <= 5x and 5x <= 4 (no solution).
209	checkSample(
210	hasSample: false, poly: parseIntegerPolyhedron(str: "(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)"));
211
212	// 1 <= 5x and 5x <= 9 (solution: x = 1).
213	checkSample(
214	hasSample: true, poly: parseIntegerPolyhedron(str: "(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(hasSample: true, poly: parseIntegerPolyhedron(
219	str: "(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(hasSample: true,
224	poly: parseIntegerPolyhedron(str: "(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(hasSample: false,
230	poly: parseIntegerPolyhedron(str: "(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(hasSample: true, poly: parseIntegerPolyhedron(
236	str: "(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(hasSample: false,
241	poly: parseIntegerPolyhedron(str: "(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	hasSample: true, poly: parseIntegerPolyhedron(str: "(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	hasSample: true, nDim: 3,
259	ineqs: {
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	eqs: {});
267
268	// Same thing with some spurious extra dimensions equated to constants.
269	checkSample(hasSample: true,
270	poly: parseIntegerPolyhedron(
271	str: "(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(hasSample: false, nDim: 3,
279	ineqs: {
280	{0, 1, 0, 0},
281	{0, -300, 299, 0},
282	{300 * 299, -89400, -299, -100 * 299},
283	{-897, 894, 0, 598},
284	},
285	eqs: {});
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(hasSample: false,
292	poly: parseIntegerPolyhedron(
293	str: "(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(hasSample: false, poly: parseIntegerPolyhedron(
297	str: "(x,y) : (x >= 0, -x + 100 >= 0, "
298	"3 * x - 3 * y + 2 >= 0, -3 * x + 3 * y - 1 >= 0)"));
299
300	checkSample(hasSample: true,
301	poly: parseIntegerPolyhedron(str: "(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(hasSample: true, poly: parseIntegerPolyhedron(
307	str: "(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	hasSample: true /* not empty */, nDim: 5,
319	ineqs: {
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	eqs: {});
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	hasSample: false /* empty */, nDim: 5,
340	ineqs: {
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	eqs: {});
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	hasSample: false /* empty */, nDim: 5,
362	ineqs: {
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	eqs: {
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(hasSample: false /* empty */, nDim: 5,
388	ineqs: {
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	eqs: {});
402
403	// Cartesian product of same tetrahedron as above and
404	// {(p, q) : 1/3 <= p <= 2/3}.
405	checkPermutationsSample(hasSample: false /* empty */, nDim: 5,
406	ineqs: {
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	eqs: {});
420
421	checkSample(hasSample: true, poly: parseIntegerPolyhedron(
422	str: "(x, y, z) : (2 * x - 1 >= 0, x - y - 1 == 0, "
423	"y - z == 0)"));
424
425	// Test with a local id.
426	checkSample(hasSample: true, poly: parseIntegerPolyhedron(str: "(x) : (x == 5*(x floordiv 2))"));
427
428	// Regression tests for the computation of dual coefficients.
429	checkSample(hasSample: false, poly: parseIntegerPolyhedron(str: "(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(hasSample: true, poly: parseIntegerPolyhedron(str: "(x, y, z) : ("
436	"3*x + 3*y + 3 >= 0,"
437	"-4*x - 8*y - z + 4 >= 0,"
438	"-7*x - 4*y + z + 1 >= 0,"
439	"2*x - 7*y - 8*z - 7 >= 0,"
440	"9*x + 8*y - 9*z - 7 >= 0)"));
441	}
442
443	TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) {
444	// 1 <= 5x and 5x <= 4 (no solution).
445	EXPECT_TRUE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)")
446	.isIntegerEmpty());
447	// 1 <= 5x and 5x <= 9 (solution: x = 1).
448	EXPECT_FALSE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)")
449	.isIntegerEmpty());
450
451	// Unbounded sets.
452	EXPECT_TRUE(
453	parseIntegerPolyhedron("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, "
454	"2 * z - 1 >= 0, 2 * x - 1 == 0)")
455	.isIntegerEmpty());
456
457	EXPECT_FALSE(parseIntegerPolyhedron(
458	"(x,y,z) : (2 * x - 1 >= 0, -3 * x + 3 >= 0, "
459	"5 * z - 6 >= 0, -7 * z + 17 >= 0, 3 * y - 2 >= 0)")
460	.isIntegerEmpty());
461
462	EXPECT_FALSE(parseIntegerPolyhedron(
463	"(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)")
464	.isIntegerEmpty());
465
466	// IntegerPolyhedron::isEmpty() does not detect the following sets to be
467	// empty.
468
469	// 3x + 7y = 1 and 0 <= x, y <= 10.
470	// Since x and y are non-negative, 3x + 7y can never be 1.
471	EXPECT_TRUE(parseIntegerPolyhedron(
472	"(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, "
473	"3 * x + 7 * y - 1 == 0)")
474	.isIntegerEmpty());
475
476	// 2x = 3y and y = x - 1 and x + y = 6z + 2 and 0 <= x, y <= 100.
477	// Substituting y = x - 1 in 3y = 2x, we obtain x = 3 and hence y = 2.
478	// Since x + y = 5 cannot be equal to 6z + 2 for any z, the set is empty.
479	EXPECT_TRUE(parseIntegerPolyhedron(
480	"(x,y,z) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, "
481	"2 * x - 3 * y == 0, x - y - 1 == 0, x + y - 6 * z - 2 == 0)")
482	.isIntegerEmpty());
483
484	// 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100.
485	// 2x = 3y implies x is a multiple of 3 and y is even.
486	// Now y = x - 1 + 6z implies y = 2 mod 3. In fact, since y is even, we have
487	// y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying
488	// x + y = 5 mod 6, which contradicts x + y = 6q + 2, so the set is empty.
489	EXPECT_TRUE(
490	parseIntegerPolyhedron(
491	"(x,y,z,q) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, "
492	"2 * x - 3 * y == 0, x - y + 6 * z - 1 == 0, x + y - 6 * q - 2 == 0)")
493	.isIntegerEmpty());
494
495	// Set with symbols.
496	EXPECT_FALSE(parseIntegerPolyhedron("(x)[s] : (x + s >= 0, x - s == 0)")
497	.isIntegerEmpty());
498	}
499
500	TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) {
501	IntegerPolyhedron poly =
502	parseIntegerPolyhedron(str: "(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(str: "(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(str: "(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	str: "(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	str: "(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(range: {0, 1, 0});
590	for (unsigned i = 0; i < 3; ++i) {
591	// Ensure that the removed constraint was the redundant constraint [3].
592	EXPECT_NE(poly5.getInequality(i),
593	ArrayRef<DynamicAPInt>(redundantConstraint));
594	}
595	}
596
597	TEST(IntegerPolyhedronTest, addConstantUpperBound) {
598	IntegerPolyhedron poly(PresburgerSpace::getSetSpace(numDims: 2));
599	poly.addBound(type: BoundType::UB, pos: 0, value: 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(type: BoundType::UB, expr: {1, 2, 3}, value: 1);
605	EXPECT_EQ(poly.atIneq(1, 0), -1);
606	EXPECT_EQ(poly.atIneq(1, 1), -2);
607	EXPECT_EQ(poly.atIneq(1, 2), -2);
608	}
609
610	TEST(IntegerPolyhedronTest, addConstantLowerBound) {
611	IntegerPolyhedron poly(PresburgerSpace::getSetSpace(numDims: 2));
612	poly.addBound(type: BoundType::LB, pos: 0, value: 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(type: BoundType::LB, expr: {1, 2, 3}, value: 1);
618	EXPECT_EQ(poly.atIneq(1, 0), 1);
619	EXPECT_EQ(poly.atIneq(1, 1), 2);
620	EXPECT_EQ(poly.atIneq(1, 2), 2);
621	}
622
623	/// Check if the expected division representation of local variables matches the
624	/// computed representation. The expected division representation is given as
625	/// a vector of expressions set in `expectedDividends` and the corressponding
626	/// denominator in `expectedDenominators`. The `denominators` and `dividends`
627	/// obtained through `getLocalRepr` function is verified against the
628	/// `expectedDenominators` and `expectedDividends` respectively.
629	static void checkDivisionRepresentation(
630	IntegerPolyhedron &poly,
631	const std::vector<SmallVector<int64_t, 8>> &expectedDividends,
632	ArrayRef<int64_t> expectedDenominators) {
633	DivisionRepr divs = poly.getLocalReprs();
634
635	// Check that the `denominators` and `expectedDenominators` match.
636	EXPECT_EQ(ArrayRef<DynamicAPInt>(getDynamicAPIntVec(expectedDenominators)),
637	divs.getDenoms());
638
639	// Check that the `dividends` and `expectedDividends` match. If the
640	// denominator for a division is zero, we ignore its dividend.
641	EXPECT_TRUE(divs.getNumDivs() == expectedDividends.size());
642	for (unsigned i = 0, e = divs.getNumDivs(); i < e; ++i) {
643	if (divs.hasRepr(i)) {
644	for (unsigned j = 0, f = divs.getNumVars() + 1; j < f; ++j) {
645	EXPECT_TRUE(expectedDividends[i][j] == divs.getDividend(i)[j]);
646	}
647	}
648	}
649	}
650
651	TEST(IntegerPolyhedronTest, computeLocalReprSimple) {
652	IntegerPolyhedron poly(PresburgerSpace::getSetSpace(numDims: 1));
653
654	poly.addLocalFloorDiv(dividend: {1, 4}, divisor: 10);
655	poly.addLocalFloorDiv(dividend: {1, 0, 100}, divisor: 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, expectedDividends: divisions, expectedDenominators: denoms);
664	}
665
666	TEST(IntegerPolyhedronTest, computeLocalReprConstantFloorDiv) {
667	IntegerPolyhedron poly(PresburgerSpace::getSetSpace(numDims: 4));
668
669	poly.addInequality(inEq: {1, 0, 3, 1, 2});
670	poly.addInequality(inEq: {1, 2, -8, 1, 10});
671	poly.addEquality(eq: {1, 2, -4, 1, 10});
672
673	poly.addLocalFloorDiv(dividend: {0, 0, 0, 0, 100}, divisor: 30);
674	poly.addLocalFloorDiv(dividend: {0, 0, 0, 0, 0, 206}, divisor: 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, expectedDividends: divisions, expectedDenominators: denoms);
682	}
683
684	TEST(IntegerPolyhedronTest, computeLocalReprRecursive) {
685	IntegerPolyhedron poly(PresburgerSpace::getSetSpace(numDims: 4));
686	poly.addInequality(inEq: {1, 0, 3, 1, 2});
687	poly.addInequality(inEq: {1, 2, -8, 1, 10});
688	poly.addEquality(eq: {1, 2, -4, 1, 10});
689
690	poly.addLocalFloorDiv(dividend: {0, -2, 7, 2, 10}, divisor: 3);
691	poly.addLocalFloorDiv(dividend: {3, 0, 9, 2, 2, 10}, divisor: 5);
692	poly.addLocalFloorDiv(dividend: {0, 1, -123, 2, 0, -4, 10}, divisor: 3);
693
694	poly.addInequality(inEq: {1, 2, -2, 1, -5, 0, 6, 100});
695	poly.addInequality(inEq: {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, expectedDividends: divisions, expectedDenominators: denoms);
706	}
707
708	TEST(IntegerPolyhedronTest, computeLocalReprTightUpperBound) {
709	{
710	IntegerPolyhedron poly = parseIntegerPolyhedron(str: "(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, expectedDividends: divisions, expectedDenominators: denoms);
727	}
728
729	{
730	IntegerPolyhedron poly = parseIntegerPolyhedron(
731	str: "(i, j, q) : (4*q - i - j + 2 >= 0, -4*q + i + j >= 0)");
732	// Convert `q` to a local variable.
733	poly.convertToLocal(kind: VarKind::SetDim, varStart: 2, varLimit: 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, expectedDividends: divisions, expectedDenominators: denoms);
740	}
741	}
742
743	TEST(IntegerPolyhedronTest, computeLocalReprFromEquality) {
744	{
745	IntegerPolyhedron poly =
746	parseIntegerPolyhedron(str: "(i, j, q) : (-4*q + i + j == 0)");
747	// Convert `q` to a local variable.
748	poly.convertToLocal(kind: VarKind::SetDim, varStart: 2, varLimit: 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, expectedDividends: divisions, expectedDenominators: denoms);
754	}
755	{
756	IntegerPolyhedron poly =
757	parseIntegerPolyhedron(str: "(i, j, q) : (4*q - i - j == 0)");
758	// Convert `q` to a local variable.
759	poly.convertToLocal(kind: VarKind::SetDim, varStart: 2, varLimit: 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, expectedDividends: divisions, expectedDenominators: denoms);
765	}
766	{
767	IntegerPolyhedron poly =
768	parseIntegerPolyhedron(str: "(i, j, q) : (3*q + i + j - 2 == 0)");
769	// Convert `q` to a local variable.
770	poly.convertToLocal(kind: VarKind::SetDim, varStart: 2, varLimit: 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, expectedDividends: divisions, expectedDenominators: denoms);
776	}
777	}
778
779	TEST(IntegerPolyhedronTest, computeLocalReprFromEqualityAndInequality) {
780	{
781	IntegerPolyhedron poly =
782	parseIntegerPolyhedron(str: "(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(kind: VarKind::SetDim, varStart: 2, varLimit: 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, expectedDividends: divisions, expectedDenominators: denoms);
792	}
793	}
794
795	TEST(IntegerPolyhedronTest, computeLocalReprNoRepr) {
796	IntegerPolyhedron poly =
797	parseIntegerPolyhedron(str: "(x, q) : (x - 3 * q >= 0, -x + 3 * q + 3 >= 0)");
798	// Convert q to a local variable.
799	poly.convertToLocal(kind: VarKind::SetDim, varStart: 1, varLimit: 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, expectedDividends: divisions, expectedDenominators: denoms);
806	}
807
808	TEST(IntegerPolyhedronTest, computeLocalReprNegConstNormalize) {
809	IntegerPolyhedron poly = parseIntegerPolyhedron(
810	str: "(x, q) : (-1 - 3*x - 6 * q >= 0, 6 + 3*x + 6*q >= 0)");
811	// Convert q to a local variable.
812	poly.convertToLocal(kind: VarKind::SetDim, varStart: 1, varLimit: 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, expectedDividends: divisions, expectedDenominators: denoms);
820	}
821
822	TEST(IntegerPolyhedronTest, simplifyLocalsTest) {
823	// (x) : (exists y: 2x + y = 1 and y = 2).
824	IntegerPolyhedron poly(PresburgerSpace::getSetSpace(numDims: 1, numSymbols: 0, numLocals: 1));
825	poly.addEquality(eq: {2, 1, -1});
826	poly.addEquality(eq: {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(numDims: 1, numSymbols: 0, numLocals: 3));
832	poly2.addEquality(eq: {3, 1, 0, 0, -1});
833	poly2.addEquality(eq: {0, 2, -1, 0, 0});
834	poly2.addEquality(eq: {0, 3, 0, -1, 0});
835	poly2.addEquality(eq: {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(numDims: 1, numSymbols: 0, numLocals: 1));
841	poly3.addInequality(inEq: {1, -1, -1});
842	poly3.addInequality(inEq: {0, 1, 1});
843	poly3.addEquality(eq: {2, 1, 0});
844
845	EXPECT_TRUE(poly3.isEmpty());
846	}
847
848	TEST(IntegerPolyhedronTest, mergeDivisionsSimple) {
849	{
850	// (x) : (exists z, y = [x / 2] : x = 3y and x + z + 1 >= 0).
851	IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(numDims: 1, numSymbols: 0, numLocals: 1));
852	poly1.addLocalFloorDiv(dividend: {1, 0, 0}, divisor: 2); // y = [x / 2].
853	poly1.addEquality(eq: {1, 0, -3, 0}); // x = 3y.
854	poly1.addInequality(inEq: {1, 1, 0, 1}); // x + z + 1 >= 0.
855
856	// (x) : (exists y = [x / 2], z : x = 5y).
857	IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(numDims: 1));
858	poly2.addLocalFloorDiv(dividend: {1, 0}, divisor: 2); // y = [x / 2].
859	poly2.addEquality(eq: {1, -5, 0}); // x = 5y.
860	poly2.appendVar(kind: VarKind::Local); // Add local id z.
861
862	poly1.mergeLocalVars(other&: 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(numDims: 1));
875	poly1.addLocalFloorDiv(dividend: {1, 0}, divisor: 5); // z = [x / 5].
876	poly1.addLocalFloorDiv(dividend: {1, 0, 0}, divisor: 2); // y = [x / 2].
877	poly1.addEquality(eq: {1, 0, -3, 0}); // x = 3y.
878
879	// (x) : (exists y = [x / 2], z = [x / 5]: x = 5z).
880	IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(numDims: 1));
881	poly2.addLocalFloorDiv(dividend: {1, 0}, divisor: 2); // y = [x / 2].
882	poly2.addLocalFloorDiv(dividend: {1, 0, 0}, divisor: 5); // z = [x / 5].
883	poly2.addEquality(eq: {1, 0, -5, 0}); // x = 5z.
884
885	poly1.mergeLocalVars(other&: 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(numDims: 1, numSymbols: 0, numLocals: 1));
899	// This division would be normalized.
900	poly1.addLocalFloorDiv(dividend: {3, 0, 0}, divisor: 6); // y = [3x / 6] -> [x/2].
901	poly1.addEquality(eq: {1, 0, -3, 0}); // x = 3z.
902	poly1.addInequality(inEq: {1, 1, 0, 1}); // x + y + 1 >= 0.
903
904	// (x) : (exists y = [x / 2], z : x = 5y).
905	IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(numDims: 1));
906	poly2.addLocalFloorDiv(dividend: {1, 0}, divisor: 2); // y = [x / 2].
907	poly2.addEquality(eq: {1, -5, 0}); // x = 5y.
908	poly2.appendVar(kind: VarKind::Local); // Add local id z.
909
910	poly1.mergeLocalVars(other&: poly2);
911
912	// Local space should be same.
913	EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
914
915	// One division should be matched + 2 unmatched local ids.
916	EXPECT_EQ(poly1.getNumLocalVars(), 3u);
917	EXPECT_EQ(poly2.getNumLocalVars(), 3u);
918	}
919	}
920
921	TEST(IntegerPolyhedronTest, mergeDivisionsNestedDivsions) {
922	{
923	// (x) : (exists y = [x / 2], z = [x + y / 3]: y + z >= x).
924	IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(numDims: 1));
925	poly1.addLocalFloorDiv(dividend: {1, 0}, divisor: 2); // y = [x / 2].
926	poly1.addLocalFloorDiv(dividend: {1, 1, 0}, divisor: 3); // z = [x + y / 3].
927	poly1.addInequality(inEq: {-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(numDims: 1));
931	poly2.addLocalFloorDiv(dividend: {1, 0}, divisor: 2); // y = [x / 2].
932	poly2.addLocalFloorDiv(dividend: {1, 1, 0}, divisor: 3); // z = [x + y / 3].
933	poly2.addInequality(inEq: {1, -1, -1, 0}); // y + z <= x.
934
935	poly1.mergeLocalVars(other&: 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(numDims: 1));
948	poly1.addLocalFloorDiv(dividend: {1, 0}, divisor: 2); // y = [x / 2].
949	poly1.addLocalFloorDiv(dividend: {1, 1, 0}, divisor: 3); // z = [x + y / 3].
950	poly1.addLocalFloorDiv(dividend: {0, 0, 1, 1}, divisor: 5); // w = [z + 1 / 5].
951	poly1.addInequality(inEq: {-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(numDims: 1));
955	poly2.addLocalFloorDiv(dividend: {1, 0}, divisor: 2); // y = [x / 2].
956	poly2.addLocalFloorDiv(dividend: {1, 1, 0}, divisor: 3); // z = [x + y / 3].
957	poly2.addLocalFloorDiv(dividend: {0, 0, 1, 1}, divisor: 5); // w = [z + 1 / 5].
958	poly2.addInequality(inEq: {1, -1, -1, 0, 0}); // y + z <= x.
959
960	poly1.mergeLocalVars(other&: 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(numDims: 1));
972	poly1.addLocalFloorDiv(dividend: {2, 0}, divisor: 4); // y = [2x / 4] -> [x / 2].
973	poly1.addLocalFloorDiv(dividend: {1, 1, 0}, divisor: 3); // z = [x + y / 3].
974	poly1.addInequality(inEq: {-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(numDims: 1));
978	poly2.addLocalFloorDiv(dividend: {1, 0}, divisor: 2); // y = [x / 2].
979	// This division would be normalized.
980	poly2.addLocalFloorDiv(dividend: {3, 3, 0}, divisor: 9); // z = [3x + 3y / 9] -> [x + y / 3].
981	poly2.addInequality(inEq: {1, -1, -1, 0}); // y + z <= x.
982
983	poly1.mergeLocalVars(other&: poly2);
984
985	// Local space should be same.
986	EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
987
988	// 2 divisions should be matched.
989	EXPECT_EQ(poly1.getNumLocalVars(), 2u);
990	EXPECT_EQ(poly2.getNumLocalVars(), 2u);
991	}
992	}
993
994	TEST(IntegerPolyhedronTest, mergeDivisionsConstants) {
995	{
996	// (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z >= x).
997	IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(numDims: 1));
998	poly1.addLocalFloorDiv(dividend: {1, 1}, divisor: 2); // y = [x + 1 / 2].
999	poly1.addLocalFloorDiv(dividend: {1, 0, 2}, divisor: 3); // z = [x + 2 / 3].
1000	poly1.addInequality(inEq: {-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(numDims: 1));
1004	poly2.addLocalFloorDiv(dividend: {1, 1}, divisor: 2); // y = [x + 1 / 2].
1005	poly2.addLocalFloorDiv(dividend: {1, 0, 2}, divisor: 3); // z = [x + 2 / 3].
1006	poly2.addInequality(inEq: {1, -1, -1, 0}); // y + z <= x.
1007
1008	poly1.mergeLocalVars(other&: 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(numDims: 1));
1020	poly1.addLocalFloorDiv(dividend: {1, 1}, divisor: 2); // y = [x + 1 / 2].
1021	// Normalization test.
1022	poly1.addLocalFloorDiv(dividend: {3, 0, 6}, divisor: 9); // z = [3x + 6 / 9] -> [x + 2 / 3].
1023	poly1.addInequality(inEq: {-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(numDims: 1));
1027	// Normalization test.
1028	poly2.addLocalFloorDiv(dividend: {2, 2}, divisor: 4); // y = [2x + 2 / 4] -> [x + 1 / 2].
1029	poly2.addLocalFloorDiv(dividend: {1, 0, 2}, divisor: 3); // z = [x + 2 / 3].
1030	poly2.addInequality(inEq: {1, -1, -1, 0}); // y + z <= x.
1031
1032	poly1.mergeLocalVars(other&: poly2);
1033
1034	// Local space should be same.
1035	EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
1036
1037	// 2 divisions should be matched.
1038	EXPECT_EQ(poly1.getNumLocalVars(), 2u);
1039	EXPECT_EQ(poly2.getNumLocalVars(), 2u);
1040	}
1041	}
1042
1043	TEST(IntegerPolyhedronTest, mergeDivisionsDuplicateInSameSet) {
1044	// (x) : (exists y = [x + 1 / 3], z = [x + 1 / 3]: y + z >= x).
1045	IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(numDims: 1));
1046	poly1.addLocalFloorDiv(dividend: {1, 1}, divisor: 3); // y = [x + 1 / 2].
1047	poly1.addLocalFloorDiv(dividend: {1, 0, 1}, divisor: 3); // z = [x + 1 / 3].
1048	poly1.addInequality(inEq: {-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(numDims: 1));
1052	poly2.addLocalFloorDiv(dividend: {1, 1}, divisor: 3); // y = [x + 1 / 3].
1053	poly2.addLocalFloorDiv(dividend: {1, 0, 2}, divisor: 3); // z = [x + 2 / 3].
1054	poly2.addInequality(inEq: {1, -1, -1, 0}); // y + z <= x.
1055
1056	poly1.mergeLocalVars(other&: poly2);
1057
1058	// Local space should be same.
1059	EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
1060
1061	// 1 divisions should be matched.
1062	EXPECT_EQ(poly1.getNumLocalVars(), 3u);
1063	EXPECT_EQ(poly2.getNumLocalVars(), 3u);
1064	}
1065
1066	TEST(IntegerPolyhedronTest, negativeDividends) {
1067	// (x) : (exists y = [-x + 1 / 2], z = [-x - 2 / 3]: y + z >= x).
1068	IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(numDims: 1));
1069	poly1.addLocalFloorDiv(dividend: {-1, 1}, divisor: 2); // y = [x + 1 / 2].
1070	// Normalization test with negative dividends
1071	poly1.addLocalFloorDiv(dividend: {-3, 0, -6}, divisor: 9); // z = [3x + 6 / 9] -> [x + 2 / 3].
1072	poly1.addInequality(inEq: {-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(numDims: 1));
1076	// Normalization test.
1077	poly2.addLocalFloorDiv(dividend: {-2, 2}, divisor: 4); // y = [-2x + 2 / 4] -> [-x + 1 / 2].
1078	poly2.addLocalFloorDiv(dividend: {-1, 0, -2}, divisor: 3); // z = [-x - 2 / 3].
1079	poly2.addInequality(inEq: {1, -1, -1, 0}); // y + z <= x.
1080
1081	poly1.mergeLocalVars(other&: 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(poly&: poly1, expectedDividends: divisions, expectedDenominators: denoms);
1088	}
1089
1090	void expectRationalLexMin(const IntegerPolyhedron &poly,
1091	ArrayRef<Fraction> min) {
1092	auto lexMin = poly.findRationalLexMin();
1093	ASSERT_TRUE(lexMin.isBounded());
1094	EXPECT_EQ(ArrayRef<Fraction>(*lexMin), min);
1095	}
1096
1097	void expectNoRationalLexMin(OptimumKind kind, const IntegerPolyhedron &poly) {
1098	ASSERT_NE(kind, OptimumKind::Bounded)
1099	<< "Use expectRationalLexMin for bounded min";
1100	EXPECT_EQ(poly.findRationalLexMin().getKind(), kind);
1101	}
1102
1103	TEST(IntegerPolyhedronTest, findRationalLexMin) {
1104	expectRationalLexMin(
1105	poly: parseIntegerPolyhedron(
1106	str: "(x, y, z) : (x + 10 >= 0, y + 40 >= 0, z + 30 >= 0)"),
1107	min: {{-10, 1}, {-40, 1}, {-30, 1}});
1108	expectRationalLexMin(
1109	poly: parseIntegerPolyhedron(
1110	str: "(x, y, z) : (2*x + 7 >= 0, 3*y - 5 >= 0, 8*z + 10 >= 0, 9*z >= 0)"),
1111	min: {{-7, 2}, {5, 3}, {0, 1}});
1112	expectRationalLexMin(
1113	poly: parseIntegerPolyhedron(str: "(x, y) : (3*x + 2*y + 10 >= 0, -3*y + 10 >= "
1114	"0, 4*x - 7*y - 10 >= 0)"),
1115	min: {{-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	poly: parseIntegerPolyhedron(
1121	str: "(x, y) : (x - 2*(x floordiv 2) == 0, y - 2*x >= 0, x - 11 >= 0)"),
1122	min: {{11, 1}, {22, 1}});
1123
1124	expectRationalLexMin(
1125	poly: parseIntegerPolyhedron(str: "(x, y) : (3*x + 2*y + 10 >= 0,"
1126	"-4*x + 7*y + 10 >= 0, -3*y + 10 >= 0)"),
1127	min: {{-50, 9}, {10, 3}});
1128
1129	// Cartesian product of above with itself.
1130	expectRationalLexMin(
1131	poly: parseIntegerPolyhedron(
1132	str: "(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	min: {{-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	poly: parseIntegerPolyhedron(
1144	str: "(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	min: {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}});
1148
1149	// Same as above with one constraint removed, making the lexmin unbounded.
1150	expectNoRationalLexMin(
1151	kind: OptimumKind::Unbounded,
1152	poly: parseIntegerPolyhedron(
1153	str: "(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	kind: OptimumKind::Unbounded,
1160	poly: parseIntegerPolyhedron(
1161	str: "(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	kind: OptimumKind::Empty,
1167	poly: parseIntegerPolyhedron(str: "(x) : (2*x >= 0, -x - 1 >= 0)"));
1168	}
1169
1170	void expectIntegerLexMin(const IntegerPolyhedron &poly, ArrayRef<int64_t> min) {
1171	MaybeOptimum<SmallVector<DynamicAPInt, 8>> lexMin = poly.findIntegerLexMin();
1172	ASSERT_TRUE(lexMin.isBounded());
1173	EXPECT_EQ(*lexMin, getDynamicAPIntVec(min));
1174	}
1175
1176	void expectNoIntegerLexMin(OptimumKind kind, const IntegerPolyhedron &poly) {
1177	ASSERT_NE(kind, OptimumKind::Bounded)
1178	<< "Use expectRationalLexMin for bounded min";
1179	EXPECT_EQ(poly.findRationalLexMin().getKind(), kind);
1180	}
1181
1182	TEST(IntegerPolyhedronTest, findIntegerLexMin) {
1183	expectIntegerLexMin(
1184	poly: parseIntegerPolyhedron(str: "(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 >= "
1185	"0, 11*z + 5*y - 3*x + 7 >= 0)"),
1186	min: {-6, -4, 0});
1187	// Similar to above but no lower bound on z.
1188	expectNoIntegerLexMin(
1189	kind: OptimumKind::Unbounded,
1190	poly: parseIntegerPolyhedron(str: "(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2 "
1191	">= 0, -11*z + 5*y - 3*x + 7 >= 0)"));
1192	}
1193
1194	void expectSymbolicIntegerLexMin(
1195	StringRef polyStr,
1196	ArrayRef<std::pair<StringRef, StringRef>> expectedLexminRepr,
1197	ArrayRef<StringRef> expectedUnboundedDomainRepr) {
1198	IntegerPolyhedron poly = parseIntegerPolyhedron(str: 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(pieces: 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(strs: expectedUnboundedDomainRepr);
1217	EXPECT_TRUE(result.unboundedDomain.isEqual(expectedUnboundedDomain));
1218	}
1219	}
1220
1221	void expectSymbolicIntegerLexMin(
1222	StringRef polyStr, ArrayRef<std::pair<StringRef, StringRef>> result) {
1223	expectSymbolicIntegerLexMin(polyStr, expectedLexminRepr: result, expectedUnboundedDomainRepr: {});
1224	}
1225
1226	TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) {
1227	expectSymbolicIntegerLexMin(polyStr: "(x)[a] : (x - a >= 0)",
1228	result: {
1229	{"()[a] : ()", "()[a] -> (a)"},
1230	});
1231
1232	expectSymbolicIntegerLexMin(
1233	polyStr: "(x)[a, b] : (x - a >= 0, x - b >= 0)",
1234	result: {
1235	{"()[a, b] : (a - b >= 0)", "()[a, b] -> (a)"},
1236	{"()[a, b] : (b - a - 1 >= 0)", "()[a, b] -> (b)"},
1237	});
1238
1239	expectSymbolicIntegerLexMin(
1240	polyStr: "(x)[a, b, c] : (x -a >= 0, x - b >= 0, x - c >= 0)",
1241	result: {
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(polyStr: "(x, y)[a] : (x - a >= 0, x + y >= 0)",
1249	result: {
1250	{"()[a] : ()", "()[a] -> (a, -a)"},
1251	});
1252
1253	expectSymbolicIntegerLexMin(polyStr: "(x, y)[a] : (x - a >= 0, x + y >= 0, y >= 0)",
1254	result: {
1255	{"()[a] : (a >= 0)", "()[a] -> (a, 0)"},
1256	{"()[a] : (-a - 1 >= 0)", "()[a] -> (a, -a)"},
1257	});
1258
1259	expectSymbolicIntegerLexMin(
1260	polyStr: "(x, y)[a, b, c] : (x - a >= 0, y - b >= 0, c - x - y >= 0)",
1261	result: {
1262	{"()[a, b, c] : (c - a - b >= 0)", "()[a, b, c] -> (a, b)"},
1263	});
1264
1265	expectSymbolicIntegerLexMin(
1266	polyStr: "(x, y, z)[a, b, c] : (c - z >= 0, b - y >= 0, x + y + z - a == 0)",
1267	result: {
1268	{"()[a, b, c] : ()", "()[a, b, c] -> (a - b - c, b, c)"},
1269	});
1270
1271	expectSymbolicIntegerLexMin(
1272	polyStr: "(x)[a, b] : (a >= 0, b >= 0, x >= 0, a + b + x - 1 >= 0)",
1273	result: {
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	polyStr: "(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	result: {
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	polyStr: "(x, y, z)[a, b] : (x - a == 0, y - b == 0, x >= 0, y >= 0, z >= 0, x + "
1290	"y + z - 1 >= 0)",
1291	result: {
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	polyStr: "(x)[a, b] : (x - a == 0, x - b >= 0)",
1300	result: {
1301	{"()[a, b] : (a - b >= 0)", "()[a, b] -> (a)"},
1302	});
1303
1304	expectSymbolicIntegerLexMin(
1305	polyStr: "(q)[a] : (a - 1 - 3*q == 0, q >= 0)",
1306	result: {
1307	{"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",
1308	"()[a] -> (a floordiv 3)"},
1309	});
1310
1311	expectSymbolicIntegerLexMin(
1312	polyStr: "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 1 - r >= 0, r >= 0)",
1313	result: {
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	polyStr: "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 2 - r >= 0, r - 1 >= 0)",
1322	result: {
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	polyStr: "(r, q)[a] : (a - r - 3*q == 0, q >= 0, r >= 0)",
1331	result: {
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	polyStr: "(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	result: {
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	polyStr: "(x, y)[a, r] : (a >= 0, r - a + 14*x + 35*y == 0)", expectedLexminRepr: {},
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	expectedUnboundedDomainRepr: {"()[a, r] : (a >= 0, r - a - 7*((r - a) floordiv 7) == 0)"});
1367
1368	// The lexmins are unbounded.
1369	expectSymbolicIntegerLexMin(polyStr: "(x, y)[a] : (9*x - 4*y - 2*a >= 0)", expectedLexminRepr: {},
1370	expectedUnboundedDomainRepr: {"()[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	polyStr: "(b, c)[a] : (a - 4*b + 2*c == 0, c - b >= 0)",
1377	result: {
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	polyStr: "(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	result: {
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	polyStr: "(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	result: {
1401	{"()[K, N, x, y] : (x + 6 - 2*N >= 0, 2*N - 5 - x >= 0, x + 1 -3*K + "
1402	"N >= 0, N + K - 2 - x >= 0, x - 4 >= 0)",
1403	"()[K, N, x, y] -> (1 + x, N)"},
1404	});
1405	}
1406
1407	static void
1408	expectComputedVolumeIsValidOverapprox(const IntegerPolyhedron &poly,
1409	std::optional<int64_t> trueVolume,
1410	std::optional<int64_t> resultBound) {
1411	expectComputedVolumeIsValidOverapprox(computedVolume: poly.computeVolume(), trueVolume,
1412	resultBound);
1413	}
1414
1415	TEST(IntegerPolyhedronTest, computeVolume) {
1416	// 0 <= x <= 3 + 1/3, -5.5 <= y <= 2 + 3/5, 3 <= z <= 1.75.
1417	// i.e. 0 <= x <= 3, -5 <= y <= 2, 3 <= z <= 3 + 1/4.
1418	// So volume is 4 * 8 * 1 = 32.
1419	expectComputedVolumeIsValidOverapprox(
1420	poly: parseIntegerPolyhedron(
1421	str: "(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	poly: parseIntegerPolyhedron(
1429	str: "(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	poly: parseIntegerPolyhedron(str: "(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	poly: parseIntegerPolyhedron(
1444	str: "(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	poly: parseIntegerPolyhedron(
1455	str: "(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	poly: parseIntegerPolyhedron(str: "(x, y) : (2*x - y >= 0, y - 3*x >= 0)"),
1463	/*trueVolume=*/{}, /*resultBound=*/{});
1464	}
1465
1466	bool containsPointNoLocal(const IntegerPolyhedron &poly,
1467	ArrayRef<int64_t> point) {
1468	return poly.containsPointNoLocal(point: getDynamicAPIntVec(range: point)).has_value();
1469	}
1470
1471	TEST(IntegerPolyhedronTest, containsPointNoLocal) {
1472	IntegerPolyhedron poly1 =
1473	parseIntegerPolyhedron(str: "(x) : ((x floordiv 2) - x == 0)");
1474	EXPECT_TRUE(poly1.containsPointNoLocal({0}));
1475	EXPECT_FALSE(poly1.containsPointNoLocal({1}));
1476
1477	IntegerPolyhedron poly2 = parseIntegerPolyhedron(
1478	str: "(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(str: "(x, y) : (2*x - y >= 0, y - 3*x >= 0)");
1484
1485	EXPECT_TRUE(poly3.containsPointNoLocal(ArrayRef<int64_t>({0, 0})));
1486	EXPECT_FALSE(poly3.containsPointNoLocal({1, 0}));
1487	}
1488
1489	TEST(IntegerPolyhedronTest, truncateEqualityRegressionTest) {
1490	// IntegerRelation::truncate was truncating inequalities to the number of
1491	// equalities.
1492	IntegerRelation set(PresburgerSpace::getSetSpace(numDims: 1));
1493	IntegerRelation::CountsSnapshot snapshot = set.getCounts();
1494	set.addEquality(eq: {1, 0});
1495	set.truncate(counts: snapshot);
1496	EXPECT_EQ(set.getNumEqualities(), 0u);
1497	}
1498