1 | //===- PresbugerParserTest.cpp - Presburger parsing unit tests --*- C++ -*-===// |
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 | // 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. |
13 | // |
14 | //===----------------------------------------------------------------------===// |
15 | |
16 | #include "Parser.h" |
17 | |
18 | #include <gtest/gtest.h> |
19 | |
20 | using namespace mlir; |
21 | using namespace presburger; |
22 | |
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(numDims: dims, numSymbols: syms, numLocals: 0)); |
31 | for (const auto &div : divs) |
32 | fac.addLocalFloorDiv(dividend: div.first, divisor: div.second); |
33 | for (const auto &eq : eqs) |
34 | fac.addEquality(eq); |
35 | for (const auto &ineq : ineqs) |
36 | fac.addInequality(inEq: ineq); |
37 | return fac; |
38 | } |
39 | |
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(set: PresburgerSet(ex)); |
45 | } |
46 | |
47 | TEST(ParseFACTest, ParseAndCompareTest) { |
48 | // constant-fold addition |
49 | EXPECT_TRUE(parseAndCompare("() : (4 + 3 >= 0)" , |
50 | makeFACFromConstraints(0, 0, {}, {}))); |
51 | |
52 | // constant-fold addition + multiplication |
53 | EXPECT_TRUE(parseAndCompare("()[a] : (4 * 3 == 10 + 2)" , |
54 | makeFACFromConstraints(0, 1, {}, {}))); |
55 | |
56 | // constant-fold ceildiv + floordiv |
57 | EXPECT_TRUE(parseAndCompare("(x) : (11 ceildiv 3 == 13 floordiv 3)" , |
58 | makeFACFromConstraints(1, 0, {}, {}))); |
59 | |
60 | // simple ineq |
61 | EXPECT_TRUE(parseAndCompare("(x)[] : (x >= 0)" , |
62 | makeFACFromConstraints(1, 0, {{1, 0}}))); |
63 | |
64 | // simple eq |
65 | EXPECT_TRUE(parseAndCompare("(x)[] : (x == 0)" , |
66 | makeFACFromConstraints(1, 0, {}, {{1, 0}}))); |
67 | |
68 | // multiple constraints |
69 | EXPECT_TRUE(parseAndCompare("(x)[] : (7 * x >= 0, -7 * x + 5 >= 0)" , |
70 | makeFACFromConstraints(1, 0, {{7, 0}, {-7, 5}}))); |
71 | |
72 | // multiplication distribution |
73 | EXPECT_TRUE( |
74 | parseAndCompare("(x) : (2 * x >= 2, (-7 + x * 9) * 5 >= 0)" , |
75 | makeFACFromConstraints(1, 0, {{2, -2}, {45, -35}}))); |
76 | |
77 | // multiple dimensions |
78 | EXPECT_TRUE(parseAndCompare("(x,y,z)[] : (x + y - z >= 0)" , |
79 | makeFACFromConstraints(3, 0, {{1, 1, -1, 0}}))); |
80 | |
81 | // dimensions and symbols |
82 | EXPECT_TRUE( |
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}}))); |
85 | |
86 | // only symbols |
87 | EXPECT_TRUE(parseAndCompare("()[a] : (2 * a - 4 == 0)" , |
88 | makeFACFromConstraints(0, 1, {}, {{2, -4}}))); |
89 | |
90 | // no linear terms |
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}}))); |
95 | |
96 | // simple floordiv |
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}}))); |
100 | |
101 | // simple ceildiv |
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}}))); |
105 | |
106 | // simple mod |
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}}))); |
110 | |
111 | // multiple floordiv |
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}}))); |
116 | |
117 | // multiple ceildiv |
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}}))); |
122 | |
123 | // multiple mod |
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}}))); |
128 | |
129 | // nested floordiv |
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}}))); |
134 | |
135 | // nested mod |
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}}))); |
140 | |
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}}))); |
147 | } |
148 | |