601 lines · 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-exception6//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 19using namespace mlir;20using namespace presburger;21 22/// Convenience functions to pass literals to Simplex.23static void addInequality(SimplexBase &simplex, ArrayRef<int64_t> coeffs) {24 simplex.addInequality(getDynamicAPIntVec(coeffs));25}26static void addEquality(SimplexBase &simplex, ArrayRef<int64_t> coeffs) {27 simplex.addEquality(getDynamicAPIntVec(coeffs));28}29static bool isRedundantInequality(Simplex &simplex, ArrayRef<int64_t> coeffs) {30 return simplex.isRedundantInequality(getDynamicAPIntVec(coeffs));31}32static bool isRedundantInequality(LexSimplex &simplex,33 ArrayRef<int64_t> coeffs) {34 return simplex.isRedundantInequality(getDynamicAPIntVec(coeffs));35}36static bool isRedundantEquality(Simplex &simplex, ArrayRef<int64_t> coeffs) {37 return simplex.isRedundantEquality(getDynamicAPIntVec(coeffs));38}39static bool isSeparateInequality(LexSimplex &simplex,40 ArrayRef<int64_t> coeffs) {41 return simplex.isSeparateInequality(getDynamicAPIntVec(coeffs));42}43 44static Simplex::IneqType findIneqType(Simplex &simplex,45 ArrayRef<int64_t> coeffs) {46 return simplex.findIneqType(getDynamicAPIntVec(coeffs));47}48 49/// Take a snapshot, add constraints making the set empty, and rollback.50/// The set should not be empty after rolling back. We add additional51/// constraints after the set is already empty and roll back the addition52/// of these. The set should be marked non-empty only once we rollback53/// past the addition of the first constraint that made it empty.54TEST(SimplexTest, emptyRollback) {55 Simplex simplex(2);56 // (u - v) >= 057 addInequality(simplex, {1, -1, 0});58 ASSERT_FALSE(simplex.isEmpty());59 60 unsigned snapshot = simplex.getSnapshot();61 // (u - v) <= -162 addInequality(simplex, {-1, 1, -1});63 ASSERT_TRUE(simplex.isEmpty());64 65 unsigned snapshot2 = simplex.getSnapshot();66 // (u - v) <= -367 addInequality(simplex, {-1, 1, -3});68 ASSERT_TRUE(simplex.isEmpty());69 70 simplex.rollback(snapshot2);71 ASSERT_TRUE(simplex.isEmpty());72 73 simplex.rollback(snapshot);74 ASSERT_FALSE(simplex.isEmpty());75}76 77/// Check that the set gets marked as empty when we add contradictory78/// constraints.79TEST(SimplexTest, addEquality_separate) {80 Simplex simplex(1);81 addInequality(simplex, {1, -1}); // x >= 1.82 ASSERT_FALSE(simplex.isEmpty());83 addEquality(simplex, {1, 0}); // x == 0.84 EXPECT_TRUE(simplex.isEmpty());85}86 87static void expectInequalityMakesSetEmpty(Simplex &simplex,88 ArrayRef<int64_t> coeffs,89 bool expect) {90 ASSERT_FALSE(simplex.isEmpty());91 unsigned snapshot = simplex.getSnapshot();92 addInequality(simplex, coeffs);93 EXPECT_EQ(simplex.isEmpty(), expect);94 simplex.rollback(snapshot);95}96 97TEST(SimplexTest, addInequality_rollback) {98 Simplex simplex(3);99 SmallVector<int64_t, 4> coeffs[]{{1, 0, 0, 0}, // u >= 0.100 {-1, 0, 0, 0}, // u <= 0.101 {1, -1, 1, 0}, // u - v + w >= 0.102 {1, 1, -1, 0}}; // u + v - w >= 0.103 // The above constraints force u = 0 and v = w.104 // The constraints below violate v = w.105 SmallVector<int64_t, 4> checkCoeffs[]{{0, 1, -1, -1}, // v - w >= 1.106 {0, -1, 1, -1}}; // v - w <= -1.107 108 for (int run = 0; run < 4; run++) {109 unsigned snapshot = simplex.getSnapshot();110 111 expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], false);112 expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], false);113 114 for (int i = 0; i < 4; i++)115 addInequality(simplex, coeffs[(run + i) % 4]);116 117 expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], true);118 expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], true);119 120 simplex.rollback(snapshot);121 EXPECT_EQ(simplex.getNumConstraints(), 0u);122 123 expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], false);124 expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], false);125 }126}127 128static Simplex simplexFromConstraints(unsigned nDim,129 ArrayRef<SmallVector<int64_t, 8>> ineqs,130 ArrayRef<SmallVector<int64_t, 8>> eqs) {131 Simplex simplex(nDim);132 for (const auto &ineq : ineqs)133 addInequality(simplex, ineq);134 for (const auto &eq : eqs)135 addEquality(simplex, eq);136 return simplex;137}138 139TEST(SimplexTest, isUnbounded) {140 EXPECT_FALSE(simplexFromConstraints(141 2, {{1, 1, 0}, {-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(149 simplexFromConstraints(2, {{-1, -1, 0}, {1, -1, 5}, {-1, 1, -5}}, {})150 .isUnbounded());151 152 EXPECT_TRUE(simplexFromConstraints(2, {}, {}).isUnbounded());153 154 EXPECT_FALSE(simplexFromConstraints(3,155 {156 {2, 0, 0, -1},157 {-2, 0, 0, 1},158 {0, 2, 0, -1},159 {0, -2, 0, 1},160 {0, 0, 2, -1},161 {0, 0, -2, 1},162 },163 {})164 .isUnbounded());165 166 EXPECT_TRUE(simplexFromConstraints(3,167 {168 {2, 0, 0, -1},169 {-2, 0, 0, 1},170 {0, 2, 0, -1},171 {0, -2, 0, 1},172 {0, 0, -2, 1},173 },174 {})175 .isUnbounded());176 177 EXPECT_TRUE(simplexFromConstraints(3,178 {179 {2, 0, 0, -1},180 {-2, 0, 0, 1},181 {0, 2, 0, -1},182 {0, -2, 0, 1},183 {0, 0, 2, -1},184 },185 {})186 .isUnbounded());187 188 // Bounded set with equalities.189 EXPECT_FALSE(simplexFromConstraints(2,190 {{1, 1, 1}, // x + y >= -1.191 {-1, -1, 1}}, // x + y <= 1.192 {{1, -1, 0}} // x = y.193 )194 .isUnbounded());195 196 // Unbounded set with equalities.197 EXPECT_TRUE(simplexFromConstraints(3,198 {{1, 1, 1, 1}, // x + y + z >= -1.199 {-1, -1, -1, 1}}, // x + y + z <= 1.200 {{1, -1, -1, 0}} // x = y + z.201 )202 .isUnbounded());203 204 // Rational empty set.205 EXPECT_FALSE(simplexFromConstraints(3,206 {207 {2, 0, 0, -1},208 {-2, 0, 0, 1},209 {0, 2, 2, -1},210 {0, -2, -2, 1},211 {3, 3, 3, -4},212 },213 {})214 .isUnbounded());215}216 217TEST(SimplexTest, getSamplePointIfIntegral) {218 // Empty set.219 EXPECT_FALSE(simplexFromConstraints(3,220 {221 {2, 0, 0, -1},222 {-2, 0, 0, 1},223 {0, 2, 2, -1},224 {0, -2, -2, 1},225 {3, 3, 3, -4},226 },227 {})228 .getSamplePointIfIntegral()229 .has_value());230 231 auto maybeSample = simplexFromConstraints(2,232 {// x = y - 2.233 {1, -1, 2},234 {-1, 1, -2},235 // x + y = 2.236 {1, 1, -2},237 {-1, -1, 2}},238 {})239 .getSamplePointIfIntegral();240 241 EXPECT_TRUE(maybeSample.has_value());242 EXPECT_THAT(*maybeSample, testing::ElementsAre(0, 2));243 244 auto maybeSample2 = simplexFromConstraints(2,245 {246 {1, 0, 0}, // x >= 0.247 {-1, 0, 0}, // x <= 0.248 },249 {250 {0, 1, -2} // y = 2.251 })252 .getSamplePointIfIntegral();253 EXPECT_TRUE(maybeSample2.has_value());254 EXPECT_THAT(*maybeSample2, testing::ElementsAre(0, 2));255 256 EXPECT_FALSE(simplexFromConstraints(1,257 {// 2x = 1. (no integer solutions)258 {2, -1},259 {-2, +1}},260 {})261 .getSamplePointIfIntegral()262 .has_value());263}264 265/// Some basic sanity checks involving zero or one variables.266TEST(SimplexTest, isMarkedRedundant_no_var_ge_zero) {267 Simplex simplex(0);268 addInequality(simplex, {0}); // 0 >= 0.269 270 simplex.detectRedundant();271 ASSERT_FALSE(simplex.isEmpty());272 EXPECT_TRUE(simplex.isMarkedRedundant(0));273}274 275TEST(SimplexTest, isMarkedRedundant_no_var_eq) {276 Simplex simplex(0);277 addEquality(simplex, {0}); // 0 == 0.278 simplex.detectRedundant();279 ASSERT_FALSE(simplex.isEmpty());280 EXPECT_TRUE(simplex.isMarkedRedundant(0));281}282 283TEST(SimplexTest, isMarkedRedundant_pos_var_eq) {284 Simplex simplex(1);285 addEquality(simplex, {1, 0}); // x == 0.286 287 simplex.detectRedundant();288 ASSERT_FALSE(simplex.isEmpty());289 EXPECT_FALSE(simplex.isMarkedRedundant(0));290}291 292TEST(SimplexTest, isMarkedRedundant_zero_var_eq) {293 Simplex simplex(1);294 addEquality(simplex, {0, 0}); // 0x == 0.295 simplex.detectRedundant();296 ASSERT_FALSE(simplex.isEmpty());297 EXPECT_TRUE(simplex.isMarkedRedundant(0));298}299 300TEST(SimplexTest, isMarkedRedundant_neg_var_eq) {301 Simplex simplex(1);302 addEquality(simplex, {-1, 0}); // -x == 0.303 simplex.detectRedundant();304 ASSERT_FALSE(simplex.isEmpty());305 EXPECT_FALSE(simplex.isMarkedRedundant(0));306}307 308TEST(SimplexTest, isMarkedRedundant_pos_var_ge) {309 Simplex simplex(1);310 addInequality(simplex, {1, 0}); // x >= 0.311 simplex.detectRedundant();312 ASSERT_FALSE(simplex.isEmpty());313 EXPECT_FALSE(simplex.isMarkedRedundant(0));314}315 316TEST(SimplexTest, isMarkedRedundant_zero_var_ge) {317 Simplex simplex(1);318 addInequality(simplex, {0, 0}); // 0x >= 0.319 simplex.detectRedundant();320 ASSERT_FALSE(simplex.isEmpty());321 EXPECT_TRUE(simplex.isMarkedRedundant(0));322}323 324TEST(SimplexTest, isMarkedRedundant_neg_var_ge) {325 Simplex simplex(1);326 addInequality(simplex, {-1, 0}); // x <= 0.327 simplex.detectRedundant();328 ASSERT_FALSE(simplex.isEmpty());329 EXPECT_FALSE(simplex.isMarkedRedundant(0));330}331 332/// None of the constraints are redundant. Slightly more complicated test333/// involving an equality.334TEST(SimplexTest, isMarkedRedundant_no_redundant) {335 Simplex simplex(3);336 337 addEquality(simplex, {-1, 0, 1, 0}); // u = w.338 addInequality(simplex, {-1, 16, 0, 15}); // 15 - (u - 16v) >= 0.339 addInequality(simplex, {1, -16, 0, 0}); // (u - 16v) >= 0.340 341 simplex.detectRedundant();342 ASSERT_FALSE(simplex.isEmpty());343 344 for (unsigned i = 0; i < simplex.getNumConstraints(); ++i)345 EXPECT_FALSE(simplex.isMarkedRedundant(i)) << "i = " << i << "\n";346}347 348TEST(SimplexTest, isMarkedRedundant_repeated_constraints) {349 Simplex simplex(3);350 351 // [4] to [7] are repeats of [0] to [3].352 addInequality(simplex, {0, -1, 0, 1}); // [0]: y <= 1.353 addInequality(simplex, {-1, 0, 8, 7}); // [1]: 8z >= x - 7.354 addInequality(simplex, {1, 0, -8, 0}); // [2]: 8z <= x.355 addInequality(simplex, {0, 1, 0, 0}); // [3]: y >= 0.356 addInequality(simplex, {-1, 0, 8, 7}); // [4]: 8z >= 7 - x.357 addInequality(simplex, {1, 0, -8, 0}); // [5]: 8z <= x.358 addInequality(simplex, {0, 1, 0, 0}); // [6]: y >= 0.359 addInequality(simplex, {0, -1, 0, 1}); // [7]: y <= 1.360 361 simplex.detectRedundant();362 ASSERT_FALSE(simplex.isEmpty());363 364 EXPECT_EQ(simplex.isMarkedRedundant(0), true);365 EXPECT_EQ(simplex.isMarkedRedundant(1), true);366 EXPECT_EQ(simplex.isMarkedRedundant(2), true);367 EXPECT_EQ(simplex.isMarkedRedundant(3), true);368 EXPECT_EQ(simplex.isMarkedRedundant(4), false);369 EXPECT_EQ(simplex.isMarkedRedundant(5), false);370 EXPECT_EQ(simplex.isMarkedRedundant(6), false);371 EXPECT_EQ(simplex.isMarkedRedundant(7), false);372}373 374TEST(SimplexTest, isMarkedRedundant) {375 Simplex simplex(3);376 addInequality(simplex, {0, -1, 0, 1}); // [0]: y <= 1.377 addInequality(simplex, {1, 0, 0, -1}); // [1]: x >= 1.378 addInequality(simplex, {-1, 0, 0, 2}); // [2]: x <= 2.379 addInequality(simplex, {-1, 0, 2, 7}); // [3]: 2z >= x - 7.380 addInequality(simplex, {1, 0, -2, 0}); // [4]: 2z <= x.381 addInequality(simplex, {0, 1, 0, 0}); // [5]: y >= 0.382 addInequality(simplex, {0, 1, -2, 1}); // [6]: y >= 2z - 1.383 addInequality(simplex, {-1, 1, 0, 1}); // [7]: y >= x - 1.384 385 simplex.detectRedundant();386 ASSERT_FALSE(simplex.isEmpty());387 388 // [0], [1], [3], [4], [7] together imply [2], [5], [6] must hold.389 //390 // From [7], [0]: x <= y + 1 <= 2, so we have [2].391 // From [7], [1]: y >= x - 1 >= 0, so we have [5].392 // From [4], [7]: 2z - 1 <= x - 1 <= y, so we have [6].393 EXPECT_FALSE(simplex.isMarkedRedundant(0));394 EXPECT_FALSE(simplex.isMarkedRedundant(1));395 EXPECT_TRUE(simplex.isMarkedRedundant(2));396 EXPECT_FALSE(simplex.isMarkedRedundant(3));397 EXPECT_FALSE(simplex.isMarkedRedundant(4));398 EXPECT_TRUE(simplex.isMarkedRedundant(5));399 EXPECT_TRUE(simplex.isMarkedRedundant(6));400 EXPECT_FALSE(simplex.isMarkedRedundant(7));401}402 403TEST(SimplexTest, isMarkedRedundantTiledLoopNestConstraints) {404 Simplex simplex(3); // Variables are x, y, N.405 addInequality(simplex, {1, 0, 0, 0}); // [0]: x >= 0.406 addInequality(simplex, {-32, 0, 1, -1}); // [1]: 32x <= N - 1.407 addInequality(simplex, {0, 1, 0, 0}); // [2]: y >= 0.408 addInequality(simplex, {-32, 1, 0, 0}); // [3]: y >= 32x.409 addInequality(simplex, {32, -1, 0, 31}); // [4]: y <= 32x + 31.410 addInequality(simplex, {0, -1, 1, -1}); // [5]: y <= N - 1.411 // [3] and [0] imply [2], as we have y >= 32x >= 0.412 // [3] and [5] imply [1], as we have 32x <= y <= N - 1.413 simplex.detectRedundant();414 EXPECT_FALSE(simplex.isMarkedRedundant(0));415 EXPECT_TRUE(simplex.isMarkedRedundant(1));416 EXPECT_TRUE(simplex.isMarkedRedundant(2));417 EXPECT_FALSE(simplex.isMarkedRedundant(3));418 EXPECT_FALSE(simplex.isMarkedRedundant(4));419 EXPECT_FALSE(simplex.isMarkedRedundant(5));420}421 422TEST(SimplexTest, pivotRedundantRegressionTest) {423 Simplex simplex(2);424 addInequality(simplex, {-1, 0, -1}); // x <= -1.425 unsigned snapshot = simplex.getSnapshot();426 427 addInequality(simplex, {-1, 0, -2}); // x <= -2.428 addInequality(simplex, {-3, 0, -6});429 430 // This first marks x <= -1 as redundant. Then it performs some more pivots431 // to check if the other constraints are redundant. Pivot must update the432 // non-redundant rows as well, otherwise these pivots result in an incorrect433 // tableau state. In particular, after the rollback below, some rows that are434 // NOT marked redundant will have an incorrect state.435 simplex.detectRedundant();436 437 // After the rollback, the only remaining constraint is x <= -1.438 // The maximum value of x should be -1.439 simplex.rollback(snapshot);440 MaybeOptimum<Fraction> maxX = simplex.computeOptimum(441 Simplex::Direction::Up, getDynamicAPIntVec({1, 0, 0}));442 EXPECT_TRUE(maxX.isBounded() && *maxX == Fraction(-1, 1));443}444 445TEST(SimplexTest, addInequality_already_redundant) {446 Simplex simplex(1);447 addInequality(simplex, {1, -1}); // x >= 1.448 addInequality(simplex, {1, 0}); // x >= 0.449 simplex.detectRedundant();450 ASSERT_FALSE(simplex.isEmpty());451 EXPECT_FALSE(simplex.isMarkedRedundant(0));452 EXPECT_TRUE(simplex.isMarkedRedundant(1));453}454 455TEST(SimplexTest, appendVariable) {456 Simplex simplex(1);457 458 unsigned snapshot1 = simplex.getSnapshot();459 simplex.appendVariable();460 simplex.appendVariable(0);461 EXPECT_EQ(simplex.getNumVariables(), 2u);462 463 int64_t yMin = 2, yMax = 5;464 addInequality(simplex, {0, 1, -yMin}); // y >= 2.465 addInequality(simplex, {0, -1, yMax}); // y <= 5.466 467 unsigned snapshot2 = simplex.getSnapshot();468 simplex.appendVariable(2);469 EXPECT_EQ(simplex.getNumVariables(), 4u);470 simplex.rollback(snapshot2);471 472 EXPECT_EQ(simplex.getNumVariables(), 2u);473 EXPECT_EQ(simplex.getNumConstraints(), 2u);474 EXPECT_EQ(simplex.computeIntegerBounds(getDynamicAPIntVec({0, 1, 0})),475 std::make_pair(MaybeOptimum<DynamicAPInt>(DynamicAPInt(yMin)),476 MaybeOptimum<DynamicAPInt>(DynamicAPInt(yMax))));477 478 simplex.rollback(snapshot1);479 EXPECT_EQ(simplex.getNumVariables(), 1u);480 EXPECT_EQ(simplex.getNumConstraints(), 0u);481}482 483TEST(SimplexTest, isRedundantInequality) {484 Simplex simplex(2);485 addInequality(simplex, {0, -1, 2}); // y <= 2.486 addInequality(simplex, {1, 0, 0}); // x >= 0.487 addEquality(simplex, {-1, 1, 0}); // y = x.488 489 EXPECT_TRUE(isRedundantInequality(simplex, {-1, 0, 2})); // x <= 2.490 EXPECT_TRUE(isRedundantInequality(simplex, {0, 1, 0})); // y >= 0.491 492 EXPECT_FALSE(isRedundantInequality(simplex, {-1, 0, -1})); // x <= -1.493 EXPECT_FALSE(isRedundantInequality(simplex, {0, 1, -2})); // y >= 2.494 EXPECT_FALSE(isRedundantInequality(simplex, {0, 1, -1})); // y >= 1.495}496 497TEST(SimplexTest, ineqType) {498 Simplex simplex(2);499 addInequality(simplex, {0, -1, 2}); // y <= 2.500 addInequality(simplex, {1, 0, 0}); // x >= 0.501 addEquality(simplex, {-1, 1, 0}); // y = x.502 503 EXPECT_EQ(findIneqType(simplex, {-1, 0, 2}),504 Simplex::IneqType::Redundant); // x <= 2.505 EXPECT_EQ(findIneqType(simplex, {0, 1, 0}),506 Simplex::IneqType::Redundant); // y >= 0.507 508 EXPECT_EQ(findIneqType(simplex, {0, 1, -1}),509 Simplex::IneqType::Cut); // y >= 1.510 EXPECT_EQ(findIneqType(simplex, {-1, 0, 1}),511 Simplex::IneqType::Cut); // x <= 1.512 EXPECT_EQ(findIneqType(simplex, {0, 1, -2}),513 Simplex::IneqType::Cut); // y >= 2.514 515 EXPECT_EQ(findIneqType(simplex, {-1, 0, -1}),516 Simplex::IneqType::Separate); // x <= -1.517}518 519TEST(SimplexTest, isRedundantEquality) {520 Simplex simplex(2);521 addInequality(simplex, {0, -1, 2}); // y <= 2.522 addInequality(simplex, {1, 0, 0}); // x >= 0.523 addEquality(simplex, {-1, 1, 0}); // y = x.524 525 EXPECT_TRUE(isRedundantEquality(simplex, {-1, 1, 0})); // y = x.526 EXPECT_TRUE(isRedundantEquality(simplex, {1, -1, 0})); // x = y.527 528 EXPECT_FALSE(isRedundantEquality(simplex, {0, 1, -1})); // y = 1.529 530 addEquality(simplex, {0, -1, 2}); // y = 2.531 532 EXPECT_TRUE(isRedundantEquality(simplex, {-1, 0, 2})); // x = 2.533}534 535TEST(SimplexTest, IsRationalSubsetOf) {536 IntegerPolyhedron univ = parseIntegerPolyhedron("(x) : ()");537 IntegerPolyhedron empty =538 parseIntegerPolyhedron("(x) : (x + 0 >= 0, -x - 1 >= 0)");539 IntegerPolyhedron s1 = parseIntegerPolyhedron("(x) : ( x >= 0, -x + 4 >= 0)");540 IntegerPolyhedron s2 =541 parseIntegerPolyhedron("(x) : (x - 1 >= 0, -x + 3 >= 0)");542 543 Simplex simUniv(univ);544 Simplex simEmpty(empty);545 Simplex sim1(s1);546 Simplex sim2(s2);547 548 EXPECT_TRUE(simUniv.isRationalSubsetOf(univ));549 EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty));550 EXPECT_TRUE(sim1.isRationalSubsetOf(s1));551 EXPECT_TRUE(sim2.isRationalSubsetOf(s2));552 553 EXPECT_TRUE(simEmpty.isRationalSubsetOf(univ));554 EXPECT_TRUE(simEmpty.isRationalSubsetOf(s1));555 EXPECT_TRUE(simEmpty.isRationalSubsetOf(s2));556 EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty));557 558 EXPECT_TRUE(simUniv.isRationalSubsetOf(univ));559 EXPECT_FALSE(simUniv.isRationalSubsetOf(s1));560 EXPECT_FALSE(simUniv.isRationalSubsetOf(s2));561 EXPECT_FALSE(simUniv.isRationalSubsetOf(empty));562 563 EXPECT_TRUE(sim1.isRationalSubsetOf(univ));564 EXPECT_TRUE(sim1.isRationalSubsetOf(s1));565 EXPECT_FALSE(sim1.isRationalSubsetOf(s2));566 EXPECT_FALSE(sim1.isRationalSubsetOf(empty));567 568 EXPECT_TRUE(sim2.isRationalSubsetOf(univ));569 EXPECT_TRUE(sim2.isRationalSubsetOf(s1));570 EXPECT_TRUE(sim2.isRationalSubsetOf(s2));571 EXPECT_FALSE(sim2.isRationalSubsetOf(empty));572}573 574TEST(SimplexTest, addDivisionVariable) {575 Simplex simplex(/*nVar=*/1);576 simplex.addDivisionVariable(getDynamicAPIntVec({1, 0}), DynamicAPInt(2));577 addInequality(simplex, {1, 0, -3}); // x >= 3.578 addInequality(simplex, {-1, 0, 9}); // x <= 9.579 std::optional<SmallVector<DynamicAPInt, 8>> sample =580 simplex.findIntegerSample();581 ASSERT_TRUE(sample.has_value());582 EXPECT_EQ((*sample)[0] / 2, (*sample)[1]);583}584 585TEST(SimplexTest, LexIneqType) {586 LexSimplex simplex(/*nVar=*/1);587 addInequality(simplex, {2, -1}); // x >= 1/2.588 589 // Redundant inequality x >= 2/3.590 EXPECT_TRUE(isRedundantInequality(simplex, {3, -2}));591 EXPECT_FALSE(isSeparateInequality(simplex, {3, -2}));592 593 // Separate inequality x <= 2/3.594 EXPECT_FALSE(isRedundantInequality(simplex, {-3, 2}));595 EXPECT_TRUE(isSeparateInequality(simplex, {-3, 2}));596 597 // Cut inequality x <= 1.598 EXPECT_FALSE(isRedundantInequality(simplex, {-1, 1}));599 EXPECT_FALSE(isSeparateInequality(simplex, {-1, 1}));600}601