1d5a29442SArjun P //===- PWMAFunctionTest.cpp - Tests for PWMAFunction ----------------------===//
2d5a29442SArjun P //
3d5a29442SArjun P // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4d5a29442SArjun P // See https://llvm.org/LICENSE.txt for license information.
5d5a29442SArjun P // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6d5a29442SArjun P //
7d5a29442SArjun P //===----------------------------------------------------------------------===//
8d5a29442SArjun P //
9d5a29442SArjun P // This file contains tests for PWMAFunction.
10d5a29442SArjun P //
11d5a29442SArjun P //===----------------------------------------------------------------------===//
12d5a29442SArjun P
138c867f78SGroverkss #include "Parser.h"
146472546fSArjun P
15d5a29442SArjun P #include "mlir/Analysis/Presburger/PWMAFunction.h"
16ff1d9a4bSGroverkss #include "mlir/Analysis/Presburger/PresburgerRelation.h"
176472546fSArjun P #include "mlir/IR/MLIRContext.h"
18d5a29442SArjun P
19d5a29442SArjun P #include <gmock/gmock.h>
20d5a29442SArjun P #include <gtest/gtest.h>
21d5a29442SArjun P
220c1f6865SGroverkss using namespace mlir;
230c1f6865SGroverkss using namespace presburger;
240c1f6865SGroverkss
25d5a29442SArjun P using testing::ElementsAre;
26d5a29442SArjun P
TEST(PWAFunctionTest,isEqual)27d5a29442SArjun P TEST(PWAFunctionTest, isEqual) {
28d5a29442SArjun P // The output expressions are different but it doesn't matter because they are
29d5a29442SArjun P // equal in this domain.
308c867f78SGroverkss PWMAFunction idAtZeros =
318c867f78SGroverkss parsePWMAF({{"(x, y) : (y == 0)", "(x, y) -> (x, y)"},
328c867f78SGroverkss {"(x, y) : (y - 1 >= 0, x == 0)", "(x, y) -> (x, y)"},
338c867f78SGroverkss {"(x, y) : (-y - 1 >= 0, x == 0)", "(x, y) -> (x, y)"}});
348c867f78SGroverkss PWMAFunction idAtZeros2 =
358c867f78SGroverkss parsePWMAF({{"(x, y) : (y == 0)", "(x, y) -> (x, 20*y)"},
368c867f78SGroverkss {"(x, y) : (y - 1 >= 0, x == 0)", "(x, y) -> (30*x, y)"},
378c867f78SGroverkss {"(x, y) : (-y - 1 > =0, x == 0)", "(x, y) -> (30*x, y)"}});
38d5a29442SArjun P EXPECT_TRUE(idAtZeros.isEqual(idAtZeros2));
39d5a29442SArjun P
408c867f78SGroverkss PWMAFunction notIdAtZeros = parsePWMAF({
418c867f78SGroverkss {"(x, y) : (y == 0)", "(x, y) -> (x, y)"},
428c867f78SGroverkss {"(x, y) : (y - 1 >= 0, x == 0)", "(x, y) -> (x, 2*y)"},
438c867f78SGroverkss {"(x, y) : (-y - 1 >= 0, x == 0)", "(x, y) -> (x, 2*y)"},
44d5a29442SArjun P });
45d5a29442SArjun P EXPECT_FALSE(idAtZeros.isEqual(notIdAtZeros));
46d5a29442SArjun P
47d5a29442SArjun P // These match at their intersection but one has a bigger domain.
488c867f78SGroverkss PWMAFunction idNoNegNegQuadrant =
498c867f78SGroverkss parsePWMAF({{"(x, y) : (x >= 0)", "(x, y) -> (x, y)"},
508c867f78SGroverkss {"(x, y) : (-x - 1 >= 0, y >= 0)", "(x, y) -> (x, y)"}});
518c867f78SGroverkss PWMAFunction idOnlyPosX = parsePWMAF({
528c867f78SGroverkss {"(x, y) : (x >= 0)", "(x, y) -> (x, y)"},
53d5a29442SArjun P });
54d5a29442SArjun P EXPECT_FALSE(idNoNegNegQuadrant.isEqual(idOnlyPosX));
55d5a29442SArjun P
56d5a29442SArjun P // Different representations of the same domain.
578c867f78SGroverkss PWMAFunction sumPlusOne = parsePWMAF({
588c867f78SGroverkss {"(x, y) : (x >= 0)", "(x, y) -> (x + y + 1)"},
598c867f78SGroverkss {"(x, y) : (-x - 1 >= 0, -y - 1 >= 0)", "(x, y) -> (x + y + 1)"},
608c867f78SGroverkss {"(x, y) : (-x - 1 >= 0, y >= 0)", "(x, y) -> (x + y + 1)"},
61d5a29442SArjun P });
628c867f78SGroverkss PWMAFunction sumPlusOne2 = parsePWMAF({
638c867f78SGroverkss {"(x, y) : ()", "(x, y) -> (x + y + 1)"},
64d5a29442SArjun P });
65d5a29442SArjun P EXPECT_TRUE(sumPlusOne.isEqual(sumPlusOne2));
66d5a29442SArjun P
67d5a29442SArjun P // Functions with zero input dimensions.
688c867f78SGroverkss PWMAFunction noInputs1 = parsePWMAF({
698c867f78SGroverkss {"() : ()", "() -> (1)"},
70d5a29442SArjun P });
718c867f78SGroverkss PWMAFunction noInputs2 = parsePWMAF({
728c867f78SGroverkss {"() : ()", "() -> (2)"},
73d5a29442SArjun P });
74d5a29442SArjun P EXPECT_TRUE(noInputs1.isEqual(noInputs1));
75d5a29442SArjun P EXPECT_FALSE(noInputs1.isEqual(noInputs2));
76d5a29442SArjun P
77d5a29442SArjun P // Mismatched dimensionalities.
78d5a29442SArjun P EXPECT_FALSE(noInputs1.isEqual(sumPlusOne));
79d5a29442SArjun P EXPECT_FALSE(idOnlyPosX.isEqual(sumPlusOne));
80d5a29442SArjun P
81d5a29442SArjun P // Divisions.
82d5a29442SArjun P // Domain is only multiples of 6; x = 6k for some k.
83d5a29442SArjun P // x + 4(x/2) + 4(x/3) == 26k.
848c867f78SGroverkss PWMAFunction mul2AndMul3 = parsePWMAF({
85d5a29442SArjun P {"(x) : (x - 2*(x floordiv 2) == 0, x - 3*(x floordiv 3) == 0)",
868c867f78SGroverkss "(x) -> (x + 4 * (x floordiv 2) + 4 * (x floordiv 3))"},
87d5a29442SArjun P });
888c867f78SGroverkss PWMAFunction mul6 = parsePWMAF({
898c867f78SGroverkss {"(x) : (x - 6*(x floordiv 6) == 0)", "(x) -> (26 * (x floordiv 6))"},
90d5a29442SArjun P });
91d5a29442SArjun P EXPECT_TRUE(mul2AndMul3.isEqual(mul6));
92d5a29442SArjun P
938c867f78SGroverkss PWMAFunction mul6diff = parsePWMAF({
948c867f78SGroverkss {"(x) : (x - 5*(x floordiv 5) == 0)", "(x) -> (52 * (x floordiv 6))"},
95d5a29442SArjun P });
96d5a29442SArjun P EXPECT_FALSE(mul2AndMul3.isEqual(mul6diff));
97d5a29442SArjun P
988c867f78SGroverkss PWMAFunction mul5 = parsePWMAF({
998c867f78SGroverkss {"(x) : (x - 5*(x floordiv 5) == 0)", "(x) -> (26 * (x floordiv 5))"},
100d5a29442SArjun P });
101d5a29442SArjun P EXPECT_FALSE(mul2AndMul3.isEqual(mul5));
102d5a29442SArjun P }
103d5a29442SArjun P
TEST(PWMAFunction,valueAt)104d5a29442SArjun P TEST(PWMAFunction, valueAt) {
1054418669fSArjun P PWMAFunction nonNegPWMAF = parsePWMAF(
1068c867f78SGroverkss {{"(x, y) : (x >= 0)", "(x, y) -> (x + 2*y + 3, 3*x + 4*y + 5)"},
1078c867f78SGroverkss {"(x, y) : (y >= 0, -x - 1 >= 0)",
1088c867f78SGroverkss "(x, y) -> (-x + 2*y + 3, -3*x + 4*y + 5)"}});
1094418669fSArjun P EXPECT_THAT(*nonNegPWMAF.valueAt({2, 3}), ElementsAre(11, 23));
1104418669fSArjun P EXPECT_THAT(*nonNegPWMAF.valueAt({-2, 3}), ElementsAre(11, 23));
1114418669fSArjun P EXPECT_THAT(*nonNegPWMAF.valueAt({2, -3}), ElementsAre(-1, -1));
112491d2701SKazu Hirata EXPECT_FALSE(nonNegPWMAF.valueAt({-2, -3}).has_value());
1134418669fSArjun P
1144418669fSArjun P PWMAFunction divPWMAF = parsePWMAF(
1158c867f78SGroverkss {{"(x, y) : (x >= 0, x - 2*(x floordiv 2) == 0)",
1168c867f78SGroverkss "(x, y) -> (2*y + (x floordiv 2) + 3, 4*y + 3*(x floordiv 2) + 5)"},
1178c867f78SGroverkss {"(x, y) : (y >= 0, -x - 1 >= 0)",
1188c867f78SGroverkss "(x, y) -> (-x + 2*y + 3, -3*x + 4*y + 5)"}});
1194418669fSArjun P EXPECT_THAT(*divPWMAF.valueAt({4, 3}), ElementsAre(11, 23));
1204418669fSArjun P EXPECT_THAT(*divPWMAF.valueAt({4, -3}), ElementsAre(-1, -1));
121491d2701SKazu Hirata EXPECT_FALSE(divPWMAF.valueAt({3, 3}).has_value());
122491d2701SKazu Hirata EXPECT_FALSE(divPWMAF.valueAt({3, -3}).has_value());
1234418669fSArjun P
1244418669fSArjun P EXPECT_THAT(*divPWMAF.valueAt({-2, 3}), ElementsAre(11, 23));
125491d2701SKazu Hirata EXPECT_FALSE(divPWMAF.valueAt({-2, -3}).has_value());
126d5a29442SArjun P }
1277f611249SArjun P
TEST(PWMAFunction,removeIdRangeRegressionTest)1287f611249SArjun P TEST(PWMAFunction, removeIdRangeRegressionTest) {
1298c867f78SGroverkss PWMAFunction pwmafA = parsePWMAF({
1308c867f78SGroverkss {"(x, y) : (x == 0, y == 0, x - 2*(x floordiv 2) == 0, y - 2*(y floordiv "
1318c867f78SGroverkss "2) == 0)",
1328c867f78SGroverkss "(x, y) -> (0, 0)"},
1337f611249SArjun P });
1348c867f78SGroverkss PWMAFunction pwmafB = parsePWMAF({
1357f611249SArjun P {"(x, y) : (x - 11*y == 0, 11*x - y == 0, x - 2*(x floordiv 2) == 0, "
1367f611249SArjun P "y - 2*(y floordiv 2) == 0)",
1378c867f78SGroverkss "(x, y) -> (0, 0)"},
1387f611249SArjun P });
139d81fa76fSArjun P EXPECT_TRUE(pwmafA.isEqual(pwmafB));
140d81fa76fSArjun P }
141d81fa76fSArjun P
TEST(PWMAFunction,eliminateRedundantLocalIdRegressionTest)142d81fa76fSArjun P TEST(PWMAFunction, eliminateRedundantLocalIdRegressionTest) {
1438c867f78SGroverkss PWMAFunction pwmafA = parsePWMAF({
1448c867f78SGroverkss {"(x, y) : (x - 2*(x floordiv 2) == 0, x - 2*y == 0)", "(x, y) -> (y)"},
145644dfbacSGroverkss });
1468c867f78SGroverkss PWMAFunction pwmafB = parsePWMAF({
147644dfbacSGroverkss {"(x, y) : (x - 2*(x floordiv 2) == 0, x - 2*y == 0)",
1488c867f78SGroverkss "(x, y) -> (x - y)"},
149d81fa76fSArjun P });
150d81fa76fSArjun P EXPECT_TRUE(pwmafA.isEqual(pwmafB));
1517f611249SArjun P }
152a18f843fSGroverkss
TEST(PWMAFunction,unionLexMaxSimple)153a18f843fSGroverkss TEST(PWMAFunction, unionLexMaxSimple) {
154a18f843fSGroverkss // func2 is better than func1, but func2's domain is empty.
155a18f843fSGroverkss {
1568c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
1578c867f78SGroverkss {"(x) : ()", "(x) -> (1)"},
158a18f843fSGroverkss });
159a18f843fSGroverkss
1608c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
1618c867f78SGroverkss {"(x) : (1 == 0)", "(x) -> (2)"},
162a18f843fSGroverkss });
163a18f843fSGroverkss
164a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(func1));
165a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(func1));
166a18f843fSGroverkss }
167a18f843fSGroverkss
168a18f843fSGroverkss // func2 is better than func1 on a subset of func1.
169a18f843fSGroverkss {
1708c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
1718c867f78SGroverkss {"(x) : ()", "(x) -> (1)"},
172a18f843fSGroverkss });
173a18f843fSGroverkss
1748c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
1758c867f78SGroverkss {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (2)"},
176a18f843fSGroverkss });
177a18f843fSGroverkss
1788c867f78SGroverkss PWMAFunction result = parsePWMAF({
1798c867f78SGroverkss {"(x) : (-1 - x >= 0)", "(x) -> (1)"},
1808c867f78SGroverkss {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (2)"},
1818c867f78SGroverkss {"(x) : (x - 11 >= 0)", "(x) -> (1)"},
182a18f843fSGroverkss });
183a18f843fSGroverkss
184a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
185a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result));
186a18f843fSGroverkss }
187a18f843fSGroverkss
188a18f843fSGroverkss // func1 and func2 are defined over the whole domain with different outputs.
189a18f843fSGroverkss {
1908c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
1918c867f78SGroverkss {"(x) : ()", "(x) -> (x)"},
192a18f843fSGroverkss });
193a18f843fSGroverkss
1948c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
1958c867f78SGroverkss {"(x) : ()", "(x) -> (-x)"},
196a18f843fSGroverkss });
197a18f843fSGroverkss
1988c867f78SGroverkss PWMAFunction result = parsePWMAF({
1998c867f78SGroverkss {"(x) : (x >= 0)", "(x) -> (x)"},
2008c867f78SGroverkss {"(x) : (-1 - x >= 0)", "(x) -> (-x)"},
201a18f843fSGroverkss });
202a18f843fSGroverkss
203a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
204a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result));
205a18f843fSGroverkss }
206a18f843fSGroverkss
207a18f843fSGroverkss // func1 and func2 have disjoint domains.
208a18f843fSGroverkss {
2098c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
2108c867f78SGroverkss {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (1)"},
2118c867f78SGroverkss {"(x) : (x - 71 >= 0, 80 - x >= 0)", "(x) -> (1)"},
212a18f843fSGroverkss });
213a18f843fSGroverkss
2148c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
2158c867f78SGroverkss {"(x) : (x - 20 >= 0, 41 - x >= 0)", "(x) -> (2)"},
2168c867f78SGroverkss {"(x) : (x - 101 >= 0, 120 - x >= 0)", "(x) -> (2)"},
217a18f843fSGroverkss });
218a18f843fSGroverkss
2198c867f78SGroverkss PWMAFunction result = parsePWMAF({
2208c867f78SGroverkss {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (1)"},
2218c867f78SGroverkss {"(x) : (x - 71 >= 0, 80 - x >= 0)", "(x) -> (1)"},
2228c867f78SGroverkss {"(x) : (x - 20 >= 0, 41 - x >= 0)", "(x) -> (2)"},
2238c867f78SGroverkss {"(x) : (x - 101 >= 0, 120 - x >= 0)", "(x) -> (2)"},
224a18f843fSGroverkss });
225a18f843fSGroverkss
226a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
227a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result));
228a18f843fSGroverkss }
229a18f843fSGroverkss }
230a18f843fSGroverkss
TEST(PWMAFunction,unionLexMinSimple)231a18f843fSGroverkss TEST(PWMAFunction, unionLexMinSimple) {
232a18f843fSGroverkss // func2 is better than func1, but func2's domain is empty.
233a18f843fSGroverkss {
2348c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
2358c867f78SGroverkss {"(x) : ()", "(x) -> (-1)"},
236a18f843fSGroverkss });
237a18f843fSGroverkss
2388c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
2398c867f78SGroverkss {"(x) : (1 == 0)", "(x) -> (-2)"},
240a18f843fSGroverkss });
241a18f843fSGroverkss
242a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(func1));
243a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(func1));
244a18f843fSGroverkss }
245a18f843fSGroverkss
246a18f843fSGroverkss // func2 is better than func1 on a subset of func1.
247a18f843fSGroverkss {
2488c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
2498c867f78SGroverkss {"(x) : ()", "(x) -> (-1)"},
250a18f843fSGroverkss });
251a18f843fSGroverkss
2528c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
2538c867f78SGroverkss {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (-2)"},
254a18f843fSGroverkss });
255a18f843fSGroverkss
2568c867f78SGroverkss PWMAFunction result = parsePWMAF({
2578c867f78SGroverkss {"(x) : (-1 - x >= 0)", "(x) -> (-1)"},
2588c867f78SGroverkss {"(x) : (x >= 0, 10 - x >= 0)", "(x) -> (-2)"},
2598c867f78SGroverkss {"(x) : (x - 11 >= 0)", "(x) -> (-1)"},
260a18f843fSGroverkss });
261a18f843fSGroverkss
262a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
263a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result));
264a18f843fSGroverkss }
265a18f843fSGroverkss
266a18f843fSGroverkss // func1 and func2 are defined over the whole domain with different outputs.
267a18f843fSGroverkss {
2688c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
2698c867f78SGroverkss {"(x) : ()", "(x) -> (-x)"},
270a18f843fSGroverkss });
271a18f843fSGroverkss
2728c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
2738c867f78SGroverkss {"(x) : ()", "(x) -> (x)"},
274a18f843fSGroverkss });
275a18f843fSGroverkss
2768c867f78SGroverkss PWMAFunction result = parsePWMAF({
2778c867f78SGroverkss {"(x) : (x >= 0)", "(x) -> (-x)"},
2788c867f78SGroverkss {"(x) : (-1 - x >= 0)", "(x) -> (x)"},
279a18f843fSGroverkss });
280a18f843fSGroverkss
281a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
282a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result));
283a18f843fSGroverkss }
284a18f843fSGroverkss }
285a18f843fSGroverkss
TEST(PWMAFunction,unionLexMaxComplex)286a18f843fSGroverkss TEST(PWMAFunction, unionLexMaxComplex) {
287a18f843fSGroverkss // Union of function containing 4 different pieces of output.
288a18f843fSGroverkss //
289a18f843fSGroverkss // x >= 21 --> func1 (func2 not defined)
290a18f843fSGroverkss // x <= 0 --> func2 (func1 not defined)
291a18f843fSGroverkss // 10 <= x <= 20, y > 0 --> func1 (x + y > x - y for y > 0)
292a18f843fSGroverkss // 10 <= x <= 20, y <= 0 --> func2 (x + y <= x - y for y <= 0)
293a18f843fSGroverkss {
2948c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
2958c867f78SGroverkss {"(x, y) : (x >= 10)", "(x, y) -> (x + y)"},
296a18f843fSGroverkss });
297a18f843fSGroverkss
2988c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
2998c867f78SGroverkss {"(x, y) : (x <= 20)", "(x, y) -> (x - y)"},
300a18f843fSGroverkss });
301a18f843fSGroverkss
3028c867f78SGroverkss PWMAFunction result = parsePWMAF({
3038c867f78SGroverkss {"(x, y) : (x >= 10, x <= 20, y >= 1)", "(x, y) -> (x + y)"},
3048c867f78SGroverkss {"(x, y) : (x >= 21)", "(x, y) -> (x + y)"},
3058c867f78SGroverkss {"(x, y) : (x <= 9)", "(x, y) -> (x - y)"},
3068c867f78SGroverkss {"(x, y) : (x >= 10, x <= 20, y <= 0)", "(x, y) -> (x - y)"},
3078c867f78SGroverkss });
308a18f843fSGroverkss
309a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
310a18f843fSGroverkss }
311a18f843fSGroverkss
312a18f843fSGroverkss // Functions with more than one output, with contribution from both functions.
313a18f843fSGroverkss //
314a18f843fSGroverkss // If y >= 1, func1 is better because in the first output,
315a18f843fSGroverkss // x + y (func1) > x (func2), when y >= 1
316a18f843fSGroverkss //
317a18f843fSGroverkss // If y == 0, the first output is same for both functions, so we look at the
318a18f843fSGroverkss // second output. -2x + 4 (func1) > 2x - 2 (func2) when 0 <= x <= 1, so we
319a18f843fSGroverkss // take func1 for this domain and func2 for the remaining.
320a18f843fSGroverkss {
3218c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
3228c867f78SGroverkss {"(x, y) : (x >= 0, y >= 0)", "(x, y) -> (x + y, -2*x + 4)"},
323a18f843fSGroverkss });
324a18f843fSGroverkss
3258c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
3268c867f78SGroverkss {"(x, y) : (x >= 0, y >= 0)", "(x, y) -> (x, 2*x - 2)"},
327a18f843fSGroverkss });
328a18f843fSGroverkss
3298c867f78SGroverkss PWMAFunction result = parsePWMAF({
3308c867f78SGroverkss {"(x, y) : (x >= 0, y >= 1)", "(x, y) -> (x + y, -2*x + 4)"},
3318c867f78SGroverkss {"(x, y) : (x >= 0, x <= 1, y == 0)", "(x, y) -> (x + y, -2*x + 4)"},
3328c867f78SGroverkss {"(x, y) : (x >= 2, y == 0)", "(x, y) -> (x, 2*x - 2)"},
3338c867f78SGroverkss });
334a18f843fSGroverkss
335a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
336a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result));
337a18f843fSGroverkss }
338a18f843fSGroverkss
339a18f843fSGroverkss // Function with three boolean variables `a, b, c` used to control which
340a18f843fSGroverkss // output will be taken lexicographically.
341a18f843fSGroverkss //
342a18f843fSGroverkss // a == 1 --> Take func2
343a18f843fSGroverkss // a == 0, b == 1 --> Take func1
344a18f843fSGroverkss // a == 0, b == 0, c == 1 --> Take func2
345a18f843fSGroverkss {
3468c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
347a18f843fSGroverkss {"(a, b, c) : (a >= 0, 1 - a >= 0, b >= 0, 1 - b >= 0, c "
348a18f843fSGroverkss ">= 0, 1 - c >= 0)",
3498c867f78SGroverkss "(a, b, c) -> (0, b, 0)"},
350a18f843fSGroverkss });
351a18f843fSGroverkss
3528c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
353a18f843fSGroverkss {"(a, b, c) : (a >= 0, 1 - a >= 0, b >= 0, 1 - b >= 0, c >= 0, 1 - "
354a18f843fSGroverkss "c >= 0)",
3558c867f78SGroverkss "(a, b, c) -> (a, 0, c)"},
356a18f843fSGroverkss });
357a18f843fSGroverkss
3588c867f78SGroverkss PWMAFunction result = parsePWMAF({
359a18f843fSGroverkss {"(a, b, c) : (a - 1 == 0, b >= 0, 1 - b >= 0, c >= 0, 1 - c >= 0)",
3608c867f78SGroverkss "(a, b, c) -> (a, 0, c)"},
361a18f843fSGroverkss {"(a, b, c) : (a == 0, b - 1 == 0, c >= 0, 1 - c >= 0)",
3628c867f78SGroverkss "(a, b, c) -> (0, b, 0)"},
363a18f843fSGroverkss {"(a, b, c) : (a == 0, b == 0, c >= 0, 1 - c >= 0)",
3648c867f78SGroverkss "(a, b, c) -> (a, 0, c)"},
365a18f843fSGroverkss });
366a18f843fSGroverkss
367a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
368a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result));
369a18f843fSGroverkss }
370a18f843fSGroverkss }
371a18f843fSGroverkss
TEST(PWMAFunction,unionLexMinComplex)372a18f843fSGroverkss TEST(PWMAFunction, unionLexMinComplex) {
373a18f843fSGroverkss // Regression test checking if lexicographic tiebreak produces disjoint
374a18f843fSGroverkss // domains.
375a18f843fSGroverkss //
376a18f843fSGroverkss // If x == 1, func1 is better since in the first output,
377a18f843fSGroverkss // -x (func1) is < 0 (func2) when x == 1.
378a18f843fSGroverkss //
379a18f843fSGroverkss // If x == 0, func1 and func2 both have the same first output. So we take a
380a18f843fSGroverkss // look at the second output. func2 is better since in the second output,
381a18f843fSGroverkss // y - 1 (func2) is < y (func1).
3828c867f78SGroverkss PWMAFunction func1 = parsePWMAF({
3838c867f78SGroverkss {"(x, y) : (x >= 0, x <= 1, y >= 0, y <= 1)", "(x, y) -> (-x, y)"},
384a18f843fSGroverkss });
385a18f843fSGroverkss
3868c867f78SGroverkss PWMAFunction func2 = parsePWMAF({
3878c867f78SGroverkss {"(x, y) : (x >= 0, x <= 1, y >= 0, y <= 1)", "(x, y) -> (0, y - 1)"},
388a18f843fSGroverkss });
389a18f843fSGroverkss
3908c867f78SGroverkss PWMAFunction result = parsePWMAF({
3918c867f78SGroverkss {"(x, y) : (x == 1, y >= 0, y <= 1)", "(x, y) -> (-x, y)"},
3928c867f78SGroverkss {"(x, y) : (x == 0, y >= 0, y <= 1)", "(x, y) -> (0, y - 1)"},
393a18f843fSGroverkss });
394a18f843fSGroverkss
395a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
396a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result));
397a18f843fSGroverkss }
398*94750af8SGroverkss
TEST(PWMAFunction,unionLexMinWithDivs)399*94750af8SGroverkss TEST(PWMAFunction, unionLexMinWithDivs) {
400*94750af8SGroverkss {
401*94750af8SGroverkss PWMAFunction func1 = parsePWMAF({
402*94750af8SGroverkss {"(x, y) : (x mod 5 == 0)", "(x, y) -> (x, 1)"},
403*94750af8SGroverkss });
404*94750af8SGroverkss
405*94750af8SGroverkss PWMAFunction func2 = parsePWMAF({
406*94750af8SGroverkss {"(x, y) : (x mod 7 == 0)", "(x, y) -> (x + y, 2)"},
407*94750af8SGroverkss });
408*94750af8SGroverkss
409*94750af8SGroverkss PWMAFunction result = parsePWMAF({
410*94750af8SGroverkss {"(x, y) : (x mod 5 == 0, x mod 7 >= 1)", "(x, y) -> (x, 1)"},
411*94750af8SGroverkss {"(x, y) : (x mod 7 == 0, x mod 5 >= 1)", "(x, y) -> (x + y, 2)"},
412*94750af8SGroverkss {"(x, y) : (x mod 5 == 0, x mod 7 == 0, y >= 0)", "(x, y) -> (x, 1)"},
413*94750af8SGroverkss {"(x, y) : (x mod 7 == 0, x mod 5 == 0, y <= -1)",
414*94750af8SGroverkss "(x, y) -> (x + y, 2)"},
415*94750af8SGroverkss });
416*94750af8SGroverkss
417*94750af8SGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
418*94750af8SGroverkss }
419*94750af8SGroverkss
420*94750af8SGroverkss {
421*94750af8SGroverkss PWMAFunction func1 = parsePWMAF({
422*94750af8SGroverkss {"(x) : (x >= 0, x <= 1000)", "(x) -> (x floordiv 16)"},
423*94750af8SGroverkss });
424*94750af8SGroverkss
425*94750af8SGroverkss PWMAFunction func2 = parsePWMAF({
426*94750af8SGroverkss {"(x) : (x >= 0, x <= 1000)", "(x) -> ((x + 10) floordiv 17)"},
427*94750af8SGroverkss });
428*94750af8SGroverkss
429*94750af8SGroverkss PWMAFunction result = parsePWMAF({
430*94750af8SGroverkss {"(x) : (x >= 0, x <= 1000, x floordiv 16 <= (x + 10) floordiv 17)",
431*94750af8SGroverkss "(x) -> (x floordiv 16)"},
432*94750af8SGroverkss {"(x) : (x >= 0, x <= 1000, x floordiv 16 >= (x + 10) floordiv 17 + 1)",
433*94750af8SGroverkss "(x) -> ((x + 10) floordiv 17)"},
434*94750af8SGroverkss });
435*94750af8SGroverkss
436*94750af8SGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
437*94750af8SGroverkss }
438*94750af8SGroverkss }
439