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 
11 #include <gmock/gmock.h>
12 #include <gtest/gtest.h>
13 
14 #include <numeric>
15 
16 namespace mlir {
17 
18 enum class TestFunction { Sample, Empty };
19 
20 /// If fn is TestFunction::Sample (default):
21 /// If hasSample is true, check that findIntegerSample returns a valid sample
22 /// for the FlatAffineConstraints fac.
23 /// If hasSample is false, check that findIntegerSample returns None.
24 ///
25 /// If fn is TestFunction::Empty, check that isIntegerEmpty returns the
26 /// opposite of hasSample.
27 static void checkSample(bool hasSample, const FlatAffineConstraints &fac,
28                         TestFunction fn = TestFunction::Sample) {
29   Optional<SmallVector<int64_t, 8>> maybeSample;
30   switch (fn) {
31   case TestFunction::Sample:
32     maybeSample = fac.findIntegerSample();
33     if (!hasSample) {
34       EXPECT_FALSE(maybeSample.hasValue());
35       if (maybeSample.hasValue()) {
36         for (auto x : *maybeSample)
37           llvm::errs() << x << ' ';
38         llvm::errs() << '\n';
39       }
40     } else {
41       ASSERT_TRUE(maybeSample.hasValue());
42       EXPECT_TRUE(fac.containsPoint(*maybeSample));
43     }
44     break;
45   case TestFunction::Empty:
46     EXPECT_EQ(!hasSample, fac.isIntegerEmpty());
47     break;
48   }
49 }
50 
51 /// Construct a FlatAffineConstraints from a set of inequality and
52 /// equality constraints.
53 static FlatAffineConstraints
54 makeFACFromConstraints(unsigned ids, ArrayRef<SmallVector<int64_t, 4>> ineqs,
55                        ArrayRef<SmallVector<int64_t, 4>> eqs,
56                        unsigned syms = 0) {
57   FlatAffineConstraints fac(ineqs.size(), eqs.size(), ids + 1, ids - syms,
58                             syms);
59   for (const auto &eq : eqs)
60     fac.addEquality(eq);
61   for (const auto &ineq : ineqs)
62     fac.addInequality(ineq);
63   return fac;
64 }
65 
66 /// Check sampling for all the permutations of the dimensions for the given
67 /// constraint set. Since the GBR algorithm progresses dimension-wise, different
68 /// orderings may cause the algorithm to proceed differently. At least some of
69 ///.these permutations should make it past the heuristics and test the
70 /// implementation of the GBR algorithm itself.
71 /// Use TestFunction fn to test.
72 static void checkPermutationsSample(bool hasSample, unsigned nDim,
73                                     ArrayRef<SmallVector<int64_t, 4>> ineqs,
74                                     ArrayRef<SmallVector<int64_t, 4>> eqs,
75                                     TestFunction fn = TestFunction::Sample) {
76   SmallVector<unsigned, 4> perm(nDim);
77   std::iota(perm.begin(), perm.end(), 0);
78   auto permute = [&perm](ArrayRef<int64_t> coeffs) {
79     SmallVector<int64_t, 4> permuted;
80     for (unsigned id : perm)
81       permuted.push_back(coeffs[id]);
82     permuted.push_back(coeffs.back());
83     return permuted;
84   };
85   do {
86     SmallVector<SmallVector<int64_t, 4>, 4> permutedIneqs, permutedEqs;
87     for (const auto &ineq : ineqs)
88       permutedIneqs.push_back(permute(ineq));
89     for (const auto &eq : eqs)
90       permutedEqs.push_back(permute(eq));
91 
92     checkSample(hasSample,
93                 makeFACFromConstraints(nDim, permutedIneqs, permutedEqs), fn);
94   } while (std::next_permutation(perm.begin(), perm.end()));
95 }
96 
97 TEST(FlatAffineConstraintsTest, FindSampleTest) {
98   // Bounded sets with only inequalities.
99 
100   // 0 <= 7x <= 5
101   checkSample(true, makeFACFromConstraints(1, {{7, 0}, {-7, 5}}, {}));
102 
103   // 1 <= 5x and 5x <= 4 (no solution).
104   checkSample(false, makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}));
105 
106   // 1 <= 5x and 5x <= 9 (solution: x = 1).
107   checkSample(true, makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}));
108 
109   // Bounded sets with equalities.
110   // x >= 8 and 40 >= y and x = y.
111   checkSample(
112       true, makeFACFromConstraints(2, {{1, 0, -8}, {0, -1, 40}}, {{1, -1, 0}}));
113 
114   // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z.
115   // solution: x = y = z = 10.
116   checkSample(true, makeFACFromConstraints(
117                         3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -10}},
118                         {{1, 2, -3, 0}}));
119 
120   // x <= 10 and y <= 10 and 11 <= z and x + 2y = 3z.
121   // This implies x + 2y >= 33 and x + 2y <= 30, which has no solution.
122   checkSample(false, makeFACFromConstraints(
123                          3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -11}},
124                          {{1, 2, -3, 0}}));
125 
126   // 0 <= r and r <= 3 and 4q + r = 7.
127   // Solution: q = 1, r = 3.
128   checkSample(true,
129               makeFACFromConstraints(2, {{0, 1, 0}, {0, -1, 3}}, {{4, 1, -7}}));
130 
131   // 4q + r = 7 and r = 0.
132   // Solution: q = 1, r = 3.
133   checkSample(false, makeFACFromConstraints(2, {}, {{4, 1, -7}, {0, 1, 0}}));
134 
135   // The next two sets are large sets that should take a long time to sample
136   // with a naive branch and bound algorithm but can be sampled efficiently with
137   // the GBR algorithm.
138   //
139   // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (10000, 10000).
140   checkSample(
141       true,
142       makeFACFromConstraints(
143           2, {{0, 1, 0}, {300000, -299999, -100000}, {-300000, 299998, 200000}},
144           {}));
145 
146   // This is a tetrahedron with vertices at
147   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
148   // The first three points form a triangular base on the xz plane with the
149   // apex at the fourth point, which is the only integer point.
150   checkPermutationsSample(
151       true, 3,
152       {
153           {0, 1, 0, 0},  // y >= 0
154           {0, -1, 1, 0}, // z >= y
155           {300000, -299998, -1,
156            -100000},                    // -300000x + 299998y + 100000 + z <= 0.
157           {-150000, 149999, 0, 100000}, // -150000x + 149999y + 100000 >= 0.
158       },
159       {});
160 
161   // Same thing with some spurious extra dimensions equated to constants.
162   checkSample(true,
163               makeFACFromConstraints(
164                   5,
165                   {
166                       {0, 1, 0, 1, -1, 0},
167                       {0, -1, 1, -1, 1, 0},
168                       {300000, -299998, -1, -9, 21, -112000},
169                       {-150000, 149999, 0, -15, 47, 68000},
170                   },
171                   {{0, 0, 0, 1, -1, 0},       // p = q.
172                    {0, 0, 0, 1, 1, -2000}})); // p + q = 20000 => p = q = 10000.
173 
174   // This is a tetrahedron with vertices at
175   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100).
176   checkPermutationsSample(false, 3,
177                           {
178                               {0, 1, 0, 0},
179                               {0, -300, 299, 0},
180                               {300 * 299, -89400, -299, -100 * 299},
181                               {-897, 894, 0, 598},
182                           },
183                           {});
184 
185   // Two tests involving equalities that are integer empty but not rational
186   // empty.
187 
188   // This is a line segment from (0, 1/3) to (100, 100 + 1/3).
189   checkSample(false, makeFACFromConstraints(
190                          2,
191                          {
192                              {1, 0, 0},   // x >= 0.
193                              {-1, 0, 100} // -x + 100 >= 0, i.e., x <= 100.
194                          },
195                          {
196                              {3, -3, 1} // 3x - 3y + 1 = 0, i.e., y = x + 1/3.
197                          }));
198 
199   // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3.
200   checkSample(false, makeFACFromConstraints(2,
201                                             {
202                                                 {1, 0, 0},    // x >= 0.
203                                                 {-1, 0, 100}, // x <= 100.
204                                                 {3, -3, 2},   // 3x - 3y >= -2.
205                                                 {-3, 3, -1},  // 3x - 3y <= -1.
206                                             },
207                                             {}));
208 
209   checkSample(true, makeFACFromConstraints(2,
210                                            {
211                                                {2, 0, 0},   // 2x >= 1.
212                                                {-2, 0, 99}, // 2x <= 99.
213                                                {0, 2, 0},   // 2y >= 0.
214                                                {0, -2, 99}, // 2y <= 99.
215                                            },
216                                            {}));
217   // 2D cone with apex at (10000, 10000) and
218   // edges passing through (1/3, 0) and (2/3, 0).
219   checkSample(
220       true,
221       makeFACFromConstraints(
222           2, {{300000, -299999, -100000}, {-300000, 299998, 200000}}, {}));
223 
224   // Cartesian product of a tetrahedron and a 2D cone.
225   // The tetrahedron has vertices at
226   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
227   // The first three points form a triangular base on the xz plane with the
228   // apex at the fourth point, which is the only integer point.
229   // The cone has apex at (10000, 10000) and
230   // edges passing through (1/3, 0) and (2/3, 0).
231   checkPermutationsSample(
232       true /* not empty */, 5,
233       {
234           // Tetrahedron contraints:
235           {0, 1, 0, 0, 0, 0},  // y >= 0
236           {0, -1, 1, 0, 0, 0}, // z >= y
237                                // -300000x + 299998y + 100000 + z <= 0.
238           {300000, -299998, -1, 0, 0, -100000},
239           // -150000x + 149999y + 100000 >= 0.
240           {-150000, 149999, 0, 0, 0, 100000},
241 
242           // Triangle constraints:
243           // 300000p - 299999q >= 100000
244           {0, 0, 0, 300000, -299999, -100000},
245           // -300000p + 299998q + 200000 >= 0
246           {0, 0, 0, -300000, 299998, 200000},
247       },
248       {});
249 
250   // Cartesian product of same tetrahedron as above and {(p, q) : 1/3 <= p <=
251   // 2/3}. Since the second set is empty, the whole set is too.
252   checkPermutationsSample(
253       false /* empty */, 5,
254       {
255           // Tetrahedron contraints:
256           {0, 1, 0, 0, 0, 0},  // y >= 0
257           {0, -1, 1, 0, 0, 0}, // z >= y
258                                // -300000x + 299998y + 100000 + z <= 0.
259           {300000, -299998, -1, 0, 0, -100000},
260           // -150000x + 149999y + 100000 >= 0.
261           {-150000, 149999, 0, 0, 0, 100000},
262 
263           // Second set constraints:
264           // 3p >= 1
265           {0, 0, 0, 3, 0, -1},
266           // 3p <= 2
267           {0, 0, 0, -3, 0, 2},
268       },
269       {});
270 
271   // Cartesian product of same tetrahedron as above and
272   // {(p, q, r) : 1 <= p <= 2 and p = 3q + 3r}.
273   // Since the second set is empty, the whole set is too.
274   checkPermutationsSample(
275       false /* empty */, 5,
276       {
277           // Tetrahedron contraints:
278           {0, 1, 0, 0, 0, 0, 0},  // y >= 0
279           {0, -1, 1, 0, 0, 0, 0}, // z >= y
280                                   // -300000x + 299998y + 100000 + z <= 0.
281           {300000, -299998, -1, 0, 0, 0, -100000},
282           // -150000x + 149999y + 100000 >= 0.
283           {-150000, 149999, 0, 0, 0, 0, 100000},
284 
285           // Second set constraints:
286           // p >= 1
287           {0, 0, 0, 1, 0, 0, -1},
288           // p <= 2
289           {0, 0, 0, -1, 0, 0, 2},
290       },
291       {
292           {0, 0, 0, 1, -3, -3, 0}, // p = 3q + 3r
293       });
294 
295   // Cartesian product of a tetrahedron and a 2D cone.
296   // The tetrahedron is empty and has vertices at
297   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), and (100, 100 - 1/3, 100).
298   // The cone has apex at (10000, 10000) and
299   // edges passing through (1/3, 0) and (2/3, 0).
300   // Since the tetrahedron is empty, the Cartesian product is too.
301   checkPermutationsSample(false /* empty */, 5,
302                           {
303                               // Tetrahedron contraints:
304                               {0, 1, 0, 0, 0, 0},
305                               {0, -300, 299, 0, 0, 0},
306                               {300 * 299, -89400, -299, 0, 0, -100 * 299},
307                               {-897, 894, 0, 0, 0, 598},
308 
309                               // Triangle constraints:
310                               // 300000p - 299999q >= 100000
311                               {0, 0, 0, 300000, -299999, -100000},
312                               // -300000p + 299998q + 200000 >= 0
313                               {0, 0, 0, -300000, 299998, 200000},
314                           },
315                           {});
316 
317   // Cartesian product of same tetrahedron as above and
318   // {(p, q) : 1/3 <= p <= 2/3}.
319   checkPermutationsSample(false /* empty */, 5,
320                           {
321                               // Tetrahedron contraints:
322                               {0, 1, 0, 0, 0, 0},
323                               {0, -300, 299, 0, 0, 0},
324                               {300 * 299, -89400, -299, 0, 0, -100 * 299},
325                               {-897, 894, 0, 0, 0, 598},
326 
327                               // Second set constraints:
328                               // 3p >= 1
329                               {0, 0, 0, 3, 0, -1},
330                               // 3p <= 2
331                               {0, 0, 0, -3, 0, 2},
332                           },
333                           {});
334 
335   checkSample(true, makeFACFromConstraints(3,
336                                            {
337                                                {2, 0, 0, -1}, // 2x >= 1
338                                            },
339                                            {{
340                                                {1, -1, 0, -1}, // y = x - 1
341                                                {0, 1, -1, 0},  // z = y
342                                            }}));
343 }
344 
345 TEST(FlatAffineConstraintsTest, IsIntegerEmptyTest) {
346   // 1 <= 5x and 5x <= 4 (no solution).
347   EXPECT_TRUE(
348       makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}).isIntegerEmpty());
349   // 1 <= 5x and 5x <= 9 (solution: x = 1).
350   EXPECT_FALSE(
351       makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}).isIntegerEmpty());
352 
353   // Unbounded sets.
354   EXPECT_TRUE(makeFACFromConstraints(3,
355                                      {
356                                          {0, 2, 0, -1}, // 2y >= 1
357                                          {0, -2, 0, 1}, // 2y <= 1
358                                          {0, 0, 2, -1}, // 2z >= 1
359                                      },
360                                      {{2, 0, 0, -1}} // 2x = 1
361                                      )
362                   .isIntegerEmpty());
363 
364   EXPECT_FALSE(makeFACFromConstraints(3,
365                                       {
366                                           {2, 0, 0, -1},  // 2x >= 1
367                                           {-3, 0, 0, 3},  // 3x <= 3
368                                           {0, 0, 5, -6},  // 5z >= 6
369                                           {0, 0, -7, 17}, // 7z <= 17
370                                           {0, 3, 0, -2},  // 3y >= 2
371                                       },
372                                       {})
373                    .isIntegerEmpty());
374 
375   EXPECT_FALSE(makeFACFromConstraints(3,
376                                       {
377                                           {2, 0, 0, -1}, // 2x >= 1
378                                       },
379                                       {{
380                                           {1, -1, 0, -1}, // y = x - 1
381                                           {0, 1, -1, 0},  // z = y
382                                       }})
383                    .isIntegerEmpty());
384 
385   // FlatAffineConstraints::isEmpty() does not detect the following sets to be
386   // empty.
387 
388   // 3x + 7y = 1 and 0 <= x, y <= 10.
389   // Since x and y are non-negative, 3x + 7y can never be 1.
390   EXPECT_TRUE(
391       makeFACFromConstraints(
392           2, {{1, 0, 0}, {-1, 0, 10}, {0, 1, 0}, {0, -1, 10}}, {{3, 7, -1}})
393           .isIntegerEmpty());
394 
395   // 2x = 3y and y = x - 1 and x + y = 6z + 2 and 0 <= x, y <= 100.
396   // Substituting y = x - 1 in 3y = 2x, we obtain x = 3 and hence y = 2.
397   // Since x + y = 5 cannot be equal to 6z + 2 for any z, the set is empty.
398   EXPECT_TRUE(
399       makeFACFromConstraints(3,
400                              {
401                                  {1, 0, 0, 0},
402                                  {-1, 0, 0, 100},
403                                  {0, 1, 0, 0},
404                                  {0, -1, 0, 100},
405                              },
406                              {{2, -3, 0, 0}, {1, -1, 0, -1}, {1, 1, -6, -2}})
407           .isIntegerEmpty());
408 
409   // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100.
410   // 2x = 3y implies x is a multiple of 3 and y is even.
411   // Now y = x - 1 + 6z implies y = 2 mod 3. In fact, since y is even, we have
412   // y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying
413   // x + y = 5 mod 6, which contradicts x + y = 6q + 2, so the set is empty.
414   EXPECT_TRUE(makeFACFromConstraints(
415                   4,
416                   {
417                       {1, 0, 0, 0, 0},
418                       {-1, 0, 0, 0, 100},
419                       {0, 1, 0, 0, 0},
420                       {0, -1, 0, 0, 100},
421                   },
422                   {{2, -3, 0, 0, 0}, {1, -1, 6, 0, -1}, {1, 1, 0, -6, -2}})
423                   .isIntegerEmpty());
424 
425   // Set with symbols.
426   FlatAffineConstraints fac6 = makeFACFromConstraints(2,
427                                                       {
428                                                           {1, 1, 0},
429                                                       },
430                                                       {
431                                                           {1, -1, 0},
432                                                       },
433                                                       1);
434   EXPECT_FALSE(fac6.isIntegerEmpty());
435 }
436 
437 TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) {
438   FlatAffineConstraints fac = makeFACFromConstraints(1,
439                                                      {
440                                                          {1, -2}, // x >= 2.
441                                                          {-1, 2}  // x <= 2.
442                                                      },
443                                                      {{1, -2}}); // x == 2.
444   fac.removeRedundantConstraints();
445 
446   // Both inequalities are redundant given the equality. Both have been removed.
447   EXPECT_EQ(fac.getNumInequalities(), 0u);
448   EXPECT_EQ(fac.getNumEqualities(), 1u);
449 
450   FlatAffineConstraints fac2 =
451       makeFACFromConstraints(2,
452                              {
453                                  {1, 0, -3}, // x >= 3.
454                                  {0, 1, -2}  // y >= 2 (redundant).
455                              },
456                              {{1, -1, 0}}); // x == y.
457   fac2.removeRedundantConstraints();
458 
459   // The second inequality is redundant and should have been removed. The
460   // remaining inequality should be the first one.
461   EXPECT_EQ(fac2.getNumInequalities(), 1u);
462   EXPECT_THAT(fac2.getInequality(0), testing::ElementsAre(1, 0, -3));
463   EXPECT_EQ(fac2.getNumEqualities(), 1u);
464 
465   FlatAffineConstraints fac3 =
466       makeFACFromConstraints(3, {},
467                              {{1, -1, 0, 0},   // x == y.
468                               {1, 0, -1, 0},   // x == z.
469                               {0, 1, -1, 0}}); // y == z.
470   fac3.removeRedundantConstraints();
471 
472   // One of the three equalities can be removed.
473   EXPECT_EQ(fac3.getNumInequalities(), 0u);
474   EXPECT_EQ(fac3.getNumEqualities(), 2u);
475 
476   FlatAffineConstraints fac4 = makeFACFromConstraints(
477       17,
478       {{0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
479        {0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 500},
480        {0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
481        {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
482        {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998},
483        {0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15},
484        {0, 0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
485        {0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
486        {0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998},
487        {0, 0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15},
488        {0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
489        {0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1},
490        {0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1},
491        {0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 500},
492        {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 16, 0, 0, 0, 0, 0, 15},
493        {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -16, 0, 0, 0, 0, 0, 0},
494        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -16, 0, 1, 0, 0, 0},
495        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1},
496        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 998},
497        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16, 0, -1, 0, 0, 15},
498        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0},
499        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 1},
500        {0, 0, 0, 0, 0, 0, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8},
501        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, 8, 8},
502        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, -8, -1},
503        {0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, -8, -1},
504        {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0},
505        {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0},
506        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, -10},
507        {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 10},
508        {0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, -13},
509        {0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 13},
510        {0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -10},
511        {0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10},
512        {1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -13},
513        {-1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 13}},
514       {});
515 
516   // The above is a large set of constraints without any redundant constraints,
517   // as verified by the Fourier-Motzkin based removeRedundantInequalities.
518   unsigned nIneq = fac4.getNumInequalities();
519   unsigned nEq = fac4.getNumEqualities();
520   fac4.removeRedundantInequalities();
521   ASSERT_EQ(fac4.getNumInequalities(), nIneq);
522   ASSERT_EQ(fac4.getNumEqualities(), nEq);
523   // Now we test that removeRedundantConstraints does not find any constraints
524   // to be redundant either.
525   fac4.removeRedundantConstraints();
526   EXPECT_EQ(fac4.getNumInequalities(), nIneq);
527   EXPECT_EQ(fac4.getNumEqualities(), nEq);
528 
529   FlatAffineConstraints fac5 =
530       makeFACFromConstraints(2,
531                              {
532                                  {128, 0, 127}, // [0]: 128x >= -127.
533                                  {-1, 0, 7},    // [1]: x <= 7.
534                                  {-128, 1, 0},  // [2]: y >= 128x.
535                                  {0, 1, 0}      // [3]: y >= 0.
536                              },
537                              {});
538   // [0] implies that 128x >= 0, since x has to be an integer. (This should be
539   // caught by GCDTightenInqualities().)
540   // So [2] and [0] imply [3] since we have y >= 128x >= 0.
541   fac5.removeRedundantConstraints();
542   EXPECT_EQ(fac5.getNumInequalities(), 3u);
543   SmallVector<int64_t, 8> redundantConstraint = {0, 1, 0};
544   for (unsigned i = 0; i < 3; ++i) {
545     // Ensure that the removed constraint was the redundant constraint [3].
546     EXPECT_NE(fac5.getInequality(i), ArrayRef<int64_t>(redundantConstraint));
547   }
548 }
549 
550 TEST(FlatAffineConstraintsTest, addConstantUpperBound) {
551   FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {});
552   fac.addConstantUpperBound(0, 1);
553   EXPECT_EQ(fac.atIneq(0, 0), -1);
554   EXPECT_EQ(fac.atIneq(0, 1), 0);
555   EXPECT_EQ(fac.atIneq(0, 2), 1);
556 
557   fac.addConstantUpperBound({1, 2, 3}, 1);
558   EXPECT_EQ(fac.atIneq(1, 0), -1);
559   EXPECT_EQ(fac.atIneq(1, 1), -2);
560   EXPECT_EQ(fac.atIneq(1, 2), -2);
561 }
562 
563 TEST(FlatAffineConstraintsTest, addConstantLowerBound) {
564   FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {});
565   fac.addConstantLowerBound(0, 1);
566   EXPECT_EQ(fac.atIneq(0, 0), 1);
567   EXPECT_EQ(fac.atIneq(0, 1), 0);
568   EXPECT_EQ(fac.atIneq(0, 2), -1);
569 
570   fac.addConstantLowerBound({1, 2, 3}, 1);
571   EXPECT_EQ(fac.atIneq(1, 0), 1);
572   EXPECT_EQ(fac.atIneq(1, 1), 2);
573   EXPECT_EQ(fac.atIneq(1, 2), 2);
574 }
575 
576 TEST(FlatAffineConstraintsTest, clearConstraints) {
577   FlatAffineConstraints fac = makeFACFromConstraints(1, {}, {});
578 
579   fac.addInequality({1, 0});
580   EXPECT_EQ(fac.atIneq(0, 0), 1);
581   EXPECT_EQ(fac.atIneq(0, 1), 0);
582 
583   fac.clearConstraints();
584 
585   fac.addInequality({1, 0});
586   EXPECT_EQ(fac.atIneq(0, 0), 1);
587   EXPECT_EQ(fac.atIneq(0, 1), 0);
588 }
589 
590 } // namespace mlir
591