[MLIR] rewrite AffineStructures and Presburger tests to use the parser

[Dinistro]

Summary

This commit rewrites most existing unittests involving FlatAffineConstraints to use the parsing utility. This helps to make the tests more understandable.

[Dinistro]

mlir/unittests/Analysis/AffineStructuresTest.cpp

163

Do you guys think that it makes sense to write these down as one constraint per line?

519

This is not actually related to this patch, should I remove these changes?

574

The parser can only introduce divisions if they actually show up in a constraint. Should I add a constraint that introduces these divisions or should we just drop that TODO?

mlir/unittests/Analysis/PresburgerSetTest.cpp

376–379

Alternatively, I could add a function that just takes a list of StringRefs which are all parsed and unioned.

[arjunp]

Thanks for the patch!

mlir/unittests/Analysis/AffineStructuresTest.cpp

163

Not sure, but at the very least it would be helpful to not break any single constraint across multiple lines.

519

I guess ideally yes. Not sure how much it matters.

574

I think you can use the parser with some dummy constraint here. We should be careful that it doesn't change the representation. (Adding a tighter constraint can change the returned numerator's constant term.) I think constraining each div to be greater than equal to zero would be good. Not sure if this works for nested divisions though; if there are any such cases we can leave them as is for now.

mlir/unittests/Analysis/PresburgerSetTest.cpp

376–379

Yeah, I think that would be helpful.

[Dinistro]

Change strings to not break constraints over multiple lines

[Dinistro]

mlir/unittests/Analysis/AffineStructuresTest.cpp

574

This does unfortunately not work as we want it to.

The internal representation of fac looks as follows:

Constraints (1 dims, 0 symbols, 2 locals), (4 constraints)
(None None None  const)
1 -10 0 4 >= 0
-1 10 0 5 >= 0
1 0 -10 100 >= 0
-1 0 10 -91 >= 0

But parsing, for example, "(x) : ((x + 4) floordiv 10 == 0, (x + 100) floordiv 10 == 0)" yields the following representation:

Constraints (1 dims, 0 symbols, 2 locals), (6 constraints)
(None None None  const)
0 1 0 0 = 0
0 0 1 10 = 0
1 -10 0 4 >= 0
-1 10 0 5 >= 0
1 0 -10 0 >= 0
-1 0 10 9 >= 0

I'm not sure what changes the representation of the divisions, but this does break the test.

Did I do something wrong or is this indeed a simplification the parser does?

[Dinistro]

Add example of a helper to parse a list of FAC strings.

[Dinistro]

mlir/unittests/Analysis/PresburgerSetTest.cpp

376–379

I added an example of such a helper function. Is this what you expected?

[arjunp]

mlir/unittests/Analysis/AffineStructuresTest.cpp

574

Yes, I think this is indeed something done by the parser. Maybe @Groverkss can confirm, but I don't think we have such simplifications anywhere else yet. I would just leave the division stuff out for now then.

In the future we will implement such simplifications internally as well, and we would want to keep these tests as is so that we can test that functionality I guess.

mlir/unittests/Analysis/PresburgerSetTest.cpp

376–379

Yes, exactly.

[Dinistro]

Use the Presburger parsing helper function for all PresburgerSet creations.

[Groverkss]

LGTM. I would wait for others to accept in case they have any remaining concerns.

mlir/unittests/Analysis/AffineStructuresTest.cpp

574

We do not have such simplifications. It's the parser that does these.

I think it's better to not use the parser here. I don't think the parser will put the divisions in the order we want them to and it may become more confusing. You can drop the TODO according to me.

[Dinistro]

Drop outdated TODO

[arjunp]

LGTM, please fix the minor comment issues below.

mlir/unittests/Analysis/AffineStructuresTest.cpp

182–188

Please add back the comment above.

// Same thing with some spurious extra dimensions equated to constants.

506–508

These comments don't make sense anymore. I would replace the [0], [1] etc. by the actual constraints.

mlir/unittests/Analysis/PresburgerSetTest.cpp

522–523

This outdated comment can be removed now.

[Dinistro]

Address remaining comments.

[arjunp]

Thanks a lot for this patch!

[mehdi_amini]

Sorry: I had to revert because this broke the ASAN/UBSAN CI (see the trace in the revert commit message(

[arjunp]

mlir/unittests/Analysis/AffineStructuresTest.cpp

222

The mutated test case is too big to be computed with 64-bits, I believe that's why I initially chose this number of digits for this test case. I can't believe I manually checked the patch and still missed this

[Dinistro]

• Fix coefficient that caused UB.

[Dinistro]

Im sorry for this problem.
Thanks for pointing out the issue, should be fixed now.

mlir/unittests/Analysis/AffineStructuresTest.cpp

TEST(FlatAffineConstraintsTest, FindSampleTest) {
   // Bounded sets with only inequalities.
 
   MLIRContext context;
 
   // 0 <= 7x <= 5
   checkSample(true, parseFAC("(x) : (7 * x >= 0, -7 * x + 5 >= 0)", &context));
 
   // 1 <= 5x and 5x <= 4 (no solution).
-  checkSample(false, makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}));
+  checkSample(false,
+              parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)", &context));
 
   // 1 <= 5x and 5x <= 9 (solution: x = 1).
-  checkSample(true, makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}));
+  checkSample(true,
+              parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)", &context));
 
   // Bounded sets with equalities.
   // x >= 8 and 40 >= y and x = y.
-  checkSample(
-      true, makeFACFromConstraints(2, {{1, 0, -8}, {0, -1, 40}}, {{1, -1, 0}}));
+  checkSample(true, parseFAC("(x,y) : (x - 8 >= 0, -y + 40 >= 0, x - y == 0)",
+                             &context));
 
   // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z.
   // solution: x = y = z = 10.
-  checkSample(true, makeFACFromConstraints(
-                        3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -10}},
-                        {{1, 2, -3, 0}}));
+  checkSample(true, parseFAC("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, "
+                             "z - 10 >= 0, x + 2 * y - 3 * z == 0)",
+                             &context));
 
   // x <= 10 and y <= 10 and 11 <= z and x + 2y = 3z.
   // This implies x + 2y >= 33 and x + 2y <= 30, which has no solution.
-  checkSample(false, makeFACFromConstraints(
-                         3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -11}},
-                         {{1, 2, -3, 0}}));
+  checkSample(false, parseFAC("(x,y,z) : (-x + 10 >= 0, -y + 10 >= 0, "
+                              "z - 11 >= 0, x + 2 * y - 3 * z == 0)",
+                              &context));
 
   // 0 <= r and r <= 3 and 4q + r = 7.
   // Solution: q = 1, r = 3.
-  checkSample(true,
-              makeFACFromConstraints(2, {{0, 1, 0}, {0, -1, 3}}, {{4, 1, -7}}));
+  checkSample(
+      true,
+      parseFAC("(q,r) : (r >= 0, -r + 3 >= 0, 4 * q + r - 7 == 0)", &context));
 
   // 4q + r = 7 and r = 0.
   // Solution: q = 1, r = 3.
-  checkSample(false, makeFACFromConstraints(2, {}, {{4, 1, -7}, {0, 1, 0}}));
+  checkSample(false,
+              parseFAC("(q,r) : (4 * q + r - 7 == 0, r == 0)", &context));
 
   // The next two sets are large sets that should take a long time to sample
   // with a naive branch and bound algorithm but can be sampled efficiently with
   // the GBR algorithm.
   //
   // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (10000, 10000).
-  checkSample(
-      true,
-      makeFACFromConstraints(
-          2, {{0, 1, 0}, {300000, -299999, -100000}, {-300000, 299998, 200000}},
-          {}));
+  checkSample(true, parseFAC("(x,y) : (y >= 0, "
+                             "300000 * x - 299999 * y - 100000 >= 0, "
+                             "-300000 * x + 299998 * y + 200000 >= 0)",
+                             &context));
 
   // This is a tetrahedron with vertices at
   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
   // The first three points form a triangular base on the xz plane with the
   // apex at the fourth point, which is the only integer point.
   checkPermutationsSample(
       true, 3,
       {
           {0, 1, 0, 0},  // y >= 0
           {0, -1, 1, 0}, // z >= y
           {300000, -299998, -1,
            -100000},                    // -300000x + 299998y + 100000 + z <= 0.
           {-150000, 149999, 0, 100000}, // -150000x + 149999y + 100000 >= 0.
       },
       {});
 
-  // Same thing with some spurious extra dimensions equated to constants.
-  checkSample(true,
-              makeFACFromConstraints(
-                  5,
-                  {
-                      {0, 1, 0, 1, -1, 0},
-                      {0, -1, 1, -1, 1, 0},
-                      {300000, -299998, -1, -9, 21, -112000},
-                      {-150000, 149999, 0, -15, 47, 68000},
-                  },
-                  {{0, 0, 0, 1, -1, 0},       // p = q.
-                   {0, 0, 0, 1, 1, -2000}})); // p + q = 20000 => p = q = 10000.
+  checkSample(
+      true,
+      parseFAC("(a,b,c,d,e) : (b + d - e >= 0, -b + c - d + e >= 0, "
+               "300000 * a - 299998 * b - c - 9 * d + 21 * e - 112000 >= 0, "
+               "-150000 * a + 149999 * b - 15 * d + 47 * e + 68000 >= 0, "
+               "d - e == 0, d + e - 2000 == 0)",
+               &context));
 
   // This is a tetrahedron with vertices at
   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100).
   checkPermutationsSample(false, 3,
                           {
                               {0, 1, 0, 0},
                               {0, -300, 299, 0},
                               {300 * 299, -89400, -299, -100 * 299},
                               {-897, 894, 0, 598},
                           },
                           {});
 
   // Two tests involving equalities that are integer empty but not rational
   // empty.
 
   // This is a line segment from (0, 1/3) to (100, 100 + 1/3).
-  checkSample(false, makeFACFromConstraints(
-                         2,
-                         {
-                             {1, 0, 0},   // x >= 0.
-                             {-1, 0, 100} // -x + 100 >= 0, i.e., x <= 100.
-                         },
-                         {
-                             {3, -3, 1} // 3x - 3y + 1 = 0, i.e., y = x + 1/3.
-                         }));
+  checkSample(
+      false, parseFAC("(x,y) : (x >= 0, -x + 100 >= 0, 3 * x - 3 * y + 1 == 0)",
+                      &context));
 
   // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3.
-  checkSample(false, makeFACFromConstraints(2,
-                                            {
-                                                {1, 0, 0},    // x >= 0.
-                                                {-1, 0, 100}, // x <= 100.
-                                                {3, -3, 2},   // 3x - 3y >= -2.
-                                                {-3, 3, -1},  // 3x - 3y <= -1.
-                                            },
-                                            {}));
+  checkSample(false,
+              parseFAC("(x,y) : (x >= 0, -x + 100 >= 0, "
+                       "3 * x - 3 * y + 2 >= 0, -3 * x + 3 * y - 1 >= 0)",
+                       &context));
+
+  checkSample(true, parseFAC("(x,y) : (2 * x >= 0, -2 * x + 99 >= 0, "
+                             "2 * y >= 0, -2 * y + 99 >= 0)",
+                             &context));
 
-  checkSample(true, makeFACFromConstraints(2,
-                                           {
-                                               {2, 0, 0},   // 2x >= 1.
-                                               {-2, 0, 99}, // 2x <= 99.
-                                               {0, 2, 0},   // 2y >= 0.
-                                               {0, -2, 99}, // 2y <= 99.
-                                           },
-                                           {}));
   // 2D cone with apex at (10000, 10000) and
   // edges passing through (1/3, 0) and (2/3, 0).
-  checkSample(
-      true,
-      makeFACFromConstraints(
-          2, {{300000, -299999, -100000}, {-300000, 299998, 200000}}, {}));
+  checkSample(true, parseFAC("(x,y) : (300000 * x - 299999 * y - 100000 >= 0, "
+                             "-300000 * x + 2999998 * y + 200000 >= 0)",
+                             &context));
 
   // Cartesian product of a tetrahedron and a 2D cone.
   // The tetrahedron has vertices at
   // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
   // The first three points form a triangular base on the xz plane with the
   // apex at the fourth point, which is the only integer point.
   // The cone has apex at (10000, 10000) and
   // edges passing through (1/3, 0) and (2/3, 0).
checkPermutationsSample(false /* empty */, 5,
                               // Second set constraints:
                               // 3p >= 1
                               {0, 0, 0, 3, 0, -1},
                               // 3p <= 2
                               {0, 0, 0, -3, 0, 2},
                           },
                           {});
 
-  checkSample(true, makeFACFromConstraints(3,
-                                           {
-                                               {2, 0, 0, -1}, // 2x >= 1
-                                           },
-                                           {{
-                                               {1, -1, 0, -1}, // y = x - 1
-                                               {0, 1, -1, 0},  // z = y
-                                           }}));
+  checkSample(true, parseFAC("(x, y, z) : (2 * x - 1 >= 0, x - y - 1 == 0, "
+                             "y - z == 0)",
+                             &context));
 
   // Regression tests for the computation of dual coefficients.
   checkSample(false, parseFAC("(x, y, z) : ("
                               "6*x - 4*y + 9*z + 2 >= 0,"
                               "x + 5*y + z + 5 >= 0,"
                               "-4*x + y + 2*z - 1 >= 0,"
                               "-3*x - 2*y - 7*z - 1 >= 0,"
                               "-7*x - 5*y - 9*z - 1 >= 0)",
                               &context));
   checkSample(true, parseFAC("(x, y, z) : ("
                              "3*x + 3*y + 3 >= 0,"
                              "-4*x - 8*y - z + 4 >= 0,"
                              "-7*x - 4*y + z + 1 >= 0,"
                              "2*x - 7*y - 8*z - 7 >= 0,"
                              "9*x + 8*y - 9*z - 7 >= 0)",
                              &context));
 }
 
 TEST(FlatAffineConstraintsTest, IsIntegerEmptyTest) {
+
+  MLIRContext context;
+
   // 1 <= 5x and 5x <= 4 (no solution).
-  EXPECT_TRUE(
-      makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}).isIntegerEmpty());
+  EXPECT_TRUE(parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 4 >= 0)", &context)
+                  .isIntegerEmpty());
   // 1 <= 5x and 5x <= 9 (solution: x = 1).
-  EXPECT_FALSE(
-      makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}).isIntegerEmpty());
+  EXPECT_FALSE(parseFAC("(x) : (5 * x - 1 >= 0, -5 * x + 9 >= 0)", &context)
+                   .isIntegerEmpty());
 
   // Unbounded sets.
-  EXPECT_TRUE(makeFACFromConstraints(3,
-                                     {
-                                         {0, 2, 0, -1}, // 2y >= 1
-                                         {0, -2, 0, 1}, // 2y <= 1
-                                         {0, 0, 2, -1}, // 2z >= 1
-                                     },
-                                     {{2, 0, 0, -1}} // 2x = 1
-                                     )
+  EXPECT_TRUE(parseFAC("(x,y,z) : (2 * y - 1 >= 0, -2 * y + 1 >= 0, "
+                       "2 * z - 1 >= 0, 2 * x - 1 == 0)",
+                       &context)
                   .isIntegerEmpty());
 
-  EXPECT_FALSE(makeFACFromConstraints(3,
-                                      {
-                                          {2, 0, 0, -1},  // 2x >= 1
-                                          {-3, 0, 0, 3},  // 3x <= 3
-                                          {0, 0, 5, -6},  // 5z >= 6
-                                          {0, 0, -7, 17}, // 7z <= 17
-                                          {0, 3, 0, -2},  // 3y >= 2
-                                      },
-                                      {})
+  EXPECT_FALSE(parseFAC("(x,y,z) : (2 * x - 1 >= 0, -3 * x + 3 >= 0, "
+                        "5 * z - 6 >= 0, -7 * z + 17 >= 0, 3 * y - 2 >= 0)",
+                        &context)
                    .isIntegerEmpty());
 
-  EXPECT_FALSE(makeFACFromConstraints(3,
-                                      {
-                                          {2, 0, 0, -1}, // 2x >= 1
-                                      },
-                                      {{
-                                          {1, -1, 0, -1}, // y = x - 1
-                                          {0, 1, -1, 0},  // z = y
-                                      }})
-                   .isIntegerEmpty());
+  EXPECT_FALSE(
+      parseFAC("(x,y,z) : (2 * x - 1 >= 0, x - y - 1 == 0, y - z == 0)",
+               &context)
 
   // FlatAffineConstraints::isEmpty() does not detect the following sets to be
   // empty.
 
   // 3x + 7y = 1 and 0 <= x, y <= 10.
   // Since x and y are non-negative, 3x + 7y can never be 1.
-  EXPECT_TRUE(
-      makeFACFromConstraints(
-          2, {{1, 0, 0}, {-1, 0, 10}, {0, 1, 0}, {0, -1, 10}}, {{3, 7, -1}})
+  EXPECT_TRUE(parseFAC("(x,y) : (x >= 0, -x + 10 >= 0, y >= 0, -y + 10 >= 0, "
+                       "3 * x + 7 * y - 1 == 0)",
+                       &context)
                   .isIntegerEmpty());
 
   // 2x = 3y and y = x - 1 and x + y = 6z + 2 and 0 <= x, y <= 100.
   // Substituting y = x - 1 in 3y = 2x, we obtain x = 3 and hence y = 2.
   // Since x + y = 5 cannot be equal to 6z + 2 for any z, the set is empty.
   EXPECT_TRUE(
-      makeFACFromConstraints(3,
-                             {
-                                 {1, 0, 0, 0},
-                                 {-1, 0, 0, 100},
-                                 {0, 1, 0, 0},
-                                 {0, -1, 0, 100},
-                             },
-                             {{2, -3, 0, 0}, {1, -1, 0, -1}, {1, 1, -6, -2}})
+      parseFAC("(x,y,z) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, "
+               "2 * x - 3 * y == 0, x - y - 1 == 0, x + y - 6 * z - 2 == 0)",
+               &context)
           .isIntegerEmpty());
 
   // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100.
   // 2x = 3y implies x is a multiple of 3 and y is even.
   // Now y = x - 1 + 6z implies y = 2 mod 3. In fact, since y is even, we have
   // y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying
   // x + y = 5 mod 6, which contradicts x + y = 6q + 2, so the set is empty.
-  EXPECT_TRUE(makeFACFromConstraints(
-                  4,
-                  {
-                      {1, 0, 0, 0, 0},
-                      {-1, 0, 0, 0, 100},
-                      {0, 1, 0, 0, 0},
-                      {0, -1, 0, 0, 100},
-                  },
-                  {{2, -3, 0, 0, 0}, {1, -1, 6, 0, -1}, {1, 1, 0, -6, -2}})
-                  .isIntegerEmpty());
+  EXPECT_TRUE(
+      parseFAC(
+          "(x,y,z,q) : (x >= 0, -x + 100 >= 0, y >= 0, -y + 100 >= 0, "
+          "2 * x - 3 * y == 0, x - y + 6 * z - 1 == 0, x + y - 6 * q - 2 == 0)",
+          &context)
 
   // Set with symbols.
-  FlatAffineConstraints fac6 = makeFACFromConstraints(2,
-                                                      {
-                                                          {1, 1, 0},
-                                                      },
-                                                      {
-                                                          {1, -1, 0},
-                                                      },
-                                                      1);
-  EXPECT_FALSE(fac6.isIntegerEmpty());
+  EXPECT_FALSE(
+      parseFAC("(x)[s] : (x + s >= 0, x - s == 0)", &context).isIntegerEmpty());
 }
 
 TEST(FlatAffineConstraintsTest, removeRedundantConstraintsTest) {
-  FlatAffineConstraints fac = makeFACFromConstraints(1,
-                                                     {
-                                                         {1, -2}, // x >= 2.
-                                                         {-1, 2}  // x <= 2.
-                                                     },
-                                                     {{1, -2}}); // x == 2.
+  MLIRContext context;
+
+  FlatAffineConstraints fac =
+      parseFAC("(x) : (x - 2 >= 0, -x + 2 >= 0, x - 2 == 0)", &context);
   fac.removeRedundantConstraints();
 
   // Both inequalities are redundant given the equality. Both have been removed.
   EXPECT_EQ(fac.getNumInequalities(), 0u);
   EXPECT_EQ(fac.getNumEqualities(), 1u);
 
   FlatAffineConstraints fac2 =
-      makeFACFromConstraints(2,
-                             {
-                                 {1, 0, -3}, // x >= 3.
-                                 {0, 1, -2}  // y >= 2 (redundant).
-                             },
-                             {{1, -1, 0}}); // x == y.
+      parseFAC("(x,y) : (x - 3 >= 0, y - 2 >= 0, x - y == 0)", &context);
   fac2.removeRedundantConstraints();
 
   // The second inequality is redundant and should have been removed. The
   // remaining inequality should be the first one.
   EXPECT_EQ(fac2.getNumInequalities(), 1u);
   EXPECT_THAT(fac2.getInequality(0), ElementsAre(1, 0, -3));
   EXPECT_EQ(fac2.getNumEqualities(), 1u);
 
   FlatAffineConstraints fac3 =
-      makeFACFromConstraints(3, {},
-                             {{1, -1, 0, 0},   // x == y.
-                              {1, 0, -1, 0},   // x == z.
-                              {0, 1, -1, 0}}); // y == z.
+      parseFAC("(x,y,z) : (x - y == 0, x - z == 0, y - z == 0)", &context);
   fac3.removeRedundantConstraints();
 
   // One of the three equalities can be removed.
   EXPECT_EQ(fac3.getNumInequalities(), 0u);
   EXPECT_EQ(fac3.getNumEqualities(), 2u);
 
-  FlatAffineConstraints fac4 = makeFACFromConstraints(
-      17,
-      {{0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
-       {0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 500},
-       {0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
-       {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
-       {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998},
-       {0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15},
-       {0, 0, 0, 0, -16, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
-       {0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1},
-       {0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 998},
-       {0, 0, 0, 0, 16, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 15},
-       {0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0},
-       {0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 500},
-       {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 16, 0, 0, 0, 0, 0, 15},
-       {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -16, 0, 0, 0, 0, 0, 0},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -16, 0, 1, 0, 0, 0},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 998},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16, 0, -1, 0, 0, 15},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 1},
-       {0, 0, 0, 0, 0, 0, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, 8, 8},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, -8, -1},
-       {0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, -8, -1},
-       {0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0},
-       {0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, -10},
-       {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 10},
-       {0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, -13},
-       {0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 13},
-       {0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -10},
-       {0, 0, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10},
-       {1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -13},
-       {-1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 13}},
-      {});
+  FlatAffineConstraints fac4 =
+      parseFAC("(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) : ("
+               "b - 1 >= 0,"
+               "-b + 500 >= 0,"
+               "-16 * d + f >= 0,"
+               "f - 1 >= 0,"
+               "-f + 998 >= 0,"
+               "16 * d - f + 15 >= 0,"
+               "-16 * e + g >= 0,"
+               "g - 1 >= 0,"
+               "-g + 998 >= 0,"
+               "16 * e - g + 15 >= 0,"
+               "h >= 0,"
+               "-h + 1 >= 0,"
+               "j - 1 >= 0,"
+               "-j + 500 >= 0,"
+               "-f + 16 * l + 15 >= 0,"
+               "f - 16 * l >= 0,"
+               "-16 * m + o >= 0,"
+               "o - 1 >= 0,"
+               "-o + 998 >= 0,"
+               "16 * m - o + 15 >= 0,"
+               "p >= 0,"
+               "-p + 1 >= 0,"
+               "-g - h + 8 * q + 8 >= 0,"
+               "-o - p + 8 * q + 8 >= 0,"
+               "o + p - 8 * q - 1 >= 0,"
+               "g + h - 8 * q - 1 >= 0,"
+               "-f + n >= 0,"
+               "f - n >= 0,"
+               "k - 10 >= 0,"
+               "-k + 10 >= 0,"
+               "i - 13 >= 0,"
+               "-i + 13 >= 0,"
+               "c - 10 >= 0,"
+               "-c + 10 >= 0,"
+               "a - 13 >= 0,"
+               "-a + 13 >= 0"
+               ")",
+               &context);
 
   // The above is a large set of constraints without any redundant constraints,
   // as verified by the Fourier-Motzkin based removeRedundantInequalities.
   unsigned nIneq = fac4.getNumInequalities();
   unsigned nEq = fac4.getNumEqualities();
   fac4.removeRedundantInequalities();
   ASSERT_EQ(fac4.getNumInequalities(), nIneq);
   ASSERT_EQ(fac4.getNumEqualities(), nEq);
   // Now we test that removeRedundantConstraints does not find any constraints
   // to be redundant either.
   fac4.removeRedundantConstraints();
   EXPECT_EQ(fac4.getNumInequalities(), nIneq);
   EXPECT_EQ(fac4.getNumEqualities(), nEq);
 
-  FlatAffineConstraints fac5 =
-      makeFACFromConstraints(2,
-                             {
-                                 {128, 0, 127}, // [0]: 128x >= -127.
-                                 {-1, 0, 7},    // [1]: x <= 7.
-                                 {-128, 1, 0},  // [2]: y >= 128x.
-                                 {0, 1, 0}      // [3]: y >= 0.
-                             },
-                             {});
+  FlatAffineConstraints fac5 = parseFAC(
+      "(x,y) : (128 * x + 127 >= 0, -x + 7 >= 0, -128 * x + y >= 0, y >= 0)",
+      &context);
   // [0] implies that 128x >= 0, since x has to be an integer. (This should be
   // caught by GCDTightenInqualities().)
   // So [2] and [0] imply [3] since we have y >= 128x >= 0.
   fac5.removeRedundantConstraints();
   EXPECT_EQ(fac5.getNumInequalities(), 3u);
   SmallVector<int64_t, 8> redundantConstraint = {0, 1, 0};
   for (unsigned i = 0; i < 3; ++i) {
     // Ensure that the removed constraint was the redundant constraint [3].
     EXPECT_NE(fac5.getInequality(i), ArrayRef<int64_t>(redundantConstraint));
   }
 }
 
 TEST(FlatAffineConstraintsTest, addConstantUpperBound) {
-  FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {});
+  FlatAffineConstraints fac(2);
   fac.addBound(FlatAffineConstraints::UB, 0, 1);
   EXPECT_EQ(fac.atIneq(0, 0), -1);
   EXPECT_EQ(fac.atIneq(0, 1), 0);
   EXPECT_EQ(fac.atIneq(0, 2), 1);
 
   fac.addBound(FlatAffineConstraints::UB, {1, 2, 3}, 1);
   EXPECT_EQ(fac.atIneq(1, 0), -1);
   EXPECT_EQ(fac.atIneq(1, 1), -2);
   EXPECT_EQ(fac.atIneq(1, 2), -2);
 }
 
 TEST(FlatAffineConstraintsTest, addConstantLowerBound) {
-  FlatAffineConstraints fac = makeFACFromConstraints(2, {}, {});
+  FlatAffineConstraints fac(2);
   fac.addBound(FlatAffineConstraints::LB, 0, 1);
   EXPECT_EQ(fac.atIneq(0, 0), 1);
   EXPECT_EQ(fac.atIneq(0, 1), 0);
   EXPECT_EQ(fac.atIneq(0, 2), -1);
 
   fac.addBound(FlatAffineConstraints::LB, {1, 2, 3}, 1);
   EXPECT_EQ(fac.atIneq(1, 0), 1);
   EXPECT_EQ(fac.atIneq(1, 1), 2);
static void checkDivisionRepresentation(
   // denominator for a division is zero, we ignore its dividend.
   EXPECT_TRUE(dividends.size() == expectedDividends.size());
   for (unsigned i = 0, e = dividends.size(); i < e; ++i)
     if (denominators[i] != 0)
       EXPECT_TRUE(expectedDividends[i] == dividends[i]);
 }
 
 TEST(FlatAffineConstraintsTest, computeLocalReprSimple) {
-  FlatAffineConstraints fac = makeFACFromConstraints(1, {}, {});
+  FlatAffineConstraints fac(1);
 
+  // TODO do this with the parser
   fac.addLocalFloorDiv({1, 4}, 10);
   fac.addLocalFloorDiv({1, 0, 100}, 10);
 
   std::vector<SmallVector<int64_t, 8>> divisions = {{1, 0, 0, 4},
                                                     {1, 0, 0, 100}};
   SmallVector<unsigned, 8> denoms = {10, 10};
 
   // Check if floordivs can be computed when no other inequalities exist
   // and floor divs do not depend on each other.
   checkDivisionRepresentation(fac, divisions, denoms);
 }
 
 TEST(FlatAffineConstraintsTest, computeLocalReprConstantFloorDiv) {
-  FlatAffineConstraints fac = makeFACFromConstraints(4, {}, {});
+  FlatAffineConstraints fac(4);
 
   fac.addInequality({1, 0, 3, 1, 2});
   fac.addInequality({1, 2, -8, 1, 10});
   fac.addEquality({1, 2, -4, 1, 10});
 
   fac.addLocalFloorDiv({0, 0, 0, 0, 10}, 30);
   fac.addLocalFloorDiv({0, 0, 0, 0, 0, 99}, 101);
 
   std::vector<SmallVector<int64_t, 8>> divisions = {{0, 0, 0, 0, 0, 0, 10},
                                                     {0, 0, 0, 0, 0, 0, 99}};
   SmallVector<unsigned, 8> denoms = {30, 101};
 
   // Check if floordivs with constant numerator can be computed.
   checkDivisionRepresentation(fac, divisions, denoms);
 }
 
 TEST(FlatAffineConstraintsTest, computeLocalReprRecursive) {
-  FlatAffineConstraints fac = makeFACFromConstraints(4, {}, {});
+  FlatAffineConstraints fac(4);
   fac.addInequality({1, 0, 3, 1, 2});
   fac.addInequality({1, 2, -8, 1, 10});
   fac.addEquality({1, 2, -4, 1, 10});
 
   fac.addLocalFloorDiv({0, -2, 7, 2, 10}, 3);
   fac.addLocalFloorDiv({3, 0, 9, 2, 2, 10}, 5);
   fac.addLocalFloorDiv({0, 1, -123, 2, 0, -4, 10}, 3);
 

mlir/unittests/Analysis/PresburgerSetTest.cpp

 static FlatAffineConstraints parseFAC(StringRef str, MLIRContext *context) {
   FailureOr<FlatAffineConstraints> fac = parseIntegerSetToFAC(str, context);
 
   EXPECT_TRUE(succeeded(fac));
 
   return *fac;
 }
 
+static PresburgerSet parsePresburgerSetFromFACStrings(unsigned numDims,
+                                                      ArrayRef<StringRef> strs,
+                                                      MLIRContext *context) {
+  PresburgerSet set = PresburgerSet::getEmptySet(numDims);
+  for (StringRef str : strs)
+    set.unionFACInPlace(parseFAC(str, context));
+  return set;
+}
+
 /// Compute the union of s and t, and check that each of the given points
 /// belongs to the union iff it belongs to at least one of s and t.
 static void testUnionAtPoints(PresburgerSet s, PresburgerSet t,
                               ArrayRef<SmallVector<int64_t, 4>> points) {
   PresburgerSet unionSet = s.unionSet(t);
   for (const SmallVector<int64_t, 4> &point : points) {
     bool inS = s.containsPoint(point);
     bool inT = t.containsPoint(point);
for (const SmallVector<int64_t, 4> &point : points) {
     bool inComplement = complement.containsPoint(point);
     if (inS)
       EXPECT_FALSE(inComplement);
     else
       EXPECT_TRUE(inComplement);
   }
 }
 
-/// Construct a FlatAffineConstraints from a set of inequality and
-/// equality constraints. `numIds` is the total number of ids, of which
-/// `numLocals` is the number of local ids.
-static FlatAffineConstraints
-makeFACFromConstraints(unsigned numIds, ArrayRef<SmallVector<int64_t, 4>> ineqs,
-                       ArrayRef<SmallVector<int64_t, 4>> eqs,
-                       unsigned numLocals = 0) {
-  FlatAffineConstraints fac(/*numReservedInequalities=*/ineqs.size(),
-                            /*numReservedEqualities=*/eqs.size(),
-                            /*numReservedCols=*/numIds + 1,
-                            /*numDims=*/numIds - numLocals,
-                            /*numSymbols=*/0, numLocals);
-  for (const SmallVector<int64_t, 4> &eq : eqs)
-    fac.addEquality(eq);
-  for (const SmallVector<int64_t, 4> &ineq : ineqs)
-    fac.addInequality(ineq);
-  return fac;
-}
-
-/// Construct a FlatAffineConstraints having `numDims` dimensions from the given
-/// set of inequality constraints. This is a convenience function to be used
-/// when the FAC to be constructed does not have any local ids and does not have
-/// equalties.
-static FlatAffineConstraints
-makeFACFromIneqs(unsigned numDims, ArrayRef<SmallVector<int64_t, 4>> ineqs) {
-  return makeFACFromConstraints(numDims, ineqs, /*eqs=*/{});
-}
-
 /// Construct a PresburgerSet having `numDims` dimensions and no symbols from
 /// the given list of FlatAffineConstraints. Each FAC in `facs` should also have
 /// `numDims` dimensions and no symbols, although it can have any number of
 /// local ids.
 static PresburgerSet makeSetFromFACs(unsigned numDims,
                                      ArrayRef<FlatAffineConstraints> facs) {
   PresburgerSet set = PresburgerSet::getEmptySet(numDims);
   for (const FlatAffineConstraints &fac : facs)
     set.unionFACInPlace(fac);
   return set;
 }
 
 TEST(SetTest, containsPoint) {
-  PresburgerSet setA =
-      makeSetFromFACs(1, {
-                             makeFACFromIneqs(1, {{1, -2},    // x >= 2.
-                                                  {-1, 8}}),  // x <= 8.
-                             makeFACFromIneqs(1, {{1, -10},   // x >= 10.
-                                                  {-1, 20}}), // x <= 20.
-                         });
+  MLIRContext context;
+
+  PresburgerSet setA = parsePresburgerSetFromFACStrings(
+      1,
+      {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"},
+      &context);
   for (unsigned x = 0; x <= 21; ++x) {
     if ((2 <= x && x <= 8) || (10 <= x && x <= 20))
       EXPECT_TRUE(setA.containsPoint({x}));
     else
       EXPECT_FALSE(setA.containsPoint({x}));
   }
 
   // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} union
   // a square with opposite corners (2, 2) and (10, 10).
-  PresburgerSet setB =
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 1, -2},   // x + y >= 4.
-                                               {-1, -1, 30}, // x + y <= 32.
-                                               {1, -1, 0},   // x - y >= 2.
-                                               {-1, 1, 10},  // x - y <= 16.
-                                           }),
-                          makeFACFromIneqs(2, {
-                                                  {1, 0, -2},  // x >= 2.
-                                                  {0, 1, -2},  // y >= 2.
-                                                  {-1, 0, 10}, // x <= 10.
-                                                  {0, -1, 10}  // y <= 10.
-                                              })});
+  PresburgerSet setB = parsePresburgerSetFromFACStrings(
+      2, {"(x,y) : (x + y - 4 >= 0, -x - y + 32 >= 0, "
+          "x - y - 2 >= 0, -x + y + 16 >= 0)",
+          "(x,y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"} &
+             context);
 
   for (unsigned x = 1; x <= 25; ++x) {
     for (unsigned y = -6; y <= 16; ++y) {
       if (4 <= x + y && x + y <= 32 && 2 <= x - y && x - y <= 16)
         EXPECT_TRUE(setB.containsPoint({x, y}));
       else if (2 <= x && x <= 10 && 2 <= y && y <= 10)
         EXPECT_TRUE(setB.containsPoint({x, y}));
       else
         EXPECT_FALSE(setB.containsPoint({x, y}));
     }
   }
 }
 
 TEST(SetTest, Union) {
-  PresburgerSet set =
-      makeSetFromFACs(1, {
-                             makeFACFromIneqs(1, {{1, -2},    // x >= 2.
-                                                  {-1, 8}}),  // x <= 8.
-                             makeFACFromIneqs(1, {{1, -10},   // x >= 10.
-                                                  {-1, 20}}), // x <= 20.
-                         });
+  MLIRContext context;
+
+  PresburgerSet set = makeSetFromFACs(
+      1, {
+             parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context),
+             parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context),
 
   // Universe union set.
   testUnionAtPoints(PresburgerSet::getUniverse(1), set,
                     {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   // empty set union set.
   testUnionAtPoints(PresburgerSet::getEmptySet(1), set,
                     {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   // empty set union Universe.
   testUnionAtPoints(PresburgerSet::getEmptySet(1),
                     PresburgerSet::getUniverse(1), {{1}, {2}, {0}, {-1}});
 
   // Universe union empty set.
   testUnionAtPoints(PresburgerSet::getUniverse(1),
                     PresburgerSet::getEmptySet(1), {{1}, {2}, {0}, {-1}});
 
   // empty set union empty set.
   testUnionAtPoints(PresburgerSet::getEmptySet(1),
                     PresburgerSet::getEmptySet(1), {{1}, {2}, {0}, {-1}});
 }
 
 TEST(SetTest, Intersect) {
-  PresburgerSet set =
-      makeSetFromFACs(1, {
-                             makeFACFromIneqs(1, {{1, -2},    // x >= 2.
-                                                  {-1, 8}}),  // x <= 8.
-                             makeFACFromIneqs(1, {{1, -10},   // x >= 10.
-                                                  {-1, 20}}), // x <= 20.
-                         });
+  MLIRContext context;
+
+  PresburgerSet set = makeSetFromFACs(
+      1, {
+             parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context),
+             parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context),
 
   // Universe intersection set.
   testIntersectAtPoints(PresburgerSet::getUniverse(1), set,
                         {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   // empty set intersection set.
   testIntersectAtPoints(PresburgerSet::getEmptySet(1), set,
                         {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   // empty set intersection Universe.
   testIntersectAtPoints(PresburgerSet::getEmptySet(1),
                         PresburgerSet::getUniverse(1), {{1}, {2}, {0}, {-1}});
 
   // Universe intersection empty set.
   testIntersectAtPoints(PresburgerSet::getUniverse(1),
                         PresburgerSet::getEmptySet(1), {{1}, {2}, {0}, {-1}});
 
   // Universe intersection Universe.
   testIntersectAtPoints(PresburgerSet::getUniverse(1),
                         PresburgerSet::getUniverse(1), {{1}, {2}, {0}, {-1}});
 }
 
 TEST(SetTest, Subtract) {
+  MLIRContext context;
   // The interval [2, 8] minus the interval [10, 20].
   testSubtractAtPoints(
-      makeSetFromFACs(1, {makeFACFromIneqs(1, {{1, -2},      // x >= 2.
-                                               {-1, 8}})}),  // x <= 8.
-      makeSetFromFACs(1, {makeFACFromIneqs(1, {{1, -10},     // x >= 10.
-                                               {-1, 20}})}), // x <= 20.
+      makeSetFromFACs(1,
+                      {parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context)}),
+      makeSetFromFACs(
+          1, {parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context)}),
       {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   // Universe minus [2, 8] U [10, 20]
   testSubtractAtPoints(
-      makeSetFromFACs(1, {makeFACFromIneqs(1, {})}),
-      makeSetFromFACs(1,
-                      {
-                          makeFACFromIneqs(1, {{1, -2},    // x >= 2.
-                                               {-1, 8}}),  // x <= 8.
-                          makeFACFromIneqs(1, {{1, -10},   // x >= 10.
-                                               {-1, 20}}), // x <= 20.
-                      }),
+      makeSetFromFACs(1, {parseFAC("(x) : ()", &context)}),
+      makeSetFromFACs(
+          1,
+              parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context),
+              parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context),
       {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   // ((-infinity, 0] U [3, 4] U [6, 7]) - ([2, 3] U [5, 6])
   testSubtractAtPoints(
       makeSetFromFACs(1,
                       {
-                          makeFACFromIneqs(1,
-                                           {
-                                               {-1, 0} // x <= 0.
-                                           }),
-                          makeFACFromIneqs(1,
-                                           {
-                                               {1, -3}, // x >= 3.
-                                               {-1, 4}  // x <= 4.
-                                           }),
-                          makeFACFromIneqs(1,
-                                           {
-                                               {1, -6}, // x >= 6.
-                                               {-1, 7}  // x <= 7.
-                                           }),
-                      }),
-      makeSetFromFACs(1, {makeFACFromIneqs(1,
-                                           {
-                                               {1, -2}, // x >= 2.
-                                               {-1, 3}, // x <= 3.
-                                           }),
-                          makeFACFromIneqs(1,
-                                           {
-                                               {1, -5}, // x >= 5.
-                                               {-1, 6}  // x <= 6.
-                                           })}),
+                          parseFAC("(x) : (-x >= 0)", &context),
+                          parseFAC("(x) : (x - 3 >= 0, -x + 4 >= 0)", &context),
+                          parseFAC("(x) : (x - 6 >= 0, -x + 7 >= 0)", &context),
+      makeSetFromFACs(1,
+                          parseFAC("(x) : (x - 2 >= 0, -x + 3 >= 0)", &context),
+                          parseFAC("(x) : (x - 5 >= 0, -x + 6 >= 0)", &context),
       {{0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}});
 
   // Expected result is {[x, y] : x > y}, i.e., {[x, y] : x >= y + 1}.
   testSubtractAtPoints(
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, -1, 0} // x >= y.
-                                           })}),
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 1, 0} // x >= -y.
-                                           })}),
+      makeSetFromFACs(2,
+                          parseFAC("(x, y) : (x - y >= 0)", &context),
+                      }),
+      makeSetFromFACs(2,
+                          parseFAC("(x, y) : (x + y >= 0)", &context),
+                      }),
       {{0, 1}, {1, 1}, {1, 0}, {1, -1}, {0, -1}});
 
   // A rectangle with corners at (2, 2) and (10, 10), minus
   // a rectangle with corners at (5, -10) and (7, 100).
   // This splits the former rectangle into two halves, (2, 2) to (5, 10) and
   // (7, 2) to (10, 10).
   testSubtractAtPoints(
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 0, -2},  // x >= 2.
-                                               {0, 1, -2},  // y >= 2.
-                                               {-1, 0, 10}, // x <= 10.
-                                               {0, -1, 10}  // y <= 10.
-                                           })}),
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 0, -5},   // x >= 5.
-                                               {0, 1, 10},   // y >= -10.
-                                               {-1, 0, 7},   // x <= 7.
-                                               {0, -1, 100}, // y <= 100.
-                                           })}),
+      makeSetFromFACs(2,
+                          parseFAC("(x, y) : (x - 2 >= 0, y - 2 >= 0, "
+                                   "-x + 10 >= 0, -y + 10 >= 0)",
+                                   &context),
+                      }),
+      makeSetFromFACs(2,
+                      {
+                          parseFAC("(x, y) : (x - 5 >= 0, y + 10 >= 0, "
+                                   "-x + 7 >= 0, -y + 100 >= 0)",
+                                   &context),
+                      }),
       {{1, 2},  {2, 2},  {4, 2},  {5, 2},  {7, 2},  {8, 2},  {11, 2},
        {1, 1},  {2, 1},  {4, 1},  {5, 1},  {7, 1},  {8, 1},  {11, 1},
        {1, 10}, {2, 10}, {4, 10}, {5, 10}, {7, 10}, {8, 10}, {11, 10},
        {1, 11}, {2, 11}, {4, 11}, {5, 11}, {7, 11}, {8, 11}, {11, 11}});
 
   // A rectangle with corners at (2, 2) and (10, 10), minus
   // a rectangle with corners at (5, 4) and (7, 8).
   // This creates a hole in the middle of the former rectangle, and the
   // resulting set can be represented as a union of four rectangles.
   testSubtractAtPoints(
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 0, -2},  // x >= 2.
-                                               {0, 1, -2},  // y >= 2.
-                                               {-1, 0, 10}, // x <= 10.
-                                               {0, -1, 10}  // y <= 10.
-                                           })}),
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 0, -5}, // x >= 5.
-                                               {0, 1, -4}, // y >= 4.
-                                               {-1, 0, 7}, // x <= 7.
-                                               {0, -1, 8}, // y <= 8.
-                                           })}),
+      makeSetFromFACs(2,
+                      {
+                          parseFAC("(x, y) : (x - 2 >= 0, y -2 >= 0, "
+                                   "-x + 10 >= 0, -y + 10 >= 0)",
+                                   &context),
+                      }),
+      makeSetFromFACs(2,
+                          parseFAC("(x, y) : (x - 5 >= 0, y - 4 >= 0, "
+                                   "-x + 7 >= 0, -y + 8 >= 0)",
+                                   &context),
+                      }),
       {{1, 1},
        {2, 2},
        {10, 10},
        {11, 11},
        {5, 4},
        {7, 4},
        {5, 8},
        {7, 8},
        {4, 4},
        {8, 4},
        {4, 8},
        {8, 8}});
 
   // The second set is a superset of the first one, since on the line x + y = 0,
   // y <= 1 is equivalent to x >= -1. So the result is empty.
   testSubtractAtPoints(
-      makeSetFromFACs(2, {makeFACFromConstraints(2,
-                                                 {
-                                                     {1, 0, 0} // x >= 0.
-                                                 },
-                                                 {
-                                                     {1, 1, 0} // x + y = 0.
-                                                 })}),
-      makeSetFromFACs(2, {makeFACFromConstraints(2,
-                                                 {
-                                                     {0, -1, 1} // y <= 1.
-                                                 },
-                                                 {
-                                                     {1, 1, 0} // x + y = 0.
-                                                 })}),
+      makeSetFromFACs(2,
+                          parseFAC("(x, y) : (x >= 0, x + y == 0)", &context),
+                      }),
+      makeSetFromFACs(
+          2,
+              parseFAC("(x, y) : (-y + 1 >= 0, x + y == 0)", &context),
+          }),
       {{0, 0},
        {1, -1},
        {2, -2},
        {-1, 1},
        {-2, 2},
        {1, 1},
        {-1, -1},
        {-1, 1},
        {1, -1}});
 
   // The result should be {0} U {2}.
   testSubtractAtPoints(
       makeSetFromFACs(1,
                       {
-                          makeFACFromIneqs(1, {{1, 0},    // x >= 0.
-                                               {-1, 2}}), // x <= 2.
+                          parseFAC("(x) : (x >= 0, -x + 2 >= 0)", &context),
                       }),
       makeSetFromFACs(1,
                       {
-                          makeFACFromConstraints(1, {},
-                                                 {
-                                                     {1, -1} // x = 1.
-                                                 }),
+                          parseFAC("(x) : (x - 1 == 0)", &context),
                       }),
       {{-1}, {0}, {1}, {2}, {3}});
 
   // Sets with lots of redundant inequalities to test the redundancy heuristic.
   // (the heuristic is for the subtrahend, the second set which is the one being
   // subtracted)
 
   // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} minus
   // a triangle with vertices {(2, 2), (10, 2), (10, 10)}.
   testSubtractAtPoints(
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 1, -2},   // x + y >= 4.
-                                               {-1, -1, 30}, // x + y <= 32.
-                                               {1, -1, 0},   // x - y >= 2.
-                                               {-1, 1, 10},  // x - y <= 16.
-                                           })}),
       makeSetFromFACs(
-          2, {makeFACFromIneqs(2,
-                               {
-                                   {1, 0, -2},   // x >= 2. [redundant]
-                                   {0, 1, -2},   // y >= 2.
-                                   {-1, 0, 10},  // x <= 10.
-                                   {0, -1, 10},  // y <= 10. [redundant]
-                                   {1, 1, -2},   // x + y >= 2. [redundant]
-                                   {-1, -1, 30}, // x + y <= 30. [redundant]
-                                   {1, -1, 0},   // x - y >= 0.
-                                   {-1, 1, 10},  // x - y <= 10.
-                               })}),
-      {{1, 2},  {2, 2},   {3, 2},   {4, 2},  {1, 1},   {2, 1},   {3, 1},
-       {4, 1},  {2, 0},   {3, 0},   {4, 0},  {5, 0},   {10, 2},  {11, 2},
-       {10, 1}, {10, 10}, {10, 11}, {10, 9}, {11, 10}, {10, -6}, {11, -6},
-       {24, 8}, {24, 7},  {17, 15}, {16, 15}});
-
-  testSubtractAtPoints(
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 1, -2},   // x + y >= 4.
-                                               {-1, -1, 30}, // x + y <= 32.
-                                               {1, -1, 0},   // x - y >= 2.
-                                               {-1, 1, 10},  // x - y <= 16.
-                                           })}),
+          2,
+              parseFAC("(x, y) : (x + y - 4 >= 0, "
+                       "-x - y + 32 >= 0, x - y - 2 >= 0, -x + y + 16 >= 0)",
+                       &context),
+          }),
       makeSetFromFACs(
-          2, {makeFACFromIneqs(2,
-                               {
-                                   {1, 0, -2},   // x >= 2. [redundant]
-                                   {0, 1, -2},   // y >= 2.
-                                   {-1, 0, 10},  // x <= 10.
-                                   {0, -1, 10},  // y <= 10. [redundant]
-                                   {1, 1, -2},   // x + y >= 2. [redundant]
-                                   {-1, -1, 30}, // x + y <= 30. [redundant]
-                                   {1, -1, 0},   // x - y >= 0.
-                                   {-1, 1, 10},  // x - y <= 10.
-                               })}),
+          2,
+              parseFAC(
+                  "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, "
+                  "-y + 10 >= 0, x + y - 2 >= 0, -x - y + 30 >= 0, x - y >= 0, "
+                  "-x + y + 10 >= 0)",
+                  &context),
+          }),
       {{1, 2},  {2, 2},   {3, 2},   {4, 2},  {1, 1},   {2, 1},   {3, 1},
        {4, 1},  {2, 0},   {3, 0},   {4, 0},  {5, 0},   {10, 2},  {11, 2},
        {10, 1}, {10, 10}, {10, 11}, {10, 9}, {11, 10}, {10, -6}, {11, -6},
        {24, 8}, {24, 7},  {17, 15}, {16, 15}});
 
   // ((-infinity, -5] U [3, 3] U [4, 4] U [5, 5]) - ([-2, -10] U [3, 4] U [6,
   // 7])
   testSubtractAtPoints(
       makeSetFromFACs(1,
                       {
-                          makeFACFromIneqs(1,
-                                           {
-                                               {-1, -5}, // x <= -5.
-                                           }),
-                          makeFACFromConstraints(1, {},
-                                                 {
-                                                     {1, -3} // x = 3.
-                                                 }),
-                          makeFACFromConstraints(1, {},
-                                                 {
-                                                     {1, -4} // x = 4.
-                                                 }),
-                          makeFACFromConstraints(1, {},
-                                                 {
-                                                     {1, -5} // x = 5.
-                                                 }),
+                          parseFAC("(x) : (-x - 5 >= 0)", &context),
+                          parseFAC("(x) : (x - 3 == 0)", &context),
+                          parseFAC("(x) : (x - 4 == 0)", &context),
+                          parseFAC("(x) : (x - 5 == 0)", &context),
                       }),
       makeSetFromFACs(
           1,
           {
-              makeFACFromIneqs(1,
-                               {
-                                   {-1, -2},  // x <= -2.
-                                   {1, -10},  // x >= -10.
-                                   {-1, 0},   // x <= 0. [redundant]
-                                   {-1, 10},  // x <= 10. [redundant]
-                                   {1, -100}, // x >= -100. [redundant]
-                                   {1, -50}   // x >= -50. [redundant]
-                               }),
-              makeFACFromIneqs(1,
-                               {
-                                   {1, -3}, // x >= 3.
-                                   {-1, 4}, // x <= 4.
-                                   {1, 1},  // x >= -1. [redundant]
-                                   {1, 7},  // x >= -7. [redundant]
-                                   {-1, 10} // x <= 10. [redundant]
-                               }),
-              makeFACFromIneqs(1,
-                               {
-                                   {1, -6}, // x >= 6.
-                                   {-1, 7}, // x <= 7.
-                                   {1, 1},  // x >= -1. [redundant]
-                                   {1, -3}, // x >= -3. [redundant]
-                                   {-1, 5}  // x <= 5. [redundant]
-                               }),
+              parseFAC(
+                  "(x) : (-x - 2 >= 0, x - 10 >= 0, -x >= 0, -x + 10 >= 0, "
+                  "x - 100 >= 0, x - 50 >= 0)",
+                  &context),
+              parseFAC("(x) : (x - 3 >= 0, -x + 4 >= 0, x + 1 >= 0, "
+                       "x + 7 >= 0, -x + 10 >= 0)",
+                       &context),
+              parseFAC(
+                  "(x) : (x - 6 >= 0, -x + 7 >= 0, x + 1 >= 0, x - 3 >= 0, "
+                  "-x + 5 >= 0)",
+                  &context),
           }),
       {{-6},
        {-5},
        {-4},
        {-9},
        {-10},
        {-11},
        {0},
        {1},
        {2},
        {3},
        {4},
        {5},
        {6},
        {7},
        {8}});
 }
 
 TEST(SetTest, Complement) {
+
+  MLIRContext context;
   // Complement of universe.
   testComplementAtPoints(
       PresburgerSet::getUniverse(1),
       {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   // Complement of empty set.
   testComplementAtPoints(
       PresburgerSet::getEmptySet(1),
       {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   testComplementAtPoints(
-      makeSetFromFACs(2, {makeFACFromIneqs(2,
-                                           {
-                                               {1, 0, -2},  // x >= 2.
-                                               {0, 1, -2},  // y >= 2.
-                                               {-1, 0, 10}, // x <= 10.
-                                               {0, -1, 10}  // y <= 10.
-                                           })}),
+      makeSetFromFACs(2,
+                          parseFAC("(x,y) : (x - 2 >= 0, y - 2 >= 0, "
+                                   "-x + 10 >= 0, -y + 10 >= 0)",
+                                   &context),
+                      }),
       {{1, 1},
        {2, 1},
        {1, 2},
        {2, 2},
        {2, 3},
        {3, 2},
        {10, 10},
        {10, 11},
        {11, 10},
        {2, 10},
        {2, 11},
        {1, 10}});
 }
 
 TEST(SetTest, isEqual) {
+
+  MLIRContext context;
   // set = [2, 8] U [10, 20].
   PresburgerSet universe = PresburgerSet::getUniverse(1);
   PresburgerSet emptySet = PresburgerSet::getEmptySet(1);
-  PresburgerSet set =
-      makeSetFromFACs(1, {
-                             makeFACFromIneqs(1, {{1, -2},    // x >= 2.
-                                                  {-1, 8}}),  // x <= 8.
-                             makeFACFromIneqs(1, {{1, -10},   // x >= 10.
-                                                  {-1, 20}}), // x <= 20.
-                         });
+  PresburgerSet set = makeSetFromFACs(
+      1, {
+             parseFAC("(x) : (x - 2 >= 0, -x + 8 >= 0)", &context),
+             parseFAC("(x) : (x - 10 >= 0, -x + 20 >= 0)", &context),
 
   // universe != emptySet.
   EXPECT_FALSE(universe.isEqual(emptySet));
   // emptySet != universe.
   EXPECT_FALSE(emptySet.isEqual(universe));
   // emptySet == emptySet.
   EXPECT_TRUE(emptySet.isEqual(emptySet));
   // universe == universe.
TEST(SetTest, isEqual) {
   // set U (universe \ set) == universe.
   EXPECT_TRUE(set.unionSet(set.complement()).isEqual(universe));
   // set U (universe \ set) != set.
   EXPECT_FALSE(set.unionSet(set.complement()).isEqual(set));
   // set != set U (universe \ set).
   EXPECT_FALSE(set.isEqual(set.unionSet(set.complement())));
 
   // square is one unit taller than rect.
-  PresburgerSet square =
-      makeSetFromFACs(2, {makeFACFromIneqs(2, {
-                                                  {1, 0, -2}, // x >= 2.
-                                                  {0, 1, -2}, // y >= 2.
-                                                  {-1, 0, 9}, // x <= 9.
-                                                  {0, -1, 9}  // y <= 9.
-                                              })});
-  PresburgerSet rect =
-      makeSetFromFACs(2, {makeFACFromIneqs(2, {
-                                                  {1, 0, -2}, // x >= 2.
-                                                  {0, 1, -2}, // y >= 2.
-                                                  {-1, 0, 9}, // x <= 9.
-                                                  {0, -1, 8}  // y <= 8.
-                                              })});
+  PresburgerSet square = makeSetFromFACs(
+      2, {
+             parseFAC(
+                 "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 9 >= 0)",
+                 &context),
+         });
+  PresburgerSet rect = makeSetFromFACs(
+      2, {
+             parseFAC(
+                 "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 8 >= 0)",
+                 &context),
+         });
   EXPECT_FALSE(square.isEqual(rect));
   PresburgerSet universeRect = square.unionSet(square.complement());
   PresburgerSet universeSquare = rect.unionSet(rect.complement());
   EXPECT_TRUE(universeRect.isEqual(universeSquare));
   EXPECT_FALSE(universeRect.isEqual(rect));
   EXPECT_FALSE(universeSquare.isEqual(square));
   EXPECT_FALSE(rect.complement().isEqual(square.complement()));
 }
 
 void expectEqual(const PresburgerSet &s, const PresburgerSet &t) {
   EXPECT_TRUE(s.isEqual(t));
 }
 
 void expectEmpty(PresburgerSet s) { EXPECT_TRUE(s.isIntegerEmpty()); }
 
 TEST(SetTest, divisions) {
   MLIRContext context;
   // Note: we currently need to add the equalities as inequalities to the FAC
   // since detecting divisions based on equalities is not yet supported.
 
   // evens = {x : exists q, x = 2q}.
   PresburgerSet evens{
-      makeFACFromConstraints(2, {{1, -2, 0}, {-1, 2, 1}}, {{1, -2, 0}}, 1)};
-  // odds = {x : exists q, x = 2q + 1}.
+      parseFAC("(x) : (x - 2 * (x floordiv 2) == 0)", &context)};
+
+  //  odds = {x : exists q, x = 2q + 1}.
   PresburgerSet odds{
-      makeFACFromConstraints(2, {{1, -2, 0}, {-1, 2, 1}}, {{1, -2, -1}}, 1)};
-  // multiples6 = {x : exists q, x = 6q}.
+      parseFAC("(x) : (x - 2 * (x floordiv 2) - 1 == 0)", &context)};
+
+  // multiples3 = {x : exists q, x = 3q}.
   PresburgerSet multiples3{
-      makeFACFromConstraints(2, {{1, -3, 0}, {-1, 3, 2}}, {{1, -3, 0}}, 1)};
+      parseFAC("(x) : (x - 3 * (x floordiv 3) == 0)", &context)};
+
   // multiples6 = {x : exists q, x = 6q}.
   PresburgerSet multiples6{
-      makeFACFromConstraints(2, {{1, -6, 0}, {-1, 6, 5}}, {{1, -6, 0}}, 1)};
+      parseFAC("(x) : (x - 6 * (x floordiv 6) == 0)", &context)};
 
   // evens /\ odds = empty.
   expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds)));
   // evens U odds = universe.
   expectEqual(evens.unionSet(odds), PresburgerSet::getUniverse(1));
   expectEqual(evens.complement(), odds);
   expectEqual(odds.complement(), evens);
   // even multiples of 3 = multiples of 6.