mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp

   1 //===- IntegerRelationTest.cpp - Tests for IntegerRelation 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 "mlir/Analysis/Presburger/IntegerRelation.h"
  10 #include "Parser.h"
  11 #include "mlir/Analysis/Presburger/PresburgerSpace.h"
  12 #include "mlir/Analysis/Presburger/Simplex.h"
  13
  14 #include <gmock/gmock.h>
  15 #include <gtest/gtest.h>
  16
  17 using namespace mlir;
  18 using namespace presburger;
  19
  20 TEST(IntegerRelationTest, getDomainAndRangeSet) {
  21   IntegerRelation rel = parseRelationFromSet(
  22       "(x, xr)[N] : (xr - x - 10 == 0, xr >= 0, N - xr >= 0)", 1);
  23
  24   IntegerPolyhedron domainSet = rel.getDomainSet();
  25
  26   IntegerPolyhedron expectedDomainSet =
  27       parseIntegerPolyhedron("(x)[N] : (x + 10 >= 0, N - x - 10 >= 0)");
  28
  29   EXPECT_TRUE(domainSet.isEqual(expectedDomainSet));
  30
  31   IntegerPolyhedron rangeSet = rel.getRangeSet();
  32
  33   IntegerPolyhedron expectedRangeSet =
  34       parseIntegerPolyhedron("(x)[N] : (x >= 0, N - x >= 0)");
  35
  36   EXPECT_TRUE(rangeSet.isEqual(expectedRangeSet));
  37 }
  38
  39 TEST(IntegerRelationTest, inverse) {
  40   IntegerRelation rel =
  41       parseRelationFromSet("(x, y, z)[N, M] : (z - x - y == 0, x >= 0, N - x "
  42                            ">= 0, y >= 0, M - y >= 0)",
  43                            2);
  44
  45   IntegerRelation inverseRel =
  46       parseRelationFromSet("(z, x, y)[N, M]  : (x >= 0, N - x >= 0, y >= 0, M "
  47                            "- y >= 0, x + y - z == 0)",
  48                            1);
  49
  50   rel.inverse();
  51
  52   EXPECT_TRUE(rel.isEqual(inverseRel));
  53 }
  54
  55 TEST(IntegerRelationTest, intersectDomainAndRange) {
  56   IntegerRelation rel = parseRelationFromSet(
  57       "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
  58       ">= 0, x + y + z floordiv 7 == 0)",
  59       1);
  60
  61   {
  62     IntegerPolyhedron poly =
  63         parseIntegerPolyhedron("(x)[N, M] : (x >= 0, M - x - 1 >= 0)");
  64
  65     IntegerRelation expectedRel = parseRelationFromSet(
  66         "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
  67         ">= 0, x + y + z floordiv 7 == 0, x >= 0, M - x - 1 >= 0)",
  68         1);
  69
  70     IntegerRelation copyRel = rel;
  71     copyRel.intersectDomain(poly);
  72     EXPECT_TRUE(copyRel.isEqual(expectedRel));
  73   }
  74
  75   {
  76     IntegerPolyhedron poly = parseIntegerPolyhedron(
  77         "(y, z)[N, M] : (y >= 0, M - y - 1 >= 0, y + z == 0)");
  78
  79     IntegerRelation expectedRel = parseRelationFromSet(
  80         "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
  81         ">= 0, x + y + z floordiv 7 == 0, y >= 0, M - y - 1 >= 0, y + z == 0)",
  82         1);
  83
  84     IntegerRelation copyRel = rel;
  85     copyRel.intersectRange(poly);
  86     EXPECT_TRUE(copyRel.isEqual(expectedRel));
  87   }
  88 }
  89
  90 TEST(IntegerRelationTest, applyDomainAndRange) {
  91
  92   {
  93     IntegerRelation map1 = parseRelationFromSet(
  94         "(x, y, a, b)[N] : (a - x - N == 0, b - y + N == 0)", 2);
  95     IntegerRelation map2 =
  96         parseRelationFromSet("(x, y, a)[N] : (a - x - y == 0)", 2);
  97
  98     map1.applyRange(map2);
  99
 100     IntegerRelation map3 =
 101         parseRelationFromSet("(x, y, a)[N] : (a - x - y == 0)", 2);
 102
 103     EXPECT_TRUE(map1.isEqual(map3));
 104   }
 105
 106   {
 107     IntegerRelation map1 = parseRelationFromSet(
 108         "(x, y, a, b)[N] : (a - x + N == 0, b - y - N == 0)", 2);
 109     IntegerRelation map2 =
 110         parseRelationFromSet("(x, y, a, b)[N] : (a - N == 0, b - N == 0)", 2);
 111
 112     IntegerRelation map3 =
 113         parseRelationFromSet("(x, y, a, b)[N] : (x - N == 0, y - N == 0)", 2);
 114
 115     map1.applyDomain(map2);
 116
 117     EXPECT_TRUE(map1.isEqual(map3));
 118   }
 119 }
 120
 121 TEST(IntegerRelationTest, symbolicLexmin) {
 122   SymbolicLexOpt lexmin =
 123       parseRelationFromSet("(a, x)[b] : (x - a >= 0, x - b >= 0)", 1)
 124           .findSymbolicIntegerLexMin();
 125
 126   PWMAFunction expectedLexmin = parsePWMAF({
 127       {"(a)[b] : (a - b >= 0)", "(a)[b] -> (a)"},     // a
 128       {"(a)[b] : (b - a - 1 >= 0)", "(a)[b] -> (b)"}, // b
 129   });
 130   EXPECT_TRUE(lexmin.unboundedDomain.isIntegerEmpty());
 131   EXPECT_TRUE(lexmin.lexopt.isEqual(expectedLexmin));
 132 }
 133
 134 TEST(IntegerRelationTest, symbolicLexmax) {
 135   SymbolicLexOpt lexmax1 =
 136       parseRelationFromSet("(a, x)[b] : (a - x >= 0, b - x >= 0)", 1)
 137           .findSymbolicIntegerLexMax();
 138
 139   PWMAFunction expectedLexmax1 = parsePWMAF({
 140       {"(a)[b] : (a - b >= 0)", "(a)[b] -> (b)"},
 141       {"(a)[b] : (b - a - 1 >= 0)", "(a)[b] -> (a)"},
 142   });
 143
 144   SymbolicLexOpt lexmax2 =
 145       parseRelationFromSet("(i, j)[N] : (i >= 0, j >= 0, N - i - j >= 0)", 1)
 146           .findSymbolicIntegerLexMax();
 147
 148   PWMAFunction expectedLexmax2 = parsePWMAF({
 149       {"(i)[N] : (i >= 0, N - i >= 0)", "(i)[N] -> (N - i)"},
 150   });
 151
 152   SymbolicLexOpt lexmax3 =
 153       parseRelationFromSet("(x, y)[N] : (x >= 0, 2 * N - x >= 0, y >= 0, x - y "
 154                            "+ 2 * N >= 0, 4 * N - x - y >= 0)",
 155                            1)
 156           .findSymbolicIntegerLexMax();
 157
 158   PWMAFunction expectedLexmax3 =
 159       parsePWMAF({{"(x)[N] : (x >= 0, 2 * N - x >= 0, x - N - 1 >= 0)",
 160                    "(x)[N] -> (4 * N - x)"},
 161                   {"(x)[N] : (x >= 0, 2 * N - x >= 0, -x + N >= 0)",
 162                    "(x)[N] -> (x + 2 * N)"}});
 163
 164   EXPECT_TRUE(lexmax1.unboundedDomain.isIntegerEmpty());
 165   EXPECT_TRUE(lexmax1.lexopt.isEqual(expectedLexmax1));
 166   EXPECT_TRUE(lexmax2.unboundedDomain.isIntegerEmpty());
 167   EXPECT_TRUE(lexmax2.lexopt.isEqual(expectedLexmax2));
 168   EXPECT_TRUE(lexmax3.unboundedDomain.isIntegerEmpty());
 169   EXPECT_TRUE(lexmax3.lexopt.isEqual(expectedLexmax3));
 170 }
 171
 172 TEST(IntegerRelationTest, swapVar) {
 173   PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 2, 0);
 174
 175   int identifiers[6] = {0, 1, 2, 3, 4};
 176
 177   // Attach identifiers to domain identifiers.
 178   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 179   space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
 180
 181   // Attach identifiers to range identifiers.
 182   space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
 183
 184   // Attach identifiers to symbol identifiers.
 185   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 186   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 187
 188   IntegerRelation rel =
 189       parseRelationFromSet("(x, y, z)[N, M] : (z - x - y == 0, x >= 0, N - x "
 190                            ">= 0, y >= 0, M - y >= 0)",
 191                            2);
 192   rel.setSpace(space);
 193   // Swap (Domain 0, Range 0)
 194   rel.swapVar(0, 2);
 195   // Swap (Domain 1, Symbol 1)
 196   rel.swapVar(1, 4);
 197
 198   PresburgerSpace swappedSpace = rel.getSpace();
 199
 200   EXPECT_TRUE(swappedSpace.getId(VarKind::Domain, 0)
 201                   .isEqual(space.getId(VarKind::Range, 0)));
 202   EXPECT_TRUE(swappedSpace.getId(VarKind::Domain, 1)
 203                   .isEqual(space.getId(VarKind::Symbol, 1)));
 204   EXPECT_TRUE(swappedSpace.getId(VarKind::Range, 0)
 205                   .isEqual(space.getId(VarKind::Domain, 0)));
 206   EXPECT_TRUE(swappedSpace.getId(VarKind::Symbol, 1)
 207                   .isEqual(space.getId(VarKind::Domain, 1)));
 208 }
 209
 210 TEST(IntegerRelationTest, mergeAndAlignSymbols) {
 211   IntegerRelation rel =
 212       parseRelationFromSet("(x, y, z, a, b, c)[N, Q] : (a - x - y == 0, "
 213                            "x >= 0, N - b >= 0, y >= 0, Q - y >= 0)",
 214                            3);
 215   IntegerRelation otherRel = parseRelationFromSet(
 216       "(x, y, z, a, b)[N, M, P] : (z - x - y == 0, x >= 0, N - x "
 217       ">= 0, y >= 0, M - y >= 0, 2 * P - 3 * a + 2 * b == 0)",
 218       3);
 219   PresburgerSpace space = PresburgerSpace::getRelationSpace(3, 3, 2, 0);
 220
 221   PresburgerSpace otherSpace = PresburgerSpace::getRelationSpace(3, 2, 3, 0);
 222
 223   // Attach identifiers.
 224   int identifiers[7] = {0, 1, 2, 3, 4, 5, 6};
 225   int otherIdentifiers[8] = {10, 11, 12, 13, 14, 15, 16, 17};
 226
 227   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 228   space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
 229   // Note the common identifier.
 230   space.setId(VarKind::Domain, 2, Identifier(&otherIdentifiers[2]));
 231   space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
 232   space.setId(VarKind::Range, 1, Identifier(&identifiers[3]));
 233   space.setId(VarKind::Range, 2, Identifier(&identifiers[4]));
 234   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[5]));
 235   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[6]));
 236
 237   otherSpace.setId(VarKind::Domain, 0, Identifier(&otherIdentifiers[0]));
 238   otherSpace.setId(VarKind::Domain, 1, Identifier(&otherIdentifiers[1]));
 239   otherSpace.setId(VarKind::Domain, 2, Identifier(&otherIdentifiers[2]));
 240   otherSpace.setId(VarKind::Range, 0, Identifier(&otherIdentifiers[3]));
 241   otherSpace.setId(VarKind::Range, 1, Identifier(&otherIdentifiers[4]));
 242   // Note the common identifier.
 243   otherSpace.setId(VarKind::Symbol, 0, Identifier(&identifiers[6]));
 244   otherSpace.setId(VarKind::Symbol, 1, Identifier(&otherIdentifiers[5]));
 245   otherSpace.setId(VarKind::Symbol, 2, Identifier(&otherIdentifiers[7]));
 246
 247   rel.setSpace(space);
 248   otherRel.setSpace(otherSpace);
 249   rel.mergeAndAlignSymbols(otherRel);
 250
 251   space = rel.getSpace();
 252   otherSpace = otherRel.getSpace();
 253
 254   // Check if merge and align is successful.
 255   // Check symbol var identifiers.
 256   EXPECT_EQ(4u, space.getNumSymbolVars());
 257   EXPECT_EQ(4u, otherSpace.getNumSymbolVars());
 258   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[5]));
 259   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[6]));
 260   EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&otherIdentifiers[5]));
 261   EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&otherIdentifiers[7]));
 262   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 0), Identifier(&identifiers[5]));
 263   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 1), Identifier(&identifiers[6]));
 264   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 2),
 265             Identifier(&otherIdentifiers[5]));
 266   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 3),
 267             Identifier(&otherIdentifiers[7]));
 268   // Check that domain and range var identifiers are not affected.
 269   EXPECT_EQ(3u, space.getNumDomainVars());
 270   EXPECT_EQ(3u, space.getNumRangeVars());
 271   EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
 272   EXPECT_EQ(space.getId(VarKind::Domain, 1), Identifier(&identifiers[1]));
 273   EXPECT_EQ(space.getId(VarKind::Domain, 2), Identifier(&otherIdentifiers[2]));
 274   EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
 275   EXPECT_EQ(space.getId(VarKind::Range, 1), Identifier(&identifiers[3]));
 276   EXPECT_EQ(space.getId(VarKind::Range, 2), Identifier(&identifiers[4]));
 277   EXPECT_EQ(3u, otherSpace.getNumDomainVars());
 278   EXPECT_EQ(2u, otherSpace.getNumRangeVars());
 279   EXPECT_EQ(otherSpace.getId(VarKind::Domain, 0),
 280             Identifier(&otherIdentifiers[0]));
 281   EXPECT_EQ(otherSpace.getId(VarKind::Domain, 1),
 282             Identifier(&otherIdentifiers[1]));
 283   EXPECT_EQ(otherSpace.getId(VarKind::Domain, 2),
 284             Identifier(&otherIdentifiers[2]));
 285   EXPECT_EQ(otherSpace.getId(VarKind::Range, 0),
 286             Identifier(&otherIdentifiers[3]));
 287   EXPECT_EQ(otherSpace.getId(VarKind::Range, 1),
 288             Identifier(&otherIdentifiers[4]));
 289 }
 290
 291 // Check that mergeAndAlignSymbols unions symbol variables when they are
 292 // disjoint.
 293 TEST(IntegerRelationTest, mergeAndAlignDisjointSymbols) {
 294   IntegerRelation rel = parseRelationFromSet(
 295       "(x, y, z)[A, B, C, D] : (x + A - C - y + D - z >= 0)", 2);
 296   IntegerRelation otherRel = parseRelationFromSet(
 297       "(u, v, a, b)[E, F, G, H] : (E - u + v == 0, v - G - H >= 0)", 2);
 298   PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 4, 0);
 299
 300   PresburgerSpace otherSpace = PresburgerSpace::getRelationSpace(2, 2, 4, 0);
 301
 302   // Attach identifiers.
 303   int identifiers[7] = {'x', 'y', 'z', 'A', 'B', 'C', 'D'};
 304   int otherIdentifiers[8] = {'u', 'v', 'a', 'b', 'E', 'F', 'G', 'H'};
 305
 306   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 307   space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
 308   space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
 309   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 310   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 311   space.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
 312   space.setId(VarKind::Symbol, 3, Identifier(&identifiers[6]));
 313
 314   otherSpace.setId(VarKind::Domain, 0, Identifier(&otherIdentifiers[0]));
 315   otherSpace.setId(VarKind::Domain, 1, Identifier(&otherIdentifiers[1]));
 316   otherSpace.setId(VarKind::Range, 0, Identifier(&otherIdentifiers[2]));
 317   otherSpace.setId(VarKind::Range, 1, Identifier(&otherIdentifiers[3]));
 318   otherSpace.setId(VarKind::Symbol, 0, Identifier(&otherIdentifiers[4]));
 319   otherSpace.setId(VarKind::Symbol, 1, Identifier(&otherIdentifiers[5]));
 320   otherSpace.setId(VarKind::Symbol, 2, Identifier(&otherIdentifiers[6]));
 321   otherSpace.setId(VarKind::Symbol, 3, Identifier(&otherIdentifiers[7]));
 322
 323   rel.setSpace(space);
 324   otherRel.setSpace(otherSpace);
 325   rel.mergeAndAlignSymbols(otherRel);
 326
 327   space = rel.getSpace();
 328   otherSpace = otherRel.getSpace();
 329
 330   // Check if merge and align is successful.
 331   // Check symbol var identifiers.
 332   EXPECT_EQ(8u, space.getNumSymbolVars());
 333   EXPECT_EQ(8u, otherSpace.getNumSymbolVars());
 334   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 335   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 336   EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&identifiers[5]));
 337   EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
 338   EXPECT_EQ(space.getId(VarKind::Symbol, 4), Identifier(&otherIdentifiers[4]));
 339   EXPECT_EQ(space.getId(VarKind::Symbol, 5), Identifier(&otherIdentifiers[5]));
 340   EXPECT_EQ(space.getId(VarKind::Symbol, 6), Identifier(&otherIdentifiers[6]));
 341   EXPECT_EQ(space.getId(VarKind::Symbol, 7), Identifier(&otherIdentifiers[7]));
 342   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 343   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 344   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 2), Identifier(&identifiers[5]));
 345   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
 346   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 4),
 347             Identifier(&otherIdentifiers[4]));
 348   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 5),
 349             Identifier(&otherIdentifiers[5]));
 350   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 6),
 351             Identifier(&otherIdentifiers[6]));
 352   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 7),
 353             Identifier(&otherIdentifiers[7]));
 354   // Check that domain and range var identifiers are not affected.
 355   EXPECT_EQ(2u, space.getNumDomainVars());
 356   EXPECT_EQ(1u, space.getNumRangeVars());
 357   EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
 358   EXPECT_EQ(space.getId(VarKind::Domain, 1), Identifier(&identifiers[1]));
 359   EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
 360   EXPECT_EQ(2u, otherSpace.getNumDomainVars());
 361   EXPECT_EQ(2u, otherSpace.getNumRangeVars());
 362   EXPECT_EQ(otherSpace.getId(VarKind::Domain, 0),
 363             Identifier(&otherIdentifiers[0]));
 364   EXPECT_EQ(otherSpace.getId(VarKind::Domain, 1),
 365             Identifier(&otherIdentifiers[1]));
 366   EXPECT_EQ(otherSpace.getId(VarKind::Range, 0),
 367             Identifier(&otherIdentifiers[2]));
 368   EXPECT_EQ(otherSpace.getId(VarKind::Range, 1),
 369             Identifier(&otherIdentifiers[3]));
 370 }
 371
 372 // Check that mergeAndAlignSymbols is correct when a suffix of identifiers is
 373 // shared; i.e. identifiers are [A, B, C, D] and [E, F, C, D].
 374 TEST(IntegerRelationTest, mergeAndAlignCommonSuffixSymbols) {
 375   IntegerRelation rel = parseRelationFromSet(
 376       "(x, y, z)[A, B, C, D] : (x + A - C - y + D - z >= 0)", 2);
 377   IntegerRelation otherRel = parseRelationFromSet(
 378       "(u, v, a, b)[E, F, C, D] : (E - u + v == 0, v - C - D >= 0)", 2);
 379   PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 4, 0);
 380
 381   PresburgerSpace otherSpace = PresburgerSpace::getRelationSpace(2, 2, 4, 0);
 382
 383   // Attach identifiers.
 384   int identifiers[7] = {'x', 'y', 'z', 'A', 'B', 'C', 'D'};
 385   int otherIdentifiers[6] = {'u', 'v', 'a', 'b', 'E', 'F'};
 386
 387   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 388   space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
 389   space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
 390   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 391   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 392   space.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
 393   space.setId(VarKind::Symbol, 3, Identifier(&identifiers[6]));
 394
 395   otherSpace.setId(VarKind::Domain, 0, Identifier(&otherIdentifiers[0]));
 396   otherSpace.setId(VarKind::Domain, 1, Identifier(&otherIdentifiers[1]));
 397   otherSpace.setId(VarKind::Range, 0, Identifier(&otherIdentifiers[2]));
 398   otherSpace.setId(VarKind::Range, 1, Identifier(&otherIdentifiers[3]));
 399   otherSpace.setId(VarKind::Symbol, 0, Identifier(&otherIdentifiers[4]));
 400   otherSpace.setId(VarKind::Symbol, 1, Identifier(&otherIdentifiers[5]));
 401   // Note common identifiers
 402   otherSpace.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
 403   otherSpace.setId(VarKind::Symbol, 3, Identifier(&identifiers[6]));
 404
 405   rel.setSpace(space);
 406   otherRel.setSpace(otherSpace);
 407   rel.mergeAndAlignSymbols(otherRel);
 408
 409   space = rel.getSpace();
 410   otherSpace = otherRel.getSpace();
 411
 412   // Check if merge and align is successful.
 413   // Check symbol var identifiers.
 414   EXPECT_EQ(6u, space.getNumSymbolVars());
 415   EXPECT_EQ(6u, otherSpace.getNumSymbolVars());
 416   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 417   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 418   EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&identifiers[5]));
 419   EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
 420   EXPECT_EQ(space.getId(VarKind::Symbol, 4), Identifier(&otherIdentifiers[4]));
 421   EXPECT_EQ(space.getId(VarKind::Symbol, 5), Identifier(&otherIdentifiers[5]));
 422   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 423   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 424   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 2), Identifier(&identifiers[5]));
 425   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
 426   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 4),
 427             Identifier(&otherIdentifiers[4]));
 428   EXPECT_EQ(otherSpace.getId(VarKind::Symbol, 5),
 429             Identifier(&otherIdentifiers[5]));
 430   // Check that domain and range var identifiers are not affected.
 431   EXPECT_EQ(2u, space.getNumDomainVars());
 432   EXPECT_EQ(1u, space.getNumRangeVars());
 433   EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
 434   EXPECT_EQ(space.getId(VarKind::Domain, 1), Identifier(&identifiers[1]));
 435   EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
 436   EXPECT_EQ(2u, otherSpace.getNumDomainVars());
 437   EXPECT_EQ(2u, otherSpace.getNumRangeVars());
 438   EXPECT_EQ(otherSpace.getId(VarKind::Domain, 0),
 439             Identifier(&otherIdentifiers[0]));
 440   EXPECT_EQ(otherSpace.getId(VarKind::Domain, 1),
 441             Identifier(&otherIdentifiers[1]));
 442   EXPECT_EQ(otherSpace.getId(VarKind::Range, 0),
 443             Identifier(&otherIdentifiers[2]));
 444   EXPECT_EQ(otherSpace.getId(VarKind::Range, 1),
 445             Identifier(&otherIdentifiers[3]));
 446 }
 447
 448 TEST(IntegerRelationTest, setId) {
 449   IntegerRelation rel = parseRelationFromSet(
 450       "(x, y, z)[A, B, C, D] : (x + A - C - y + D - z >= 0)", 2);
 451   PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 4, 0);
 452
 453   // Attach identifiers.
 454   int identifiers[7] = {'x', 'y', 'z', 'A', 'B', 'C', 'D'};
 455   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 456   space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
 457   space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
 458   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 459   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 460   space.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
 461   space.setId(VarKind::Symbol, 3, Identifier(&identifiers[6]));
 462   rel.setSpace(space);
 463
 464   int newIdentifiers[3] = {1, 2, 3};
 465   rel.setId(VarKind::Domain, 1, Identifier(&newIdentifiers[0]));
 466   rel.setId(VarKind::Range, 0, Identifier(&newIdentifiers[1]));
 467   rel.setId(VarKind::Symbol, 2, Identifier(&newIdentifiers[2]));
 468
 469   space = rel.getSpace();
 470   // Check that new identifiers are set correctly.
 471   EXPECT_EQ(space.getId(VarKind::Domain, 1), Identifier(&newIdentifiers[0]));
 472   EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&newIdentifiers[1]));
 473   EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&newIdentifiers[2]));
 474   // Check that old identifier are not changed.
 475   EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
 476   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 477   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 478   EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&identifiers[6]));
 479 }
 480
 481 TEST(IntegerRelationTest, convertVarKind) {
 482   PresburgerSpace space = PresburgerSpace::getSetSpace(3, 3, 0);
 483
 484   // Attach identifiers.
 485   int identifiers[6] = {0, 1, 2, 3, 4, 5};
 486   space.setId(VarKind::SetDim, 0, Identifier(&identifiers[0]));
 487   space.setId(VarKind::SetDim, 1, Identifier(&identifiers[1]));
 488   space.setId(VarKind::SetDim, 2, Identifier(&identifiers[2]));
 489   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 490   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 491   space.setId(VarKind::Symbol, 2, Identifier(&identifiers[5]));
 492
 493   // Cannot call parseIntegerRelation to test convertVarKind as
 494   // parseIntegerRelation uses convertVarKind.
 495   IntegerRelation rel = parseIntegerPolyhedron(
 496       // 0  1  2  3  4  5
 497       "(x, y, a)[U, V, W] : (x - U == 0, y + a - W == 0, U - V >= 0,"
 498       "y - a >= 0)");
 499   rel.setSpace(space);
 500
 501   // Make a few kind conversions.
 502   rel.convertVarKind(VarKind::Symbol, 1, 2, VarKind::Domain, 0);
 503   rel.convertVarKind(VarKind::Range, 2, 3, VarKind::Domain, 0);
 504   rel.convertVarKind(VarKind::Range, 0, 2, VarKind::Symbol, 1);
 505   rel.convertVarKind(VarKind::Domain, 1, 2, VarKind::Range, 0);
 506   rel.convertVarKind(VarKind::Domain, 0, 1, VarKind::Range, 1);
 507
 508   space = rel.getSpace();
 509
 510   // Expected rel.
 511   IntegerRelation expectedRel = parseIntegerPolyhedron(
 512       "(V, a)[U, x, y, W] : (x - U == 0, y + a - W == 0, U - V >= 0,"
 513       "y - a >= 0)");
 514   expectedRel.setSpace(space);
 515
 516   EXPECT_TRUE(rel.isEqual(expectedRel));
 517
 518   EXPECT_EQ(space.getId(VarKind::SetDim, 0), Identifier(&identifiers[4]));
 519   EXPECT_EQ(space.getId(VarKind::SetDim, 1), Identifier(&identifiers[2]));
 520   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 521   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[0]));
 522   EXPECT_EQ(space.getId(VarKind::Symbol, 2), Identifier(&identifiers[1]));
 523   EXPECT_EQ(space.getId(VarKind::Symbol, 3), Identifier(&identifiers[5]));
 524 }
 525
 526 TEST(IntegerRelationTest, convertVarKindToLocal) {
 527   // Convert all range variables to local variables.
 528   IntegerRelation rel = parseRelationFromSet(
 529       "(x, y, z)[N, M] : (x - y >= 0, y - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)",
 530       1);
 531   PresburgerSpace space = rel.getSpace();
 532   // Attach identifiers.
 533   char identifiers[5] = {'x', 'y', 'z', 'N', 'M'};
 534   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 535   space.setId(VarKind::Range, 0, Identifier(&identifiers[1]));
 536   space.setId(VarKind::Range, 1, Identifier(&identifiers[2]));
 537   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 538   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 539   rel.setSpace(space);
 540   rel.convertToLocal(VarKind::Range, 0, rel.getNumRangeVars());
 541   IntegerRelation expectedRel =
 542       parseRelationFromSet("(x)[N, M] : (x - N >= 0, 2 * M - 5 >= 0)", 1);
 543   EXPECT_TRUE(rel.isEqual(expectedRel));
 544   space = rel.getSpace();
 545   EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
 546   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 547   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 548
 549   // Convert all domain variables to local variables.
 550   IntegerRelation rel2 = parseRelationFromSet(
 551       "(x, y, z)[N, M] : (x - y >= 0, y - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)",
 552       2);
 553   space = rel2.getSpace();
 554   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 555   space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
 556   space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
 557   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 558   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 559   rel2.setSpace(space);
 560   rel2.convertToLocal(VarKind::Domain, 0, rel2.getNumDomainVars());
 561   expectedRel =
 562       parseIntegerPolyhedron("(z)[N, M] : (3 - z >= 0, 2 * M - 5 >= 0)");
 563   EXPECT_TRUE(rel2.isEqual(expectedRel));
 564   space = rel2.getSpace();
 565   EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
 566   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 567   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 568
 569   // Convert a prefix of range variables to local variables.
 570   IntegerRelation rel3 = parseRelationFromSet(
 571       "(x, y, z)[N, M] : (x - y >= 0, y - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)",
 572       1);
 573   space = rel3.getSpace();
 574   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 575   space.setId(VarKind::Range, 0, Identifier(&identifiers[1]));
 576   space.setId(VarKind::Range, 1, Identifier(&identifiers[2]));
 577   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 578   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 579   rel3.setSpace(space);
 580   rel3.convertToLocal(VarKind::Range, 0, 1);
 581   expectedRel = parseRelationFromSet(
 582       "(x, z)[N, M] : (x - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)", 1);
 583   EXPECT_TRUE(rel3.isEqual(expectedRel));
 584   space = rel3.getSpace();
 585   EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
 586   EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
 587   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 588   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 589
 590   // Convert a suffix of domain variables to local variables.
 591   IntegerRelation rel4 = parseRelationFromSet(
 592       "(x, y, z)[N, M] : (x - y >= 0, y - N >= 0, 3 - z >= 0, 2 * M - 5 >= 0)",
 593       2);
 594   space = rel4.getSpace();
 595   space.setId(VarKind::Domain, 0, Identifier(&identifiers[0]));
 596   space.setId(VarKind::Domain, 1, Identifier(&identifiers[1]));
 597   space.setId(VarKind::Range, 0, Identifier(&identifiers[2]));
 598   space.setId(VarKind::Symbol, 0, Identifier(&identifiers[3]));
 599   space.setId(VarKind::Symbol, 1, Identifier(&identifiers[4]));
 600   rel4.setSpace(space);
 601   rel4.convertToLocal(VarKind::Domain, rel4.getNumDomainVars() - 1,
 602                       rel4.getNumDomainVars());
 603   // expectedRel same as before.
 604   EXPECT_TRUE(rel4.isEqual(expectedRel));
 605   space = rel4.getSpace();
 606   EXPECT_EQ(space.getId(VarKind::Domain, 0), Identifier(&identifiers[0]));
 607   EXPECT_EQ(space.getId(VarKind::Range, 0), Identifier(&identifiers[2]));
 608   EXPECT_EQ(space.getId(VarKind::Symbol, 0), Identifier(&identifiers[3]));
 609   EXPECT_EQ(space.getId(VarKind::Symbol, 1), Identifier(&identifiers[4]));
 610 }