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
136472546fSArjun P #include "./Utils.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.
30d5a29442SArjun P PWMAFunction idAtZeros = parsePWMAF(
31d5a29442SArjun P /*numInputs=*/2, /*numOutputs=*/2,
32d5a29442SArjun P {
33d5a29442SArjun P {"(x, y) : (y == 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y).
34d5a29442SArjun P {"(x, y) : (y - 1 >= 0, x == 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y).
35d5a29442SArjun P {"(x, y) : (-y - 1 >= 0, x == 0)", {{1, 0, 0}, {0, 1, 0}}} // (x, y).
36d5a29442SArjun P });
37d5a29442SArjun P PWMAFunction idAtZeros2 = parsePWMAF(
38d5a29442SArjun P /*numInputs=*/2, /*numOutputs=*/2,
39d5a29442SArjun P {
40d5a29442SArjun P {"(x, y) : (y == 0)", {{1, 0, 0}, {0, 20, 0}}}, // (x, 20y).
41d5a29442SArjun P {"(x, y) : (y - 1 >= 0, x == 0)", {{30, 0, 0}, {0, 1, 0}}}, //(30x, y)
42d5a29442SArjun P {"(x, y) : (-y - 1 > =0, x == 0)", {{30, 0, 0}, {0, 1, 0}}} //(30x, y)
43d5a29442SArjun P });
44d5a29442SArjun P EXPECT_TRUE(idAtZeros.isEqual(idAtZeros2));
45d5a29442SArjun P
46d5a29442SArjun P PWMAFunction notIdAtZeros = parsePWMAF(
47d5a29442SArjun P /*numInputs=*/2, /*numOutputs=*/2,
48d5a29442SArjun P {
49d5a29442SArjun P {"(x, y) : (y == 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y).
50d5a29442SArjun P {"(x, y) : (y - 1 >= 0, x == 0)", {{1, 0, 0}, {0, 2, 0}}}, // (x, 2y)
51d5a29442SArjun P {"(x, y) : (-y - 1 >= 0, x == 0)", {{1, 0, 0}, {0, 2, 0}}}, // (x, 2y)
52d5a29442SArjun P });
53d5a29442SArjun P EXPECT_FALSE(idAtZeros.isEqual(notIdAtZeros));
54d5a29442SArjun P
55d5a29442SArjun P // These match at their intersection but one has a bigger domain.
56d5a29442SArjun P PWMAFunction idNoNegNegQuadrant = parsePWMAF(
57d5a29442SArjun P /*numInputs=*/2, /*numOutputs=*/2,
58d5a29442SArjun P {
59d5a29442SArjun P {"(x, y) : (x >= 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y).
60d5a29442SArjun P {"(x, y) : (-x - 1 >= 0, y >= 0)", {{1, 0, 0}, {0, 1, 0}}} // (x, y).
61d5a29442SArjun P });
62d5a29442SArjun P PWMAFunction idOnlyPosX =
63d5a29442SArjun P parsePWMAF(/*numInputs=*/2, /*numOutputs=*/2,
64d5a29442SArjun P {
65d5a29442SArjun P {"(x, y) : (x >= 0)", {{1, 0, 0}, {0, 1, 0}}}, // (x, y).
66d5a29442SArjun P });
67d5a29442SArjun P EXPECT_FALSE(idNoNegNegQuadrant.isEqual(idOnlyPosX));
68d5a29442SArjun P
69d5a29442SArjun P // Different representations of the same domain.
70d5a29442SArjun P PWMAFunction sumPlusOne = parsePWMAF(
71d5a29442SArjun P /*numInputs=*/2, /*numOutputs=*/1,
72d5a29442SArjun P {
73d5a29442SArjun P {"(x, y) : (x >= 0)", {{1, 1, 1}}}, // x + y + 1.
74d5a29442SArjun P {"(x, y) : (-x - 1 >= 0, -y - 1 >= 0)", {{1, 1, 1}}}, // x + y + 1.
75d5a29442SArjun P {"(x, y) : (-x - 1 >= 0, y >= 0)", {{1, 1, 1}}} // x + y + 1.
76d5a29442SArjun P });
77d5a29442SArjun P PWMAFunction sumPlusOne2 =
78d5a29442SArjun P parsePWMAF(/*numInputs=*/2, /*numOutputs=*/1,
79d5a29442SArjun P {
80d5a29442SArjun P {"(x, y) : ()", {{1, 1, 1}}}, // x + y + 1.
81d5a29442SArjun P });
82d5a29442SArjun P EXPECT_TRUE(sumPlusOne.isEqual(sumPlusOne2));
83d5a29442SArjun P
84d5a29442SArjun P // Functions with zero input dimensions.
85d5a29442SArjun P PWMAFunction noInputs1 = parsePWMAF(/*numInputs=*/0, /*numOutputs=*/1,
86d5a29442SArjun P {
87d5a29442SArjun P {"() : ()", {{1}}}, // 1.
88d5a29442SArjun P });
89d5a29442SArjun P PWMAFunction noInputs2 = parsePWMAF(/*numInputs=*/0, /*numOutputs=*/1,
90d5a29442SArjun P {
91d5a29442SArjun P {"() : ()", {{2}}}, // 1.
92d5a29442SArjun P });
93d5a29442SArjun P EXPECT_TRUE(noInputs1.isEqual(noInputs1));
94d5a29442SArjun P EXPECT_FALSE(noInputs1.isEqual(noInputs2));
95d5a29442SArjun P
96d5a29442SArjun P // Mismatched dimensionalities.
97d5a29442SArjun P EXPECT_FALSE(noInputs1.isEqual(sumPlusOne));
98d5a29442SArjun P EXPECT_FALSE(idOnlyPosX.isEqual(sumPlusOne));
99d5a29442SArjun P
100d5a29442SArjun P // Divisions.
101d5a29442SArjun P // Domain is only multiples of 6; x = 6k for some k.
102d5a29442SArjun P // x + 4(x/2) + 4(x/3) == 26k.
103d5a29442SArjun P PWMAFunction mul2AndMul3 = parsePWMAF(
104d5a29442SArjun P /*numInputs=*/1, /*numOutputs=*/1,
105d5a29442SArjun P {
106d5a29442SArjun P {"(x) : (x - 2*(x floordiv 2) == 0, x - 3*(x floordiv 3) == 0)",
107d5a29442SArjun P {{1, 4, 4, 0}}}, // x + 4(x/2) + 4(x/3).
108d5a29442SArjun P });
109d5a29442SArjun P PWMAFunction mul6 = parsePWMAF(
110d5a29442SArjun P /*numInputs=*/1, /*numOutputs=*/1,
111d5a29442SArjun P {
112d5a29442SArjun P {"(x) : (x - 6*(x floordiv 6) == 0)", {{0, 26, 0}}}, // 26(x/6).
113d5a29442SArjun P });
114d5a29442SArjun P EXPECT_TRUE(mul2AndMul3.isEqual(mul6));
115d5a29442SArjun P
116d5a29442SArjun P PWMAFunction mul6diff = parsePWMAF(
117d5a29442SArjun P /*numInputs=*/1, /*numOutputs=*/1,
118d5a29442SArjun P {
119d5a29442SArjun P {"(x) : (x - 5*(x floordiv 5) == 0)", {{0, 52, 0}}}, // 52(x/6).
120d5a29442SArjun P });
121d5a29442SArjun P EXPECT_FALSE(mul2AndMul3.isEqual(mul6diff));
122d5a29442SArjun P
123d5a29442SArjun P PWMAFunction mul5 = parsePWMAF(
124d5a29442SArjun P /*numInputs=*/1, /*numOutputs=*/1,
125d5a29442SArjun P {
126d5a29442SArjun P {"(x) : (x - 5*(x floordiv 5) == 0)", {{0, 26, 0}}}, // 26(x/5).
127d5a29442SArjun P });
128d5a29442SArjun P EXPECT_FALSE(mul2AndMul3.isEqual(mul5));
129d5a29442SArjun P }
130d5a29442SArjun P
TEST(PWMAFunction,valueAt)131d5a29442SArjun P TEST(PWMAFunction, valueAt) {
1324418669fSArjun P PWMAFunction nonNegPWMAF = parsePWMAF(
133d5a29442SArjun P /*numInputs=*/2, /*numOutputs=*/2,
134d5a29442SArjun P {
135d5a29442SArjun P {"(x, y) : (x >= 0)", {{1, 2, 3}, {3, 4, 5}}}, // (x, y).
136d5a29442SArjun P {"(x, y) : (y >= 0, -x - 1 >= 0)", {{-1, 2, 3}, {-3, 4, 5}}} // (x, y)
137d5a29442SArjun P });
1384418669fSArjun P EXPECT_THAT(*nonNegPWMAF.valueAt({2, 3}), ElementsAre(11, 23));
1394418669fSArjun P EXPECT_THAT(*nonNegPWMAF.valueAt({-2, 3}), ElementsAre(11, 23));
1404418669fSArjun P EXPECT_THAT(*nonNegPWMAF.valueAt({2, -3}), ElementsAre(-1, -1));
141*491d2701SKazu Hirata EXPECT_FALSE(nonNegPWMAF.valueAt({-2, -3}).has_value());
1424418669fSArjun P
1434418669fSArjun P PWMAFunction divPWMAF = parsePWMAF(
1444418669fSArjun P /*numInputs=*/2, /*numOutputs=*/2,
1454418669fSArjun P {
1464418669fSArjun P {"(x, y) : (x >= 0, x - 2*(x floordiv 2) == 0)",
1474418669fSArjun P {{0, 2, 1, 3}, {0, 4, 3, 5}}}, // (x, y).
1484418669fSArjun P {"(x, y) : (y >= 0, -x - 1 >= 0)", {{-1, 2, 3}, {-3, 4, 5}}} // (x, y)
1494418669fSArjun P });
1504418669fSArjun P EXPECT_THAT(*divPWMAF.valueAt({4, 3}), ElementsAre(11, 23));
1514418669fSArjun P EXPECT_THAT(*divPWMAF.valueAt({4, -3}), ElementsAre(-1, -1));
152*491d2701SKazu Hirata EXPECT_FALSE(divPWMAF.valueAt({3, 3}).has_value());
153*491d2701SKazu Hirata EXPECT_FALSE(divPWMAF.valueAt({3, -3}).has_value());
1544418669fSArjun P
1554418669fSArjun P EXPECT_THAT(*divPWMAF.valueAt({-2, 3}), ElementsAre(11, 23));
156*491d2701SKazu Hirata EXPECT_FALSE(divPWMAF.valueAt({-2, -3}).has_value());
157d5a29442SArjun P }
1587f611249SArjun P
TEST(PWMAFunction,removeIdRangeRegressionTest)1597f611249SArjun P TEST(PWMAFunction, removeIdRangeRegressionTest) {
160d81fa76fSArjun P PWMAFunction pwmafA = parsePWMAF(
1617f611249SArjun P /*numInputs=*/2, /*numOutputs=*/1,
1627f611249SArjun P {
1637f611249SArjun P {"(x, y) : (x == 0, y == 0, x - 2*(x floordiv 2) == 0, y - 2*(y "
1647f611249SArjun P "floordiv 2) == 0)",
1657f611249SArjun P {{0, 0, 0, 0, 0}}} // (0, 0)
1667f611249SArjun P });
167d81fa76fSArjun P PWMAFunction pwmafB = parsePWMAF(
1687f611249SArjun P /*numInputs=*/2, /*numOutputs=*/1,
1697f611249SArjun P {
1707f611249SArjun P {"(x, y) : (x - 11*y == 0, 11*x - y == 0, x - 2*(x floordiv 2) == 0, "
1717f611249SArjun P "y - 2*(y floordiv 2) == 0)",
1727f611249SArjun P {{0, 0, 0, 0, 0}}} // (0, 0)
1737f611249SArjun P });
174d81fa76fSArjun P EXPECT_TRUE(pwmafA.isEqual(pwmafB));
175d81fa76fSArjun P }
176d81fa76fSArjun P
TEST(PWMAFunction,eliminateRedundantLocalIdRegressionTest)177d81fa76fSArjun P TEST(PWMAFunction, eliminateRedundantLocalIdRegressionTest) {
178d81fa76fSArjun P PWMAFunction pwmafA = parsePWMAF(
179d81fa76fSArjun P /*numInputs=*/2, /*numOutputs=*/1,
180d81fa76fSArjun P {
181d81fa76fSArjun P {"(x, y) : (x - 2*(x floordiv 2) == 0, x - 2*y == 0)",
182d81fa76fSArjun P {{0, 1, 0, 0}}} // (0, 0)
183d81fa76fSArjun P });
184d81fa76fSArjun P PWMAFunction pwmafB = parsePWMAF(
185d81fa76fSArjun P /*numInputs=*/2, /*numOutputs=*/1,
186d81fa76fSArjun P {
187d81fa76fSArjun P {"(x, y) : (x - 2*(x floordiv 2) == 0, x - 2*y == 0)",
188d81fa76fSArjun P {{1, -1, 0, 0}}} // (0, 0)
189d81fa76fSArjun P });
190d81fa76fSArjun P EXPECT_TRUE(pwmafA.isEqual(pwmafB));
1917f611249SArjun P }
192a18f843fSGroverkss
TEST(PWMAFunction,unionLexMaxSimple)193a18f843fSGroverkss TEST(PWMAFunction, unionLexMaxSimple) {
194a18f843fSGroverkss // func2 is better than func1, but func2's domain is empty.
195a18f843fSGroverkss {
196a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
197a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
198a18f843fSGroverkss {
199a18f843fSGroverkss {"(x) : ()", {{0, 1}}},
200a18f843fSGroverkss });
201a18f843fSGroverkss
202a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
203a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
204a18f843fSGroverkss {
205a18f843fSGroverkss {"(x) : (1 == 0)", {{0, 2}}},
206a18f843fSGroverkss });
207a18f843fSGroverkss
208a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(func1));
209a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(func1));
210a18f843fSGroverkss }
211a18f843fSGroverkss
212a18f843fSGroverkss // func2 is better than func1 on a subset of func1.
213a18f843fSGroverkss {
214a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
215a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
216a18f843fSGroverkss {
217a18f843fSGroverkss {"(x) : ()", {{0, 1}}},
218a18f843fSGroverkss });
219a18f843fSGroverkss
220a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
221a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
222a18f843fSGroverkss {
223a18f843fSGroverkss {"(x) : (x >= 0, 10 - x >= 0)", {{0, 2}}},
224a18f843fSGroverkss });
225a18f843fSGroverkss
226a18f843fSGroverkss PWMAFunction result = parsePWMAF(
227a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
228a18f843fSGroverkss {
229a18f843fSGroverkss {"(x) : (-1 - x >= 0)", {{0, 1}}},
230a18f843fSGroverkss {"(x) : (x >= 0, 10 - x >= 0)", {{0, 2}}},
231a18f843fSGroverkss {"(x) : (x - 11 >= 0)", {{0, 1}}},
232a18f843fSGroverkss });
233a18f843fSGroverkss
234a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
235a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result));
236a18f843fSGroverkss }
237a18f843fSGroverkss
238a18f843fSGroverkss // func1 and func2 are defined over the whole domain with different outputs.
239a18f843fSGroverkss {
240a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
241a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
242a18f843fSGroverkss {
243a18f843fSGroverkss {"(x) : ()", {{1, 0}}},
244a18f843fSGroverkss });
245a18f843fSGroverkss
246a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
247a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
248a18f843fSGroverkss {
249a18f843fSGroverkss {"(x) : ()", {{-1, 0}}},
250a18f843fSGroverkss });
251a18f843fSGroverkss
252a18f843fSGroverkss PWMAFunction result = parsePWMAF(
253a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
254a18f843fSGroverkss {
255a18f843fSGroverkss {"(x) : (x >= 0)", {{1, 0}}},
256a18f843fSGroverkss {"(x) : (-1 - x >= 0)", {{-1, 0}}},
257a18f843fSGroverkss });
258a18f843fSGroverkss
259a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
260a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result));
261a18f843fSGroverkss }
262a18f843fSGroverkss
263a18f843fSGroverkss // func1 and func2 have disjoint domains.
264a18f843fSGroverkss {
265a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
266a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
267a18f843fSGroverkss {
268a18f843fSGroverkss {"(x) : (x >= 0, 10 - x >= 0)", {{0, 1}}},
269a18f843fSGroverkss {"(x) : (x - 71 >= 0, 80 - x >= 0)", {{0, 1}}},
270a18f843fSGroverkss });
271a18f843fSGroverkss
272a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
273a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
274a18f843fSGroverkss {
275a18f843fSGroverkss {"(x) : (x - 20 >= 0, 41 - x >= 0)", {{0, 2}}},
276a18f843fSGroverkss {"(x) : (x - 101 >= 0, 120 - x >= 0)", {{0, 2}}},
277a18f843fSGroverkss });
278a18f843fSGroverkss
279a18f843fSGroverkss PWMAFunction result = parsePWMAF(
280a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
281a18f843fSGroverkss {
282a18f843fSGroverkss {"(x) : (x >= 0, 10 - x >= 0)", {{0, 1}}},
283a18f843fSGroverkss {"(x) : (x - 71 >= 0, 80 - x >= 0)", {{0, 1}}},
284a18f843fSGroverkss {"(x) : (x - 20 >= 0, 41 - x >= 0)", {{0, 2}}},
285a18f843fSGroverkss {"(x) : (x - 101 >= 0, 120 - x >= 0)", {{0, 2}}},
286a18f843fSGroverkss });
287a18f843fSGroverkss
288a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
289a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result));
290a18f843fSGroverkss }
291a18f843fSGroverkss }
292a18f843fSGroverkss
TEST(PWMAFunction,unionLexMinSimple)293a18f843fSGroverkss TEST(PWMAFunction, unionLexMinSimple) {
294a18f843fSGroverkss // func2 is better than func1, but func2's domain is empty.
295a18f843fSGroverkss {
296a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
297a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
298a18f843fSGroverkss {
299a18f843fSGroverkss {"(x) : ()", {{0, -1}}},
300a18f843fSGroverkss });
301a18f843fSGroverkss
302a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
303a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
304a18f843fSGroverkss {
305a18f843fSGroverkss {"(x) : (1 == 0)", {{0, -2}}},
306a18f843fSGroverkss });
307a18f843fSGroverkss
308a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(func1));
309a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(func1));
310a18f843fSGroverkss }
311a18f843fSGroverkss
312a18f843fSGroverkss // func2 is better than func1 on a subset of func1.
313a18f843fSGroverkss {
314a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
315a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
316a18f843fSGroverkss {
317a18f843fSGroverkss {"(x) : ()", {{0, -1}}},
318a18f843fSGroverkss });
319a18f843fSGroverkss
320a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
321a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
322a18f843fSGroverkss {
323a18f843fSGroverkss {"(x) : (x >= 0, 10 - x >= 0)", {{0, -2}}},
324a18f843fSGroverkss });
325a18f843fSGroverkss
326a18f843fSGroverkss PWMAFunction result = parsePWMAF(
327a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
328a18f843fSGroverkss {
329a18f843fSGroverkss {"(x) : (-1 - x >= 0)", {{0, -1}}},
330a18f843fSGroverkss {"(x) : (x >= 0, 10 - x >= 0)", {{0, -2}}},
331a18f843fSGroverkss {"(x) : (x - 11 >= 0)", {{0, -1}}},
332a18f843fSGroverkss });
333a18f843fSGroverkss
334a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
335a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result));
336a18f843fSGroverkss }
337a18f843fSGroverkss
338a18f843fSGroverkss // func1 and func2 are defined over the whole domain with different outputs.
339a18f843fSGroverkss {
340a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
341a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
342a18f843fSGroverkss {
343a18f843fSGroverkss {"(x) : ()", {{-1, 0}}},
344a18f843fSGroverkss });
345a18f843fSGroverkss
346a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
347a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
348a18f843fSGroverkss {
349a18f843fSGroverkss {"(x) : ()", {{1, 0}}},
350a18f843fSGroverkss });
351a18f843fSGroverkss
352a18f843fSGroverkss PWMAFunction result = parsePWMAF(
353a18f843fSGroverkss /*numInputs=*/1, /*numOutputs=*/1,
354a18f843fSGroverkss {
355a18f843fSGroverkss {"(x) : (x >= 0)", {{-1, 0}}},
356a18f843fSGroverkss {"(x) : (-1 - x >= 0)", {{1, 0}}},
357a18f843fSGroverkss });
358a18f843fSGroverkss
359a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
360a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result));
361a18f843fSGroverkss }
362a18f843fSGroverkss }
363a18f843fSGroverkss
TEST(PWMAFunction,unionLexMaxComplex)364a18f843fSGroverkss TEST(PWMAFunction, unionLexMaxComplex) {
365a18f843fSGroverkss // Union of function containing 4 different pieces of output.
366a18f843fSGroverkss //
367a18f843fSGroverkss // x >= 21 --> func1 (func2 not defined)
368a18f843fSGroverkss // x <= 0 --> func2 (func1 not defined)
369a18f843fSGroverkss // 10 <= x <= 20, y > 0 --> func1 (x + y > x - y for y > 0)
370a18f843fSGroverkss // 10 <= x <= 20, y <= 0 --> func2 (x + y <= x - y for y <= 0)
371a18f843fSGroverkss {
372a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
373a18f843fSGroverkss /*numInputs=*/2, /*numOutputs=*/1,
374a18f843fSGroverkss {
375a18f843fSGroverkss {"(x, y) : (x >= 10)", {{1, 1, 0}}},
376a18f843fSGroverkss });
377a18f843fSGroverkss
378a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
379a18f843fSGroverkss /*numInputs=*/2, /*numOutputs=*/1,
380a18f843fSGroverkss {
381a18f843fSGroverkss {"(x, y) : (x <= 20)", {{1, -1, 0}}},
382a18f843fSGroverkss });
383a18f843fSGroverkss
384a18f843fSGroverkss PWMAFunction result = parsePWMAF(/*numInputs=*/2, /*numOutputs=*/1,
385a18f843fSGroverkss {{"(x, y) : (x >= 10, x <= 20, y >= 1)",
386a18f843fSGroverkss {
387a18f843fSGroverkss {1, 1, 0},
388a18f843fSGroverkss }},
389a18f843fSGroverkss {"(x, y) : (x >= 21)",
390a18f843fSGroverkss {
391a18f843fSGroverkss {1, 1, 0},
392a18f843fSGroverkss }},
393a18f843fSGroverkss {"(x, y) : (x <= 9)",
394a18f843fSGroverkss {
395a18f843fSGroverkss {1, -1, 0},
396a18f843fSGroverkss }},
397a18f843fSGroverkss {"(x, y) : (x >= 10, x <= 20, y <= 0)",
398a18f843fSGroverkss {
399a18f843fSGroverkss {1, -1, 0},
400a18f843fSGroverkss }}});
401a18f843fSGroverkss
402a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
403a18f843fSGroverkss }
404a18f843fSGroverkss
405a18f843fSGroverkss // Functions with more than one output, with contribution from both functions.
406a18f843fSGroverkss //
407a18f843fSGroverkss // If y >= 1, func1 is better because in the first output,
408a18f843fSGroverkss // x + y (func1) > x (func2), when y >= 1
409a18f843fSGroverkss //
410a18f843fSGroverkss // If y == 0, the first output is same for both functions, so we look at the
411a18f843fSGroverkss // second output. -2x + 4 (func1) > 2x - 2 (func2) when 0 <= x <= 1, so we
412a18f843fSGroverkss // take func1 for this domain and func2 for the remaining.
413a18f843fSGroverkss {
414a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
415a18f843fSGroverkss /*numInputs=*/2, /*numOutputs=*/2,
416a18f843fSGroverkss {
417a18f843fSGroverkss {"(x, y) : (x >= 0, y >= 0)", {{1, 1, 0}, {-2, 0, 4}}},
418a18f843fSGroverkss });
419a18f843fSGroverkss
420a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
421a18f843fSGroverkss /*numInputs=*/2, /*numOutputs=*/2,
422a18f843fSGroverkss {
423a18f843fSGroverkss {"(x, y) : (x >= 0, y >= 0)", {{1, 0, 0}, {2, 0, -2}}},
424a18f843fSGroverkss });
425a18f843fSGroverkss
426a18f843fSGroverkss PWMAFunction result = parsePWMAF(/*numInputs=*/2, /*numOutputs=*/2,
427a18f843fSGroverkss {{"(x, y) : (x >= 0, y >= 1)",
428a18f843fSGroverkss {
429a18f843fSGroverkss {1, 1, 0},
430a18f843fSGroverkss {-2, 0, 4},
431a18f843fSGroverkss }},
432a18f843fSGroverkss {"(x, y) : (x >= 0, x <= 1, y == 0)",
433a18f843fSGroverkss {
434a18f843fSGroverkss {1, 1, 0},
435a18f843fSGroverkss {-2, 0, 4},
436a18f843fSGroverkss }},
437a18f843fSGroverkss {"(x, y) : (x >= 2, y == 0)",
438a18f843fSGroverkss {
439a18f843fSGroverkss {1, 0, 0},
440a18f843fSGroverkss {2, 0, -2},
441a18f843fSGroverkss }}});
442a18f843fSGroverkss
443a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
444a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result));
445a18f843fSGroverkss }
446a18f843fSGroverkss
447a18f843fSGroverkss // Function with three boolean variables `a, b, c` used to control which
448a18f843fSGroverkss // output will be taken lexicographically.
449a18f843fSGroverkss //
450a18f843fSGroverkss // a == 1 --> Take func2
451a18f843fSGroverkss // a == 0, b == 1 --> Take func1
452a18f843fSGroverkss // a == 0, b == 0, c == 1 --> Take func2
453a18f843fSGroverkss {
454a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
455a18f843fSGroverkss /*numInputs=*/3, /*numOutputs=*/3,
456a18f843fSGroverkss {
457a18f843fSGroverkss {"(a, b, c) : (a >= 0, 1 - a >= 0, b >= 0, 1 - b >= 0, c "
458a18f843fSGroverkss ">= 0, 1 - c >= 0)",
459a18f843fSGroverkss {{0, 0, 0, 0}, {0, 1, 0, 0}, {0, 0, 0, 0}}},
460a18f843fSGroverkss });
461a18f843fSGroverkss
462a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
463a18f843fSGroverkss /*numInputs=*/3, /*numOutputs=*/3,
464a18f843fSGroverkss {
465a18f843fSGroverkss {"(a, b, c) : (a >= 0, 1 - a >= 0, b >= 0, 1 - b >= 0, c >= 0, 1 - "
466a18f843fSGroverkss "c >= 0)",
467a18f843fSGroverkss {{1, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 1, 0}}},
468a18f843fSGroverkss });
469a18f843fSGroverkss
470a18f843fSGroverkss PWMAFunction result = parsePWMAF(
471a18f843fSGroverkss /*numInputs=*/3, /*numOutputs=*/3,
472a18f843fSGroverkss {
473a18f843fSGroverkss {"(a, b, c) : (a - 1 == 0, b >= 0, 1 - b >= 0, c >= 0, 1 - c >= 0)",
474a18f843fSGroverkss {{1, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 1, 0}}},
475a18f843fSGroverkss {"(a, b, c) : (a == 0, b - 1 == 0, c >= 0, 1 - c >= 0)",
476a18f843fSGroverkss {{0, 0, 0, 0}, {0, 1, 0, 0}, {0, 0, 0, 0}}},
477a18f843fSGroverkss {"(a, b, c) : (a == 0, b == 0, c >= 0, 1 - c >= 0)",
478a18f843fSGroverkss {{1, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 1, 0}}},
479a18f843fSGroverkss });
480a18f843fSGroverkss
481a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMax(func2).isEqual(result));
482a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMax(func1).isEqual(result));
483a18f843fSGroverkss }
484a18f843fSGroverkss }
485a18f843fSGroverkss
TEST(PWMAFunction,unionLexMinComplex)486a18f843fSGroverkss TEST(PWMAFunction, unionLexMinComplex) {
487a18f843fSGroverkss // Regression test checking if lexicographic tiebreak produces disjoint
488a18f843fSGroverkss // domains.
489a18f843fSGroverkss //
490a18f843fSGroverkss // If x == 1, func1 is better since in the first output,
491a18f843fSGroverkss // -x (func1) is < 0 (func2) when x == 1.
492a18f843fSGroverkss //
493a18f843fSGroverkss // If x == 0, func1 and func2 both have the same first output. So we take a
494a18f843fSGroverkss // look at the second output. func2 is better since in the second output,
495a18f843fSGroverkss // y - 1 (func2) is < y (func1).
496a18f843fSGroverkss PWMAFunction func1 = parsePWMAF(
497a18f843fSGroverkss /*numInputs=*/2, /*numOutputs=*/2,
498a18f843fSGroverkss {
499a18f843fSGroverkss {"(x, y) : (x >= 0, x <= 1, y >= 0, y <= 1)",
500a18f843fSGroverkss {{-1, 0, 0}, {0, 1, 0}}},
501a18f843fSGroverkss });
502a18f843fSGroverkss
503a18f843fSGroverkss PWMAFunction func2 = parsePWMAF(
504a18f843fSGroverkss /*numInputs=*/2, /*numOutputs=*/2,
505a18f843fSGroverkss {
506a18f843fSGroverkss {"(x, y) : (x >= 0, x <= 1, y >= 0, y <= 1)",
507a18f843fSGroverkss {{0, 0, 0}, {0, 1, -1}}},
508a18f843fSGroverkss });
509a18f843fSGroverkss
510a18f843fSGroverkss PWMAFunction result = parsePWMAF(
511a18f843fSGroverkss /*numInputs=*/2, /*numOutputs=*/2,
512a18f843fSGroverkss {
513a18f843fSGroverkss {"(x, y) : (x == 1, y >= 0, y <= 1)", {{-1, 0, 0}, {0, 1, 0}}},
514a18f843fSGroverkss {"(x, y) : (x == 0, y >= 0, y <= 1)", {{0, 0, 0}, {0, 1, -1}}},
515a18f843fSGroverkss });
516a18f843fSGroverkss
517a18f843fSGroverkss EXPECT_TRUE(func1.unionLexMin(func2).isEqual(result));
518a18f843fSGroverkss EXPECT_TRUE(func2.unionLexMin(func1).isEqual(result));
519a18f843fSGroverkss }
520