1 //===- PresbugerParserTest.cpp - Presburger parsing unit tests --*- C++ -*-===//
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
7 //===----------------------------------------------------------------------===//
9 // This file contains tests for parsing IntegerSets to IntegerPolyhedron.
10 // The tests with invalid input check that the parser only accepts well-formed
11 // IntegerSets. The tests with well-formed input compare the returned FACs to
12 // manually constructed FACs with a PresburgerSet equality check.
14 //===----------------------------------------------------------------------===//
18 #include <gtest/gtest.h>
21 using namespace presburger
;
23 /// Construct a IntegerPolyhedron from a set of inequality, equality, and
24 /// division constraints.
25 static IntegerPolyhedron
makeFACFromConstraints(
26 unsigned dims
, unsigned syms
, ArrayRef
<SmallVector
<int64_t, 4>> ineqs
,
27 ArrayRef
<SmallVector
<int64_t, 4>> eqs
= {},
28 ArrayRef
<std::pair
<SmallVector
<int64_t, 4>, int64_t>> divs
= {}) {
29 IntegerPolyhedron
fac(ineqs
.size(), eqs
.size(), dims
+ syms
+ 1,
30 PresburgerSpace::getSetSpace(dims
, syms
, 0));
31 for (const auto &div
: divs
)
32 fac
.addLocalFloorDiv(div
.first
, div
.second
);
33 for (const auto &eq
: eqs
)
35 for (const auto &ineq
: ineqs
)
36 fac
.addInequality(ineq
);
40 /// Parses and compares the `str` to the `ex`. The equality check is performed
41 /// by using PresburgerSet::isEqual
42 static bool parseAndCompare(StringRef str
, const IntegerPolyhedron
&ex
) {
43 IntegerPolyhedron poly
= parseIntegerPolyhedron(str
);
44 return PresburgerSet(poly
).isEqual(PresburgerSet(ex
));
47 TEST(ParseFACTest
, ParseAndCompareTest
) {
48 // constant-fold addition
49 EXPECT_TRUE(parseAndCompare("() : (4 + 3 >= 0)",
50 makeFACFromConstraints(0, 0, {}, {})));
52 // constant-fold addition + multiplication
53 EXPECT_TRUE(parseAndCompare("()[a] : (4 * 3 == 10 + 2)",
54 makeFACFromConstraints(0, 1, {}, {})));
56 // constant-fold ceildiv + floordiv
57 EXPECT_TRUE(parseAndCompare("(x) : (11 ceildiv 3 == 13 floordiv 3)",
58 makeFACFromConstraints(1, 0, {}, {})));
61 EXPECT_TRUE(parseAndCompare("(x)[] : (x >= 0)",
62 makeFACFromConstraints(1, 0, {{1, 0}})));
65 EXPECT_TRUE(parseAndCompare("(x)[] : (x == 0)",
66 makeFACFromConstraints(1, 0, {}, {{1, 0}})));
68 // multiple constraints
69 EXPECT_TRUE(parseAndCompare("(x)[] : (7 * x >= 0, -7 * x + 5 >= 0)",
70 makeFACFromConstraints(1, 0, {{7, 0}, {-7, 5}})));
72 // multiplication distribution
74 parseAndCompare("(x) : (2 * x >= 2, (-7 + x * 9) * 5 >= 0)",
75 makeFACFromConstraints(1, 0, {{2, -2}, {45, -35}})));
77 // multiple dimensions
78 EXPECT_TRUE(parseAndCompare("(x,y,z)[] : (x + y - z >= 0)",
79 makeFACFromConstraints(3, 0, {{1, 1, -1, 0}})));
81 // dimensions and symbols
83 parseAndCompare("(x,y,z)[a,b] : (x + y - z + 2 * a - 15 * b >= 0)",
84 makeFACFromConstraints(3, 2, {{1, 1, -1, 2, -15, 0}})));
87 EXPECT_TRUE(parseAndCompare("()[a] : (2 * a - 4 == 0)",
88 makeFACFromConstraints(0, 1, {}, {{2, -4}})));
91 EXPECT_TRUE(parseAndCompare(
92 "(x, y) : (26 * (x floordiv 6) == y floordiv 3)",
93 makeFACFromConstraints(2, 0, {}, {{0, 0, 26, -1, 0}},
94 {{{1, 0, 0}, 6}, {{0, 1, 0, 0}, 3}})));
97 EXPECT_TRUE(parseAndCompare(
98 "(x, y) : (y - 3 * ((x + y - 13) floordiv 3) - 42 == 0)",
99 makeFACFromConstraints(2, 0, {}, {{0, 1, -3, -42}}, {{{1, 1, -13}, 3}})));
102 EXPECT_TRUE(parseAndCompare(
103 "(x, y) : (y - 3 * ((x + y - 13) ceildiv 3) - 42 == 0)",
104 makeFACFromConstraints(2, 0, {}, {{0, 1, -3, -42}}, {{{1, 1, -11}, 3}})));
107 EXPECT_TRUE(parseAndCompare(
108 "(x, y) : (y - 3 * ((x + y - 13) mod 3) - 42 == 0)",
109 makeFACFromConstraints(2, 0, {}, {{-3, -2, 9, -3}}, {{{1, 1, -13}, 3}})));
112 EXPECT_TRUE(parseAndCompare(
113 "(x, y) : (y - x floordiv 3 - y floordiv 2 == 0)",
114 makeFACFromConstraints(2, 0, {}, {{0, 1, -1, -1, 0}},
115 {{{1, 0, 0}, 3}, {{0, 1, 0, 0}, 2}})));
118 EXPECT_TRUE(parseAndCompare(
119 "(x, y) : (y - x ceildiv 3 - y ceildiv 2 == 0)",
120 makeFACFromConstraints(2, 0, {}, {{0, 1, -1, -1, 0}},
121 {{{1, 0, 2}, 3}, {{0, 1, 0, 1}, 2}})));
124 EXPECT_TRUE(parseAndCompare(
125 "(x, y) : (y - x mod 3 - y mod 2 == 0)",
126 makeFACFromConstraints(2, 0, {}, {{-1, 0, 3, 2, 0}},
127 {{{1, 0, 0}, 3}, {{0, 1, 0, 0}, 2}})));
130 EXPECT_TRUE(parseAndCompare(
131 "(x, y) : (y - (x + y floordiv 2) floordiv 3 == 0)",
132 makeFACFromConstraints(2, 0, {}, {{0, 1, 0, -1, 0}},
133 {{{0, 1, 0}, 2}, {{1, 0, 1, 0}, 3}})));
136 EXPECT_TRUE(parseAndCompare(
137 "(x, y) : (y - (x + y mod 2) mod 3 == 0)",
138 makeFACFromConstraints(2, 0, {}, {{-1, 0, 2, 3, 0}},
139 {{{0, 1, 0}, 2}, {{1, 1, -2, 0}, 3}})));
141 // nested floordiv + ceildiv + mod
142 EXPECT_TRUE(parseAndCompare(
143 "(x, y) : ((2 * x + 3 * (y floordiv 2) + x mod 7 + 1) ceildiv 3 == 42)",
144 makeFACFromConstraints(
145 2, 0, {}, {{0, 0, 0, 0, 1, -42}},
146 {{{0, 1, 0}, 2}, {{1, 0, 0, 0}, 7}, {{3, 0, 3, -7, 3}, 3}})));