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