[mlir][Analysis][Presburger] Remove redundant local vars after composition (#211023)

Call `removeRedundantLocalVars()` at the end of
`IntegerRelation::compose` to simplify existential constraints generated
when projecting out intermediate dimensions.

Removing redundant local vars also happens in
`IntegerRelation::mergeAndCompose` and `FlatAffineRelation::compose`.

When composing A->B with B->C, intermediate vars B are converted to
local existential variables. When performing multiple compositions, this
causes bloat of existential variables that impact later performance,
bounds checks, and emptiness checks.

Signed-off-by: Asra Ali <asraa@google.com>

mlir/lib/Analysis/Presburger/IntegerRelation.cpp

@@ -2573,6 +2573,9 @@ void IntegerRelation::compose(const IntegerRelation &rel) {
 
   // Project out B in R1.
   convertVarKind(VarKind::Range, 0, numBVars, VarKind::Local);
+
+  // Eliminate local variables
+  removeRedundantLocalVars();
 }
 
 void IntegerRelation::applyDomain(const IntegerRelation &rel) {

mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp

@@ -119,6 +119,25 @@ TEST(IntegerRelationTest, applyDomainAndRange) {
   }
 }
 
+TEST(IntegerRelationTest, composeRemoveRedundantLocalVars) {
+  // map x to  y = x + 10.
+  IntegerRelation map1 =
+      parseRelationFromSet("(x, y) : (y - x - 10 == 0)", /*numDomain=*/1);
+
+  // map y to z = y + 20.
+  IntegerRelation map2 =
+      parseRelationFromSet("(y, z) : (z - y - 20 == 0)", /*numDomain=*/1);
+
+  // composing projects out y (converting it to a local variable)
+  map1.compose(map2);
+
+  // y is fully determined by x so should be eliminated after composition
+  EXPECT_EQ(map1.getNumLocalVars(), 0u);
+  IntegerRelation expectedMap =
+      parseRelationFromSet("(x, z) : (z - x - 30 == 0)", /*numDomain=*/1);
+  EXPECT_TRUE(map1.isEqual(expectedMap));
+}
+
 TEST(IntegerRelationTest, symbolicLexmin) {
   SymbolicLexOpt lexmin =
       parseRelationFromSet("(a, x)[b] : (x - a >= 0, x - b >= 0)", 1)