319 lines · cpp
1//===- PresburgerRelationTest.cpp - Tests for PresburgerRelation 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#include "mlir/Analysis/Presburger/PresburgerRelation.h"9#include "Parser.h"10#include "mlir/Analysis/Presburger/IntegerRelation.h"11#include "mlir/Analysis/Presburger/Simplex.h"12 13#include <gmock/gmock.h>14#include <gtest/gtest.h>15#include <iostream>16 17using namespace mlir;18using namespace presburger;19 20TEST(PresburgerRelationTest, intersectDomainAndRange) {21 {22 PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(23 {// (x, y) -> (x + N, y - N)24 "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)",25 // (x, y) -> (x + y, x - y)26 "(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0)",27 // (x, y) -> (x - y, y - x)}28 "(x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0)"},29 2);30 31 PresburgerSet set =32 parsePresburgerSet({// (2x, x)33 "(a, b)[N] : (a - 2 * b == 0)",34 // (x, -x)35 "(a, b)[N] : (a + b == 0)",36 // (N, N)37 "(a, b)[N] : (a - N == 0, b - N == 0)"});38 39 PresburgerRelation expectedRel = parsePresburgerRelationFromPresburgerSet(40 {"(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, x - 2 * y == 0)",41 "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, x + y == 0)",42 "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, x - N == 0, y - N "43 "== 0)",44 "(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, x - 2 * y == 0)",45 "(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, x + y == 0)",46 "(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, x - N == 0, y - N "47 "== 0)",48 "(x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, x - 2 * y == 0)",49 "(x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, x + y == 0)",50 "(x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, x - N == 0, y - N "51 "== 0)"},52 2);53 54 PresburgerRelation computedRel = rel.intersectDomain(set);55 EXPECT_TRUE(computedRel.isEqual(expectedRel));56 }57 58 {59 PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(60 {// (x)[N] -> (x + N, x - N)61 "(x, a, b)[N] : (a - x - N == 0, b - x + N == 0)",62 // (x)[N] -> (x, -x)63 "(x, a, b)[N] : (a - x == 0, b + x == 0)",64 // (x)[N] -> (N - x, 2 * x)}65 "(x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0)"},66 1);67 68 PresburgerSet set =69 parsePresburgerSet({// (2x, x)70 "(a, b)[N] : (a - 2 * b == 0)",71 // (x, -x)72 "(a, b)[N] : (a + b == 0)",73 // (N, N)74 "(a, b)[N] : (a - N == 0, b - N == 0)"});75 76 PresburgerRelation expectedRel = parsePresburgerRelationFromPresburgerSet(77 {"(x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a - 2 * b == 0)",78 "(x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a + b == 0)",79 "(x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a - N == 0, b - N "80 "== 0)",81 "(x, a, b)[N] : (a - x == 0, b + x == 0, a - 2 * b == 0)",82 "(x, a, b)[N] : (a - x == 0, b + x == 0, a + b == 0)",83 "(x, a, b)[N] : (a - x == 0, b + x == 0, a - N == 0, b - N "84 "== 0)",85 "(x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a - 2 * b == 0)",86 "(x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a + b == 0)",87 "(x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a - N == 0, b - N "88 "== 0)"},89 1);90 91 PresburgerRelation computedRel = rel.intersectRange(set);92 EXPECT_TRUE(computedRel.isEqual(expectedRel));93 }94}95 96TEST(PresburgerRelationTest, applyDomainAndRange) {97 {98 PresburgerRelation map1 = parsePresburgerRelationFromPresburgerSet(99 {// (x, y) -> (y, x)100 "(x, y, a, b)[N] : (y - a == 0, x - b == 0)",101 // (x, y) -> (x + N, y - N)102 "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)"},103 2);104 PresburgerRelation map2 = parsePresburgerRelationFromPresburgerSet(105 {// (x, y) -> (x - y)106 "(x, y, r)[N] : (x - y - r == 0)",107 // (x, y) -> N108 "(x, y, r)[N] : (N - r == 0)"},109 2);110 111 map1.applyDomain(map2);112 113 PresburgerRelation map3 = parsePresburgerRelationFromPresburgerSet(114 {// (y - x) -> (x, y)115 "(r, x, y)[N] : (y - x - r == 0)",116 // (x - y - 2N) -> (x, y)117 "(r, x, y)[N] : (x - y - 2 * N - r == 0)",118 // (x, y) -> N119 "(r, x, y)[N] : (N - r == 0)"},120 1);121 122 EXPECT_TRUE(map1.isEqual(map3));123 }124}125 126TEST(PresburgerRelationTest, inverse) {127 {128 PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(129 {// (x, y) -> (-y, -x)130 "(x, y, a, b)[N] : (y + a == 0, x + b == 0)",131 // (x, y) -> (x + N, y - N)132 "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)"},133 2);134 135 rel.inverse();136 137 PresburgerRelation inverseRel = parsePresburgerRelationFromPresburgerSet(138 {// (x, y) -> (-y, -x)139 "(x, y, a, b)[N] : (y + a == 0, x + b == 0)",140 // (x, y) -> (x - N, y + N)141 "(x, y, a, b)[N] : (x - N - a == 0, y + N - b == 0)"},142 2);143 144 EXPECT_TRUE(rel.isEqual(inverseRel));145 }146}147 148TEST(PresburgerRelationTest, symbolicLexOpt) {149 PresburgerRelation rel1 = parsePresburgerRelationFromPresburgerSet(150 {"(x, y)[N, M] : (x >= 0, y >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1>= 0, "151 "2 * N - x >= 0, 2 * N - y >= 0)",152 "(x, y)[N, M] : (x >= 0, y >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1>= 0, "153 "x - N >= 0, M - x >= 0, y - 2 * N >= 0, M - y >= 0)"},154 1);155 156 SymbolicLexOpt lexmin1 = rel1.findSymbolicIntegerLexMin();157 158 PWMAFunction expectedLexMin1 = parsePWMAF({159 {"(x)[N, M] : (x >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1 >= 0, "160 "2 * N - x >= 0)",161 "(x)[N, M] -> (0)"},162 {"(x)[N, M] : (x >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1 >= 0, "163 "x - 2 * N- 1 >= 0, M - x >= 0)",164 "(x)[N, M] -> (2 * N)"},165 });166 167 SymbolicLexOpt lexmax1 = rel1.findSymbolicIntegerLexMax();168 169 PWMAFunction expectedLexMax1 = parsePWMAF({170 {"(x)[N, M] : (x >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1 >= 0, "171 "N - 1 - x >= 0)",172 "(x)[N, M] -> (2 * N)"},173 {"(x)[N, M] : (x >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1 >= 0, "174 "x - N >= 0, M - x >= 0)",175 "(x)[N, M] -> (M)"},176 });177 178 EXPECT_TRUE(lexmin1.unboundedDomain.isIntegerEmpty());179 EXPECT_TRUE(lexmin1.lexopt.isEqual(expectedLexMin1));180 EXPECT_TRUE(lexmax1.unboundedDomain.isIntegerEmpty());181 EXPECT_TRUE(lexmax1.lexopt.isEqual(expectedLexMax1));182 183 PresburgerRelation rel2 = parsePresburgerRelationFromPresburgerSet(184 // x or y or z185 // lexmin = (x, 0, 1 - x)186 // lexmax = (x, 1, 1)187 {"(x, y, z) : (x >= 0, y >= 0, z >= 0, 1 - x >= 0, 1 - y >= 0, "188 "1 - z >= 0, x + y + z - 1 >= 0)",189 // (x or y) and (y or z) and (z or x)190 // lexmin = (x, 1 - x, 1)191 // lexmax = (x, 1, 1)192 "(x, y, z) : (x >= 0, y >= 0, z >= 0, 1 - x >= 0, 1 - y >= 0, "193 "1 - z >= 0, x + y - 1 >= 0, y + z - 1 >= 0, z + x - 1 >= 0)",194 // x => (not y) or (not z)195 // lexmin = (x, 0, 0)196 // lexmax = (x, 1, 1 - x)197 "(x, y, z) : (x >= 0, y >= 0, z >= 0, 1 - x >= 0, 1 - y >= 0, "198 "1 - z >= 0, 2 - x - y - z >= 0)"},199 1);200 201 SymbolicLexOpt lexmin2 = rel2.findSymbolicIntegerLexMin();202 203 PWMAFunction expectedLexMin2 =204 parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (0, 0)"}});205 206 SymbolicLexOpt lexmax2 = rel2.findSymbolicIntegerLexMax();207 208 PWMAFunction expectedLexMax2 =209 parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (1, 1)"}});210 211 EXPECT_TRUE(lexmin2.unboundedDomain.isIntegerEmpty());212 EXPECT_TRUE(lexmin2.lexopt.isEqual(expectedLexMin2));213 EXPECT_TRUE(lexmax2.unboundedDomain.isIntegerEmpty());214 EXPECT_TRUE(lexmax2.lexopt.isEqual(expectedLexMax2));215 216 PresburgerRelation rel3 = parsePresburgerRelationFromPresburgerSet(217 // (x => u or v or w) and (x or v) and (x or (not w))218 // lexmin = (x, 0, 0, 1 - x)219 // lexmax = (x, 1, 1 - x, x)220 {"(x, u, v, w) : (x >= 0, u >= 0, v >= 0, w >= 0, 1 - x >= 0, "221 "1 - u >= 0, 1 - v >= 0, 1 - w >= 0, -x + u + v + w >= 0, "222 "x + v - 1 >= 0, x - w >= 0)",223 // x => (u => (v => w)) and (x or (not v)) and (x or (not w))224 // lexmin = (x, 0, 0, x)225 // lexmax = (x, 1, x, x)226 "(x, u, v, w) : (x >= 0, u >= 0, v >= 0, w >= 0, 1 - x >= 0, "227 "1 - u >= 0, 1 - v >= 0, 1 - w >= 0, -x - u - v + w + 2 >= 0, "228 "x - v >= 0, x - w >= 0)",229 // (x or (u or (not v))) and ((not x) or ((not u) or w))230 // and (x or (not v)) and (x or (not w))231 // lexmin = (x, 0, 0, x)232 // lexmax = (x, 1, x, x)233 "(x, u, v, w) : (x >= 0, u >= 0, v >= 0, w >= 0, 1 - x >= 0, "234 "1 - u >= 0, 1 - v >= 0, 1 - w >= 0, x + u - v >= 0, x - u + w >= 0, "235 "x - v >= 0, x - w >= 0)"},236 1);237 238 SymbolicLexOpt lexmin3 = rel3.findSymbolicIntegerLexMin();239 240 PWMAFunction expectedLexMin3 =241 parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (0, 0, 0)"}});242 243 SymbolicLexOpt lexmax3 = rel3.findSymbolicIntegerLexMax();244 245 PWMAFunction expectedLexMax3 =246 parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (1, 1, x)"}});247 248 EXPECT_TRUE(lexmin3.unboundedDomain.isIntegerEmpty());249 EXPECT_TRUE(lexmin3.lexopt.isEqual(expectedLexMin3));250 EXPECT_TRUE(lexmax3.unboundedDomain.isIntegerEmpty());251 EXPECT_TRUE(lexmax3.lexopt.isEqual(expectedLexMax3));252}253 254TEST(PresburgerRelationTest, getDomainAndRangeSet) {255 PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(256 {// (x, y) -> (x + N, y - N)257 "(x, y, a, b)[N] : (a >= 0, b >= 0, N - a >= 0, N - b >= 0, x - a + N "258 "== 0, y - b - N == 0)",259 // (x, y) -> (- y, - x)260 "(x, y, a, b)[N] : (a >= 0, b >= 0, 2 * N - a >= 0, 2 * N - b >= 0, a + "261 "y == 0, b + x == 0)"},262 2);263 264 PresburgerSet domainSet = rel.getDomainSet();265 266 PresburgerSet expectedDomainSet = parsePresburgerSet(267 {"(x, y)[N] : (x + N >= 0, -x >= 0, y - N >= 0, 2 * N - y >= 0)",268 "(x, y)[N] : (x + 2 * N >= 0, -x >= 0, y + 2 * N >= 0, -y >= 0)"});269 270 EXPECT_TRUE(domainSet.isEqual(expectedDomainSet));271 272 PresburgerSet rangeSet = rel.getRangeSet();273 274 PresburgerSet expectedRangeSet = parsePresburgerSet(275 {"(x, y)[N] : (x >= 0, 2 * N - x >= 0, y >= 0, 2 * N - y >= 0)"});276 277 EXPECT_TRUE(rangeSet.isEqual(expectedRangeSet));278}279 280TEST(PresburgerRelationTest, convertVarKind) {281 PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 3, 0);282 283 IntegerRelation disj1 = parseRelationFromSet(284 "(x, y, a)[U, V, W] : (x - U == 0, y + a - W == 0,"285 "U - V >= 0, y - a >= 0)",286 2),287 disj2 = parseRelationFromSet(288 "(x, y, a)[U, V, W] : (x + y - U == 0, x - a + V == 0,"289 "V - U >= 0, y + a >= 0)",290 2);291 292 PresburgerRelation rel(disj1);293 rel.unionInPlace(disj2);294 295 // Make a few kind conversions.296 rel.convertVarKind(VarKind::Domain, 0, 1, VarKind::Range, 0);297 rel.convertVarKind(VarKind::Symbol, 1, 2, VarKind::Domain, 1);298 rel.convertVarKind(VarKind::Symbol, 0, 1, VarKind::Range, 1);299 300 // Expected rel.301 disj1.convertVarKind(VarKind::Domain, 0, 1, VarKind::Range, 0);302 disj1.convertVarKind(VarKind::Symbol, 1, 3, VarKind::Domain, 1);303 disj1.convertVarKind(VarKind::Symbol, 0, 1, VarKind::Range, 1);304 disj2.convertVarKind(VarKind::Domain, 0, 1, VarKind::Range, 0);305 disj2.convertVarKind(VarKind::Symbol, 1, 3, VarKind::Domain, 1);306 disj2.convertVarKind(VarKind::Symbol, 0, 1, VarKind::Range, 1);307 308 PresburgerRelation expectedRel(disj1);309 expectedRel.unionInPlace(disj2);310 311 // Check if var counts are correct.312 EXPECT_EQ(rel.getNumDomainVars(), 3u);313 EXPECT_EQ(rel.getNumRangeVars(), 3u);314 EXPECT_EQ(rel.getNumSymbolVars(), 0u);315 316 // Check if identifiers are transferred correctly.317 EXPECT_TRUE(expectedRel.isEqual(rel));318}319