Skip to content

Commit 4db6e14

Browse files
iambrjGroverkss
iambrj
authored and
Groverkss
committed
[MLIR][Presburger] Implement composition for PresburgerRelation
This patch implements range and domain composition for PresburgerRelations Reviewed By: Groverkss Differential Revision: https://reviews.llvm.org/D154444
1 parent 7a749fe commit 4db6e14

File tree

4 files changed

+188
-0
lines changed

4 files changed

+188
-0
lines changed

‎mlir/include/mlir/Analysis/Presburger/PresburgerRelation.h

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,27 @@ class PresburgerRelation {
8383
/// Return the intersection of this set and the given set.
8484
PresburgerRelation intersect(const PresburgerRelation &set) const;
8585

86+
/// Invert the relation, i.e. swap its domain and range.
87+
///
88+
/// Formally, if `this`: A -> B then `inverse` updates `this` in-place to
89+
/// `this`: B -> A.
90+
void inverse();
91+
92+
/// Compose `this` relation with the given relation `rel` in-place.
93+
///
94+
/// Formally, if `this`: A -> B, and `rel`: B -> C, then this function updates
95+
/// `this` to `result`: A -> C where a point (a, c) belongs to `result`
96+
/// iff there exists b such that (a, b) is in `this` and, (b, c) is in rel.
97+
void compose(const PresburgerRelation &rel);
98+
99+
/// Apply the domain of given relation `rel` to `this` relation.
100+
///
101+
/// Formally, R1.applyDomain(R2) = R2.inverse().compose(R1).
102+
void applyDomain(const PresburgerRelation &rel);
103+
104+
/// Same as compose, provided for uniformity with applyDomain.
105+
void applyRange(const PresburgerRelation &rel);
106+
86107
/// Return true if the set contains the given point, and false otherwise.
87108
bool containsPoint(ArrayRef<MPInt> point) const;
88109
bool containsPoint(ArrayRef<int64_t> point) const {

‎mlir/lib/Analysis/Presburger/PresburgerRelation.cpp

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
//===----------------------------------------------------------------------===//
88

99
#include "mlir/Analysis/Presburger/PresburgerRelation.h"
10+
#include "mlir/Analysis/Presburger/IntegerRelation.h"
1011
#include "mlir/Analysis/Presburger/Simplex.h"
1112
#include "mlir/Analysis/Presburger/Utils.h"
1213
#include "llvm/ADT/STLExtras.h"
@@ -108,6 +109,47 @@ PresburgerRelation::intersect(const PresburgerRelation &set) const {
108109
return result;
109110
}
110111

112+
void PresburgerRelation::inverse() {
113+
for (IntegerRelation &cs : disjuncts)
114+
cs.inverse();
115+
116+
if (getNumDisjuncts())
117+
setSpace(getDisjunct(0).getSpaceWithoutLocals());
118+
}
119+
120+
void PresburgerRelation::compose(const PresburgerRelation &rel) {
121+
assert(getSpace().getRangeSpace().isCompatible(
122+
rel.getSpace().getDomainSpace()) &&
123+
"Range of `this` should be compatible with domain of `rel`");
124+
125+
PresburgerRelation result =
126+
PresburgerRelation::getEmpty(PresburgerSpace::getRelationSpace(
127+
getNumDomainVars(), rel.getNumRangeVars(), getNumSymbolVars()));
128+
for (const IntegerRelation &csA : disjuncts) {
129+
for (const IntegerRelation &csB : rel.disjuncts) {
130+
IntegerRelation composition = csA;
131+
composition.compose(csB);
132+
if (!composition.isEmpty())
133+
result.unionInPlace(composition);
134+
}
135+
}
136+
*this = result;
137+
}
138+
139+
void PresburgerRelation::applyDomain(const PresburgerRelation &rel) {
140+
assert(getSpace().getDomainSpace().isCompatible(
141+
rel.getSpace().getDomainSpace()) &&
142+
"Domain of `this` should be compatible with domain of `rel`");
143+
144+
inverse();
145+
compose(rel);
146+
inverse();
147+
}
148+
149+
void PresburgerRelation::applyRange(const PresburgerRelation &rel) {
150+
compose(rel);
151+
}
152+
111153
/// Return the coefficients of the ineq in `rel` specified by `idx`.
112154
/// `idx` can refer not only to an actual inequality of `rel`, but also
113155
/// to either of the inequalities that make up an equality in `rel`.

‎mlir/unittests/Analysis/Presburger/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ add_mlir_unittest(MLIRPresburgerTests
77
Parser.h
88
ParserTest.cpp
99
PresburgerSetTest.cpp
10+
PresburgerRelationTest.cpp
1011
PresburgerSpaceTest.cpp
1112
PWMAFunctionTest.cpp
1213
SimplexTest.cpp

‎mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
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+
11+
#include <gmock/gmock.h>
12+
#include <gtest/gtest.h>
13+
#include <iostream>
14+
15+
using namespace mlir;
16+
using namespace presburger;
17+
18+
static PresburgerRelation
19+
parsePresburgerRelationFromPresburgerSet(ArrayRef<StringRef> strs,
20+
unsigned numDomain) {
21+
assert(!strs.empty() && "strs should not be empty");
22+
23+
IntegerRelation rel = parseIntegerPolyhedron(strs[0]);
24+
rel.convertVarKind(VarKind::SetDim, 0, numDomain, VarKind::Domain);
25+
PresburgerRelation result(rel);
26+
for (unsigned i = 1, e = strs.size(); i < e; ++i) {
27+
rel = parseIntegerPolyhedron(strs[i]);
28+
rel.convertVarKind(VarKind::SetDim, 0, numDomain, VarKind::Domain);
29+
result.unionInPlace(rel);
30+
}
31+
return result;
32+
}
33+
34+
TEST(PresburgerRelationTest, applyDomainAndRange) {
35+
{
36+
PresburgerRelation map1 = parsePresburgerRelationFromPresburgerSet(
37+
{// (x, y) -> (x + N, y - N)
38+
"(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)",
39+
// (x, y) -> (y, x)
40+
"(x, y, a, b)[N] : (a - y == 0, b - x == 0)",
41+
// (x, y) -> (x + y, x - y)
42+
"(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0)"},
43+
2);
44+
PresburgerRelation map2 = parsePresburgerRelationFromPresburgerSet(
45+
{// (x, y) -> (x + y)
46+
"(x, y, r)[N] : (r - x - y == 0)",
47+
// (x, y) -> (N)
48+
"(x, y, r)[N] : (r - N == 0)",
49+
// (x, y) -> (y - x)
50+
"(x, y, r)[N] : (r + x - y == 0)"},
51+
2);
52+
53+
map1.applyRange(map2);
54+
55+
PresburgerRelation map3 = parsePresburgerRelationFromPresburgerSet(
56+
{
57+
// (x, y) -> (x + y)
58+
"(x, y, r)[N] : (r - x - y == 0)",
59+
// (x, y) -> (N)
60+
"(x, y, r)[N] : (r - N == 0)",
61+
// (x, y) -> (y - x - 2N)
62+
"(x, y, r)[N] : (r - y + x + 2 * N == 0)",
63+
// (x, y) -> (x - y)
64+
"(x, y, r)[N] : (r - x + y == 0)",
65+
// (x, y) -> (2x)
66+
"(x, y, r)[N] : (r - 2 * x == 0)",
67+
// (x, y) -> (-2y)
68+
"(x, y, r)[N] : (r + 2 * y == 0)",
69+
},
70+
2);
71+
72+
EXPECT_TRUE(map1.isEqual(map3));
73+
}
74+
75+
{
76+
PresburgerRelation map1 = parsePresburgerRelationFromPresburgerSet(
77+
{// (x, y) -> (y, x)
78+
"(x, y, a, b)[N] : (y - a == 0, x - b == 0)",
79+
// (x, y) -> (x + N, y - N)
80+
"(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)"},
81+
2);
82+
PresburgerRelation map2 = parsePresburgerRelationFromPresburgerSet(
83+
{// (x, y) -> (x - y)
84+
"(x, y, r)[N] : (x - y - r == 0)",
85+
// (x, y) -> N
86+
"(x, y, r)[N] : (N - r == 0)"},
87+
2);
88+
89+
map1.applyDomain(map2);
90+
91+
PresburgerRelation map3 = parsePresburgerRelationFromPresburgerSet(
92+
{// (y - x) -> (x, y)
93+
"(r, x, y)[N] : (y - x - r == 0)",
94+
// (x - y - 2N) -> (x, y)
95+
"(r, x, y)[N] : (x - y - 2 * N - r == 0)",
96+
// (x, y) -> N
97+
"(r, x, y)[N] : (N - r == 0)"},
98+
1);
99+
100+
EXPECT_TRUE(map1.isEqual(map3));
101+
}
102+
}
103+
104+
TEST(PresburgerRelationTest, inverse) {
105+
{
106+
PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(
107+
{// (x, y) -> (-y, -x)
108+
"(x, y, a, b)[N] : (y + a == 0, x + b == 0)",
109+
// (x, y) -> (x + N, y - N)
110+
"(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)"},
111+
2);
112+
113+
rel.inverse();
114+
115+
PresburgerRelation inverseRel = parsePresburgerRelationFromPresburgerSet(
116+
{// (x, y) -> (-y, -x)
117+
"(x, y, a, b)[N] : (y + a == 0, x + b == 0)",
118+
// (x, y) -> (x - N, y + N)
119+
"(x, y, a, b)[N] : (x - N - a == 0, y + N - b == 0)"},
120+
2);
121+
122+
EXPECT_TRUE(rel.isEqual(inverseRel));
123+
}
124+
}

0 commit comments

Comments
 (0)