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