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-exception
6//
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 strs: {// (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 numDomain: 2);
30
31 PresburgerSet set =
32 parsePresburgerSet(strs: {// (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 strs: {"(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 numDomain: 2);
53
54 PresburgerRelation computedRel = rel.intersectDomain(set);
55 EXPECT_TRUE(computedRel.isEqual(expectedRel));
56 }
57
58 {
59 PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(
60 strs: {// (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 numDomain: 1);
67
68 PresburgerSet set =
69 parsePresburgerSet(strs: {// (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 strs: {"(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 numDomain: 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 strs: {// (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 numDomain: 2);
104 PresburgerRelation map2 = parsePresburgerRelationFromPresburgerSet(
105 strs: {// (x, y) -> (x - y)
106 "(x, y, r)[N] : (x - y - r == 0)",
107 // (x, y) -> N
108 "(x, y, r)[N] : (N - r == 0)"},
109 numDomain: 2);
110
111 map1.applyDomain(rel: map2);
112
113 PresburgerRelation map3 = parsePresburgerRelationFromPresburgerSet(
114 strs: {// (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) -> N
119 "(r, x, y)[N] : (N - r == 0)"},
120 numDomain: 1);
121
122 EXPECT_TRUE(map1.isEqual(map3));
123 }
124}
125
126TEST(PresburgerRelationTest, inverse) {
127 {
128 PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(
129 strs: {// (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 numDomain: 2);
134
135 rel.inverse();
136
137 PresburgerRelation inverseRel = parsePresburgerRelationFromPresburgerSet(
138 strs: {// (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 numDomain: 2);
143
144 EXPECT_TRUE(rel.isEqual(inverseRel));
145 }
146}
147
148TEST(PresburgerRelationTest, symbolicLexOpt) {
149 PresburgerRelation rel1 = parsePresburgerRelationFromPresburgerSet(
150 strs: {"(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 numDomain: 1);
155
156 SymbolicLexOpt lexmin1 = rel1.findSymbolicIntegerLexMin();
157
158 PWMAFunction expectedLexMin1 = parsePWMAF(pieces: {
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(pieces: {
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 z
185 // lexmin = (x, 0, 1 - x)
186 // lexmax = (x, 1, 1)
187 strs: {"(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 numDomain: 1);
200
201 SymbolicLexOpt lexmin2 = rel2.findSymbolicIntegerLexMin();
202
203 PWMAFunction expectedLexMin2 =
204 parsePWMAF(pieces: {{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (0, 0)"}});
205
206 SymbolicLexOpt lexmax2 = rel2.findSymbolicIntegerLexMax();
207
208 PWMAFunction expectedLexMax2 =
209 parsePWMAF(pieces: {{"(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 strs: {"(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 numDomain: 1);
237
238 SymbolicLexOpt lexmin3 = rel3.findSymbolicIntegerLexMin();
239
240 PWMAFunction expectedLexMin3 =
241 parsePWMAF(pieces: {{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (0, 0, 0)"}});
242
243 SymbolicLexOpt lexmax3 = rel3.findSymbolicIntegerLexMax();
244
245 PWMAFunction expectedLexMax3 =
246 parsePWMAF(pieces: {{"(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 strs: {// (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 numDomain: 2);
263
264 PresburgerSet domainSet = rel.getDomainSet();
265
266 PresburgerSet expectedDomainSet = parsePresburgerSet(
267 strs: {"(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 strs: {"(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(numDomain: 2, numRange: 1, numSymbols: 3, numLocals: 0);
282
283 IntegerRelation disj1 = parseRelationFromSet(
284 set: "(x, y, a)[U, V, W] : (x - U == 0, y + a - W == 0,"
285 "U - V >= 0, y - a >= 0)",
286 numDomain: 2),
287 disj2 = parseRelationFromSet(
288 set: "(x, y, a)[U, V, W] : (x + y - U == 0, x - a + V == 0,"
289 "V - U >= 0, y + a >= 0)",
290 numDomain: 2);
291
292 PresburgerRelation rel(disj1);
293 rel.unionInPlace(disjunct: disj2);
294
295 // Make a few kind conversions.
296 rel.convertVarKind(srcKind: VarKind::Domain, srcPos: 0, num: 1, dstKind: VarKind::Range, dstPos: 0);
297 rel.convertVarKind(srcKind: VarKind::Symbol, srcPos: 1, num: 2, dstKind: VarKind::Domain, dstPos: 1);
298 rel.convertVarKind(srcKind: VarKind::Symbol, srcPos: 0, num: 1, dstKind: VarKind::Range, dstPos: 1);
299
300 // Expected rel.
301 disj1.convertVarKind(srcKind: VarKind::Domain, varStart: 0, varLimit: 1, dstKind: VarKind::Range, pos: 0);
302 disj1.convertVarKind(srcKind: VarKind::Symbol, varStart: 1, varLimit: 3, dstKind: VarKind::Domain, pos: 1);
303 disj1.convertVarKind(srcKind: VarKind::Symbol, varStart: 0, varLimit: 1, dstKind: VarKind::Range, pos: 1);
304 disj2.convertVarKind(srcKind: VarKind::Domain, varStart: 0, varLimit: 1, dstKind: VarKind::Range, pos: 0);
305 disj2.convertVarKind(srcKind: VarKind::Symbol, varStart: 1, varLimit: 3, dstKind: VarKind::Domain, pos: 1);
306 disj2.convertVarKind(srcKind: VarKind::Symbol, varStart: 0, varLimit: 1, dstKind: VarKind::Range, pos: 1);
307
308 PresburgerRelation expectedRel(disj1);
309 expectedRel.unionInPlace(disjunct: 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

source code of mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp