mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp

   1 //===- IntegerPolyhedron.cpp - Tests for IntegerPolyhedron class ----------===//
   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 #include "mlir/Analysis/Presburger/IntegerRelation.h"
  12 #include "mlir/Analysis/Presburger/PWMAFunction.h"
  13 #include "mlir/Analysis/Presburger/Simplex.h"
  14
  15 #include <gmock/gmock.h>
  16 #include <gtest/gtest.h>
  17
  18 #include <numeric>
  19 #include <optional>
  20
  21 using namespace mlir;
  22 using namespace presburger;
  23
  24 using testing::ElementsAre;
  25
  26 enum class TestFunction { Sample, Empty };
  27
  28 /// Construct a IntegerPolyhedron from a set of inequality and
  29 /// equality constraints.
  30 static IntegerPolyhedron
  31 makeSetFromConstraints(unsigned ids, ArrayRef<SmallVector<int64_t, 4>> ineqs,
  32                        ArrayRef<SmallVector<int64_t, 4>> eqs,
  33                        unsigned syms = 0) {
  34   IntegerPolyhedron set(
  35       ineqs.size(), eqs.size(), ids + 1,
  36       PresburgerSpace::getSetSpace(ids - syms, syms, /*numLocals=*/0));
  37   for (const auto &eq : eqs)
  38     set.addEquality(eq);
  39   for (const auto &ineq : ineqs)
  40     set.addInequality(ineq);
  41   return set;
  42 }
  43
  44 static void dump(ArrayRef<DynamicAPInt> vec) {
  45   for (const DynamicAPInt &x : vec)
  46     llvm::errs() << x << ' ';
  47   llvm::errs() << '\n';
  48 }
  49
  50 /// If fn is TestFunction::Sample (default):
  51 ///
  52 ///   If hasSample is true, check that findIntegerSample returns a valid sample
  53 ///   for the IntegerPolyhedron poly. Also check that getIntegerLexmin finds a
  54 ///   non-empty lexmin.
  55 ///
  56 ///   If hasSample is false, check that findIntegerSample returns std::nullopt
  57 ///   and findIntegerLexMin returns Empty.
  58 ///
  59 /// If fn is TestFunction::Empty, check that isIntegerEmpty returns the
  60 /// opposite of hasSample.
  61 static void checkSample(bool hasSample, const IntegerPolyhedron &poly,
  62                         TestFunction fn = TestFunction::Sample) {
  63   std::optional<SmallVector<DynamicAPInt, 8>> maybeSample;
  64   MaybeOptimum<SmallVector<DynamicAPInt, 8>> maybeLexMin;
  65   switch (fn) {
  66   case TestFunction::Sample:
  67     maybeSample = poly.findIntegerSample();
  68     maybeLexMin = poly.findIntegerLexMin();
  69
  70     if (!hasSample) {
  71       EXPECT_FALSE(maybeSample.has_value());
  72       if (maybeSample.has_value()) {
  73         llvm::errs() << "findIntegerSample gave sample: ";
  74         dump(*maybeSample);
  75       }
  76
  77       EXPECT_TRUE(maybeLexMin.isEmpty());
  78       if (maybeLexMin.isBounded()) {
  79         llvm::errs() << "findIntegerLexMin gave sample: ";
  80         dump(*maybeLexMin);
  81       }
  82     } else {
  83       ASSERT_TRUE(maybeSample.has_value());
  84       EXPECT_TRUE(poly.containsPoint(*maybeSample));
  85
  86       ASSERT_FALSE(maybeLexMin.isEmpty());
  87       if (maybeLexMin.isUnbounded()) {
  88         EXPECT_TRUE(Simplex(poly).isUnbounded());
  89       }
  90       if (maybeLexMin.isBounded()) {
  91         EXPECT_TRUE(poly.containsPointNoLocal(*maybeLexMin));
  92       }
  93     }
  94     break;
  95   case TestFunction::Empty:
  96     EXPECT_EQ(!hasSample, poly.isIntegerEmpty());
  97     break;
  98   }
  99 }
 100
 101 /// Check sampling for all the permutations of the dimensions for the given
 102 /// constraint set. Since the GBR algorithm progresses dimension-wise, different
 103 /// orderings may cause the algorithm to proceed differently. At least some of
 104 ///.these permutations should make it past the heuristics and test the
 105 /// implementation of the GBR algorithm itself.
 106 /// Use TestFunction fn to test.
 107 static void checkPermutationsSample(bool hasSample, unsigned nDim,
 108                                     ArrayRef<SmallVector<int64_t, 4>> ineqs,
 109                                     ArrayRef<SmallVector<int64_t, 4>> eqs,
 110                                     TestFunction fn = TestFunction::Sample) {
 111   SmallVector<unsigned, 4> perm(nDim);
 112   std::iota(perm.begin(), perm.end(), 0);
 113   auto permute = [&perm](ArrayRef<int64_t> coeffs) {
 114     SmallVector<int64_t, 4> permuted;
 115     for (unsigned id : perm)
 116       permuted.push_back(coeffs[id]);
 117     permuted.push_back(coeffs.back());
 118     return permuted;
 119   };
 120   do {
 121     SmallVector<SmallVector<int64_t, 4>, 4> permutedIneqs, permutedEqs;
 122     for (const auto &ineq : ineqs)
 123       permutedIneqs.push_back(permute(ineq));
 124     for (const auto &eq : eqs)
 125       permutedEqs.push_back(permute(eq));
 126
 127     checkSample(hasSample,
 128                 makeSetFromConstraints(nDim, permutedIneqs, permutedEqs), fn);
 129   } while (std::next_permutation(perm.begin(), perm.end()));
 130 }
 131
 132 TEST(IntegerPolyhedronTest, removeInequality) {
 133   IntegerPolyhedron set =
 134       makeSetFromConstraints(1, {{0, 0}, {1, 1}, {2, 2}, {3, 3}, {4, 4}}, {});
 135
 136   set.removeInequalityRange(0, 0);
 137   EXPECT_EQ(set.getNumInequalities(), 5u);
 138
 139   set.removeInequalityRange(1, 3);
 140   EXPECT_EQ(set.getNumInequalities(), 3u);
 141   EXPECT_THAT(set.getInequality(0), ElementsAre(0, 0));
 142   EXPECT_THAT(set.getInequality(1), ElementsAre(3, 3));
 143   EXPECT_THAT(set.getInequality(2), ElementsAre(4, 4));
 144
 145   set.removeInequality(1);
 146   EXPECT_EQ(set.getNumInequalities(), 2u);
 147   EXPECT_THAT(set.getInequality(0), ElementsAre(0, 0));
 148   EXPECT_THAT(set.getInequality(1), ElementsAre(4, 4));
 149 }
 150
 151 TEST(IntegerPolyhedronTest, removeEquality) {
 152   IntegerPolyhedron set =
 153       makeSetFromConstraints(1, {}, {{0, 0}, {1, 1}, {2, 2}, {3, 3}, {4, 4}});
 154
 155   set.removeEqualityRange(0, 0);
 156   EXPECT_EQ(set.getNumEqualities(), 5u);
 157
 158   set.removeEqualityRange(1, 3);
 159   EXPECT_EQ(set.getNumEqualities(), 3u);
 160   EXPECT_THAT(set.getEquality(0), ElementsAre(0, 0));
 161   EXPECT_THAT(set.getEquality(1), ElementsAre(3, 3));
 162   EXPECT_THAT(set.getEquality(2), ElementsAre(4, 4));
 163
 164   set.removeEquality(1);
 165   EXPECT_EQ(set.getNumEqualities(), 2u);
 166   EXPECT_THAT(set.getEquality(0), ElementsAre(0, 0));
 167   EXPECT_THAT(set.getEquality(1), ElementsAre(4, 4));
 168 }
 169
 170 TEST(IntegerPolyhedronTest, clearConstraints) {
 171   IntegerPolyhedron set = makeSetFromConstraints(1, {}, {});
 172
 173   set.addInequality({1, 0});
 174   EXPECT_EQ(set.atIneq(0, 0), 1);
 175   EXPECT_EQ(set.atIneq(0, 1), 0);
 176
 177   set.clearConstraints();
 178
 179   set.addInequality({1, 0});
 180   EXPECT_EQ(set.atIneq(0, 0), 1);
 181   EXPECT_EQ(set.atIneq(0, 1), 0);
 182 }
 183
 184 TEST(IntegerPolyhedronTest, removeIdRange) {
 185   IntegerPolyhedron set(PresburgerSpace::getSetSpace(3, 2, 1));
 186
 187   set.addInequality({10, 11, 12, 20, 21, 30, 40});
 188   set.removeVar(VarKind::Symbol, 1);
 189   EXPECT_THAT(set.getInequality(0),
 190               testing::ElementsAre(10, 11, 12, 20, 30, 40));
 191
 192   set.removeVarRange(VarKind::SetDim, 0, 2);
 193   EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 30, 40));
 194
 195   set.removeVarRange(VarKind::Local, 1, 1);
 196   EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 30, 40));
 197
 198   set.removeVarRange(VarKind::Local, 0, 1);
 199   EXPECT_THAT(set.getInequality(0), testing::ElementsAre(12, 20, 40));
 200 }
 201
 202 TEST(IntegerPolyhedronTest, FindSampleTest) {
 203   // Bounded sets with only inequalities.
 204   // 0 <= 7x <= 5
 205   checkSample(true,
 206               parseIntegerPolyhedron("(x) : (7 * x >= 0, -7 * x + 5 >= 0)"));
 207
 208   // 1 <= 5x and 5x <= 4 (no solution).
 209   checkSample(
 210       false, parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)"));
 211
 212   // 1 <= 5x and 5x <= 9 (solution: x = 1).
 213   checkSample(
 214       true, parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)"));
 215
 216   // Bounded sets with equalities.
 217   // x >= 8 and 40 >= y and x = y.
 218   checkSample(true, parseIntegerPolyhedron(
 219                         "(x,y) : (x - 8 >= 0, -y + 40 >= 0, x - y == 0)"));
 220
 221   // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z.
 222   // solution: x = y = z = 10.
 223   checkSample(true,
 224               parseIntegerPolyhedron("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, "
 225                                      "z - 10 >= 0, x + 2 * y - 3 * z == 0)"));
 226
 227   // x <= 10 and y <= 10 and 11 <= z and x + 2y = 3z.
 228   // This implies x + 2y >= 33 and x + 2y <= 30, which has no solution.
 229   checkSample(false,
 230               parseIntegerPolyhedron("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, "
 231                                      "z - 11 >= 0, x + 2 * y - 3 * z == 0)"));
 232
 233   // 0 <= r and r <= 3 and 4q + r = 7.
 234   // Solution: q = 1, r = 3.
 235   checkSample(true, parseIntegerPolyhedron(
 236                         "(q,r) : (r >= 0, -r + 3 >= 0, 4 * q + r - 7 == 0)"));
 237
 238   // 4q + r = 7 and r = 0.
 239   // Solution: q = 1, r = 3.
 240   checkSample(false,
 241               parseIntegerPolyhedron("(q,r) : (4 * q + r - 7 == 0, r == 0)"));
 242
 243   // The next two sets are large sets that should take a long time to sample
 244   // with a naive branch and bound algorithm but can be sampled efficiently with
 245   // the GBR algorithm.
 246   //
 247   // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (10000, 10000).
 248   checkSample(
 249       true, parseIntegerPolyhedron("(x,y) : (y >= 0, "
 250                                    "300000 * x - 299999 * y - 100000 >= 0, "
 251                                    "-300000 * x + 299998 * y + 200000 >= 0)"));
 252
 253   // This is a tetrahedron with vertices at
 254   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
 255   // The first three points form a triangular base on the xz plane with the
 256   // apex at the fourth point, which is the only integer point.
 257   checkPermutationsSample(
 258       true, 3,
 259       {
 260           {0, 1, 0, 0},  // y >= 0
 261           {0, -1, 1, 0}, // z >= y
 262           {300000, -299998, -1,
 263            -100000},                    // -300000x + 299998y + 100000 + z <= 0.
 264           {-150000, 149999, 0, 100000}, // -150000x + 149999y + 100000 >= 0.
 265       },
 266       {});
 267
 268   // Same thing with some spurious extra dimensions equated to constants.
 269   checkSample(true,
 270               parseIntegerPolyhedron(
 271                   "(a,b,c,d,e) : (b + d - e >= 0, -b + c - d + e >= 0, "
 272                   "300000 * a - 299998 * b - c - 9 * d + 21 * e - 112000 >= 0, "
 273                   "-150000 * a + 149999 * b - 15 * d + 47 * e + 68000 >= 0, "
 274                   "d - e == 0, d + e - 2000 == 0)"));
 275
 276   // This is a tetrahedron with vertices at
 277   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100).
 278   checkPermutationsSample(false, 3,
 279                           {
 280                               {0, 1, 0, 0},
 281                               {0, -300, 299, 0},
 282                               {300 * 299, -89400, -299, -100 * 299},
 283                               {-897, 894, 0, 598},
 284                           },
 285                           {});
 286
 287   // Two tests involving equalities that are integer empty but not rational
 288   // empty.
 289
 290   // This is a line segment from (0, 1/3) to (100, 100 + 1/3).
 291   checkSample(false,
 292               parseIntegerPolyhedron(
 293                   "(x,y) : (x >= 0, -x + 100 >= 0, 3 * x - 3 * y + 1 == 0)"));
 294
 295   // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3.
 296   checkSample(false, parseIntegerPolyhedron(
 297                          "(x,y) : (x >= 0, -x + 100 >= 0, "
 298                          "3 * x - 3 * y + 2 >= 0, -3 * x + 3 * y - 1 >= 0)"));
 299
 300   checkSample(true,
 301               parseIntegerPolyhedron("(x,y) : (2 * x >= 0, -2 * x + 99 >= 0, "
 302                                      "2 * y >= 0, -2 * y + 99 >= 0)"));
 303
 304   // 2D cone with apex at (10000, 10000) and
 305   // edges passing through (1/3, 0) and (2/3, 0).
 306   checkSample(true, parseIntegerPolyhedron(
 307                         "(x,y) : (300000 * x - 299999 * y - 100000 >= 0, "
 308                         "-300000 * x + 299998 * y + 200000 >= 0)"));
 309
 310   // Cartesian product of a tetrahedron and a 2D cone.
 311   // The tetrahedron has vertices at
 312   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
 313   // The first three points form a triangular base on the xz plane with the
 314   // apex at the fourth point, which is the only integer point.
 315   // The cone has apex at (10000, 10000) and
 316   // edges passing through (1/3, 0) and (2/3, 0).
 317   checkPermutationsSample(
 318       true /* not empty */, 5,
 319       {
 320           // Tetrahedron contraints:
 321           {0, 1, 0, 0, 0, 0},  // y >= 0
 322           {0, -1, 1, 0, 0, 0}, // z >= y
 323                                // -300000x + 299998y + 100000 + z <= 0.
 324           {300000, -299998, -1, 0, 0, -100000},
 325           // -150000x + 149999y + 100000 >= 0.
 326           {-150000, 149999, 0, 0, 0, 100000},
 327
 328           // Triangle constraints:
 329           // 300000p - 299999q >= 100000
 330           {0, 0, 0, 300000, -299999, -100000},
 331           // -300000p + 299998q + 200000 >= 0
 332           {0, 0, 0, -300000, 299998, 200000},
 333       },
 334       {});
 335
 336   // Cartesian product of same tetrahedron as above and {(p, q) : 1/3 <= p <=
 337   // 2/3}. Since the second set is empty, the whole set is too.
 338   checkPermutationsSample(
 339       false /* empty */, 5,
 340       {
 341           // Tetrahedron contraints:
 342           {0, 1, 0, 0, 0, 0},  // y >= 0
 343           {0, -1, 1, 0, 0, 0}, // z >= y
 344                                // -300000x + 299998y + 100000 + z <= 0.
 345           {300000, -299998, -1, 0, 0, -100000},
 346           // -150000x + 149999y + 100000 >= 0.
 347           {-150000, 149999, 0, 0, 0, 100000},
 348
 349           // Second set constraints:
 350           // 3p >= 1
 351           {0, 0, 0, 3, 0, -1},
 352           // 3p <= 2
 353           {0, 0, 0, -3, 0, 2},
 354       },
 355       {});
 356
 357   // Cartesian product of same tetrahedron as above and
 358   // {(p, q, r) : 1 <= p <= 2 and p = 3q + 3r}.
 359   // Since the second set is empty, the whole set is too.
 360   checkPermutationsSample(
 361       false /* empty */, 5,
 362       {
 363           // Tetrahedron contraints:
 364           {0, 1, 0, 0, 0, 0, 0},  // y >= 0
 365           {0, -1, 1, 0, 0, 0, 0}, // z >= y
 366                                   // -300000x + 299998y + 100000 + z <= 0.
 367           {300000, -299998, -1, 0, 0, 0, -100000},
 368           // -150000x + 149999y + 100000 >= 0.
 369           {-150000, 149999, 0, 0, 0, 0, 100000},
 370
 371           // Second set constraints:
 372           // p >= 1
 373           {0, 0, 0, 1, 0, 0, -1},
 374           // p <= 2
 375           {0, 0, 0, -1, 0, 0, 2},
 376       },
 377       {
 378           {0, 0, 0, 1, -3, -3, 0}, // p = 3q + 3r
 379       });
 380
 381   // Cartesian product of a tetrahedron and a 2D cone.
 382   // The tetrahedron is empty and has vertices at
 383   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), and (100, 100 - 1/3, 100).
 384   // The cone has apex at (10000, 10000) and
 385   // edges passing through (1/3, 0) and (2/3, 0).
 386   // Since the tetrahedron is empty, the Cartesian product is too.
 387   checkPermutationsSample(false /* empty */, 5,
 388                           {
 389                               // Tetrahedron contraints:
 390                               {0, 1, 0, 0, 0, 0},
 391                               {0, -300, 299, 0, 0, 0},
 392                               {300 * 299, -89400, -299, 0, 0, -100 * 299},
 393                               {-897, 894, 0, 0, 0, 598},
 394
 395                               // Triangle constraints:
 396                               // 300000p - 299999q >= 100000
 397                               {0, 0, 0, 300000, -299999, -100000},
 398                               // -300000p + 299998q + 200000 >= 0
 399                               {0, 0, 0, -300000, 299998, 200000},
 400                           },
 401                           {});
 402
 403   // Cartesian product of same tetrahedron as above and
 404   // {(p, q) : 1/3 <= p <= 2/3}.
 405   checkPermutationsSample(false /* empty */, 5,
 406                           {
 407                               // Tetrahedron contraints:
 408                               {0, 1, 0, 0, 0, 0},
 409                               {0, -300, 299, 0, 0, 0},
 410                               {300 * 299, -89400, -299, 0, 0, -100 * 299},
 411                               {-897, 894, 0, 0, 0, 598},
 412
 413                               // Second set constraints:
 414                               // 3p >= 1
 415                               {0, 0, 0, 3, 0, -1},
 416                               // 3p <= 2
 417                               {0, 0, 0, -3, 0, 2},
 418                           },
 419                           {});
 420
 421   checkSample(true, parseIntegerPolyhedron(
 422                         "(x, y, z) : (2 * x - 1 >= 0, x - y - 1 == 0, "
 423                         "y - z == 0)"));
 424
 425   // Test with a local id.
 426   checkSample(true, parseIntegerPolyhedron("(x) : (x == 5*(x floordiv 2))"));
 427
 428   // Regression tests for the computation of dual coefficients.
 429   checkSample(false, parseIntegerPolyhedron("(x, y, z) : ("
 430                                             "6*x - 4*y + 9*z + 2 >= 0,"
 431                                             "x + 5*y + z + 5 >= 0,"
 432                                             "-4*x + y + 2*z - 1 >= 0,"
 433                                             "-3*x - 2*y - 7*z - 1 >= 0,"
 434                                             "-7*x - 5*y - 9*z - 1 >= 0)"));
 435   checkSample(true, parseIntegerPolyhedron("(x, y, z) : ("
 436                                            "3*x + 3*y + 3 >= 0,"
 437                                            "-4*x - 8*y - z + 4 >= 0,"
 438                                            "-7*x - 4*y + z + 1 >= 0,"
 439                                            "2*x - 7*y - 8*z - 7 >= 0,"
 440                                            "9*x + 8*y - 9*z - 7 >= 0)"));
 441 }
 442
 443 TEST(IntegerPolyhedronTest, IsIntegerEmptyTest) {
 444   // 1 <= 5x and 5x <= 4 (no solution).
 445   EXPECT_TRUE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)")
 446                   .isIntegerEmpty());
 447   // 1 <= 5x and 5x <= 9 (solution: x = 1).
 448   EXPECT_FALSE(parseIntegerPolyhedron("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)")
 449                    .isIntegerEmpty());
 450
 451   // Unbounded sets.
 452   EXPECT_TRUE(
 453       parseIntegerPolyhedron("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, "
 454                              "2 * z - 1 >= 0, 2 * x - 1 == 0)")
 455           .isIntegerEmpty());
 456
 457   EXPECT_FALSE(parseIntegerPolyhedron(
 458                    "(x,y,z) : (2 * x - 1 >= 0, -3 * x + 3 >= 0, "
 459                    "5 * z - 6 >= 0, -7 * z + 17 >= 0, 3 * y - 2 >= 0)")
 460                    .isIntegerEmpty());
 461
 462   EXPECT_FALSE(parseIntegerPolyhedron(
 463                    "(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)")
 464                    .isIntegerEmpty());
 465
 466   // IntegerPolyhedron::isEmpty() does not detect the following sets to be
 467   // empty.
 468
 469   // 3x + 7y = 1 and 0 <= x, y <= 10.
 470   // Since x and y are non-negative, 3x + 7y can never be 1.
 471   EXPECT_TRUE(parseIntegerPolyhedron(
 472                   "(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, "
 473                   "3 * x + 7 * y - 1 == 0)")
 474                   .isIntegerEmpty());
 475
 476   // 2x = 3y and y = x - 1 and x + y = 6z + 2 and 0 <= x, y <= 100.
 477   // Substituting y = x - 1 in 3y = 2x, we obtain x = 3 and hence y = 2.
 478   // Since x + y = 5 cannot be equal to 6z + 2 for any z, the set is empty.
 479   EXPECT_TRUE(parseIntegerPolyhedron(
 480                   "(x,y,z) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, "
 481                   "2 * x - 3 * y == 0, x - y - 1 == 0, x + y - 6 * z - 2 == 0)")
 482                   .isIntegerEmpty());
 483
 484   // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100.
 485   // 2x = 3y implies x is a multiple of 3 and y is even.
 486   // Now y = x - 1 + 6z implies y = 2 mod 3. In fact, since y is even, we have
 487   // y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying
 488   // x + y = 5 mod 6, which contradicts x + y = 6q + 2, so the set is empty.
 489   EXPECT_TRUE(
 490       parseIntegerPolyhedron(
 491           "(x,y,z,q) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, "
 492           "2 * x - 3 * y == 0, x - y + 6 * z - 1 == 0, x + y - 6 * q - 2 == 0)")
 493           .isIntegerEmpty());
 494
 495   // Set with symbols.
 496   EXPECT_FALSE(parseIntegerPolyhedron("(x)[s] : (x + s >= 0, x - s == 0)")
 497                    .isIntegerEmpty());
 498 }
 499
 500 TEST(IntegerPolyhedronTest, removeRedundantConstraintsTest) {
 501   IntegerPolyhedron poly =
 502       parseIntegerPolyhedron("(x) : (x - 2 >= 0, -x + 2 >= 0, x - 2 == 0)");
 503   poly.removeRedundantConstraints();
 504
 505   // Both inequalities are redundant given the equality. Both have been removed.
 506   EXPECT_EQ(poly.getNumInequalities(), 0u);
 507   EXPECT_EQ(poly.getNumEqualities(), 1u);
 508
 509   IntegerPolyhedron poly2 =
 510       parseIntegerPolyhedron("(x,y) : (x - 3 >= 0, y - 2 >= 0, x - y == 0)");
 511   poly2.removeRedundantConstraints();
 512
 513   // The second inequality is redundant and should have been removed. The
 514   // remaining inequality should be the first one.
 515   EXPECT_EQ(poly2.getNumInequalities(), 1u);
 516   EXPECT_THAT(poly2.getInequality(0), ElementsAre(1, 0, -3));
 517   EXPECT_EQ(poly2.getNumEqualities(), 1u);
 518
 519   IntegerPolyhedron poly3 =
 520       parseIntegerPolyhedron("(x,y,z) : (x - y == 0, x - z == 0, y - z == 0)");
 521   poly3.removeRedundantConstraints();
 522
 523   // One of the three equalities can be removed.
 524   EXPECT_EQ(poly3.getNumInequalities(), 0u);
 525   EXPECT_EQ(poly3.getNumEqualities(), 2u);
 526
 527   IntegerPolyhedron poly4 = parseIntegerPolyhedron(
 528       "(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) : ("
 529       "b - 1 >= 0,"
 530       "-b + 500 >= 0,"
 531       "-16 * d + f >= 0,"
 532       "f - 1 >= 0,"
 533       "-f + 998 >= 0,"
 534       "16 * d - f + 15 >= 0,"
 535       "-16 * e + g >= 0,"
 536       "g - 1 >= 0,"
 537       "-g + 998 >= 0,"
 538       "16 * e - g + 15 >= 0,"
 539       "h >= 0,"
 540       "-h + 1 >= 0,"
 541       "j - 1 >= 0,"
 542       "-j + 500 >= 0,"
 543       "-f + 16 * l + 15 >= 0,"
 544       "f - 16 * l >= 0,"
 545       "-16 * m + o >= 0,"
 546       "o - 1 >= 0,"
 547       "-o + 998 >= 0,"
 548       "16 * m - o + 15 >= 0,"
 549       "p >= 0,"
 550       "-p + 1 >= 0,"
 551       "-g - h + 8 * q + 8 >= 0,"
 552       "-o - p + 8 * q + 8 >= 0,"
 553       "o + p - 8 * q - 1 >= 0,"
 554       "g + h - 8 * q - 1 >= 0,"
 555       "-f + n >= 0,"
 556       "f - n >= 0,"
 557       "k - 10 >= 0,"
 558       "-k + 10 >= 0,"
 559       "i - 13 >= 0,"
 560       "-i + 13 >= 0,"
 561       "c - 10 >= 0,"
 562       "-c + 10 >= 0,"
 563       "a - 13 >= 0,"
 564       "-a + 13 >= 0"
 565       ")");
 566
 567   // The above is a large set of constraints without any redundant constraints,
 568   // as verified by the Fourier-Motzkin based removeRedundantInequalities.
 569   unsigned nIneq = poly4.getNumInequalities();
 570   unsigned nEq = poly4.getNumEqualities();
 571   poly4.removeRedundantInequalities();
 572   ASSERT_EQ(poly4.getNumInequalities(), nIneq);
 573   ASSERT_EQ(poly4.getNumEqualities(), nEq);
 574   // Now we test that removeRedundantConstraints does not find any constraints
 575   // to be redundant either.
 576   poly4.removeRedundantConstraints();
 577   EXPECT_EQ(poly4.getNumInequalities(), nIneq);
 578   EXPECT_EQ(poly4.getNumEqualities(), nEq);
 579
 580   IntegerPolyhedron poly5 = parseIntegerPolyhedron(
 581       "(x,y) : (128 * x + 127 >= 0, -x + 7 >= 0, -128 * x + y >= 0, y >= 0)");
 582   // 128x + 127 >= 0  implies that 128x >= 0, since x has to be an integer.
 583   // (This should be caught by GCDTightenInqualities().)
 584   // So -128x + y >= 0 and 128x + 127 >= 0 imply y >= 0 since we have
 585   // y >= 128x >= 0.
 586   poly5.removeRedundantConstraints();
 587   EXPECT_EQ(poly5.getNumInequalities(), 3u);
 588   SmallVector<DynamicAPInt, 8> redundantConstraint =
 589       getDynamicAPIntVec({0, 1, 0});
 590   for (unsigned i = 0; i < 3; ++i) {
 591     // Ensure that the removed constraint was the redundant constraint [3].
 592     EXPECT_NE(poly5.getInequality(i),
 593               ArrayRef<DynamicAPInt>(redundantConstraint));
 594   }
 595 }
 596
 597 TEST(IntegerPolyhedronTest, addConstantUpperBound) {
 598   IntegerPolyhedron poly(PresburgerSpace::getSetSpace(2));
 599   poly.addBound(BoundType::UB, 0, 1);
 600   EXPECT_EQ(poly.atIneq(0, 0), -1);
 601   EXPECT_EQ(poly.atIneq(0, 1), 0);
 602   EXPECT_EQ(poly.atIneq(0, 2), 1);
 603
 604   poly.addBound(BoundType::UB, {1, 2, 3}, 1);
 605   EXPECT_EQ(poly.atIneq(1, 0), -1);
 606   EXPECT_EQ(poly.atIneq(1, 1), -2);
 607   EXPECT_EQ(poly.atIneq(1, 2), -2);
 608 }
 609
 610 TEST(IntegerPolyhedronTest, addConstantLowerBound) {
 611   IntegerPolyhedron poly(PresburgerSpace::getSetSpace(2));
 612   poly.addBound(BoundType::LB, 0, 1);
 613   EXPECT_EQ(poly.atIneq(0, 0), 1);
 614   EXPECT_EQ(poly.atIneq(0, 1), 0);
 615   EXPECT_EQ(poly.atIneq(0, 2), -1);
 616
 617   poly.addBound(BoundType::LB, {1, 2, 3}, 1);
 618   EXPECT_EQ(poly.atIneq(1, 0), 1);
 619   EXPECT_EQ(poly.atIneq(1, 1), 2);
 620   EXPECT_EQ(poly.atIneq(1, 2), 2);
 621 }
 622
 623 /// Check if the expected division representation of local variables matches the
 624 /// computed representation. The expected division representation is given as
 625 /// a vector of expressions set in `expectedDividends` and the corressponding
 626 /// denominator in `expectedDenominators`. The `denominators` and `dividends`
 627 /// obtained through `getLocalRepr` function is verified against the
 628 /// `expectedDenominators` and `expectedDividends` respectively.
 629 static void checkDivisionRepresentation(
 630     IntegerPolyhedron &poly,
 631     const std::vector<SmallVector<int64_t, 8>> &expectedDividends,
 632     ArrayRef<int64_t> expectedDenominators) {
 633   DivisionRepr divs = poly.getLocalReprs();
 634
 635   // Check that the `denominators` and `expectedDenominators` match.
 636   EXPECT_EQ(ArrayRef<DynamicAPInt>(getDynamicAPIntVec(expectedDenominators)),
 637             divs.getDenoms());
 638
 639   // Check that the `dividends` and `expectedDividends` match. If the
 640   // denominator for a division is zero, we ignore its dividend.
 641   EXPECT_TRUE(divs.getNumDivs() == expectedDividends.size());
 642   for (unsigned i = 0, e = divs.getNumDivs(); i < e; ++i) {
 643     if (divs.hasRepr(i)) {
 644       for (unsigned j = 0, f = divs.getNumVars() + 1; j < f; ++j) {
 645         EXPECT_TRUE(expectedDividends[i][j] == divs.getDividend(i)[j]);
 646       }
 647     }
 648   }
 649 }
 650
 651 TEST(IntegerPolyhedronTest, computeLocalReprSimple) {
 652   IntegerPolyhedron poly(PresburgerSpace::getSetSpace(1));
 653
 654   poly.addLocalFloorDiv({1, 4}, 10);
 655   poly.addLocalFloorDiv({1, 0, 100}, 10);
 656
 657   std::vector<SmallVector<int64_t, 8>> divisions = {{1, 0, 0, 4},
 658                                                     {1, 0, 0, 100}};
 659   SmallVector<int64_t, 8> denoms = {10, 10};
 660
 661   // Check if floordivs can be computed when no other inequalities exist
 662   // and floor divs do not depend on each other.
 663   checkDivisionRepresentation(poly, divisions, denoms);
 664 }
 665
 666 TEST(IntegerPolyhedronTest, computeLocalReprConstantFloorDiv) {
 667   IntegerPolyhedron poly(PresburgerSpace::getSetSpace(4));
 668
 669   poly.addInequality({1, 0, 3, 1, 2});
 670   poly.addInequality({1, 2, -8, 1, 10});
 671   poly.addEquality({1, 2, -4, 1, 10});
 672
 673   poly.addLocalFloorDiv({0, 0, 0, 0, 100}, 30);
 674   poly.addLocalFloorDiv({0, 0, 0, 0, 0, 206}, 101);
 675
 676   std::vector<SmallVector<int64_t, 8>> divisions = {{0, 0, 0, 0, 0, 0, 3},
 677                                                     {0, 0, 0, 0, 0, 0, 2}};
 678   SmallVector<int64_t, 8> denoms = {1, 1};
 679
 680   // Check if floordivs with constant numerator can be computed.
 681   checkDivisionRepresentation(poly, divisions, denoms);
 682 }
 683
 684 TEST(IntegerPolyhedronTest, computeLocalReprRecursive) {
 685   IntegerPolyhedron poly(PresburgerSpace::getSetSpace(4));
 686   poly.addInequality({1, 0, 3, 1, 2});
 687   poly.addInequality({1, 2, -8, 1, 10});
 688   poly.addEquality({1, 2, -4, 1, 10});
 689
 690   poly.addLocalFloorDiv({0, -2, 7, 2, 10}, 3);
 691   poly.addLocalFloorDiv({3, 0, 9, 2, 2, 10}, 5);
 692   poly.addLocalFloorDiv({0, 1, -123, 2, 0, -4, 10}, 3);
 693
 694   poly.addInequality({1, 2, -2, 1, -5, 0, 6, 100});
 695   poly.addInequality({1, 2, -8, 1, 3, 7, 0, -9});
 696
 697   std::vector<SmallVector<int64_t, 8>> divisions = {
 698       {0, -2, 7, 2, 0, 0, 0, 10},
 699       {3, 0, 9, 2, 2, 0, 0, 10},
 700       {0, 1, -123, 2, 0, -4, 0, 10}};
 701
 702   SmallVector<int64_t, 8> denoms = {3, 5, 3};
 703
 704   // Check if floordivs which may depend on other floordivs can be computed.
 705   checkDivisionRepresentation(poly, divisions, denoms);
 706 }
 707
 708 TEST(IntegerPolyhedronTest, computeLocalReprTightUpperBound) {
 709   {
 710     IntegerPolyhedron poly = parseIntegerPolyhedron("(i) : (i mod 3 - 1 >= 0)");
 711
 712     // The set formed by the poly is:
 713     //        3q - i + 2 >= 0             <-- Division lower bound
 714     //       -3q + i - 1 >= 0
 715     //       -3q + i     >= 0             <-- Division upper bound
 716     // We remove redundant constraints to get the set:
 717     //        3q - i + 2 >= 0             <-- Division lower bound
 718     //       -3q + i - 1 >= 0             <-- Tighter division upper bound
 719     // thus, making the upper bound tighter.
 720     poly.removeRedundantConstraints();
 721
 722     std::vector<SmallVector<int64_t, 8>> divisions = {{1, 0, 0}};
 723     SmallVector<int64_t, 8> denoms = {3};
 724
 725     // Check if the divisions can be computed even with a tighter upper bound.
 726     checkDivisionRepresentation(poly, divisions, denoms);
 727   }
 728
 729   {
 730     IntegerPolyhedron poly = parseIntegerPolyhedron(
 731         "(i, j, q) : (4*q - i - j + 2 >= 0, -4*q + i + j >= 0)");
 732     // Convert `q` to a local variable.
 733     poly.convertToLocal(VarKind::SetDim, 2, 3);
 734
 735     std::vector<SmallVector<int64_t, 8>> divisions = {{1, 1, 0, 1}};
 736     SmallVector<int64_t, 8> denoms = {4};
 737
 738     // Check if the divisions can be computed even with a tighter upper bound.
 739     checkDivisionRepresentation(poly, divisions, denoms);
 740   }
 741 }
 742
 743 TEST(IntegerPolyhedronTest, computeLocalReprFromEquality) {
 744   {
 745     IntegerPolyhedron poly =
 746         parseIntegerPolyhedron("(i, j, q) : (-4*q + i + j == 0)");
 747     // Convert `q` to a local variable.
 748     poly.convertToLocal(VarKind::SetDim, 2, 3);
 749
 750     std::vector<SmallVector<int64_t, 8>> divisions = {{1, 1, 0, 0}};
 751     SmallVector<int64_t, 8> denoms = {4};
 752
 753     checkDivisionRepresentation(poly, divisions, denoms);
 754   }
 755   {
 756     IntegerPolyhedron poly =
 757         parseIntegerPolyhedron("(i, j, q) : (4*q - i - j == 0)");
 758     // Convert `q` to a local variable.
 759     poly.convertToLocal(VarKind::SetDim, 2, 3);
 760
 761     std::vector<SmallVector<int64_t, 8>> divisions = {{1, 1, 0, 0}};
 762     SmallVector<int64_t, 8> denoms = {4};
 763
 764     checkDivisionRepresentation(poly, divisions, denoms);
 765   }
 766   {
 767     IntegerPolyhedron poly =
 768         parseIntegerPolyhedron("(i, j, q) : (3*q + i + j - 2 == 0)");
 769     // Convert `q` to a local variable.
 770     poly.convertToLocal(VarKind::SetDim, 2, 3);
 771
 772     std::vector<SmallVector<int64_t, 8>> divisions = {{-1, -1, 0, 2}};
 773     SmallVector<int64_t, 8> denoms = {3};
 774
 775     checkDivisionRepresentation(poly, divisions, denoms);
 776   }
 777 }
 778
 779 TEST(IntegerPolyhedronTest, computeLocalReprFromEqualityAndInequality) {
 780   {
 781     IntegerPolyhedron poly =
 782         parseIntegerPolyhedron("(i, j, q, k) : (-3*k + i + j == 0, 4*q - "
 783                                "i - j + 2 >= 0, -4*q + i + j >= 0)");
 784     // Convert `q` and `k` to local variables.
 785     poly.convertToLocal(VarKind::SetDim, 2, 4);
 786
 787     std::vector<SmallVector<int64_t, 8>> divisions = {{1, 1, 0, 0, 1},
 788                                                       {1, 1, 0, 0, 0}};
 789     SmallVector<int64_t, 8> denoms = {4, 3};
 790
 791     checkDivisionRepresentation(poly, divisions, denoms);
 792   }
 793 }
 794
 795 TEST(IntegerPolyhedronTest, computeLocalReprNoRepr) {
 796   IntegerPolyhedron poly =
 797       parseIntegerPolyhedron("(x, q) : (x - 3 * q >= 0, -x + 3 * q + 3 >= 0)");
 798   // Convert q to a local variable.
 799   poly.convertToLocal(VarKind::SetDim, 1, 2);
 800
 801   std::vector<SmallVector<int64_t, 8>> divisions = {{0, 0, 0}};
 802   SmallVector<int64_t, 8> denoms = {0};
 803
 804   // Check that no division is computed.
 805   checkDivisionRepresentation(poly, divisions, denoms);
 806 }
 807
 808 TEST(IntegerPolyhedronTest, computeLocalReprNegConstNormalize) {
 809   IntegerPolyhedron poly = parseIntegerPolyhedron(
 810       "(x, q) : (-1 - 3*x - 6 * q >= 0, 6 + 3*x + 6*q >= 0)");
 811   // Convert q to a local variable.
 812   poly.convertToLocal(VarKind::SetDim, 1, 2);
 813
 814   // q = floor((-1/3 - x)/2)
 815   //   = floor((1/3) + (-1 - x)/2)
 816   //   = floor((-1 - x)/2).
 817   std::vector<SmallVector<int64_t, 8>> divisions = {{-1, 0, -1}};
 818   SmallVector<int64_t, 8> denoms = {2};
 819   checkDivisionRepresentation(poly, divisions, denoms);
 820 }
 821
 822 TEST(IntegerPolyhedronTest, simplifyLocalsTest) {
 823   // (x) : (exists y: 2x + y = 1 and y = 2).
 824   IntegerPolyhedron poly(PresburgerSpace::getSetSpace(1, 0, 1));
 825   poly.addEquality({2, 1, -1});
 826   poly.addEquality({0, 1, -2});
 827
 828   EXPECT_TRUE(poly.isEmpty());
 829
 830   // (x) : (exists y, z, w: 3x + y = 1 and 2y = z and 3y = w and z = w).
 831   IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1, 0, 3));
 832   poly2.addEquality({3, 1, 0, 0, -1});
 833   poly2.addEquality({0, 2, -1, 0, 0});
 834   poly2.addEquality({0, 3, 0, -1, 0});
 835   poly2.addEquality({0, 0, 1, -1, 0});
 836
 837   EXPECT_TRUE(poly2.isEmpty());
 838
 839   // (x) : (exists y: x >= y + 1 and 2x + y = 0 and y >= -1).
 840   IntegerPolyhedron poly3(PresburgerSpace::getSetSpace(1, 0, 1));
 841   poly3.addInequality({1, -1, -1});
 842   poly3.addInequality({0, 1, 1});
 843   poly3.addEquality({2, 1, 0});
 844
 845   EXPECT_TRUE(poly3.isEmpty());
 846 }
 847
 848 TEST(IntegerPolyhedronTest, mergeDivisionsSimple) {
 849   {
 850     // (x) : (exists z, y  = [x / 2] : x = 3y and x + z + 1 >= 0).
 851     IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1, 0, 1));
 852     poly1.addLocalFloorDiv({1, 0, 0}, 2); // y = [x / 2].
 853     poly1.addEquality({1, 0, -3, 0});     // x = 3y.
 854     poly1.addInequality({1, 1, 0, 1});    // x + z + 1 >= 0.
 855
 856     // (x) : (exists y = [x / 2], z : x = 5y).
 857     IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
 858     poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2].
 859     poly2.addEquality({1, -5, 0});     // x = 5y.
 860     poly2.appendVar(VarKind::Local);   // Add local id z.
 861
 862     poly1.mergeLocalVars(poly2);
 863
 864     // Local space should be same.
 865     EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
 866
 867     // 1 division should be matched + 2 unmatched local ids.
 868     EXPECT_EQ(poly1.getNumLocalVars(), 3u);
 869     EXPECT_EQ(poly2.getNumLocalVars(), 3u);
 870   }
 871
 872   {
 873     // (x) : (exists z = [x / 5], y = [x / 2] : x = 3y).
 874     IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1));
 875     poly1.addLocalFloorDiv({1, 0}, 5);    // z = [x / 5].
 876     poly1.addLocalFloorDiv({1, 0, 0}, 2); // y = [x / 2].
 877     poly1.addEquality({1, 0, -3, 0});     // x = 3y.
 878
 879     // (x) : (exists y = [x / 2], z = [x / 5]: x = 5z).
 880     IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
 881     poly2.addLocalFloorDiv({1, 0}, 2);    // y = [x / 2].
 882     poly2.addLocalFloorDiv({1, 0, 0}, 5); // z = [x / 5].
 883     poly2.addEquality({1, 0, -5, 0});     // x = 5z.
 884
 885     poly1.mergeLocalVars(poly2);
 886
 887     // Local space should be same.
 888     EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
 889
 890     // 2 divisions should be matched.
 891     EXPECT_EQ(poly1.getNumLocalVars(), 2u);
 892     EXPECT_EQ(poly2.getNumLocalVars(), 2u);
 893   }
 894
 895   {
 896     // Division Normalization test.
 897     // (x) : (exists z, y  = [x / 2] : x = 3y and x + z + 1 >= 0).
 898     IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1, 0, 1));
 899     // This division would be normalized.
 900     poly1.addLocalFloorDiv({3, 0, 0}, 6); // y = [3x / 6] -> [x/2].
 901     poly1.addEquality({1, 0, -3, 0});     // x = 3z.
 902     poly1.addInequality({1, 1, 0, 1});    // x + y + 1 >= 0.
 903
 904     // (x) : (exists y = [x / 2], z : x = 5y).
 905     IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
 906     poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2].
 907     poly2.addEquality({1, -5, 0});     // x = 5y.
 908     poly2.appendVar(VarKind::Local);   // Add local id z.
 909
 910     poly1.mergeLocalVars(poly2);
 911
 912     // Local space should be same.
 913     EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
 914
 915     // One division should be matched + 2 unmatched local ids.
 916     EXPECT_EQ(poly1.getNumLocalVars(), 3u);
 917     EXPECT_EQ(poly2.getNumLocalVars(), 3u);
 918   }
 919 }
 920
 921 TEST(IntegerPolyhedronTest, mergeDivisionsNestedDivsions) {
 922   {
 923     // (x) : (exists y = [x / 2], z = [x + y / 3]: y + z >= x).
 924     IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1));
 925     poly1.addLocalFloorDiv({1, 0}, 2);    // y = [x / 2].
 926     poly1.addLocalFloorDiv({1, 1, 0}, 3); // z = [x + y / 3].
 927     poly1.addInequality({-1, 1, 1, 0});   // y + z >= x.
 928
 929     // (x) : (exists y = [x / 2], z = [x + y / 3]: y + z <= x).
 930     IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
 931     poly2.addLocalFloorDiv({1, 0}, 2);    // y = [x / 2].
 932     poly2.addLocalFloorDiv({1, 1, 0}, 3); // z = [x + y / 3].
 933     poly2.addInequality({1, -1, -1, 0});  // y + z <= x.
 934
 935     poly1.mergeLocalVars(poly2);
 936
 937     // Local space should be same.
 938     EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
 939
 940     // 2 divisions should be matched.
 941     EXPECT_EQ(poly1.getNumLocalVars(), 2u);
 942     EXPECT_EQ(poly2.getNumLocalVars(), 2u);
 943   }
 944
 945   {
 946     // (x) : (exists y = [x / 2], z = [x + y / 3], w = [z + 1 / 5]: y + z >= x).
 947     IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1));
 948     poly1.addLocalFloorDiv({1, 0}, 2);       // y = [x / 2].
 949     poly1.addLocalFloorDiv({1, 1, 0}, 3);    // z = [x + y / 3].
 950     poly1.addLocalFloorDiv({0, 0, 1, 1}, 5); // w = [z + 1 / 5].
 951     poly1.addInequality({-1, 1, 1, 0, 0});   // y + z >= x.
 952
 953     // (x) : (exists y = [x / 2], z = [x + y / 3], w = [z + 1 / 5]: y + z <= x).
 954     IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
 955     poly2.addLocalFloorDiv({1, 0}, 2);       // y = [x / 2].
 956     poly2.addLocalFloorDiv({1, 1, 0}, 3);    // z = [x + y / 3].
 957     poly2.addLocalFloorDiv({0, 0, 1, 1}, 5); // w = [z + 1 / 5].
 958     poly2.addInequality({1, -1, -1, 0, 0});  // y + z <= x.
 959
 960     poly1.mergeLocalVars(poly2);
 961
 962     // Local space should be same.
 963     EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
 964
 965     // 3 divisions should be matched.
 966     EXPECT_EQ(poly1.getNumLocalVars(), 3u);
 967     EXPECT_EQ(poly2.getNumLocalVars(), 3u);
 968   }
 969   {
 970     // (x) : (exists y = [x / 2], z = [x + y / 3]: y + z >= x).
 971     IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1));
 972     poly1.addLocalFloorDiv({2, 0}, 4);    // y = [2x / 4] -> [x / 2].
 973     poly1.addLocalFloorDiv({1, 1, 0}, 3); // z = [x + y / 3].
 974     poly1.addInequality({-1, 1, 1, 0});   // y + z >= x.
 975
 976     // (x) : (exists y = [x / 2], z = [x + y / 3]: y + z <= x).
 977     IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
 978     poly2.addLocalFloorDiv({1, 0}, 2); // y = [x / 2].
 979     // This division would be normalized.
 980     poly2.addLocalFloorDiv({3, 3, 0}, 9); // z = [3x + 3y / 9] -> [x + y / 3].
 981     poly2.addInequality({1, -1, -1, 0});  // y + z <= x.
 982
 983     poly1.mergeLocalVars(poly2);
 984
 985     // Local space should be same.
 986     EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
 987
 988     // 2 divisions should be matched.
 989     EXPECT_EQ(poly1.getNumLocalVars(), 2u);
 990     EXPECT_EQ(poly2.getNumLocalVars(), 2u);
 991   }
 992 }
 993
 994 TEST(IntegerPolyhedronTest, mergeDivisionsConstants) {
 995   {
 996     // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z >= x).
 997     IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1));
 998     poly1.addLocalFloorDiv({1, 1}, 2);    // y = [x + 1 / 2].
 999     poly1.addLocalFloorDiv({1, 0, 2}, 3); // z = [x + 2 / 3].
1000     poly1.addInequality({-1, 1, 1, 0});   // y + z >= x.
1001
1002     // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x).
1003     IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
1004     poly2.addLocalFloorDiv({1, 1}, 2);    // y = [x + 1 / 2].
1005     poly2.addLocalFloorDiv({1, 0, 2}, 3); // z = [x + 2 / 3].
1006     poly2.addInequality({1, -1, -1, 0});  // y + z <= x.
1007
1008     poly1.mergeLocalVars(poly2);
1009
1010     // Local space should be same.
1011     EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
1012
1013     // 2 divisions should be matched.
1014     EXPECT_EQ(poly1.getNumLocalVars(), 2u);
1015     EXPECT_EQ(poly2.getNumLocalVars(), 2u);
1016   }
1017   {
1018     // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z >= x).
1019     IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1));
1020     poly1.addLocalFloorDiv({1, 1}, 2); // y = [x + 1 / 2].
1021     // Normalization test.
1022     poly1.addLocalFloorDiv({3, 0, 6}, 9); // z = [3x + 6 / 9] -> [x + 2 / 3].
1023     poly1.addInequality({-1, 1, 1, 0});   // y + z >= x.
1024
1025     // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x).
1026     IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
1027     // Normalization test.
1028     poly2.addLocalFloorDiv({2, 2}, 4);    // y = [2x + 2 / 4] -> [x + 1 / 2].
1029     poly2.addLocalFloorDiv({1, 0, 2}, 3); // z = [x + 2 / 3].
1030     poly2.addInequality({1, -1, -1, 0});  // y + z <= x.
1031
1032     poly1.mergeLocalVars(poly2);
1033
1034     // Local space should be same.
1035     EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
1036
1037     // 2 divisions should be matched.
1038     EXPECT_EQ(poly1.getNumLocalVars(), 2u);
1039     EXPECT_EQ(poly2.getNumLocalVars(), 2u);
1040   }
1041 }
1042
1043 TEST(IntegerPolyhedronTest, mergeDivisionsDuplicateInSameSet) {
1044   // (x) : (exists y = [x + 1 / 3], z = [x + 1 / 3]: y + z >= x).
1045   IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1));
1046   poly1.addLocalFloorDiv({1, 1}, 3);    // y = [x + 1 / 2].
1047   poly1.addLocalFloorDiv({1, 0, 1}, 3); // z = [x + 1 / 3].
1048   poly1.addInequality({-1, 1, 1, 0});   // y + z >= x.
1049
1050   // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x).
1051   IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
1052   poly2.addLocalFloorDiv({1, 1}, 3);    // y = [x + 1 / 3].
1053   poly2.addLocalFloorDiv({1, 0, 2}, 3); // z = [x + 2 / 3].
1054   poly2.addInequality({1, -1, -1, 0});  // y + z <= x.
1055
1056   poly1.mergeLocalVars(poly2);
1057
1058   // Local space should be same.
1059   EXPECT_EQ(poly1.getNumLocalVars(), poly2.getNumLocalVars());
1060
1061   // 1 divisions should be matched.
1062   EXPECT_EQ(poly1.getNumLocalVars(), 3u);
1063   EXPECT_EQ(poly2.getNumLocalVars(), 3u);
1064 }
1065
1066 TEST(IntegerPolyhedronTest, negativeDividends) {
1067   // (x) : (exists y = [-x + 1 / 2], z = [-x - 2 / 3]: y + z >= x).
1068   IntegerPolyhedron poly1(PresburgerSpace::getSetSpace(1));
1069   poly1.addLocalFloorDiv({-1, 1}, 2); // y = [x + 1 / 2].
1070   // Normalization test with negative dividends
1071   poly1.addLocalFloorDiv({-3, 0, -6}, 9); // z = [3x + 6 / 9] -> [x + 2 / 3].
1072   poly1.addInequality({-1, 1, 1, 0});     // y + z >= x.
1073
1074   // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x).
1075   IntegerPolyhedron poly2(PresburgerSpace::getSetSpace(1));
1076   // Normalization test.
1077   poly2.addLocalFloorDiv({-2, 2}, 4);     // y = [-2x + 2 / 4] -> [-x + 1 / 2].
1078   poly2.addLocalFloorDiv({-1, 0, -2}, 3); // z = [-x - 2 / 3].
1079   poly2.addInequality({1, -1, -1, 0});    // y + z <= x.
1080
1081   poly1.mergeLocalVars(poly2);
1082
1083   // Merging triggers normalization.
1084   std::vector<SmallVector<int64_t, 8>> divisions = {{-1, 0, 0, 1},
1085                                                     {-1, 0, 0, -2}};
1086   SmallVector<int64_t, 8> denoms = {2, 3};
1087   checkDivisionRepresentation(poly1, divisions, denoms);
1088 }
1089
1090 void expectRationalLexMin(const IntegerPolyhedron &poly,
1091                           ArrayRef<Fraction> min) {
1092   auto lexMin = poly.findRationalLexMin();
1093   ASSERT_TRUE(lexMin.isBounded());
1094   EXPECT_EQ(ArrayRef<Fraction>(*lexMin), min);
1095 }
1096
1097 void expectNoRationalLexMin(OptimumKind kind, const IntegerPolyhedron &poly) {
1098   ASSERT_NE(kind, OptimumKind::Bounded)
1099       << "Use expectRationalLexMin for bounded min";
1100   EXPECT_EQ(poly.findRationalLexMin().getKind(), kind);
1101 }
1102
1103 TEST(IntegerPolyhedronTest, findRationalLexMin) {
1104   expectRationalLexMin(
1105       parseIntegerPolyhedron(
1106           "(x, y, z) : (x + 10 >= 0, y + 40 >= 0, z + 30 >= 0)"),
1107       {{-10, 1}, {-40, 1}, {-30, 1}});
1108   expectRationalLexMin(
1109       parseIntegerPolyhedron(
1110           "(x, y, z) : (2*x + 7 >= 0, 3*y - 5 >= 0, 8*z + 10 >= 0, 9*z >= 0)"),
1111       {{-7, 2}, {5, 3}, {0, 1}});
1112   expectRationalLexMin(
1113       parseIntegerPolyhedron("(x, y) : (3*x + 2*y + 10 >= 0, -3*y + 10 >= "
1114                              "0, 4*x - 7*y - 10 >= 0)"),
1115       {{-50, 29}, {-70, 29}});
1116
1117   // Test with some locals. This is basically x >= 11, 0 <= x - 2e <= 1.
1118   // It'll just choose x = 11, e = 5.5 since it's rational lexmin.
1119   expectRationalLexMin(
1120       parseIntegerPolyhedron(
1121           "(x, y) : (x - 2*(x floordiv 2) == 0, y - 2*x >= 0, x - 11 >= 0)"),
1122       {{11, 1}, {22, 1}});
1123
1124   expectRationalLexMin(
1125       parseIntegerPolyhedron("(x, y) : (3*x + 2*y + 10 >= 0,"
1126                              "-4*x + 7*y + 10 >= 0, -3*y + 10 >= 0)"),
1127       {{-50, 9}, {10, 3}});
1128
1129   // Cartesian product of above with itself.
1130   expectRationalLexMin(
1131       parseIntegerPolyhedron(
1132           "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0,"
1133           "-3*y + 10 >= 0, 3*z + 2*w + 10 >= 0, -4*z + 7*w + 10 >= 0,"
1134           "-3*w + 10 >= 0)"),
1135       {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}});
1136
1137   // Same as above but for the constraints on z and w, we express "10" in terms
1138   // of x and y. We know that x and y still have to take the values
1139   // -50/9 and 10/3 since their constraints are the same and their values are
1140   // minimized first. Accordingly, the values -9x - 12y,  -9x - 0y - 10,
1141   // and -9x - 15y + 10 are all equal to 10.
1142   expectRationalLexMin(
1143       parseIntegerPolyhedron(
1144           "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0, "
1145           "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0,"
1146           "-4*z + 7*w + - 9*x - 9*y - 10 >= 0, -3*w - 9*x - 15*y + 10 >= 0)"),
1147       {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}});
1148
1149   // Same as above with one constraint removed, making the lexmin unbounded.
1150   expectNoRationalLexMin(
1151       OptimumKind::Unbounded,
1152       parseIntegerPolyhedron(
1153           "(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0,"
1154           "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0,"
1155           "-4*z + 7*w + - 9*x - 9*y - 10>= 0)"));
1156
1157   // Again, the lexmin is unbounded.
1158   expectNoRationalLexMin(
1159       OptimumKind::Unbounded,
1160       parseIntegerPolyhedron(
1161           "(x, y, z) : (2*x + 5*y + 8*z - 10 >= 0,"
1162           "2*x + 10*y + 8*z - 10 >= 0, 2*x + 5*y + 10*z - 10 >= 0)"));
1163
1164   // The set is empty.
1165   expectNoRationalLexMin(
1166       OptimumKind::Empty,
1167       parseIntegerPolyhedron("(x) : (2*x >= 0, -x - 1 >= 0)"));
1168 }
1169
1170 void expectIntegerLexMin(const IntegerPolyhedron &poly, ArrayRef<int64_t> min) {
1171   MaybeOptimum<SmallVector<DynamicAPInt, 8>> lexMin = poly.findIntegerLexMin();
1172   ASSERT_TRUE(lexMin.isBounded());
1173   EXPECT_EQ(*lexMin, getDynamicAPIntVec(min));
1174 }
1175
1176 void expectNoIntegerLexMin(OptimumKind kind, const IntegerPolyhedron &poly) {
1177   ASSERT_NE(kind, OptimumKind::Bounded)
1178       << "Use expectRationalLexMin for bounded min";
1179   EXPECT_EQ(poly.findRationalLexMin().getKind(), kind);
1180 }
1181
1182 TEST(IntegerPolyhedronTest, findIntegerLexMin) {
1183   expectIntegerLexMin(
1184       parseIntegerPolyhedron("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2  >= "
1185                              "0, 11*z + 5*y - 3*x + 7 >= 0)"),
1186       {-6, -4, 0});
1187   // Similar to above but no lower bound on z.
1188   expectNoIntegerLexMin(
1189       OptimumKind::Unbounded,
1190       parseIntegerPolyhedron("(x, y, z) : (2*x + 13 >= 0, 4*y - 3*x - 2  "
1191                              ">= 0, -11*z + 5*y - 3*x + 7 >= 0)"));
1192 }
1193
1194 void expectSymbolicIntegerLexMin(
1195     StringRef polyStr,
1196     ArrayRef<std::pair<StringRef, StringRef>> expectedLexminRepr,
1197     ArrayRef<StringRef> expectedUnboundedDomainRepr) {
1198   IntegerPolyhedron poly = parseIntegerPolyhedron(polyStr);
1199
1200   ASSERT_NE(poly.getNumDimVars(), 0u);
1201   ASSERT_NE(poly.getNumSymbolVars(), 0u);
1202
1203   SymbolicLexOpt result = poly.findSymbolicIntegerLexMin();
1204
1205   if (expectedLexminRepr.empty()) {
1206     EXPECT_TRUE(result.lexopt.getDomain().isIntegerEmpty());
1207   } else {
1208     PWMAFunction expectedLexmin = parsePWMAF(expectedLexminRepr);
1209     EXPECT_TRUE(result.lexopt.isEqual(expectedLexmin));
1210   }
1211
1212   if (expectedUnboundedDomainRepr.empty()) {
1213     EXPECT_TRUE(result.unboundedDomain.isIntegerEmpty());
1214   } else {
1215     PresburgerSet expectedUnboundedDomain =
1216         parsePresburgerSet(expectedUnboundedDomainRepr);
1217     EXPECT_TRUE(result.unboundedDomain.isEqual(expectedUnboundedDomain));
1218   }
1219 }
1220
1221 void expectSymbolicIntegerLexMin(
1222     StringRef polyStr, ArrayRef<std::pair<StringRef, StringRef>> result) {
1223   expectSymbolicIntegerLexMin(polyStr, result, {});
1224 }
1225
1226 TEST(IntegerPolyhedronTest, findSymbolicIntegerLexMin) {
1227   expectSymbolicIntegerLexMin("(x)[a] : (x - a >= 0)",
1228                               {
1229                                   {"()[a] : ()", "()[a] -> (a)"},
1230                               });
1231
1232   expectSymbolicIntegerLexMin(
1233       "(x)[a, b] : (x - a >= 0, x - b >= 0)",
1234       {
1235           {"()[a, b] : (a - b >= 0)", "()[a, b] -> (a)"},
1236           {"()[a, b] : (b - a - 1 >= 0)", "()[a, b] -> (b)"},
1237       });
1238
1239   expectSymbolicIntegerLexMin(
1240       "(x)[a, b, c] : (x -a >= 0, x - b >= 0, x - c >= 0)",
1241       {
1242           {"()[a, b, c] : (a - b >= 0, a - c >= 0)", "()[a, b, c] -> (a)"},
1243           {"()[a, b, c] : (b - a - 1 >= 0, b - c >= 0)", "()[a, b, c] -> (b)"},
1244           {"()[a, b, c] : (c - a - 1 >= 0, c - b - 1 >= 0)",
1245            "()[a, b, c] -> (c)"},
1246       });
1247
1248   expectSymbolicIntegerLexMin("(x, y)[a] : (x - a >= 0, x + y >= 0)",
1249                               {
1250                                   {"()[a] : ()", "()[a] -> (a, -a)"},
1251                               });
1252
1253   expectSymbolicIntegerLexMin("(x, y)[a] : (x - a >= 0, x + y >= 0, y >= 0)",
1254                               {
1255                                   {"()[a] : (a >= 0)", "()[a] -> (a, 0)"},
1256                                   {"()[a] : (-a - 1 >= 0)", "()[a] -> (a, -a)"},
1257                               });
1258
1259   expectSymbolicIntegerLexMin(
1260       "(x, y)[a, b, c] : (x - a >= 0, y - b >= 0, c - x - y >= 0)",
1261       {
1262           {"()[a, b, c] : (c - a - b >= 0)", "()[a, b, c] -> (a, b)"},
1263       });
1264
1265   expectSymbolicIntegerLexMin(
1266       "(x, y, z)[a, b, c] : (c - z >= 0, b - y >= 0, x + y + z - a == 0)",
1267       {
1268           {"()[a, b, c] : ()", "()[a, b, c] -> (a - b - c, b, c)"},
1269       });
1270
1271   expectSymbolicIntegerLexMin(
1272       "(x)[a, b] : (a >= 0, b >= 0, x >= 0, a + b + x - 1 >= 0)",
1273       {
1274           {"()[a, b] : (a >= 0, b >= 0, a + b - 1 >= 0)", "()[a, b] -> (0)"},
1275           {"()[a, b] : (a == 0, b == 0)", "()[a, b] -> (1)"},
1276       });
1277
1278   expectSymbolicIntegerLexMin(
1279       "(x)[a, b] : (1 - a >= 0, a >= 0, 1 - b >= 0, b >= 0, 1 - x >= 0, x >= "
1280       "0, a + b + x - 1 >= 0)",
1281       {
1282           {"()[a, b] : (1 - a >= 0, a >= 0, 1 - b >= 0, b >= 0, a + b - 1 >= "
1283            "0)",
1284            "()[a, b] -> (0)"},
1285           {"()[a, b] : (a == 0, b == 0)", "()[a, b] -> (1)"},
1286       });
1287
1288   expectSymbolicIntegerLexMin(
1289       "(x, y, z)[a, b] : (x - a == 0, y - b == 0, x >= 0, y >= 0, z >= 0, x + "
1290       "y + z - 1 >= 0)",
1291       {
1292           {"()[a, b] : (a >= 0, b >= 0, 1 - a - b >= 0)",
1293            "()[a, b] -> (a, b, 1 - a - b)"},
1294           {"()[a, b] : (a >= 0, b >= 0, a + b - 2 >= 0)",
1295            "()[a, b] -> (a, b, 0)"},
1296       });
1297
1298   expectSymbolicIntegerLexMin(
1299       "(x)[a, b] : (x - a == 0, x - b >= 0)",
1300       {
1301           {"()[a, b] : (a - b >= 0)", "()[a, b] -> (a)"},
1302       });
1303
1304   expectSymbolicIntegerLexMin(
1305       "(q)[a] : (a - 1 - 3*q == 0, q >= 0)",
1306       {
1307           {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",
1308            "()[a] -> (a floordiv 3)"},
1309       });
1310
1311   expectSymbolicIntegerLexMin(
1312       "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 1 - r >= 0, r >= 0)",
1313       {
1314           {"()[a] : (a - 0 - 3*(a floordiv 3) == 0, a >= 0)",
1315            "()[a] -> (0, a floordiv 3)"},
1316           {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",
1317            "()[a] -> (1, a floordiv 3)"}, // (1 a floordiv 3)
1318       });
1319
1320   expectSymbolicIntegerLexMin(
1321       "(r, q)[a] : (a - r - 3*q == 0, q >= 0, 2 - r >= 0, r - 1 >= 0)",
1322       {
1323           {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",
1324            "()[a] -> (1, a floordiv 3)"},
1325           {"()[a] : (a - 2 - 3*(a floordiv 3) == 0, a >= 0)",
1326            "()[a] -> (2, a floordiv 3)"},
1327       });
1328
1329   expectSymbolicIntegerLexMin(
1330       "(r, q)[a] : (a - r - 3*q == 0, q >= 0, r >= 0)",
1331       {
1332           {"()[a] : (a - 3*(a floordiv 3) == 0, a >= 0)",
1333            "()[a] -> (0, a floordiv 3)"},
1334           {"()[a] : (a - 1 - 3*(a floordiv 3) == 0, a >= 0)",
1335            "()[a] -> (1, a floordiv 3)"},
1336           {"()[a] : (a - 2 - 3*(a floordiv 3) == 0, a >= 0)",
1337            "()[a] -> (2, a floordiv 3)"},
1338       });
1339
1340   expectSymbolicIntegerLexMin(
1341       "(x, y, z, w)[g] : ("
1342       // x, y, z, w are boolean variables.
1343       "1 - x >= 0, x >= 0, 1 - y >= 0, y >= 0,"
1344       "1 - z >= 0, z >= 0, 1 - w >= 0, w >= 0,"
1345       // We have some constraints on them:
1346       "x + y + z - 1 >= 0,"             // x or y or z
1347       "x + y + w - 1 >= 0,"             // x or y or w
1348       "1 - x + 1 - y + 1 - w - 1 >= 0," // ~x or ~y or ~w
1349       // What's the lexmin solution using exactly g true vars?
1350       "g - x - y - z - w == 0)",
1351       {
1352           {"()[g] : (g - 1 == 0)", "()[g] -> (0, 1, 0, 0)"},
1353           {"()[g] : (g - 2 == 0)", "()[g] -> (0, 0, 1, 1)"},
1354           {"()[g] : (g - 3 == 0)", "()[g] -> (0, 1, 1, 1)"},
1355       });
1356
1357   // Bezout's lemma: if a, b are constants,
1358   // the set of values that ax + by can take is all multiples of gcd(a, b).
1359   expectSymbolicIntegerLexMin(
1360       // If (x, y) is a solution for a given [a, r], then so is (x - 5, y + 2).
1361       // So the lexmin is unbounded if it exists.
1362       "(x, y)[a, r] : (a >= 0, r - a + 14*x + 35*y == 0)", {},
1363       // According to Bezout's lemma, 14x + 35y can take on all multiples
1364       // of 7 and no other values. So the solution exists iff r - a is a
1365       // multiple of 7.
1366       {"()[a, r] : (a >= 0, r - a - 7*((r - a) floordiv 7) == 0)"});
1367
1368   // The lexmins are unbounded.
1369   expectSymbolicIntegerLexMin("(x, y)[a] : (9*x - 4*y - 2*a >= 0)", {},
1370                               {"()[a] : ()"});
1371
1372   // Test cases adapted from isl.
1373   expectSymbolicIntegerLexMin(
1374       // a = 2b - 2(c - b), c - b >= 0.
1375       // So b is minimized when c = b.
1376       "(b, c)[a] : (a - 4*b + 2*c == 0, c - b >= 0)",
1377       {
1378           {"()[a] : (a - 2*(a floordiv 2) == 0)",
1379            "()[a] -> (a floordiv 2, a floordiv 2)"},
1380       });
1381
1382   expectSymbolicIntegerLexMin(
1383       // 0 <= b <= 255, 1 <= a - 512b <= 509,
1384       // b + 8 >= 1 + 16*(b + 8 floordiv 16) // i.e. b % 16 != 8
1385       "(b)[a] : (255 - b >= 0, b >= 0, a - 512*b - 1 >= 0, 512*b -a + 509 >= "
1386       "0, b + 7 - 16*((8 + b) floordiv 16) >= 0)",
1387       {
1388           {"()[a] : (255 - (a floordiv 512) >= 0, a >= 0, a - 512*(a floordiv "
1389            "512) - 1 >= 0, 512*(a floordiv 512) - a + 509 >= 0, (a floordiv "
1390            "512) + 7 - 16*((8 + (a floordiv 512)) floordiv 16) >= 0)",
1391            "()[a] -> (a floordiv 512)"},
1392       });
1393
1394   expectSymbolicIntegerLexMin(
1395       "(a, b)[K, N, x, y] : (N - K - 2 >= 0, K + 4 - N >= 0, x - 4 >= 0, x + 6 "
1396       "- 2*N >= 0, K+N - x - 1 >= 0, a - N + 1 >= 0, K+N-1-a >= 0,a + 6 - b - "
1397       "N >= 0, 2*N - 4 - a >= 0,"
1398       "2*N - 3*K + a - b >= 0, 4*N - K + 1 - 3*b >= 0, b - N >= 0, a - x - 1 "
1399       ">= 0)",
1400       {
1401           {"()[K, N, x, y] : (x + 6 - 2*N >= 0, 2*N - 5 - x >= 0, x + 1 -3*K + "
1402            "N >= 0, N + K - 2 - x >= 0, x - 4 >= 0)",
1403            "()[K, N, x, y] -> (1 + x, N)"},
1404       });
1405 }
1406
1407 static void
1408 expectComputedVolumeIsValidOverapprox(const IntegerPolyhedron &poly,
1409                                       std::optional<int64_t> trueVolume,
1410                                       std::optional<int64_t> resultBound) {
1411   expectComputedVolumeIsValidOverapprox(poly.computeVolume(), trueVolume,
1412                                         resultBound);
1413 }
1414
1415 TEST(IntegerPolyhedronTest, computeVolume) {
1416   // 0 <= x <= 3 + 1/3, -5.5 <= y <= 2 + 3/5, 3 <= z <= 1.75.
1417   // i.e. 0 <= x <= 3, -5 <= y <= 2, 3 <= z <= 3 + 1/4.
1418   // So volume is 4 * 8 * 1 = 32.
1419   expectComputedVolumeIsValidOverapprox(
1420       parseIntegerPolyhedron(
1421           "(x, y, z) : (x >= 0, -3*x + 10 >= 0, 2*y + 11 >= 0,"
1422           "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"),
1423       /*trueVolume=*/32ull, /*resultBound=*/32ull);
1424
1425   // Same as above but y has bounds 2 + 1/5 <= y <= 2 + 3/5. So the volume is
1426   // zero.
1427   expectComputedVolumeIsValidOverapprox(
1428       parseIntegerPolyhedron(
1429           "(x, y, z) : (x >= 0, -3*x + 10 >= 0, 5*y - 11 >= 0,"
1430           "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"),
1431       /*trueVolume=*/0ull, /*resultBound=*/0ull);
1432
1433   // Now x is unbounded below but y still has no integer values.
1434   expectComputedVolumeIsValidOverapprox(
1435       parseIntegerPolyhedron("(x, y, z) : (-3*x + 10 >= 0, 5*y - 11 >= 0,"
1436                              "-5*y + 13 >= 0, z - 3 >= 0, -4*z + 13 >= 0)"),
1437       /*trueVolume=*/0ull, /*resultBound=*/0ull);
1438
1439   // A diamond shape, 0 <= x + y <= 10, 0 <= x - y <= 10,
1440   // with vertices at (0, 0), (5, 5), (5, 5), (10, 0).
1441   // x and y can take 11 possible values so result computed is 11*11 = 121.
1442   expectComputedVolumeIsValidOverapprox(
1443       parseIntegerPolyhedron(
1444           "(x, y) : (x + y >= 0, -x - y + 10 >= 0, x - y >= 0,"
1445           "-x + y + 10 >= 0)"),
1446       /*trueVolume=*/61ull, /*resultBound=*/121ull);
1447
1448   // Effectively the same diamond as above; constrain the variables to be even
1449   // and double the constant terms of the constraints. The algorithm can't
1450   // eliminate locals exactly, so the result is an overapproximation by
1451   // computing that x and y can take 21 possible values so result is 21*21 =
1452   // 441.
1453   expectComputedVolumeIsValidOverapprox(
1454       parseIntegerPolyhedron(
1455           "(x, y) : (x + y >= 0, -x - y + 20 >= 0, x - y >= 0,"
1456           " -x + y + 20 >= 0, x - 2*(x floordiv 2) == 0,"
1457           "y - 2*(y floordiv 2) == 0)"),
1458       /*trueVolume=*/61ull, /*resultBound=*/441ull);
1459
1460   // Unbounded polytope.
1461   expectComputedVolumeIsValidOverapprox(
1462       parseIntegerPolyhedron("(x, y) : (2*x - y >= 0, y - 3*x >= 0)"),
1463       /*trueVolume=*/{}, /*resultBound=*/{});
1464 }
1465
1466 bool containsPointNoLocal(const IntegerPolyhedron &poly,
1467                           ArrayRef<int64_t> point) {
1468   return poly.containsPointNoLocal(getDynamicAPIntVec(point)).has_value();
1469 }
1470
1471 TEST(IntegerPolyhedronTest, containsPointNoLocal) {
1472   IntegerPolyhedron poly1 =
1473       parseIntegerPolyhedron("(x) : ((x floordiv 2) - x == 0)");
1474   EXPECT_TRUE(poly1.containsPointNoLocal({0}));
1475   EXPECT_FALSE(poly1.containsPointNoLocal({1}));
1476
1477   IntegerPolyhedron poly2 = parseIntegerPolyhedron(
1478       "(x) : (x - 2*(x floordiv 2) == 0, x - 4*(x floordiv 4) - 2 == 0)");
1479   EXPECT_TRUE(containsPointNoLocal(poly2, {6}));
1480   EXPECT_FALSE(containsPointNoLocal(poly2, {4}));
1481
1482   IntegerPolyhedron poly3 =
1483       parseIntegerPolyhedron("(x, y) : (2*x - y >= 0, y - 3*x >= 0)");
1484
1485   EXPECT_TRUE(poly3.containsPointNoLocal(ArrayRef<int64_t>({0, 0})));
1486   EXPECT_FALSE(poly3.containsPointNoLocal({1, 0}));
1487 }
1488
1489 TEST(IntegerPolyhedronTest, truncateEqualityRegressionTest) {
1490   // IntegerRelation::truncate was truncating inequalities to the number of
1491   // equalities.
1492   IntegerRelation set(PresburgerSpace::getSetSpace(1));
1493   IntegerRelation::CountsSnapshot snapshot = set.getCounts();
1494   set.addEquality({1, 0});
1495   set.truncate(snapshot);
1496   EXPECT_EQ(set.getNumEqualities(), 0u);
1497 }