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