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 
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 
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 
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 
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 
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 
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