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 "./Utils.h"
11 #include "mlir/Analysis/Presburger/Simplex.h"
12
13 #include <gmock/gmock.h>
14 #include <gtest/gtest.h>
15
16 using namespace mlir;
17 using namespace presburger;
18
parseRelationFromSet(StringRef set,unsigned numDomain)19 static IntegerRelation parseRelationFromSet(StringRef set, unsigned numDomain) {
20 IntegerRelation rel = parsePoly(set);
21
22 rel.convertVarKind(VarKind::SetDim, 0, numDomain, VarKind::Domain);
23
24 return rel;
25 }
26
TEST(IntegerRelationTest,getDomainAndRangeSet)27 TEST(IntegerRelationTest, getDomainAndRangeSet) {
28 IntegerRelation rel = parseRelationFromSet(
29 "(x, xr)[N] : (xr - x - 10 == 0, xr >= 0, N - xr >= 0)", 1);
30
31 IntegerPolyhedron domainSet = rel.getDomainSet();
32
33 IntegerPolyhedron expectedDomainSet =
34 parsePoly("(x)[N] : (x + 10 >= 0, N - x - 10 >= 0)");
35
36 EXPECT_TRUE(domainSet.isEqual(expectedDomainSet));
37
38 IntegerPolyhedron rangeSet = rel.getRangeSet();
39
40 IntegerPolyhedron expectedRangeSet =
41 parsePoly("(x)[N] : (x >= 0, N - x >= 0)");
42
43 EXPECT_TRUE(rangeSet.isEqual(expectedRangeSet));
44 }
45
TEST(IntegerRelationTest,inverse)46 TEST(IntegerRelationTest, inverse) {
47 IntegerRelation rel =
48 parseRelationFromSet("(x, y, z)[N, M] : (z - x - y == 0, x >= 0, N - x "
49 ">= 0, y >= 0, M - y >= 0)",
50 2);
51
52 IntegerRelation inverseRel =
53 parseRelationFromSet("(z, x, y)[N, M] : (x >= 0, N - x >= 0, y >= 0, M "
54 "- y >= 0, x + y - z == 0)",
55 1);
56
57 rel.inverse();
58
59 EXPECT_TRUE(rel.isEqual(inverseRel));
60 }
61
TEST(IntegerRelationTest,intersectDomainAndRange)62 TEST(IntegerRelationTest, intersectDomainAndRange) {
63 IntegerRelation rel = parseRelationFromSet(
64 "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
65 ">= 0, x + y + z floordiv 7 == 0)",
66 1);
67
68 {
69 IntegerPolyhedron poly = parsePoly("(x)[N, M] : (x >= 0, M - x - 1 >= 0)");
70
71 IntegerRelation expectedRel = parseRelationFromSet(
72 "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
73 ">= 0, x + y + z floordiv 7 == 0, x >= 0, M - x - 1 >= 0)",
74 1);
75
76 IntegerRelation copyRel = rel;
77 copyRel.intersectDomain(poly);
78 EXPECT_TRUE(copyRel.isEqual(expectedRel));
79 }
80
81 {
82 IntegerPolyhedron poly =
83 parsePoly("(y, z)[N, M] : (y >= 0, M - y - 1 >= 0, y + z == 0)");
84
85 IntegerRelation expectedRel = parseRelationFromSet(
86 "(x, y, z)[N, M]: (y floordiv 2 - N >= 0, z floordiv 5 - M"
87 ">= 0, x + y + z floordiv 7 == 0, y >= 0, M - y - 1 >= 0, y + z == 0)",
88 1);
89
90 IntegerRelation copyRel = rel;
91 copyRel.intersectRange(poly);
92 EXPECT_TRUE(copyRel.isEqual(expectedRel));
93 }
94 }
95
TEST(IntegerRelationTest,applyDomainAndRange)96 TEST(IntegerRelationTest, applyDomainAndRange) {
97
98 {
99 IntegerRelation map1 = parseRelationFromSet(
100 "(x, y, a, b)[N] : (a - x - N == 0, b - y + N == 0)", 2);
101 IntegerRelation map2 =
102 parseRelationFromSet("(x, y, a)[N] : (a - x - y == 0)", 2);
103
104 map1.applyRange(map2);
105
106 IntegerRelation map3 =
107 parseRelationFromSet("(x, y, a)[N] : (a - x - y == 0)", 2);
108
109 EXPECT_TRUE(map1.isEqual(map3));
110 }
111
112 {
113 IntegerRelation map1 = parseRelationFromSet(
114 "(x, y, a, b)[N] : (a - x + N == 0, b - y - N == 0)", 2);
115 IntegerRelation map2 =
116 parseRelationFromSet("(x, y, a, b)[N] : (a - N == 0, b - N == 0)", 2);
117
118 IntegerRelation map3 =
119 parseRelationFromSet("(x, y, a, b)[N] : (x - N == 0, y - N == 0)", 2);
120
121 map1.applyDomain(map2);
122
123 EXPECT_TRUE(map1.isEqual(map3));
124 }
125 }
126
TEST(IntegerRelationTest,symbolicLexmin)127 TEST(IntegerRelationTest, symbolicLexmin) {
128 SymbolicLexMin lexmin =
129 parseRelationFromSet("(a, x)[b] : (x - a >= 0, x - b >= 0)", 1)
130 .findSymbolicIntegerLexMin();
131
132 PWMAFunction expectedLexmin =
133 parsePWMAF(/*numInputs=*/2,
134 /*numOutputs=*/1,
135 {
136 {"(a)[b] : (a - b >= 0)", {{1, 0, 0}}}, // a
137 {"(a)[b] : (b - a - 1 >= 0)", {{0, 1, 0}}}, // b
138 },
139 /*numSymbols=*/1);
140 EXPECT_TRUE(lexmin.unboundedDomain.isIntegerEmpty());
141 EXPECT_TRUE(lexmin.lexmin.isEqual(expectedLexmin));
142 }
143