mlir/unittests/Analysis/Presburger/SimplexTest.cpp

   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.
  23 void addInequality(SimplexBase &simplex, ArrayRef<int64_t> coeffs) {
  24   simplex.addInequality(getDynamicAPIntVec(coeffs));
  25 }
  26 void addEquality(SimplexBase &simplex, ArrayRef<int64_t> coeffs) {
  27   simplex.addEquality(getDynamicAPIntVec(coeffs));
  28 }
  29 bool isRedundantInequality(Simplex &simplex, ArrayRef<int64_t> coeffs) {
  30   return simplex.isRedundantInequality(getDynamicAPIntVec(coeffs));
  31 }
  32 bool isRedundantInequality(LexSimplex &simplex, ArrayRef<int64_t> coeffs) {
  33   return simplex.isRedundantInequality(getDynamicAPIntVec(coeffs));
  34 }
  35 bool isRedundantEquality(Simplex &simplex, ArrayRef<int64_t> coeffs) {
  36   return simplex.isRedundantEquality(getDynamicAPIntVec(coeffs));
  37 }
  38 bool isSeparateInequality(LexSimplex &simplex, ArrayRef<int64_t> coeffs) {
  39   return simplex.isSeparateInequality(getDynamicAPIntVec(coeffs));
  40 }
  41
  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.
  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.
  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
  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
  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
 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
 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
 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.
 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
 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
 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
 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
 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
 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
 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
 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.
 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
 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
 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
 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
 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
 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
 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
 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
 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
 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
 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
 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
 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 }