1 //===- SimplexTest.cpp - Tests for Simplex --------------------------------===//
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
12 #include "mlir/Analysis/Presburger/Simplex.h"
13 #include "mlir/IR/MLIRContext.h"
14
15 #include <gmock/gmock.h>
16 #include <gtest/gtest.h>
17 #include <optional>
18
19 using namespace mlir;
20 using namespace presburger;
21
22 /// Convenience functions to pass literals to Simplex.
addInequality(SimplexBase & simplex,ArrayRef<int64_t> coeffs)23 void addInequality(SimplexBase &simplex, ArrayRef<int64_t> coeffs) {
24 simplex.addInequality(getDynamicAPIntVec(coeffs));
25 }
addEquality(SimplexBase & simplex,ArrayRef<int64_t> coeffs)26 void addEquality(SimplexBase &simplex, ArrayRef<int64_t> coeffs) {
27 simplex.addEquality(getDynamicAPIntVec(coeffs));
28 }
isRedundantInequality(Simplex & simplex,ArrayRef<int64_t> coeffs)29 bool isRedundantInequality(Simplex &simplex, ArrayRef<int64_t> coeffs) {
30 return simplex.isRedundantInequality(getDynamicAPIntVec(coeffs));
31 }
isRedundantInequality(LexSimplex & simplex,ArrayRef<int64_t> coeffs)32 bool isRedundantInequality(LexSimplex &simplex, ArrayRef<int64_t> coeffs) {
33 return simplex.isRedundantInequality(getDynamicAPIntVec(coeffs));
34 }
isRedundantEquality(Simplex & simplex,ArrayRef<int64_t> coeffs)35 bool isRedundantEquality(Simplex &simplex, ArrayRef<int64_t> coeffs) {
36 return simplex.isRedundantEquality(getDynamicAPIntVec(coeffs));
37 }
isSeparateInequality(LexSimplex & simplex,ArrayRef<int64_t> coeffs)38 bool isSeparateInequality(LexSimplex &simplex, ArrayRef<int64_t> coeffs) {
39 return simplex.isSeparateInequality(getDynamicAPIntVec(coeffs));
40 }
41
findIneqType(Simplex & simplex,ArrayRef<int64_t> coeffs)42 Simplex::IneqType findIneqType(Simplex &simplex, ArrayRef<int64_t> coeffs) {
43 return simplex.findIneqType(getDynamicAPIntVec(coeffs));
44 }
45
46 /// Take a snapshot, add constraints making the set empty, and rollback.
47 /// The set should not be empty after rolling back. We add additional
48 /// constraints after the set is already empty and roll back the addition
49 /// of these. The set should be marked non-empty only once we rollback
50 /// past the addition of the first constraint that made it empty.
TEST(SimplexTest,emptyRollback)51 TEST(SimplexTest, emptyRollback) {
52 Simplex simplex(2);
53 // (u - v) >= 0
54 addInequality(simplex, {1, -1, 0});
55 ASSERT_FALSE(simplex.isEmpty());
56
57 unsigned snapshot = simplex.getSnapshot();
58 // (u - v) <= -1
59 addInequality(simplex, {-1, 1, -1});
60 ASSERT_TRUE(simplex.isEmpty());
61
62 unsigned snapshot2 = simplex.getSnapshot();
63 // (u - v) <= -3
64 addInequality(simplex, {-1, 1, -3});
65 ASSERT_TRUE(simplex.isEmpty());
66
67 simplex.rollback(snapshot2);
68 ASSERT_TRUE(simplex.isEmpty());
69
70 simplex.rollback(snapshot);
71 ASSERT_FALSE(simplex.isEmpty());
72 }
73
74 /// Check that the set gets marked as empty when we add contradictory
75 /// constraints.
TEST(SimplexTest,addEquality_separate)76 TEST(SimplexTest, addEquality_separate) {
77 Simplex simplex(1);
78 addInequality(simplex, {1, -1}); // x >= 1.
79 ASSERT_FALSE(simplex.isEmpty());
80 addEquality(simplex, {1, 0}); // x == 0.
81 EXPECT_TRUE(simplex.isEmpty());
82 }
83
expectInequalityMakesSetEmpty(Simplex & simplex,ArrayRef<int64_t> coeffs,bool expect)84 void expectInequalityMakesSetEmpty(Simplex &simplex, ArrayRef<int64_t> coeffs,
85 bool expect) {
86 ASSERT_FALSE(simplex.isEmpty());
87 unsigned snapshot = simplex.getSnapshot();
88 addInequality(simplex, coeffs);
89 EXPECT_EQ(simplex.isEmpty(), expect);
90 simplex.rollback(snapshot);
91 }
92
TEST(SimplexTest,addInequality_rollback)93 TEST(SimplexTest, addInequality_rollback) {
94 Simplex simplex(3);
95 SmallVector<int64_t, 4> coeffs[]{{1, 0, 0, 0}, // u >= 0.
96 {-1, 0, 0, 0}, // u <= 0.
97 {1, -1, 1, 0}, // u - v + w >= 0.
98 {1, 1, -1, 0}}; // u + v - w >= 0.
99 // The above constraints force u = 0 and v = w.
100 // The constraints below violate v = w.
101 SmallVector<int64_t, 4> checkCoeffs[]{{0, 1, -1, -1}, // v - w >= 1.
102 {0, -1, 1, -1}}; // v - w <= -1.
103
104 for (int run = 0; run < 4; run++) {
105 unsigned snapshot = simplex.getSnapshot();
106
107 expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], false);
108 expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], false);
109
110 for (int i = 0; i < 4; i++)
111 addInequality(simplex, coeffs[(run + i) % 4]);
112
113 expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], true);
114 expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], true);
115
116 simplex.rollback(snapshot);
117 EXPECT_EQ(simplex.getNumConstraints(), 0u);
118
119 expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], false);
120 expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], false);
121 }
122 }
123
simplexFromConstraints(unsigned nDim,ArrayRef<SmallVector<int64_t,8>> ineqs,ArrayRef<SmallVector<int64_t,8>> eqs)124 Simplex simplexFromConstraints(unsigned nDim,
125 ArrayRef<SmallVector<int64_t, 8>> ineqs,
126 ArrayRef<SmallVector<int64_t, 8>> eqs) {
127 Simplex simplex(nDim);
128 for (const auto &ineq : ineqs)
129 addInequality(simplex, ineq);
130 for (const auto &eq : eqs)
131 addEquality(simplex, eq);
132 return simplex;
133 }
134
TEST(SimplexTest,isUnbounded)135 TEST(SimplexTest, isUnbounded) {
136 EXPECT_FALSE(simplexFromConstraints(
137 2, {{1, 1, 0}, {-1, -1, 0}, {1, -1, 5}, {-1, 1, -5}}, {})
138 .isUnbounded());
139
140 EXPECT_TRUE(
141 simplexFromConstraints(2, {{1, 1, 0}, {1, -1, 5}, {-1, 1, -5}}, {})
142 .isUnbounded());
143
144 EXPECT_TRUE(
145 simplexFromConstraints(2, {{-1, -1, 0}, {1, -1, 5}, {-1, 1, -5}}, {})
146 .isUnbounded());
147
148 EXPECT_TRUE(simplexFromConstraints(2, {}, {}).isUnbounded());
149
150 EXPECT_FALSE(simplexFromConstraints(3,
151 {
152 {2, 0, 0, -1},
153 {-2, 0, 0, 1},
154 {0, 2, 0, -1},
155 {0, -2, 0, 1},
156 {0, 0, 2, -1},
157 {0, 0, -2, 1},
158 },
159 {})
160 .isUnbounded());
161
162 EXPECT_TRUE(simplexFromConstraints(3,
163 {
164 {2, 0, 0, -1},
165 {-2, 0, 0, 1},
166 {0, 2, 0, -1},
167 {0, -2, 0, 1},
168 {0, 0, -2, 1},
169 },
170 {})
171 .isUnbounded());
172
173 EXPECT_TRUE(simplexFromConstraints(3,
174 {
175 {2, 0, 0, -1},
176 {-2, 0, 0, 1},
177 {0, 2, 0, -1},
178 {0, -2, 0, 1},
179 {0, 0, 2, -1},
180 },
181 {})
182 .isUnbounded());
183
184 // Bounded set with equalities.
185 EXPECT_FALSE(simplexFromConstraints(2,
186 {{1, 1, 1}, // x + y >= -1.
187 {-1, -1, 1}}, // x + y <= 1.
188 {{1, -1, 0}} // x = y.
189 )
190 .isUnbounded());
191
192 // Unbounded set with equalities.
193 EXPECT_TRUE(simplexFromConstraints(3,
194 {{1, 1, 1, 1}, // x + y + z >= -1.
195 {-1, -1, -1, 1}}, // x + y + z <= 1.
196 {{1, -1, -1, 0}} // x = y + z.
197 )
198 .isUnbounded());
199
200 // Rational empty set.
201 EXPECT_FALSE(simplexFromConstraints(3,
202 {
203 {2, 0, 0, -1},
204 {-2, 0, 0, 1},
205 {0, 2, 2, -1},
206 {0, -2, -2, 1},
207 {3, 3, 3, -4},
208 },
209 {})
210 .isUnbounded());
211 }
212
TEST(SimplexTest,getSamplePointIfIntegral)213 TEST(SimplexTest, getSamplePointIfIntegral) {
214 // Empty set.
215 EXPECT_FALSE(simplexFromConstraints(3,
216 {
217 {2, 0, 0, -1},
218 {-2, 0, 0, 1},
219 {0, 2, 2, -1},
220 {0, -2, -2, 1},
221 {3, 3, 3, -4},
222 },
223 {})
224 .getSamplePointIfIntegral()
225 .has_value());
226
227 auto maybeSample = simplexFromConstraints(2,
228 {// x = y - 2.
229 {1, -1, 2},
230 {-1, 1, -2},
231 // x + y = 2.
232 {1, 1, -2},
233 {-1, -1, 2}},
234 {})
235 .getSamplePointIfIntegral();
236
237 EXPECT_TRUE(maybeSample.has_value());
238 EXPECT_THAT(*maybeSample, testing::ElementsAre(0, 2));
239
240 auto maybeSample2 = simplexFromConstraints(2,
241 {
242 {1, 0, 0}, // x >= 0.
243 {-1, 0, 0}, // x <= 0.
244 },
245 {
246 {0, 1, -2} // y = 2.
247 })
248 .getSamplePointIfIntegral();
249 EXPECT_TRUE(maybeSample2.has_value());
250 EXPECT_THAT(*maybeSample2, testing::ElementsAre(0, 2));
251
252 EXPECT_FALSE(simplexFromConstraints(1,
253 {// 2x = 1. (no integer solutions)
254 {2, -1},
255 {-2, +1}},
256 {})
257 .getSamplePointIfIntegral()
258 .has_value());
259 }
260
261 /// Some basic sanity checks involving zero or one variables.
TEST(SimplexTest,isMarkedRedundant_no_var_ge_zero)262 TEST(SimplexTest, isMarkedRedundant_no_var_ge_zero) {
263 Simplex simplex(0);
264 addInequality(simplex, {0}); // 0 >= 0.
265
266 simplex.detectRedundant();
267 ASSERT_FALSE(simplex.isEmpty());
268 EXPECT_TRUE(simplex.isMarkedRedundant(0));
269 }
270
TEST(SimplexTest,isMarkedRedundant_no_var_eq)271 TEST(SimplexTest, isMarkedRedundant_no_var_eq) {
272 Simplex simplex(0);
273 addEquality(simplex, {0}); // 0 == 0.
274 simplex.detectRedundant();
275 ASSERT_FALSE(simplex.isEmpty());
276 EXPECT_TRUE(simplex.isMarkedRedundant(0));
277 }
278
TEST(SimplexTest,isMarkedRedundant_pos_var_eq)279 TEST(SimplexTest, isMarkedRedundant_pos_var_eq) {
280 Simplex simplex(1);
281 addEquality(simplex, {1, 0}); // x == 0.
282
283 simplex.detectRedundant();
284 ASSERT_FALSE(simplex.isEmpty());
285 EXPECT_FALSE(simplex.isMarkedRedundant(0));
286 }
287
TEST(SimplexTest,isMarkedRedundant_zero_var_eq)288 TEST(SimplexTest, isMarkedRedundant_zero_var_eq) {
289 Simplex simplex(1);
290 addEquality(simplex, {0, 0}); // 0x == 0.
291 simplex.detectRedundant();
292 ASSERT_FALSE(simplex.isEmpty());
293 EXPECT_TRUE(simplex.isMarkedRedundant(0));
294 }
295
TEST(SimplexTest,isMarkedRedundant_neg_var_eq)296 TEST(SimplexTest, isMarkedRedundant_neg_var_eq) {
297 Simplex simplex(1);
298 addEquality(simplex, {-1, 0}); // -x == 0.
299 simplex.detectRedundant();
300 ASSERT_FALSE(simplex.isEmpty());
301 EXPECT_FALSE(simplex.isMarkedRedundant(0));
302 }
303
TEST(SimplexTest,isMarkedRedundant_pos_var_ge)304 TEST(SimplexTest, isMarkedRedundant_pos_var_ge) {
305 Simplex simplex(1);
306 addInequality(simplex, {1, 0}); // x >= 0.
307 simplex.detectRedundant();
308 ASSERT_FALSE(simplex.isEmpty());
309 EXPECT_FALSE(simplex.isMarkedRedundant(0));
310 }
311
TEST(SimplexTest,isMarkedRedundant_zero_var_ge)312 TEST(SimplexTest, isMarkedRedundant_zero_var_ge) {
313 Simplex simplex(1);
314 addInequality(simplex, {0, 0}); // 0x >= 0.
315 simplex.detectRedundant();
316 ASSERT_FALSE(simplex.isEmpty());
317 EXPECT_TRUE(simplex.isMarkedRedundant(0));
318 }
319
TEST(SimplexTest,isMarkedRedundant_neg_var_ge)320 TEST(SimplexTest, isMarkedRedundant_neg_var_ge) {
321 Simplex simplex(1);
322 addInequality(simplex, {-1, 0}); // x <= 0.
323 simplex.detectRedundant();
324 ASSERT_FALSE(simplex.isEmpty());
325 EXPECT_FALSE(simplex.isMarkedRedundant(0));
326 }
327
328 /// None of the constraints are redundant. Slightly more complicated test
329 /// involving an equality.
TEST(SimplexTest,isMarkedRedundant_no_redundant)330 TEST(SimplexTest, isMarkedRedundant_no_redundant) {
331 Simplex simplex(3);
332
333 addEquality(simplex, {-1, 0, 1, 0}); // u = w.
334 addInequality(simplex, {-1, 16, 0, 15}); // 15 - (u - 16v) >= 0.
335 addInequality(simplex, {1, -16, 0, 0}); // (u - 16v) >= 0.
336
337 simplex.detectRedundant();
338 ASSERT_FALSE(simplex.isEmpty());
339
340 for (unsigned i = 0; i < simplex.getNumConstraints(); ++i)
341 EXPECT_FALSE(simplex.isMarkedRedundant(i)) << "i = " << i << "\n";
342 }
343
TEST(SimplexTest,isMarkedRedundant_repeated_constraints)344 TEST(SimplexTest, isMarkedRedundant_repeated_constraints) {
345 Simplex simplex(3);
346
347 // [4] to [7] are repeats of [0] to [3].
348 addInequality(simplex, {0, -1, 0, 1}); // [0]: y <= 1.
349 addInequality(simplex, {-1, 0, 8, 7}); // [1]: 8z >= x - 7.
350 addInequality(simplex, {1, 0, -8, 0}); // [2]: 8z <= x.
351 addInequality(simplex, {0, 1, 0, 0}); // [3]: y >= 0.
352 addInequality(simplex, {-1, 0, 8, 7}); // [4]: 8z >= 7 - x.
353 addInequality(simplex, {1, 0, -8, 0}); // [5]: 8z <= x.
354 addInequality(simplex, {0, 1, 0, 0}); // [6]: y >= 0.
355 addInequality(simplex, {0, -1, 0, 1}); // [7]: y <= 1.
356
357 simplex.detectRedundant();
358 ASSERT_FALSE(simplex.isEmpty());
359
360 EXPECT_EQ(simplex.isMarkedRedundant(0), true);
361 EXPECT_EQ(simplex.isMarkedRedundant(1), true);
362 EXPECT_EQ(simplex.isMarkedRedundant(2), true);
363 EXPECT_EQ(simplex.isMarkedRedundant(3), true);
364 EXPECT_EQ(simplex.isMarkedRedundant(4), false);
365 EXPECT_EQ(simplex.isMarkedRedundant(5), false);
366 EXPECT_EQ(simplex.isMarkedRedundant(6), false);
367 EXPECT_EQ(simplex.isMarkedRedundant(7), false);
368 }
369
TEST(SimplexTest,isMarkedRedundant)370 TEST(SimplexTest, isMarkedRedundant) {
371 Simplex simplex(3);
372 addInequality(simplex, {0, -1, 0, 1}); // [0]: y <= 1.
373 addInequality(simplex, {1, 0, 0, -1}); // [1]: x >= 1.
374 addInequality(simplex, {-1, 0, 0, 2}); // [2]: x <= 2.
375 addInequality(simplex, {-1, 0, 2, 7}); // [3]: 2z >= x - 7.
376 addInequality(simplex, {1, 0, -2, 0}); // [4]: 2z <= x.
377 addInequality(simplex, {0, 1, 0, 0}); // [5]: y >= 0.
378 addInequality(simplex, {0, 1, -2, 1}); // [6]: y >= 2z - 1.
379 addInequality(simplex, {-1, 1, 0, 1}); // [7]: y >= x - 1.
380
381 simplex.detectRedundant();
382 ASSERT_FALSE(simplex.isEmpty());
383
384 // [0], [1], [3], [4], [7] together imply [2], [5], [6] must hold.
385 //
386 // From [7], [0]: x <= y + 1 <= 2, so we have [2].
387 // From [7], [1]: y >= x - 1 >= 0, so we have [5].
388 // From [4], [7]: 2z - 1 <= x - 1 <= y, so we have [6].
389 EXPECT_FALSE(simplex.isMarkedRedundant(0));
390 EXPECT_FALSE(simplex.isMarkedRedundant(1));
391 EXPECT_TRUE(simplex.isMarkedRedundant(2));
392 EXPECT_FALSE(simplex.isMarkedRedundant(3));
393 EXPECT_FALSE(simplex.isMarkedRedundant(4));
394 EXPECT_TRUE(simplex.isMarkedRedundant(5));
395 EXPECT_TRUE(simplex.isMarkedRedundant(6));
396 EXPECT_FALSE(simplex.isMarkedRedundant(7));
397 }
398
TEST(SimplexTest,isMarkedRedundantTiledLoopNestConstraints)399 TEST(SimplexTest, isMarkedRedundantTiledLoopNestConstraints) {
400 Simplex simplex(3); // Variables are x, y, N.
401 addInequality(simplex, {1, 0, 0, 0}); // [0]: x >= 0.
402 addInequality(simplex, {-32, 0, 1, -1}); // [1]: 32x <= N - 1.
403 addInequality(simplex, {0, 1, 0, 0}); // [2]: y >= 0.
404 addInequality(simplex, {-32, 1, 0, 0}); // [3]: y >= 32x.
405 addInequality(simplex, {32, -1, 0, 31}); // [4]: y <= 32x + 31.
406 addInequality(simplex, {0, -1, 1, -1}); // [5]: y <= N - 1.
407 // [3] and [0] imply [2], as we have y >= 32x >= 0.
408 // [3] and [5] imply [1], as we have 32x <= y <= N - 1.
409 simplex.detectRedundant();
410 EXPECT_FALSE(simplex.isMarkedRedundant(0));
411 EXPECT_TRUE(simplex.isMarkedRedundant(1));
412 EXPECT_TRUE(simplex.isMarkedRedundant(2));
413 EXPECT_FALSE(simplex.isMarkedRedundant(3));
414 EXPECT_FALSE(simplex.isMarkedRedundant(4));
415 EXPECT_FALSE(simplex.isMarkedRedundant(5));
416 }
417
TEST(SimplexTest,pivotRedundantRegressionTest)418 TEST(SimplexTest, pivotRedundantRegressionTest) {
419 Simplex simplex(2);
420 addInequality(simplex, {-1, 0, -1}); // x <= -1.
421 unsigned snapshot = simplex.getSnapshot();
422
423 addInequality(simplex, {-1, 0, -2}); // x <= -2.
424 addInequality(simplex, {-3, 0, -6});
425
426 // This first marks x <= -1 as redundant. Then it performs some more pivots
427 // to check if the other constraints are redundant. Pivot must update the
428 // non-redundant rows as well, otherwise these pivots result in an incorrect
429 // tableau state. In particular, after the rollback below, some rows that are
430 // NOT marked redundant will have an incorrect state.
431 simplex.detectRedundant();
432
433 // After the rollback, the only remaining constraint is x <= -1.
434 // The maximum value of x should be -1.
435 simplex.rollback(snapshot);
436 MaybeOptimum<Fraction> maxX = simplex.computeOptimum(
437 Simplex::Direction::Up, getDynamicAPIntVec({1, 0, 0}));
438 EXPECT_TRUE(maxX.isBounded() && *maxX == Fraction(-1, 1));
439 }
440
TEST(SimplexTest,addInequality_already_redundant)441 TEST(SimplexTest, addInequality_already_redundant) {
442 Simplex simplex(1);
443 addInequality(simplex, {1, -1}); // x >= 1.
444 addInequality(simplex, {1, 0}); // x >= 0.
445 simplex.detectRedundant();
446 ASSERT_FALSE(simplex.isEmpty());
447 EXPECT_FALSE(simplex.isMarkedRedundant(0));
448 EXPECT_TRUE(simplex.isMarkedRedundant(1));
449 }
450
TEST(SimplexTest,appendVariable)451 TEST(SimplexTest, appendVariable) {
452 Simplex simplex(1);
453
454 unsigned snapshot1 = simplex.getSnapshot();
455 simplex.appendVariable();
456 simplex.appendVariable(0);
457 EXPECT_EQ(simplex.getNumVariables(), 2u);
458
459 int64_t yMin = 2, yMax = 5;
460 addInequality(simplex, {0, 1, -yMin}); // y >= 2.
461 addInequality(simplex, {0, -1, yMax}); // y <= 5.
462
463 unsigned snapshot2 = simplex.getSnapshot();
464 simplex.appendVariable(2);
465 EXPECT_EQ(simplex.getNumVariables(), 4u);
466 simplex.rollback(snapshot2);
467
468 EXPECT_EQ(simplex.getNumVariables(), 2u);
469 EXPECT_EQ(simplex.getNumConstraints(), 2u);
470 EXPECT_EQ(simplex.computeIntegerBounds(getDynamicAPIntVec({0, 1, 0})),
471 std::make_pair(MaybeOptimum<DynamicAPInt>(DynamicAPInt(yMin)),
472 MaybeOptimum<DynamicAPInt>(DynamicAPInt(yMax))));
473
474 simplex.rollback(snapshot1);
475 EXPECT_EQ(simplex.getNumVariables(), 1u);
476 EXPECT_EQ(simplex.getNumConstraints(), 0u);
477 }
478
TEST(SimplexTest,isRedundantInequality)479 TEST(SimplexTest, isRedundantInequality) {
480 Simplex simplex(2);
481 addInequality(simplex, {0, -1, 2}); // y <= 2.
482 addInequality(simplex, {1, 0, 0}); // x >= 0.
483 addEquality(simplex, {-1, 1, 0}); // y = x.
484
485 EXPECT_TRUE(isRedundantInequality(simplex, {-1, 0, 2})); // x <= 2.
486 EXPECT_TRUE(isRedundantInequality(simplex, {0, 1, 0})); // y >= 0.
487
488 EXPECT_FALSE(isRedundantInequality(simplex, {-1, 0, -1})); // x <= -1.
489 EXPECT_FALSE(isRedundantInequality(simplex, {0, 1, -2})); // y >= 2.
490 EXPECT_FALSE(isRedundantInequality(simplex, {0, 1, -1})); // y >= 1.
491 }
492
TEST(SimplexTest,ineqType)493 TEST(SimplexTest, ineqType) {
494 Simplex simplex(2);
495 addInequality(simplex, {0, -1, 2}); // y <= 2.
496 addInequality(simplex, {1, 0, 0}); // x >= 0.
497 addEquality(simplex, {-1, 1, 0}); // y = x.
498
499 EXPECT_EQ(findIneqType(simplex, {-1, 0, 2}),
500 Simplex::IneqType::Redundant); // x <= 2.
501 EXPECT_EQ(findIneqType(simplex, {0, 1, 0}),
502 Simplex::IneqType::Redundant); // y >= 0.
503
504 EXPECT_EQ(findIneqType(simplex, {0, 1, -1}),
505 Simplex::IneqType::Cut); // y >= 1.
506 EXPECT_EQ(findIneqType(simplex, {-1, 0, 1}),
507 Simplex::IneqType::Cut); // x <= 1.
508 EXPECT_EQ(findIneqType(simplex, {0, 1, -2}),
509 Simplex::IneqType::Cut); // y >= 2.
510
511 EXPECT_EQ(findIneqType(simplex, {-1, 0, -1}),
512 Simplex::IneqType::Separate); // x <= -1.
513 }
514
TEST(SimplexTest,isRedundantEquality)515 TEST(SimplexTest, isRedundantEquality) {
516 Simplex simplex(2);
517 addInequality(simplex, {0, -1, 2}); // y <= 2.
518 addInequality(simplex, {1, 0, 0}); // x >= 0.
519 addEquality(simplex, {-1, 1, 0}); // y = x.
520
521 EXPECT_TRUE(isRedundantEquality(simplex, {-1, 1, 0})); // y = x.
522 EXPECT_TRUE(isRedundantEquality(simplex, {1, -1, 0})); // x = y.
523
524 EXPECT_FALSE(isRedundantEquality(simplex, {0, 1, -1})); // y = 1.
525
526 addEquality(simplex, {0, -1, 2}); // y = 2.
527
528 EXPECT_TRUE(isRedundantEquality(simplex, {-1, 0, 2})); // x = 2.
529 }
530
TEST(SimplexTest,IsRationalSubsetOf)531 TEST(SimplexTest, IsRationalSubsetOf) {
532 IntegerPolyhedron univ = parseIntegerPolyhedron("(x) : ()");
533 IntegerPolyhedron empty =
534 parseIntegerPolyhedron("(x) : (x + 0 >= 0, -x - 1 >= 0)");
535 IntegerPolyhedron s1 = parseIntegerPolyhedron("(x) : ( x >= 0, -x + 4 >= 0)");
536 IntegerPolyhedron s2 =
537 parseIntegerPolyhedron("(x) : (x - 1 >= 0, -x + 3 >= 0)");
538
539 Simplex simUniv(univ);
540 Simplex simEmpty(empty);
541 Simplex sim1(s1);
542 Simplex sim2(s2);
543
544 EXPECT_TRUE(simUniv.isRationalSubsetOf(univ));
545 EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty));
546 EXPECT_TRUE(sim1.isRationalSubsetOf(s1));
547 EXPECT_TRUE(sim2.isRationalSubsetOf(s2));
548
549 EXPECT_TRUE(simEmpty.isRationalSubsetOf(univ));
550 EXPECT_TRUE(simEmpty.isRationalSubsetOf(s1));
551 EXPECT_TRUE(simEmpty.isRationalSubsetOf(s2));
552 EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty));
553
554 EXPECT_TRUE(simUniv.isRationalSubsetOf(univ));
555 EXPECT_FALSE(simUniv.isRationalSubsetOf(s1));
556 EXPECT_FALSE(simUniv.isRationalSubsetOf(s2));
557 EXPECT_FALSE(simUniv.isRationalSubsetOf(empty));
558
559 EXPECT_TRUE(sim1.isRationalSubsetOf(univ));
560 EXPECT_TRUE(sim1.isRationalSubsetOf(s1));
561 EXPECT_FALSE(sim1.isRationalSubsetOf(s2));
562 EXPECT_FALSE(sim1.isRationalSubsetOf(empty));
563
564 EXPECT_TRUE(sim2.isRationalSubsetOf(univ));
565 EXPECT_TRUE(sim2.isRationalSubsetOf(s1));
566 EXPECT_TRUE(sim2.isRationalSubsetOf(s2));
567 EXPECT_FALSE(sim2.isRationalSubsetOf(empty));
568 }
569
TEST(SimplexTest,addDivisionVariable)570 TEST(SimplexTest, addDivisionVariable) {
571 Simplex simplex(/*nVar=*/1);
572 simplex.addDivisionVariable(getDynamicAPIntVec({1, 0}), DynamicAPInt(2));
573 addInequality(simplex, {1, 0, -3}); // x >= 3.
574 addInequality(simplex, {-1, 0, 9}); // x <= 9.
575 std::optional<SmallVector<DynamicAPInt, 8>> sample =
576 simplex.findIntegerSample();
577 ASSERT_TRUE(sample.has_value());
578 EXPECT_EQ((*sample)[0] / 2, (*sample)[1]);
579 }
580
TEST(SimplexTest,LexIneqType)581 TEST(SimplexTest, LexIneqType) {
582 LexSimplex simplex(/*nVar=*/1);
583 addInequality(simplex, {2, -1}); // x >= 1/2.
584
585 // Redundant inequality x >= 2/3.
586 EXPECT_TRUE(isRedundantInequality(simplex, {3, -2}));
587 EXPECT_FALSE(isSeparateInequality(simplex, {3, -2}));
588
589 // Separate inequality x <= 2/3.
590 EXPECT_FALSE(isRedundantInequality(simplex, {-3, 2}));
591 EXPECT_TRUE(isSeparateInequality(simplex, {-3, 2}));
592
593 // Cut inequality x <= 1.
594 EXPECT_FALSE(isRedundantInequality(simplex, {-1, 1}));
595 EXPECT_FALSE(isSeparateInequality(simplex, {-1, 1}));
596 }
597