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