1 //===- AffineStructuresTest.cpp - Tests for AffineStructures ----*- 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 #include "mlir/Analysis/AffineStructures.h"
10 #include "mlir/IR/IntegerSet.h"
11 #include "mlir/IR/MLIRContext.h"
12 
13 #include <gmock/gmock.h>
14 #include <gtest/gtest.h>
15 
16 #include <numeric>
17 
18 namespace mlir {
19 
20 using testing::ElementsAre;
21 
22 enum class TestFunction { Sample, Empty };
23 
24 /// If fn is TestFunction::Sample (default):
25 /// If hasSample is true, check that findIntegerSample returns a valid sample
26 /// for the FlatAffineConstraints fac.
27 /// If hasSample is false, check that findIntegerSample returns None.
28 ///
29 /// If fn is TestFunction::Empty, check that isIntegerEmpty returns the
30 /// opposite of hasSample.
checkSample(bool hasSample,const FlatAffineConstraints & fac,TestFunction fn=TestFunction::Sample)31 static void checkSample(bool hasSample, const FlatAffineConstraints &fac,
32                         TestFunction fn = TestFunction::Sample) {
33   Optional<SmallVector<int64_t, 8>> maybeSample;
34   switch (fn) {
35   case TestFunction::Sample:
36     maybeSample = fac.findIntegerSample();
37     if (!hasSample) {
38       EXPECT_FALSE(maybeSample.hasValue());
39       if (maybeSample.hasValue()) {
40         for (auto x : *maybeSample)
41           llvm::errs() << x << ' ';
42         llvm::errs() << '\n';
43       }
44     } else {
45       ASSERT_TRUE(maybeSample.hasValue());
46       EXPECT_TRUE(fac.containsPoint(*maybeSample));
47     }
48     break;
49   case TestFunction::Empty:
50     EXPECT_EQ(!hasSample, fac.isIntegerEmpty());
51     break;
52   }
53 }
54 
55 /// Construct a FlatAffineConstraints from a set of inequality and
56 /// equality constraints.
57 static FlatAffineConstraints
makeFACFromConstraints(unsigned ids,ArrayRef<SmallVector<int64_t,4>> ineqs,ArrayRef<SmallVector<int64_t,4>> eqs,unsigned syms=0)58 makeFACFromConstraints(unsigned ids, ArrayRef<SmallVector<int64_t, 4>> ineqs,
59                        ArrayRef<SmallVector<int64_t, 4>> eqs,
60                        unsigned syms = 0) {
61   FlatAffineConstraints fac(ineqs.size(), eqs.size(), ids + 1, ids - syms, syms,
62                             /*numLocals=*/0);
63   for (const auto &eq : eqs)
64     fac.addEquality(eq);
65   for (const auto &ineq : ineqs)
66     fac.addInequality(ineq);
67   return fac;
68 }
69 
70 /// Check sampling for all the permutations of the dimensions for the given
71 /// constraint set. Since the GBR algorithm progresses dimension-wise, different
72 /// orderings may cause the algorithm to proceed differently. At least some of
73 ///.these permutations should make it past the heuristics and test the
74 /// implementation of the GBR algorithm itself.
75 /// Use TestFunction fn to test.
checkPermutationsSample(bool hasSample,unsigned nDim,ArrayRef<SmallVector<int64_t,4>> ineqs,ArrayRef<SmallVector<int64_t,4>> eqs,TestFunction fn=TestFunction::Sample)76 static void checkPermutationsSample(bool hasSample, unsigned nDim,
77                                     ArrayRef<SmallVector<int64_t, 4>> ineqs,
78                                     ArrayRef<SmallVector<int64_t, 4>> eqs,
79                                     TestFunction fn = TestFunction::Sample) {
80   SmallVector<unsigned, 4> perm(nDim);
81   std::iota(perm.begin(), perm.end(), 0);
82   auto permute = [&perm](ArrayRef<int64_t> coeffs) {
83     SmallVector<int64_t, 4> permuted;
84     for (unsigned id : perm)
85       permuted.push_back(coeffs[id]);
86     permuted.push_back(coeffs.back());
87     return permuted;
88   };
89   do {
90     SmallVector<SmallVector<int64_t, 4>, 4> permutedIneqs, permutedEqs;
91     for (const auto &ineq : ineqs)
92       permutedIneqs.push_back(permute(ineq));
93     for (const auto &eq : eqs)
94       permutedEqs.push_back(permute(eq));
95 
96     checkSample(hasSample,
97                 makeFACFromConstraints(nDim, permutedIneqs, permutedEqs), fn);
98   } while (std::next_permutation(perm.begin(), perm.end()));
99 }
100 
TEST(FlatAffineConstraintsTest,FindSampleTest)101 TEST(FlatAffineConstraintsTest, FindSampleTest) {
102   // Bounded sets with only inequalities.
103 
104   // 0 <= 7x <= 5
105   checkSample(true, makeFACFromConstraints(1, {{7, 0}, {-7, 5}}, {}));
106 
107   // 1 <= 5x and 5x <= 4 (no solution).
108   checkSample(false, makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}));
109 
110   // 1 <= 5x and 5x <= 9 (solution: x = 1).
111   checkSample(true, makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}));
112 
113   // Bounded sets with equalities.
114   // x >= 8 and 40 >= y and x = y.
115   checkSample(
116       true, makeFACFromConstraints(2, {{1, 0, -8}, {0, -1, 40}}, {{1, -1, 0}}));
117 
118   // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z.
119   // solution: x = y = z = 10.
120   checkSample(true, makeFACFromConstraints(
121                         3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -10}},
122                         {{1, 2, -3, 0}}));
123 
124   // x <= 10 and y <= 10 and 11 <= z and x + 2y = 3z.
125   // This implies x + 2y >= 33 and x + 2y <= 30, which has no solution.
126   checkSample(false, makeFACFromConstraints(
127                          3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -11}},
128                          {{1, 2, -3, 0}}));
129 
130   // 0 <= r and r <= 3 and 4q + r = 7.
131   // Solution: q = 1, r = 3.
132   checkSample(true,
133               makeFACFromConstraints(2, {{0, 1, 0}, {0, -1, 3}}, {{4, 1, -7}}));
134 
135   // 4q + r = 7 and r = 0.
136   // Solution: q = 1, r = 3.
137   checkSample(false, makeFACFromConstraints(2, {}, {{4, 1, -7}, {0, 1, 0}}));
138 
139   // The next two sets are large sets that should take a long time to sample
140   // with a naive branch and bound algorithm but can be sampled efficiently with
141   // the GBR algorithm.
142   //
143   // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (10000, 10000).
144   checkSample(
145       true,
146       makeFACFromConstraints(
147           2, {{0, 1, 0}, {300000, -299999, -100000}, {-300000, 299998, 200000}},
148           {}));
149 
150   // This is a tetrahedron with vertices at
151   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
152   // The first three points form a triangular base on the xz plane with the
153   // apex at the fourth point, which is the only integer point.
154   checkPermutationsSample(
155       true, 3,
156       {
157           {0, 1, 0, 0},  // y >= 0
158           {0, -1, 1, 0}, // z >= y
159           {300000, -299998, -1,
160            -100000},                    // -300000x + 299998y + 100000 + z <= 0.
161           {-150000, 149999, 0, 100000}, // -150000x + 149999y + 100000 >= 0.
162       },
163       {});
164 
165   // Same thing with some spurious extra dimensions equated to constants.
166   checkSample(true,
167               makeFACFromConstraints(
168                   5,
169                   {
170                       {0, 1, 0, 1, -1, 0},
171                       {0, -1, 1, -1, 1, 0},
172                       {300000, -299998, -1, -9, 21, -112000},
173                       {-150000, 149999, 0, -15, 47, 68000},
174                   },
175                   {{0, 0, 0, 1, -1, 0},       // p = q.
176                    {0, 0, 0, 1, 1, -2000}})); // p + q = 20000 => p = q = 10000.
177 
178   // This is a tetrahedron with vertices at
179   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100).
180   checkPermutationsSample(false, 3,
181                           {
182                               {0, 1, 0, 0},
183                               {0, -300, 299, 0},
184                               {300 * 299, -89400, -299, -100 * 299},
185                               {-897, 894, 0, 598},
186                           },
187                           {});
188 
189   // Two tests involving equalities that are integer empty but not rational
190   // empty.
191 
192   // This is a line segment from (0, 1/3) to (100, 100 + 1/3).
193   checkSample(false, makeFACFromConstraints(
194                          2,
195                          {
196                              {1, 0, 0},   // x >= 0.
197                              {-1, 0, 100} // -x + 100 >= 0, i.e., x <= 100.
198                          },
199                          {
200                              {3, -3, 1} // 3x - 3y + 1 = 0, i.e., y = x + 1/3.
201                          }));
202 
203   // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3.
204   checkSample(false, makeFACFromConstraints(2,
205                                             {
206                                                 {1, 0, 0},    // x >= 0.
207                                                 {-1, 0, 100}, // x <= 100.
208                                                 {3, -3, 2},   // 3x - 3y >= -2.
209                                                 {-3, 3, -1},  // 3x - 3y <= -1.
210                                             },
211                                             {}));
212 
213   checkSample(true, makeFACFromConstraints(2,
214                                            {
215                                                {2, 0, 0},   // 2x >= 1.
216                                                {-2, 0, 99}, // 2x <= 99.
217                                                {0, 2, 0},   // 2y >= 0.
218                                                {0, -2, 99}, // 2y <= 99.
219                                            },
220                                            {}));
221   // 2D cone with apex at (10000, 10000) and
222   // edges passing through (1/3, 0) and (2/3, 0).
223   checkSample(
224       true,
225       makeFACFromConstraints(
226           2, {{300000, -299999, -100000}, {-300000, 299998, 200000}}, {}));
227 
228   // Cartesian product of a tetrahedron and a 2D cone.
229   // The tetrahedron has vertices at
230   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
231   // The first three points form a triangular base on the xz plane with the
232   // apex at the fourth point, which is the only integer point.
233   // The cone has apex at (10000, 10000) and
234   // edges passing through (1/3, 0) and (2/3, 0).
235   checkPermutationsSample(
236       true /* not empty */, 5,
237       {
238           // Tetrahedron contraints:
239           {0, 1, 0, 0, 0, 0},  // y >= 0
240           {0, -1, 1, 0, 0, 0}, // z >= y
241                                // -300000x + 299998y + 100000 + z <= 0.
242           {300000, -299998, -1, 0, 0, -100000},
243           // -150000x + 149999y + 100000 >= 0.
244           {-150000, 149999, 0, 0, 0, 100000},
245 
246           // Triangle constraints:
247           // 300000p - 299999q >= 100000
248           {0, 0, 0, 300000, -299999, -100000},
249           // -300000p + 299998q + 200000 >= 0
250           {0, 0, 0, -300000, 299998, 200000},
251       },
252       {});
253 
254   // Cartesian product of same tetrahedron as above and {(p, q) : 1/3 <= p <=
255   // 2/3}. Since the second set is empty, the whole set is too.
256   checkPermutationsSample(
257       false /* empty */, 5,
258       {
259           // Tetrahedron contraints:
260           {0, 1, 0, 0, 0, 0},  // y >= 0
261           {0, -1, 1, 0, 0, 0}, // z >= y
262                                // -300000x + 299998y + 100000 + z <= 0.
263           {300000, -299998, -1, 0, 0, -100000},
264           // -150000x + 149999y + 100000 >= 0.
265           {-150000, 149999, 0, 0, 0, 100000},
266 
267           // Second set constraints:
268           // 3p >= 1
269           {0, 0, 0, 3, 0, -1},
270           // 3p <= 2
271           {0, 0, 0, -3, 0, 2},
272       },
273       {});
274 
275   // Cartesian product of same tetrahedron as above and
276   // {(p, q, r) : 1 <= p <= 2 and p = 3q + 3r}.
277   // Since the second set is empty, the whole set is too.
278   checkPermutationsSample(
279       false /* empty */, 5,
280       {
281           // Tetrahedron contraints:
282           {0, 1, 0, 0, 0, 0, 0},  // y >= 0
283           {0, -1, 1, 0, 0, 0, 0}, // z >= y
284                                   // -300000x + 299998y + 100000 + z <= 0.
285           {300000, -299998, -1, 0, 0, 0, -100000},
286           // -150000x + 149999y + 100000 >= 0.
287           {-150000, 149999, 0, 0, 0, 0, 100000},
288 
289           // Second set constraints:
290           // p >= 1
291           {0, 0, 0, 1, 0, 0, -1},
292           // p <= 2
293           {0, 0, 0, -1, 0, 0, 2},
294       },
295       {
296           {0, 0, 0, 1, -3, -3, 0}, // p = 3q + 3r
297       });
298 
299   // Cartesian product of a tetrahedron and a 2D cone.
300   // The tetrahedron is empty and has vertices at
301   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), and (100, 100 - 1/3, 100).
302   // The cone has apex at (10000, 10000) and
303   // edges passing through (1/3, 0) and (2/3, 0).
304   // Since the tetrahedron is empty, the Cartesian product is too.
305   checkPermutationsSample(false /* empty */, 5,
306                           {
307                               // Tetrahedron contraints:
308                               {0, 1, 0, 0, 0, 0},
309                               {0, -300, 299, 0, 0, 0},
310                               {300 * 299, -89400, -299, 0, 0, -100 * 299},
311                               {-897, 894, 0, 0, 0, 598},
312 
313                               // Triangle constraints:
314                               // 300000p - 299999q >= 100000
315                               {0, 0, 0, 300000, -299999, -100000},
316                               // -300000p + 299998q + 200000 >= 0
317                               {0, 0, 0, -300000, 299998, 200000},
318                           },
319                           {});
320 
321   // Cartesian product of same tetrahedron as above and
322   // {(p, q) : 1/3 <= p <= 2/3}.
323   checkPermutationsSample(false /* empty */, 5,
324                           {
325                               // Tetrahedron contraints:
326                               {0, 1, 0, 0, 0, 0},
327                               {0, -300, 299, 0, 0, 0},
328                               {300 * 299, -89400, -299, 0, 0, -100 * 299},
329                               {-897, 894, 0, 0, 0, 598},
330 
331                               // Second set constraints:
332                               // 3p >= 1
333                               {0, 0, 0, 3, 0, -1},
334                               // 3p <= 2
335                               {0, 0, 0, -3, 0, 2},
336                           },
337                           {});
338 
339   checkSample(true, makeFACFromConstraints(3,
340                                            {
341                                                {2, 0, 0, -1}, // 2x >= 1
342                                            },
343                                            {{
344                                                {1, -1, 0, -1}, // y = x - 1
345                                                {0, 1, -1, 0},  // z = y
346                                            }}));
347 }
348 
TEST(FlatAffineConstraintsTest,IsIntegerEmptyTest)349 TEST(FlatAffineConstraintsTest, IsIntegerEmptyTest) {
350   // 1 <= 5x and 5x <= 4 (no solution).
351   EXPECT_TRUE(
352       makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}).isIntegerEmpty());
353   // 1 <= 5x and 5x <= 9 (solution: x = 1).
354   EXPECT_FALSE(
355       makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}).isIntegerEmpty());
356 
357   // Unbounded sets.
358   EXPECT_TRUE(makeFACFromConstraints(3,
359                                      {
360                                          {0, 2, 0, -1}, // 2y >= 1
361                                          {0, -2, 0, 1}, // 2y <= 1
362                                          {0, 0, 2, -1}, // 2z >= 1
363                                      },
364                                      {{2, 0, 0, -1}} // 2x = 1
365                                      )
366                   .isIntegerEmpty());
367 
368   EXPECT_FALSE(makeFACFromConstraints(3,
369                                       {
370                                           {2, 0, 0, -1},  // 2x >= 1
371                                           {-3, 0, 0, 3},  // 3x <= 3
372                                           {0, 0, 5, -6},  // 5z >= 6
373                                           {0, 0, -7, 17}, // 7z <= 17
374                                           {0, 3, 0, -2},  // 3y >= 2
375                                       },
376                                       {})
377                    .isIntegerEmpty());
378 
379   EXPECT_FALSE(makeFACFromConstraints(3,
380                                       {
381                                           {2, 0, 0, -1}, // 2x >= 1
382                                       },
383                                       {{
384                                           {1, -1, 0, -1}, // y = x - 1
385                                           {0, 1, -1, 0},  // z = y
386                                       }})
387                    .isIntegerEmpty());
388 
389   // FlatAffineConstraints::isEmpty() does not detect the following sets to be
390   // empty.
391 
392   // 3x + 7y = 1 and 0 <= x, y <= 10.
393   // Since x and y are non-negative, 3x + 7y can never be 1.
394   EXPECT_TRUE(
395       makeFACFromConstraints(
396           2, {{1, 0, 0}, {-1, 0, 10}, {0, 1, 0}, {0, -1, 10}}, {{3, 7, -1}})
397           .isIntegerEmpty());
398 
399   // 2x = 3y and y = x - 1 and x + y = 6z + 2 and 0 <= x, y <= 100.
400   // Substituting y = x - 1 in 3y = 2x, we obtain x = 3 and hence y = 2.
401   // Since x + y = 5 cannot be equal to 6z + 2 for any z, the set is empty.
402   EXPECT_TRUE(
403       makeFACFromConstraints(3,
404                              {
405                                  {1, 0, 0, 0},
406                                  {-1, 0, 0, 100},
407                                  {0, 1, 0, 0},
408                                  {0, -1, 0, 100},
409                              },
410                              {{2, -3, 0, 0}, {1, -1, 0, -1}, {1, 1, -6, -2}})
411           .isIntegerEmpty());
412 
413   // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100.
414   // 2x = 3y implies x is a multiple of 3 and y is even.
415   // Now y = x - 1 + 6z implies y = 2 mod 3. In fact, since y is even, we have
416   // y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying
417   // x + y = 5 mod 6, which contradicts x + y = 6q + 2, so the set is empty.
418   EXPECT_TRUE(makeFACFromConstraints(
419                   4,
420                   {
421                       {1, 0, 0, 0, 0},
422                       {-1, 0, 0, 0, 100},
423                       {0, 1, 0, 0, 0},
424                       {0, -1, 0, 0, 100},
425                   },
426                   {{2, -3, 0, 0, 0}, {1, -1, 6, 0, -1}, {1, 1, 0, -6, -2}})
427                   .isIntegerEmpty());
428 
429   // Set with symbols.
430   FlatAffineConstraints fac6 = makeFACFromConstraints(2,
431                                                       {
432                                                           {1, 1, 0},
433                                                       },
434                                                       {
435                                                           {1, -1, 0},
436                                                       },
437                                                       1);
438   EXPECT_FALSE(fac6.isIntegerEmpty());
439 }
440 
TEST(FlatAffineConstraintsTest,removeRedundantConstraintsTest)441 TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) {
442   FlatAffineConstraints fac = makeFACFromConstraints(1,
443                                                      {
444                                                          {1, -2}, // x >= 2.
445                                                          {-1, 2}  // x <= 2.
446                                                      },
447                                                      {{1, -2}}); // x == 2.
448   fac.removeRedundantConstraints();
449 
450   // Both inequalities are redundant given the equality. Both have been removed.
451   EXPECT_EQ(fac.getNumInequalities(), 0u);
452   EXPECT_EQ(fac.getNumEqualities(), 1u);
453 
454   FlatAffineConstraints fac2 =
455       makeFACFromConstraints(2,
456                              {
457                                  {1, 0, -3}, // x >= 3.
458                                  {0, 1, -2}  // y >= 2 (redundant).
459                              },
460                              {{1, -1, 0}}); // x == y.
461   fac2.removeRedundantConstraints();
462 
463   // The second inequality is redundant and should have been removed. The
464   // remaining inequality should be the first one.
465   EXPECT_EQ(fac2.getNumInequalities(), 1u);
466   EXPECT_THAT(fac2.getInequality(0), ElementsAre(1, 0, -3));
467   EXPECT_EQ(fac2.getNumEqualities(), 1u);
468 
469   FlatAffineConstraints fac3 =
470       makeFACFromConstraints(3, {},
471                              {{1, -1, 0, 0},   // x == y.
472                               {1, 0, -1, 0},   // x == z.
473                               {0, 1, -1, 0}}); // y == z.
474   fac3.removeRedundantConstraints();
475 
476   // One of the three equalities can be removed.
477   EXPECT_EQ(fac3.getNumInequalities(), 0u);
478   EXPECT_EQ(fac3.getNumEqualities(), 2u);
479 
480   FlatAffineConstraints fac4 = makeFACFromConstraints(
481       17,
482       {{0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
483        {0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 500},
484        {0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
485        {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
486        {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998},
487        {0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15},
488        {0, 0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
489        {0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
490        {0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998},
491        {0, 0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15},
492        {0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
493        {0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1},
494        {0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1},
495        {0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 500},
496        {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 16, 0, 0, 0, 0, 0, 15},
497        {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -16, 0, 0, 0, 0, 0, 0},
498        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -16, 0, 1, 0, 0, 0},
499        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1},
500        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 998},
501        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16, 0, -1, 0, 0, 15},
502        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0},
503        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 1},
504        {0, 0, 0, 0, 0, 0, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8},
505        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, 8, 8},
506        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, -8, -1},
507        {0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, -8, -1},
508        {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0},
509        {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0},
510        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, -10},
511        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 10},
512        {0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, -13},
513        {0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 13},
514        {0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -10},
515        {0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10},
516        {1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -13},
517        {-1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 13}},
518       {});
519 
520   // The above is a large set of constraints without any redundant constraints,
521   // as verified by the Fourier-Motzkin based removeRedundantInequalities.
522   unsigned nIneq = fac4.getNumInequalities();
523   unsigned nEq = fac4.getNumEqualities();
524   fac4.removeRedundantInequalities();
525   ASSERT_EQ(fac4.getNumInequalities(), nIneq);
526   ASSERT_EQ(fac4.getNumEqualities(), nEq);
527   // Now we test that removeRedundantConstraints does not find any constraints
528   // to be redundant either.
529   fac4.removeRedundantConstraints();
530   EXPECT_EQ(fac4.getNumInequalities(), nIneq);
531   EXPECT_EQ(fac4.getNumEqualities(), nEq);
532 
533   FlatAffineConstraints fac5 =
534       makeFACFromConstraints(2,
535                              {
536                                  {128, 0, 127}, // [0]: 128x >= -127.
537                                  {-1, 0, 7},    // [1]: x <= 7.
538                                  {-128, 1, 0},  // [2]: y >= 128x.
539                                  {0, 1, 0}      // [3]: y >= 0.
540                              },
541                              {});
542   // [0] implies that 128x >= 0, since x has to be an integer. (This should be
543   // caught by GCDTightenInqualities().)
544   // So [2] and [0] imply [3] since we have y >= 128x >= 0.
545   fac5.removeRedundantConstraints();
546   EXPECT_EQ(fac5.getNumInequalities(), 3u);
547   SmallVector<int64_t, 8> redundantConstraint = {0, 1, 0};
548   for (unsigned i = 0; i < 3; ++i) {
549     // Ensure that the removed constraint was the redundant constraint [3].
550     EXPECT_NE(fac5.getInequality(i), ArrayRef<int64_t>(redundantConstraint));
551   }
552 }
553 
TEST(FlatAffineConstraintsTest,addConstantUpperBound)554 TEST(FlatAffineConstraintsTest, addConstantUpperBound) {
555   FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {});
556   fac.addBound(FlatAffineConstraints::UB, 0, 1);
557   EXPECT_EQ(fac.atIneq(0, 0), -1);
558   EXPECT_EQ(fac.atIneq(0, 1), 0);
559   EXPECT_EQ(fac.atIneq(0, 2), 1);
560 
561   fac.addBound(FlatAffineConstraints::UB, {1, 2, 3}, 1);
562   EXPECT_EQ(fac.atIneq(1, 0), -1);
563   EXPECT_EQ(fac.atIneq(1, 1), -2);
564   EXPECT_EQ(fac.atIneq(1, 2), -2);
565 }
566 
TEST(FlatAffineConstraintsTest,addConstantLowerBound)567 TEST(FlatAffineConstraintsTest, addConstantLowerBound) {
568   FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {});
569   fac.addBound(FlatAffineConstraints::LB, 0, 1);
570   EXPECT_EQ(fac.atIneq(0, 0), 1);
571   EXPECT_EQ(fac.atIneq(0, 1), 0);
572   EXPECT_EQ(fac.atIneq(0, 2), -1);
573 
574   fac.addBound(FlatAffineConstraints::LB, {1, 2, 3}, 1);
575   EXPECT_EQ(fac.atIneq(1, 0), 1);
576   EXPECT_EQ(fac.atIneq(1, 1), 2);
577   EXPECT_EQ(fac.atIneq(1, 2), 2);
578 }
579 
TEST(FlatAffineConstraintsTest,removeInequality)580 TEST(FlatAffineConstraintsTest, removeInequality) {
581   FlatAffineConstraints fac =
582       makeFACFromConstraints(1, {{0, 0}, {1, 1}, {2, 2}, {3, 3}, {4, 4}}, {});
583 
584   fac.removeInequalityRange(0, 0);
585   EXPECT_EQ(fac.getNumInequalities(), 5u);
586 
587   fac.removeInequalityRange(1, 3);
588   EXPECT_EQ(fac.getNumInequalities(), 3u);
589   EXPECT_THAT(fac.getInequality(0), ElementsAre(0, 0));
590   EXPECT_THAT(fac.getInequality(1), ElementsAre(3, 3));
591   EXPECT_THAT(fac.getInequality(2), ElementsAre(4, 4));
592 
593   fac.removeInequality(1);
594   EXPECT_EQ(fac.getNumInequalities(), 2u);
595   EXPECT_THAT(fac.getInequality(0), ElementsAre(0, 0));
596   EXPECT_THAT(fac.getInequality(1), ElementsAre(4, 4));
597 }
598 
TEST(FlatAffineConstraintsTest,removeEquality)599 TEST(FlatAffineConstraintsTest, removeEquality) {
600   FlatAffineConstraints fac =
601       makeFACFromConstraints(1, {}, {{0, 0}, {1, 1}, {2, 2}, {3, 3}, {4, 4}});
602 
603   fac.removeEqualityRange(0, 0);
604   EXPECT_EQ(fac.getNumEqualities(), 5u);
605 
606   fac.removeEqualityRange(1, 3);
607   EXPECT_EQ(fac.getNumEqualities(), 3u);
608   EXPECT_THAT(fac.getEquality(0), ElementsAre(0, 0));
609   EXPECT_THAT(fac.getEquality(1), ElementsAre(3, 3));
610   EXPECT_THAT(fac.getEquality(2), ElementsAre(4, 4));
611 
612   fac.removeEquality(1);
613   EXPECT_EQ(fac.getNumEqualities(), 2u);
614   EXPECT_THAT(fac.getEquality(0), ElementsAre(0, 0));
615   EXPECT_THAT(fac.getEquality(1), ElementsAre(4, 4));
616 }
617 
TEST(FlatAffineConstraintsTest,clearConstraints)618 TEST(FlatAffineConstraintsTest, clearConstraints) {
619   FlatAffineConstraints fac = makeFACFromConstraints(1, {}, {});
620 
621   fac.addInequality({1, 0});
622   EXPECT_EQ(fac.atIneq(0, 0), 1);
623   EXPECT_EQ(fac.atIneq(0, 1), 0);
624 
625   fac.clearConstraints();
626 
627   fac.addInequality({1, 0});
628   EXPECT_EQ(fac.atIneq(0, 0), 1);
629   EXPECT_EQ(fac.atIneq(0, 1), 0);
630 }
631 
632 /// Check if the expected division representation of local variables matches the
633 /// computed representation. The expected division representation is given as
634 /// a vector of expressions set in `divisions` and the corressponding
635 /// denominator in `denoms`. If expected denominator for a variable is
636 /// non-positive, the local variable is expected to not have a computed
637 /// representation.
checkDivisionRepresentation(FlatAffineConstraints & fac,const std::vector<SmallVector<int64_t,8>> & divisions,const SmallVector<int64_t,8> & denoms)638 static void checkDivisionRepresentation(
639     FlatAffineConstraints &fac,
640     const std::vector<SmallVector<int64_t, 8>> &divisions,
641     const SmallVector<int64_t, 8> &denoms) {
642 
643   assert(divisions.size() == fac.getNumLocalIds() &&
644          "Size of expected divisions does not match number of local variables");
645   assert(
646       denoms.size() == fac.getNumLocalIds() &&
647       "Size of expected denominators does not match number of local variables");
648 
649   std::vector<llvm::Optional<std::pair<unsigned, unsigned>>> res(
650       fac.getNumLocalIds(), llvm::None);
651   fac.getLocalReprLbUbPairs(res);
652 
653   // Check if all expected divisions are computed.
654   for (unsigned i = 0, e = fac.getNumLocalIds(); i < e; ++i)
655     if (denoms[i] > 0)
656       EXPECT_TRUE(res[i].hasValue());
657     else
658       EXPECT_FALSE(res[i].hasValue());
659 
660   unsigned divOffset = fac.getNumDimAndSymbolIds();
661   for (unsigned i = 0, e = fac.getNumLocalIds(); i < e; ++i) {
662     if (!res[i])
663       continue;
664 
665     // Check if the bounds are of the form:
666     //      0 <= expr - divisor * id <= divisor - 1
667     // Rearranging, we have:
668     //       divisor * id - expr + (divisor - 1) >= 0  <-- Lower bound for 'id'
669     //      -divisor * id + expr                 >= 0  <-- Upper bound for 'id'
670     // where `id = expr floordiv divisor`.
671     unsigned ubPos = res[i]->first, lbPos = res[i]->second;
672     const SmallVector<int64_t, 8> &expr = divisions[i];
673 
674     // Check if lower bound is of the correct form.
675     int64_t computedDivisorLb = fac.atIneq(lbPos, i + divOffset);
676     EXPECT_EQ(computedDivisorLb, denoms[i]);
677     for (unsigned c = 0, f = fac.getNumLocalIds(); c < f; ++c) {
678       if (c == i + divOffset)
679         continue;
680       EXPECT_EQ(fac.atIneq(lbPos, c), -expr[c]);
681     }
682     // Check if constant term of lower bound matches expected constant term.
683     EXPECT_EQ(fac.atIneq(lbPos, fac.getNumCols() - 1),
684               -expr.back() + (denoms[i] - 1));
685 
686     // Check if upper bound is of the correct form.
687     int64_t computedDivisorUb = fac.atIneq(ubPos, i + divOffset);
688     EXPECT_EQ(computedDivisorUb, -denoms[i]);
689     for (unsigned c = 0, f = fac.getNumLocalIds(); c < f; ++c) {
690       if (c == i + divOffset)
691         continue;
692       EXPECT_EQ(fac.atIneq(ubPos, c), expr[c]);
693     }
694     // Check if constant term of upper bound matches expected constant term.
695     EXPECT_EQ(fac.atIneq(ubPos, fac.getNumCols() - 1), expr.back());
696   }
697 }
698 
TEST(FlatAffineConstraintsTest,computeLocalReprSimple)699 TEST(FlatAffineConstraintsTest, computeLocalReprSimple) {
700   FlatAffineConstraints fac = makeFACFromConstraints(1, {}, {});
701 
702   fac.addLocalFloorDiv({1, 4}, 10);
703   fac.addLocalFloorDiv({1, 0, 100}, 10);
704 
705   std::vector<SmallVector<int64_t, 8>> divisions = {{1, 0, 0, 4},
706                                                     {1, 0, 0, 100}};
707   SmallVector<int64_t, 8> denoms = {10, 10};
708 
709   // Check if floordivs can be computed when no other inequalities exist
710   // and floor divs do not depend on each other.
711   checkDivisionRepresentation(fac, divisions, denoms);
712 }
713 
TEST(FlatAffineConstraintsTest,computeLocalReprConstantFloorDiv)714 TEST(FlatAffineConstraintsTest, computeLocalReprConstantFloorDiv) {
715   FlatAffineConstraints fac = makeFACFromConstraints(4, {}, {});
716 
717   fac.addInequality({1, 0, 3, 1, 2});
718   fac.addInequality({1, 2, -8, 1, 10});
719   fac.addEquality({1, 2, -4, 1, 10});
720 
721   fac.addLocalFloorDiv({0, 0, 0, 0, 10}, 30);
722   fac.addLocalFloorDiv({0, 0, 0, 0, 0, 99}, 101);
723 
724   std::vector<SmallVector<int64_t, 8>> divisions = {{0, 0, 0, 0, 0, 0, 10},
725                                                     {0, 0, 0, 0, 0, 0, 99}};
726   SmallVector<int64_t, 8> denoms = {30, 101};
727 
728   // Check if floordivs with constant numerator can be computed.
729   checkDivisionRepresentation(fac, divisions, denoms);
730 }
731 
TEST(FlatAffineConstraintsTest,computeLocalReprRecursive)732 TEST(FlatAffineConstraintsTest, computeLocalReprRecursive) {
733   FlatAffineConstraints fac = makeFACFromConstraints(4, {}, {});
734   fac.addInequality({1, 0, 3, 1, 2});
735   fac.addInequality({1, 2, -8, 1, 10});
736   fac.addEquality({1, 2, -4, 1, 10});
737 
738   fac.addLocalFloorDiv({0, -2, 7, 2, 10}, 3);
739   fac.addLocalFloorDiv({3, 0, 9, 2, 2, 10}, 5);
740   fac.addLocalFloorDiv({0, 1, -123, 2, 0, -4, 10}, 3);
741 
742   fac.addInequality({1, 2, -2, 1, -5, 0, 6, 100});
743   fac.addInequality({1, 2, -8, 1, 3, 7, 0, -9});
744 
745   std::vector<SmallVector<int64_t, 8>> divisions = {{0, -2, 7, 2, 0, 0, 0, 10},
746                                                     {3, 0, 9, 2, 2, 0, 0, 10},
747                                                     {0, 1, -123, 2, 0, -4, 10}};
748   SmallVector<int64_t, 8> denoms = {3, 5, 3};
749 
750   // Check if floordivs which may depend on other floordivs can be computed.
751   checkDivisionRepresentation(fac, divisions, denoms);
752 }
753 
TEST(FlatAffineConstraintsTest,removeIdRange)754 TEST(FlatAffineConstraintsTest, removeIdRange) {
755   FlatAffineConstraints fac(3, 2, 1);
756 
757   fac.addInequality({10, 11, 12, 20, 21, 30, 40});
758   fac.removeId(FlatAffineConstraints::IdKind::Symbol, 1);
759   EXPECT_THAT(fac.getInequality(0),
760               testing::ElementsAre(10, 11, 12, 20, 30, 40));
761 
762   fac.removeIdRange(FlatAffineConstraints::IdKind::Dimension, 0, 2);
763   EXPECT_THAT(fac.getInequality(0), testing::ElementsAre(12, 20, 30, 40));
764 
765   fac.removeIdRange(FlatAffineConstraints::IdKind::Local, 1, 1);
766   EXPECT_THAT(fac.getInequality(0), testing::ElementsAre(12, 20, 30, 40));
767 
768   fac.removeIdRange(FlatAffineConstraints::IdKind::Local, 0, 1);
769   EXPECT_THAT(fac.getInequality(0), testing::ElementsAre(12, 20, 40));
770 }
771 
TEST(FlatAffineConstraintsTest,simplifyLocalsTest)772 TEST(FlatAffineConstraintsTest, simplifyLocalsTest) {
773   // (x) : (exists y: 2x + y = 1 and y = 2).
774   FlatAffineConstraints fac(1, 0, 1);
775   fac.addEquality({2, 1, -1});
776   fac.addEquality({0, 1, -2});
777 
778   EXPECT_TRUE(fac.isEmpty());
779 
780   // (x) : (exists y, z, w: 3x + y = 1 and 2y = z and 3y = w and z = w).
781   FlatAffineConstraints fac2(1, 0, 3);
782   fac2.addEquality({3, 1, 0, 0, -1});
783   fac2.addEquality({0, 2, -1, 0, 0});
784   fac2.addEquality({0, 3, 0, -1, 0});
785   fac2.addEquality({0, 0, 1, -1, 0});
786 
787   EXPECT_TRUE(fac2.isEmpty());
788 
789   // (x) : (exists y: x >= y + 1 and 2x + y = 0 and y >= -1).
790   FlatAffineConstraints fac3(1, 0, 1);
791   fac3.addInequality({1, -1, -1});
792   fac3.addInequality({0, 1, 1});
793   fac3.addEquality({2, 1, 0});
794 
795   EXPECT_TRUE(fac3.isEmpty());
796 }
797 
798 } // namespace mlir
799