[MLIR][NFC] Move PresburgerSet to Presburger/ directory

[Groverkss]

Summary

This patch moves PresburgerSet to Presburger/ directory. This patch is purely
mechincal, it only moves and renames functionality and tests.

This patch is part of a series of patches to move presburger functionality to
Presburger/ directory.

[arjunp]

Seems good to me, just fix the singular/plural issues below.

mlir/include/mlir/Analysis/Presburger/PresburgerSet.h

9

Should be IntegerPolyhedrons or IntegerPolyhedra. I think the first is better since it's a class name

20

Pleas use IntegerPolyhedrons or IntegerPolyhedra, and Polys below for all "FACs" being replaced

36

Polys

44

Plural

94

"FACs" should be replaced with Polys, plural.

99

Also here.

mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp

25

[Groverkss]

• Address Arjun's comments

mlir/include/mlir/Analysis/Presburger/PresburgerSet.h

 //===- Set.h - MLIR PresburgerSet Class -------------------------*- C++ -*-===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
-// A class to represent unions of FlatAffineConstraints.
+// A class to represent unions of IntegerPolyhedron.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef MLIR_ANALYSIS_PRESBURGERSET_H
 #define MLIR_ANALYSIS_PRESBURGERSET_H
 
-#include "mlir/Analysis/AffineStructures.h"
+#include "mlir/Analysis/Presburger/IntegerPolyhedron.h"
 
 namespace mlir {
 
-/// This class can represent a union of FlatAffineConstraints, with support for
+/// This class can represent a union of IntegerPolyhedron, with support for
 /// union, intersection, subtraction and complement operations, as well as
 /// sampling.
 ///
-/// The FlatAffineConstraints (FACs) are stored in a vector, and the set
-/// represents the union of these FACs. An empty list corresponds to the empty
+/// The IntegerPolyhedron (Poly) are stored in a vector, and the set
+/// represents the union of these Poly. An empty list corresponds to the empty
 /// set.
 ///
-/// Note that there are no invariants guaranteed on the list of FACs other than
+/// Note that there are no invariants guaranteed on the list of Poly other than
 /// that they are all in the same space, i.e., they all have the same number of
-/// dimensions and symbols. For example, the FACs may overlap each other.
+/// dimensions and symbols. For example, the Poly may overlap each other.
 class PresburgerSet {
 public:
-  explicit PresburgerSet(const FlatAffineConstraints &fac);
+  explicit PresburgerSet(const IntegerPolyhedron &poly);
 
-  /// Return the number of FACs in the union.
-  unsigned getNumFACs() const;
+  /// Return the number of Poly in the union.
+  unsigned getNumPoly() const;
 
   /// Return the number of real dimensions.
   unsigned getNumDims() const;
 
   /// Return the number of symbolic dimensions.
   unsigned getNumSyms() const;
 
-  /// Return a reference to the list of FlatAffineConstraints.
-  ArrayRef<FlatAffineConstraints> getAllFlatAffineConstraints() const;
+  /// Return a reference to the list of IntegerPolyhedron.
+  ArrayRef<IntegerPolyhedron> getAllIntegerPolyhedron() const;
 
-  /// Return the FlatAffineConstraints at the specified index.
-  const FlatAffineConstraints &getFlatAffineConstraints(unsigned index) const;
+  /// Return the IntegerPolyhedron at the specified index.
+  const IntegerPolyhedron &getIntegerPolyhedron(unsigned index) const;
 
   /// Mutate this set, turning it into the union of this set and the given
-  /// FlatAffineConstraints.
-  void unionFACInPlace(const FlatAffineConstraints &fac);
+  /// IntegerPolyhedron.
+  void unionPolyInPlace(const IntegerPolyhedron &poly);
 
   /// Mutate this set, turning it into the union of this set and the given set.
   void unionSetInPlace(const PresburgerSet &set);
 
   /// Return the union of this set and the given set.
   PresburgerSet unionSet(const PresburgerSet &set) const;
 
   /// Return the intersection of this set and the given set.
public:
   /// Return an empty set of the specified type that contains no points.
   static PresburgerSet getEmptySet(unsigned nDim = 0, unsigned nSym = 0);
 
   /// Return true if all the sets in the union are known to be integer empty
   /// false otherwise.
   bool isIntegerEmpty() const;
 
   /// Find an integer sample from the given set. This should not be called if
-  /// any of the FACs in the union are unbounded.
+  /// any of the Poly in the union are unbounded.
   bool findIntegerSample(SmallVectorImpl<int64_t> &sample);
 
   /// Simplifies the representation of a PresburgerSet.
   ///
-  /// In particular, removes all FACs which are subsets of other FACs in the
+  /// In particular, removes all Poly which are subsets of other Poly in the
   /// union.
   PresburgerSet coalesce() const;
 
 private:
   /// Construct an empty PresburgerSet.
   PresburgerSet(unsigned nDim = 0, unsigned nSym = 0)
       : nDim(nDim), nSym(nSym) {}
 
-  /// Return the set difference fac \ set.
-  static PresburgerSet getSetDifference(FlatAffineConstraints fac,
+  /// Return the set difference poly \ set.
+  static PresburgerSet getSetDifference(IntegerPolyhedron poly,
                                         const PresburgerSet &set);
 
   /// Number of identifiers corresponding to real dimensions.
   unsigned nDim;
 
   /// Number of symbolic dimensions, unknown but constant for analysis, as in
-  /// FlatAffineConstraints.
+  /// IntegerPolyhedron.
   unsigned nSym;
 
-  /// The list of flatAffineConstraints that this set is the union of.
-  SmallVector<FlatAffineConstraints, 2> flatAffineConstraints;
+  /// The list of integerPolyhedrons that this set is the union of.
+  SmallVector<IntegerPolyhedron, 2> integerPolyhedrons;
 };
 
 } // namespace mlir
 
 #endif // MLIR_ANALYSIS_PRESBURGERSET_H

mlir/lib/Analysis/CMakeLists.txt

 set(LLVM_OPTIONAL_SOURCES
   AliasAnalysis.cpp
   AffineAnalysis.cpp
   AffineStructures.cpp
   BufferViewFlowAnalysis.cpp
   CallGraph.cpp
   DataFlowAnalysis.cpp
   DataLayoutAnalysis.cpp
   Liveness.cpp
   LoopAnalysis.cpp
   NestedMatcher.cpp
   NumberOfExecutions.cpp
-  PresburgerSet.cpp
   SliceAnalysis.cpp
   Utils.cpp
 
   AliasAnalysis/LocalAliasAnalysis.cpp
   )
 
 add_mlir_library(MLIRAnalysis
   AliasAnalysis.cpp
add_mlir_library(MLIRAnalysis
   MLIRViewLikeInterface
   )
 
 add_mlir_library(MLIRLoopAnalysis
   AffineAnalysis.cpp
   AffineStructures.cpp
   LoopAnalysis.cpp
   NestedMatcher.cpp
-  PresburgerSet.cpp
   Utils.cpp
 
   ADDITIONAL_HEADER_DIRS
   ${MLIR_MAIN_INCLUDE_DIR}/mlir/Analysis
 
   DEPENDS
   mlir-headers
 

mlir/lib/Analysis/Presburger/CMakeLists.txt

 add_mlir_library(MLIRPresburger
   IntegerPolyhedron.cpp
   LinearTransform.cpp
   Matrix.cpp
+  PresburgerSet.cpp
   Simplex.cpp
   Utils.cpp
 
   LINK_LIBS PUBLIC
   MLIRSupport
   )

mlir/lib/Analysis/Presburger/PresburgerSet.cpp

 //===- Set.cpp - MLIR PresburgerSet Class ---------------------------------===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 
-#include "mlir/Analysis/PresburgerSet.h"
+#include "mlir/Analysis/Presburger/PresburgerSet.h"
 #include "mlir/Analysis/Presburger/Simplex.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/SmallBitVector.h"
 
 using namespace mlir;
 
-PresburgerSet::PresburgerSet(const FlatAffineConstraints &fac)
-    : nDim(fac.getNumDimIds()), nSym(fac.getNumSymbolIds()) {
-  unionFACInPlace(fac);
+PresburgerSet::PresburgerSet(const IntegerPolyhedron &poly)
+    : nDim(poly.getNumDimIds()), nSym(poly.getNumSymbolIds()) {
+  unionPolyInPlace(poly);
 }
 
-unsigned PresburgerSet::getNumFACs() const {
-  return flatAffineConstraints.size();
-}
+unsigned PresburgerSet::getNumPoly() const { return integerPolyhedrons.size(); }
 
 unsigned PresburgerSet::getNumDims() const { return nDim; }
 
 unsigned PresburgerSet::getNumSyms() const { return nSym; }
 
-ArrayRef<FlatAffineConstraints>
-PresburgerSet::getAllFlatAffineConstraints() const {
-  return flatAffineConstraints;
+ArrayRef<IntegerPolyhedron> PresburgerSet::getAllIntegerPolyhedron() const {
+  return integerPolyhedrons;
 }
 
-const FlatAffineConstraints &
-PresburgerSet::getFlatAffineConstraints(unsigned index) const {
-  assert(index < flatAffineConstraints.size() && "index out of bounds!");
-  return flatAffineConstraints[index];
+const IntegerPolyhedron &
+PresburgerSet::getIntegerPolyhedron(unsigned index) const {
+  assert(index < integerPolyhedrons.size() && "index out of bounds!");
+  return integerPolyhedrons[index];
 }
 
-/// Assert that the FlatAffineConstraints and PresburgerSet live in
+/// Assert that the IntegerPolyhedron and PresburgerSet live in
 /// compatible spaces.
-static void assertDimensionsCompatible(const FlatAffineConstraints &fac,
+static void assertDimensionsCompatible(const IntegerPolyhedron &poly,
                                        const PresburgerSet &set) {
-  assert(fac.getNumDimIds() == set.getNumDims() &&
-         "Number of dimensions of the FlatAffineConstraints and PresburgerSet"
+  assert(poly.getNumDimIds() == set.getNumDims() &&
+         "Number of dimensions of the IntegerPolyhedron and PresburgerSet"
          "do not match!");
-  assert(fac.getNumSymbolIds() == set.getNumSyms() &&
-         "Number of symbols of the FlatAffineConstraints and PresburgerSet"
+  assert(poly.getNumSymbolIds() == set.getNumSyms() &&
+         "Number of symbols of the IntegerPolyhedron and PresburgerSet"
          "do not match!");
 }
 
 /// Assert that the two PresburgerSets live in compatible spaces.
 static void assertDimensionsCompatible(const PresburgerSet &setA,
                                        const PresburgerSet &setB) {
   assert(setA.getNumDims() == setB.getNumDims() &&
          "Number of dimensions of the PresburgerSets do not match!");
   assert(setA.getNumSyms() == setB.getNumSyms() &&
          "Number of symbols of the PresburgerSets do not match!");
 }
 
 /// Mutate this set, turning it into the union of this set and the given
-/// FlatAffineConstraints.
-void PresburgerSet::unionFACInPlace(const FlatAffineConstraints &fac) {
-  assertDimensionsCompatible(fac, *this);
-  flatAffineConstraints.push_back(fac);
+/// IntegerPolyhedron.
+void PresburgerSet::unionPolyInPlace(const IntegerPolyhedron &poly) {
+  assertDimensionsCompatible(poly, *this);
+  integerPolyhedrons.push_back(poly);
 }
 
 /// Mutate this set, turning it into the union of this set and the given set.
 ///
-/// This is accomplished by simply adding all the FACs of the given set to this
+/// This is accomplished by simply adding all the Poly of the given set to this
 /// set.
 void PresburgerSet::unionSetInPlace(const PresburgerSet &set) {
   assertDimensionsCompatible(set, *this);
-  for (const FlatAffineConstraints &fac : set.flatAffineConstraints)
-    unionFACInPlace(fac);
+  for (const IntegerPolyhedron &poly : set.integerPolyhedrons)
+    unionPolyInPlace(poly);
 }
 
 /// Return the union of this set and the given set.
 PresburgerSet PresburgerSet::unionSet(const PresburgerSet &set) const {
   assertDimensionsCompatible(set, *this);
   PresburgerSet result = *this;
   result.unionSetInPlace(set);
   return result;
 }
 
 /// A point is contained in the union iff any of the parts contain the point.
 bool PresburgerSet::containsPoint(ArrayRef<int64_t> point) const {
-  return llvm::any_of(flatAffineConstraints,
-                      [&](const FlatAffineConstraints &fac) {
-                        return (fac.containsPoint(point));
-                      });
+  return llvm::any_of(integerPolyhedrons, [&](const IntegerPolyhedron &poly) {
+    return (poly.containsPoint(point));
 }
 
 PresburgerSet PresburgerSet::getUniverse(unsigned nDim, unsigned nSym) {
   PresburgerSet result(nDim, nSym);
-  result.unionFACInPlace(FlatAffineConstraints::getUniverse(nDim, nSym));
+  result.unionPolyInPlace(IntegerPolyhedron::getUniverse(nDim, nSym));
   return result;
 }
 
 PresburgerSet PresburgerSet::getEmptySet(unsigned nDim, unsigned nSym) {
   return PresburgerSet(nDim, nSym);
 }
 
 // Return the intersection of this set with the given set.
 //
 // We directly compute (S_1 or S_2 ...) and (T_1 or T_2 ...)
 // as (S_1 and T_1) or (S_1 and T_2) or ...
 //
 // If S_i or T_j have local variables, then S_i and T_j contains the local
 // variables of both.
 PresburgerSet PresburgerSet::intersect(const PresburgerSet &set) const {
   assertDimensionsCompatible(set, *this);
 
   PresburgerSet result(nDim, nSym);
-  for (const FlatAffineConstraints &csA : flatAffineConstraints) {
-    for (const FlatAffineConstraints &csB : set.flatAffineConstraints) {
-      FlatAffineConstraints csACopy = csA, csBCopy = csB;
+  for (const IntegerPolyhedron &csA : integerPolyhedrons) {
+    for (const IntegerPolyhedron &csB : set.integerPolyhedrons) {
+      IntegerPolyhedron csACopy = csA, csBCopy = csB;
       csACopy.mergeLocalIds(csBCopy);
       csACopy.append(csBCopy);
       if (!csACopy.isEmpty())
-        result.unionFACInPlace(csACopy);
+        result.unionPolyInPlace(csACopy);
     }
   }
   return result;
 }
 
 /// Return `coeffs` with all the elements negated.
 static SmallVector<int64_t, 8> getNegatedCoeffs(ArrayRef<int64_t> coeffs) {
   SmallVector<int64_t, 8> negatedCoeffs;
static SmallVector<int64_t, 8> getComplementIneq(ArrayRef<int64_t> ineq) {
   return coeffs;
 }
 
 /// Return the set difference b \ s and accumulate the result into `result`.
 /// `simplex` must correspond to b.
 ///
 /// In the following, U denotes union, ^ denotes intersection, \ denotes set
 /// difference and ~ denotes complement.
-/// Let b be the FlatAffineConstraints and s = (U_i s_i) be the set. We want
+/// Let b be the IntegerPolyhedron and s = (U_i s_i) be the set. We want
 /// b \ (U_i s_i).
 ///
 /// Let s_i = ^_j s_ij, where each s_ij is a single inequality. To compute
 /// b \ s_i = b ^ ~s_i, we partition s_i based on the first violated inequality:
 /// ~s_i = (~s_i1) U (s_i1 ^ ~s_i2) U (s_i1 ^ s_i2 ^ ~s_i3) U ...
 /// And the required result is (b ^ ~s_i1) U (b ^ s_i1 ^ ~s_i2) U ...
 /// We recurse by subtracting U_{j > i} S_j from each of these parts and
 /// returning the union of the results. Each equality is handled as a
 /// conjunction of two inequalities.
 ///
 /// Note that the same approach works even if an inequality involves a floor
 /// division. For example, the complement of x <= 7*floor(x/7) is still
 /// x > 7*floor(x/7). Since b \ s_i contains the inequalities of both b and s_i
 /// (or the complements of those inequalities), b \ s_i may contain the
 /// divisions present in both b and s_i. Therefore, we need to add the local
 /// division variables of both b and s_i to each part in the result. This means
 /// adding the local variables of both b and s_i, as well as the corresponding
 /// division inequalities to each part. Since the division inequalities are
 /// added to each part, we can skip the parts where the complement of any
 /// division inequality is added, as these parts will become empty anyway.
 ///
 /// As a heuristic, we try adding all the constraints and check if simplex
-/// says that the intersection is empty. If it is, then subtracting this FAC is
+/// says that the intersection is empty. If it is, then subtracting this Poly is
 /// a no-op and we just skip it. Also, in the process we find out that some
 /// constraints are redundant. These redundant constraints are ignored.
 ///
 /// b and simplex are callee saved, i.e., their values on return are
 /// semantically equivalent to their values when the function is called.
-static void subtractRecursively(FlatAffineConstraints &b, Simplex &simplex,
+static void subtractRecursively(IntegerPolyhedron &b, Simplex &simplex,
                                 const PresburgerSet &s, unsigned i,
                                 PresburgerSet &result) {
-  if (i == s.getNumFACs()) {
-    result.unionFACInPlace(b);
+  if (i == s.getNumPoly()) {
+    result.unionPolyInPlace(b);
     return;
   }
-  FlatAffineConstraints sI = s.getFlatAffineConstraints(i);
+  IntegerPolyhedron sI = s.getIntegerPolyhedron(i);
 
   // Below, we append some additional constraints and ids to b. We want to
   // rollback b to its initial state before returning, which we will do by
   // removing all constraints beyond the original number of inequalities
   // and equalities, so we store these counts first.
   const unsigned bInitNumIneqs = b.getNumInequalities();
   const unsigned bInitNumEqs = b.getNumEqualities();
   const unsigned bInitNumLocals = b.getNumLocalIds();
   // Similarly, we also want to rollback simplex to its original state.
   const unsigned initialSnapshot = simplex.getSnapshot();
 
   // Automatically restore the original state when we return.
   auto restoreState = [&]() {
-    b.removeIdRange(FlatAffineConstraints::IdKind::Local, bInitNumLocals,
+    b.removeIdRange(IntegerPolyhedron::IdKind::Local, bInitNumLocals,
                     b.getNumLocalIds());
     b.removeInequalityRange(bInitNumIneqs, b.getNumInequalities());
     b.removeEqualityRange(bInitNumEqs, b.getNumEqualities());
     simplex.rollback(initialSnapshot);
   };
 
   // Find out which inequalities of sI correspond to division inequalities for
   // the local variables of sI.
if (!isMarkedRedundant[offset + 2 * j])
       processInequality(coeffs);
     if (!isMarkedRedundant[offset + 2 * j + 1])
       processInequality(getNegatedCoeffs(coeffs));
   }
 
   restoreState();
 }
 
-/// Return the set difference fac \ set.
+/// Return the set difference poly \ set.
 ///
-/// The FAC here is modified in subtractRecursively, so it cannot be a const
+/// The Poly here is modified in subtractRecursively, so it cannot be a const
 /// reference even though it is restored to its original state before returning
 /// from that function.
-PresburgerSet PresburgerSet::getSetDifference(FlatAffineConstraints fac,
+PresburgerSet PresburgerSet::getSetDifference(IntegerPolyhedron poly,
                                               const PresburgerSet &set) {
-  assertDimensionsCompatible(fac, set);
-  if (fac.isEmptyByGCDTest())
-    return PresburgerSet::getEmptySet(fac.getNumDimIds(),
-                                      fac.getNumSymbolIds());
-
-  PresburgerSet result(fac.getNumDimIds(), fac.getNumSymbolIds());
-  Simplex simplex(fac);
-  subtractRecursively(fac, simplex, set, 0, result);
+  assertDimensionsCompatible(poly, set);
+  if (poly.isEmptyByGCDTest())
+    return PresburgerSet::getEmptySet(poly.getNumDimIds(),
+                                      poly.getNumSymbolIds());
+
+  PresburgerSet result(poly.getNumDimIds(), poly.getNumSymbolIds());
+  Simplex simplex(poly);
+  subtractRecursively(poly, simplex, set, 0, result);
   return result;
 }
 
 /// Return the complement of this set.
 PresburgerSet PresburgerSet::complement() const {
   return getSetDifference(
-      FlatAffineConstraints::getUniverse(getNumDims(), getNumSyms()), *this);
+      IntegerPolyhedron::getUniverse(getNumDims(), getNumSyms()), *this);
 }
 
 /// Return the result of subtract the given set from this set, i.e.,
 /// return `this \ set`.
 PresburgerSet PresburgerSet::subtract(const PresburgerSet &set) const {
   assertDimensionsCompatible(set, *this);
   PresburgerSet result(nDim, nSym);
   // We compute (U_i t_i) \ (U_i set_i) as U_i (t_i \ V_i set_i).
-  for (const FlatAffineConstraints &fac : flatAffineConstraints)
-    result.unionSetInPlace(getSetDifference(fac, set));
+  for (const IntegerPolyhedron &poly : integerPolyhedrons)
+    result.unionSetInPlace(getSetDifference(poly, set));
   return result;
 }
 
 /// Two sets S and T are equal iff S contains T and T contains S.
 /// By "S contains T", we mean that S is a superset of or equal to T.
 ///
 /// S contains T iff T \ S is empty, since if T \ S contains a
 /// point then this is a point that is contained in T but not S.
 ///
 /// Therefore, S is equal to T iff S \ T and T \ S are both empty.
 bool PresburgerSet::isEqual(const PresburgerSet &set) const {
   assertDimensionsCompatible(set, *this);
   return this->subtract(set).isIntegerEmpty() &&
          set.subtract(*this).isIntegerEmpty();
 }
 
 /// Return true if all the sets in the union are known to be integer empty,
 /// false otherwise.
 bool PresburgerSet::isIntegerEmpty() const {
   // The set is empty iff all of the disjuncts are empty.
-  for (const FlatAffineConstraints &fac : flatAffineConstraints) {
-    if (!fac.isIntegerEmpty())
+  for (const IntegerPolyhedron &poly : integerPolyhedrons) {
+    if (!poly.isIntegerEmpty())
       return false;
   }
   return true;
 }
 
 bool PresburgerSet::findIntegerSample(SmallVectorImpl<int64_t> &sample) {
   // A sample exists iff any of the disjuncts contains a sample.
-  for (const FlatAffineConstraints &fac : flatAffineConstraints) {
-    if (Optional<SmallVector<int64_t, 8>> opt = fac.findIntegerSample()) {
+  for (const IntegerPolyhedron &poly : integerPolyhedrons) {
+    if (Optional<SmallVector<int64_t, 8>> opt = poly.findIntegerSample()) {
       sample = std::move(*opt);
       return true;
     }
   }
   return false;
 }
 
 PresburgerSet PresburgerSet::coalesce() const {
   PresburgerSet newSet = PresburgerSet::getEmptySet(getNumDims(), getNumSyms());
-  llvm::SmallBitVector isRedundant(getNumFACs());
+  llvm::SmallBitVector isRedundant(getNumPoly());
 
-  for (unsigned i = 0, e = flatAffineConstraints.size(); i < e; ++i) {
+  for (unsigned i = 0, e = integerPolyhedrons.size(); i < e; ++i) {
     if (isRedundant[i])
       continue;
-    Simplex simplex(flatAffineConstraints[i]);
+    Simplex simplex(integerPolyhedrons[i]);
 
     // Check whether the polytope of `simplex` is empty. If so, it is trivially
     // redundant.
     if (simplex.isEmpty()) {
       isRedundant[i] = true;
       continue;
     }
 
-    // Check whether `FlatAffineConstraints[i]` is contained in any FAC, that is
+    // Check whether `IntegerPolyhedron[i]` is contained in any Poly, that is
     // different from itself and not yet marked as redundant.
-    for (unsigned j = 0, e = flatAffineConstraints.size(); j < e; ++j) {
+    for (unsigned j = 0, e = integerPolyhedrons.size(); j < e; ++j) {
       if (j == i || isRedundant[j])
         continue;
 
-      if (simplex.isRationalSubsetOf(flatAffineConstraints[j])) {
+      if (simplex.isRationalSubsetOf(integerPolyhedrons[j])) {
         isRedundant[i] = true;
         break;
       }
     }
   }
 
-  for (unsigned i = 0, e = flatAffineConstraints.size(); i < e; ++i)
+  for (unsigned i = 0, e = integerPolyhedrons.size(); i < e; ++i)
     if (!isRedundant[i])
-      newSet.unionFACInPlace(flatAffineConstraints[i]);
+      newSet.unionPolyInPlace(integerPolyhedrons[i]);
 
   return newSet;
 }
 
 void PresburgerSet::print(raw_ostream &os) const {
-  os << getNumFACs() << " FlatAffineConstraints:\n";
-  for (const FlatAffineConstraints &fac : flatAffineConstraints) {
-    fac.print(os);
+  os << getNumPoly() << " IntegerPolyhedron:\n";
+  for (const IntegerPolyhedron &poly : integerPolyhedrons) {
+    poly.print(os);
     os << '\n';
   }
 }
 
 void PresburgerSet::dump() const { print(llvm::errs()); }

mlir/lib/Analysis/Utils.cpp

 //===- Utils.cpp ---- Misc utilities for analysis -------------------------===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
 // This file implements miscellaneous analysis routines for non-loop IR
 // structures.
 //
 //===----------------------------------------------------------------------===//
 
 #include "mlir/Analysis/Utils.h"
 #include "mlir/Analysis/AffineAnalysis.h"
 #include "mlir/Analysis/LoopAnalysis.h"
-#include "mlir/Analysis/PresburgerSet.h"
+#include "mlir/Analysis/Presburger/PresburgerSet.h"
 #include "mlir/Dialect/Affine/IR/AffineOps.h"
 #include "mlir/Dialect/Affine/IR/AffineValueMap.h"
 #include "mlir/Dialect/Arithmetic/IR/Arithmetic.h"
 #include "mlir/Dialect/StandardOps/IR/Ops.h"
 #include "mlir/IR/IntegerSet.h"
 #include "llvm/ADT/SmallPtrSet.h"
 #include "llvm/Support/Debug.h"
 #include "llvm/Support/raw_ostream.h"

mlir/unittests/Analysis/AffineStructuresParserTest.cpp

 //===- AffineStructuresParserTest.cpp - FAC parsing unit tests --*- C++ -*-===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
 // This file contains tests for parsing IntegerSets to FlatAffineConstraints.
 // The tests with invalid input check that the parser only accepts well-formed
 // IntegerSets. The tests with well-formed input compare the returned FACs to
 // manually constructed FACs with a PresburgerSet equality check.
 //
 //===----------------------------------------------------------------------===//
 
 #include "./AffineStructuresParser.h"
-#include "mlir/Analysis/PresburgerSet.h"
+#include "mlir/Analysis/Presburger/PresburgerSet.h"
 
 #include <gtest/gtest.h>
 
 namespace mlir {
 
 /// Construct a FlatAffineConstraints from a set of inequality, equality, and
 /// division onstraints.
 static FlatAffineConstraints makeFACFromConstraints(

mlir/unittests/Analysis/CMakeLists.txt

 add_mlir_unittest(MLIRAnalysisTests
   AffineStructuresParser.cpp
   AffineStructuresParserTest.cpp
-  PresburgerSetTest.cpp
 )
 
 target_link_libraries(MLIRAnalysisTests
   PRIVATE
   MLIRLoopAnalysis
   MLIRParser
   )
 
 add_subdirectory(Presburger)

mlir/unittests/Analysis/Presburger/CMakeLists.txt

 add_mlir_unittest(MLIRPresburgerTests
   IntegerPolyhedronTest.cpp
   LinearTransformTest.cpp
   MatrixTest.cpp
+  PresburgerSetTest.cpp
   SimplexTest.cpp
   ../AffineStructuresParser.cpp
 )
 
 target_link_libraries(MLIRPresburgerTests
   PRIVATE MLIRPresburger
   MLIRLoopAnalysis
   MLIRParser
   )

mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp

 //===- SetTest.cpp - Tests for PresburgerSet ------------------------------===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
 // This file contains tests for PresburgerSet. The tests for union,
 // intersection, subtract, and complement work by computing the operation on
 // two sets and checking, for a set of points, that the resulting set contains
 // the point iff the result is supposed to contain it. The test for isEqual just
 // checks if the result for two sets matches the expected result.
 //
 //===----------------------------------------------------------------------===//
 
-#include "mlir/Analysis/PresburgerSet.h"
-#include "./AffineStructuresParser.h"
+#include "mlir/Analysis/Presburger/PresburgerSet.h"
+#include "../AffineStructuresParser.h"
 
 #include <gmock/gmock.h>
 #include <gtest/gtest.h>
 
 namespace mlir {
 
-/// Parses a FlatAffineConstraints from a StringRef. It is expected that the
+/// Parses a IntegerPolyhedron from a StringRef. It is expected that the
 /// string represents a valid IntegerSet, otherwise it will violate a gtest
 /// assertion.
-static FlatAffineConstraints parseFAC(StringRef str, MLIRContext *context) {
-  FailureOr<FlatAffineConstraints> fac = parseIntegerSetToFAC(str, context);
+static IntegerPolyhedron parsePoly(StringRef str, MLIRContext *context) {
+  FailureOr<IntegerPolyhedron> poly = parseIntegerSetToFAC(str, context);
 
-  EXPECT_TRUE(succeeded(fac));
+  EXPECT_TRUE(succeeded(poly));
 
-  return *fac;
+  return *poly;
 }
 
-/// Parse a list of StringRefs to FlatAffineConstraints and combine them into a
+/// Parse a list of StringRefs to IntegerPolyhedron and combine them into a
 /// PresburgerSet be using the union operation. It is expected that the strings
 /// are all valid IntegerSet representation and that all of them have the same
 /// number of dimensions as is specified by the numDims argument.
-static PresburgerSet parsePresburgerSetFromFACStrings(unsigned numDims,
+static PresburgerSet parsePresburgerSetFromPolyStrings(unsigned numDims,
                                                        ArrayRef<StringRef> strs,
                                                        MLIRContext *context) {
   PresburgerSet set = PresburgerSet::getEmptySet(numDims);
   for (StringRef str : strs)
-    set.unionFACInPlace(parseFAC(str, context));
+    set.unionPolyInPlace(parsePoly(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(const PresburgerSet &s, const PresburgerSet &t,
                               ArrayRef<SmallVector<int64_t, 4>> points) {
   PresburgerSet unionSet = s.unionSet(t);
for (const SmallVector<int64_t, 4> &point : points) {
     if (inS)
       EXPECT_FALSE(inComplement);
     else
       EXPECT_TRUE(inComplement);
   }
 }
 
 /// Construct a PresburgerSet having `numDims` dimensions and no symbols from
-/// the given list of FlatAffineConstraints. Each FAC in `facs` should also have
+/// the given list of IntegerPolyhedron. Each Poly in `polys` 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) {
+static PresburgerSet makeSetFromPoly(unsigned numDims,
+                                     ArrayRef<IntegerPolyhedron> polys) {
   PresburgerSet set = PresburgerSet::getEmptySet(numDims);
-  for (const FlatAffineConstraints &fac : facs)
-    set.unionFACInPlace(fac);
+  for (const IntegerPolyhedron &poly : polys)
+    set.unionPolyInPlace(poly);
   return set;
 }
 
 TEST(SetTest, containsPoint) {
   MLIRContext context;
 
-  PresburgerSet setA = parsePresburgerSetFromFACStrings(
+  PresburgerSet setA = parsePresburgerSetFromPolyStrings(
       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 = parsePresburgerSetFromFACStrings(
+  PresburgerSet setB = parsePresburgerSetFromPolyStrings(
       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) {
   MLIRContext context;
 
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1,
       {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"},
       &context);
 
   // Universe union set.
   testUnionAtPoints(PresburgerSet::getUniverse(1), set,
                     {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
TEST(SetTest, Union) {
   // empty set union empty set.
   testUnionAtPoints(PresburgerSet::getEmptySet(1),
                     PresburgerSet::getEmptySet(1), {{1}, {2}, {0}, {-1}});
 }
 
 TEST(SetTest, Intersect) {
   MLIRContext context;
 
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1,
       {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"},
       &context);
 
   // Universe intersection set.
   testIntersectAtPoints(PresburgerSet::getUniverse(1), set,
                         {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
TEST(SetTest, Intersect) {
   // 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(parsePresburgerSetFromFACStrings(
+  testSubtractAtPoints(parsePresburgerSetFromPolyStrings(
                            1, {"(x) : (x - 2 >= 0, -x + 8 >= 0)"}, &context),
-                       parsePresburgerSetFromFACStrings(
+                       parsePresburgerSetFromPolyStrings(
                            1, {"(x) : (x - 10 >= 0, -x + 20 >= 0)"}, &context),
                        {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
 
   // Universe minus [2, 8] U [10, 20]
   testSubtractAtPoints(
-      parsePresburgerSetFromFACStrings(1, {"(x) : ()"}, &context),
-      parsePresburgerSetFromFACStrings(1,
+      parsePresburgerSetFromPolyStrings(1, {"(x) : ()"}, &context),
+      parsePresburgerSetFromPolyStrings(1,
                                         {"(x) : (x - 2 >= 0, -x + 8 >= 0)",
                                          "(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(
-      parsePresburgerSetFromFACStrings(1,
+      parsePresburgerSetFromPolyStrings(1,
                                         {"(x) : (-x >= 0)",
                                          "(x) : (x - 3 >= 0, -x + 4 >= 0)",
                                          "(x) : (x - 6 >= 0, -x + 7 >= 0)"},
                                         &context),
-      parsePresburgerSetFromFACStrings(1,
+      parsePresburgerSetFromPolyStrings(1,
                                         {"(x) : (x - 2 >= 0, -x + 3 >= 0)",
                                          "(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(
-      parsePresburgerSetFromFACStrings(2, {"(x, y) : (x - y >= 0)"}, &context),
-      parsePresburgerSetFromFACStrings(2, {"(x, y) : (x + y >= 0)"}, &context),
+      parsePresburgerSetFromPolyStrings(2, {"(x, y) : (x - y >= 0)"}, &context),
+      parsePresburgerSetFromPolyStrings(2, {"(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(
-      parsePresburgerSetFromFACStrings(
+      parsePresburgerSetFromPolyStrings(
           2,
           {
               "(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 10 >= 0, -y + 10 >= 0)",
           },
           &context),
-      parsePresburgerSetFromFACStrings(
+      parsePresburgerSetFromPolyStrings(
           2,
           {
               "(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(
-      parsePresburgerSetFromFACStrings(
+      parsePresburgerSetFromPolyStrings(
           2, {"(x, y) : (x - 2 >= 0, y -2 >= 0, -x + 10 >= 0, -y + 10 >= 0)"},
           &context),
-      parsePresburgerSetFromFACStrings(
+      parsePresburgerSetFromPolyStrings(
           2,
           {
               "(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(parsePresburgerSetFromFACStrings(
+  testSubtractAtPoints(parsePresburgerSetFromPolyStrings(
                            2, {"(x, y) : (x >= 0, x + y == 0)"}, &context),
-                       parsePresburgerSetFromFACStrings(
+                       parsePresburgerSetFromPolyStrings(
                            2, {"(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(
-      parsePresburgerSetFromFACStrings(1, {"(x) : (x >= 0, -x + 2 >= 0)"},
+      parsePresburgerSetFromPolyStrings(1, {"(x) : (x >= 0, -x + 2 >= 0)"},
                                         &context),
-      parsePresburgerSetFromFACStrings(1, {"(x) : (x - 1 == 0)"}, &context),
+      parsePresburgerSetFromPolyStrings(1, {"(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(
-      parsePresburgerSetFromFACStrings(
+      parsePresburgerSetFromPolyStrings(
           2,
           {
               "(x, y) : (x + y - 4 >= 0, -x - y + 32 >= 0, x - y - 2 >= 0, "
               "-x + y + 16 >= 0)",
           },
           &context),
-      parsePresburgerSetFromFACStrings(
+      parsePresburgerSetFromPolyStrings(
           2,
           {"(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(
-      parsePresburgerSetFromFACStrings(
+      parsePresburgerSetFromPolyStrings(
           1,
           {"(x) : (-x - 5 >= 0)", "(x) : (x - 3 == 0)", "(x) : (x - 4 == 0)",
            "(x) : (x - 5 == 0)"},
           &context),
-      parsePresburgerSetFromFACStrings(
+      parsePresburgerSetFromPolyStrings(
           1,
           {"(x) : (-x - 2 >= 0, x - 10 >= 0, -x >= 0, -x + 10 >= 0, "
            "x - 100 >= 0, x - 50 >= 0)",
            "(x) : (x - 3 >= 0, -x + 4 >= 0, x + 1 >= 0, "
            "x + 7 >= 0, -x + 10 >= 0)",
            "(x) : (x - 6 >= 0, -x + 7 >= 0, x + 1 >= 0, x - 3 >= 0, "
            "-x + 5 >= 0)"},
           &context),
testComplementAtPoints(
       {{-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(
-      parsePresburgerSetFromFACStrings(2,
+      parsePresburgerSetFromPolyStrings(2,
                                         {"(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 = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1,
       {"(x) : (x - 2 >= 0, -x + 8 >= 0)", "(x) : (x - 10 >= 0, -x + 20 >= 0)"},
       &context);
 
   // universe != emptySet.
   EXPECT_FALSE(universe.isEqual(emptySet));
   // emptySet != universe.
   EXPECT_FALSE(emptySet.isEqual(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 = parsePresburgerSetFromFACStrings(
+  PresburgerSet square = parsePresburgerSetFromPolyStrings(
       2, {"(x, y) : (x - 2 >= 0, y - 2 >= 0, -x + 9 >= 0, -y + 9 >= 0)"},
       &context);
-  PresburgerSet rect = parsePresburgerSetFromFACStrings(
+  PresburgerSet rect = parsePresburgerSetFromPolyStrings(
       2, {"(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(const PresburgerSet &s) { EXPECT_TRUE(s.isIntegerEmpty()); }
 
 TEST(SetTest, divisions) {
   MLIRContext context;
 
   // evens = {x : exists q, x = 2q}.
   PresburgerSet evens{
-      parseFAC("(x) : (x - 2 * (x floordiv 2) == 0)", &context)};
+      parsePoly("(x) : (x - 2 * (x floordiv 2) == 0)", &context)};
 
   //  odds = {x : exists q, x = 2q + 1}.
   PresburgerSet odds{
-      parseFAC("(x) : (x - 2 * (x floordiv 2) - 1 == 0)", &context)};
+      parsePoly("(x) : (x - 2 * (x floordiv 2) - 1 == 0)", &context)};
 
   // multiples3 = {x : exists q, x = 3q}.
   PresburgerSet multiples3{
-      parseFAC("(x) : (x - 3 * (x floordiv 3) == 0)", &context)};
+      parsePoly("(x) : (x - 3 * (x floordiv 3) == 0)", &context)};
 
   // multiples6 = {x : exists q, x = 6q}.
   PresburgerSet multiples6{
-      parseFAC("(x) : (x - 6 * (x floordiv 6) == 0)", &context)};
+      parsePoly("(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.
   expectEqual(multiples3.intersect(evens), multiples6);
 
-  PresburgerSet setA{parseFAC("(x) : (-x >= 0)", &context)};
-  PresburgerSet setB{parseFAC("(x) : (x floordiv 2 - 4 >= 0)", &context)};
+  PresburgerSet setA{parsePoly("(x) : (-x >= 0)", &context)};
+  PresburgerSet setB{parsePoly("(x) : (x floordiv 2 - 4 >= 0)", &context)};
   EXPECT_TRUE(setA.subtract(setB).isEqual(setA));
 }
 
 /// Coalesce `set` and check that the `newSet` is equal to `set and that
-/// `expectedNumFACs` matches the number of FACs in the coalesced set.
+/// `expectedNumPoly` matches the number of Poly in the coalesced set.
 /// If one of the two
-void expectCoalesce(size_t expectedNumFACs, const PresburgerSet &set) {
+void expectCoalesce(size_t expectedNumPoly, const PresburgerSet &set) {
   PresburgerSet newSet = set.coalesce();
   EXPECT_TRUE(set.isEqual(newSet));
-  EXPECT_TRUE(expectedNumFACs == newSet.getNumFACs());
+  EXPECT_TRUE(expectedNumPoly == newSet.getNumPoly());
 }
 
-TEST(SetTest, coalesceNoFAC) {
-  PresburgerSet set = makeSetFromFACs(0, {});
+TEST(SetTest, coalesceNoPoly) {
+  PresburgerSet set = makeSetFromPoly(0, {});
   expectCoalesce(0, set);
 }
 
 TEST(SetTest, coalesceContainedOneDim) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : (x >= 0, -x + 4 >= 0)", "(x) : (x - 1 >= 0, -x + 2 >= 0)"},
       &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceFirstEmpty) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ( x - 1 >= 0, -x + 2 >= 0)"},
       &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceSecondEmpty) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : (x - 1 >= 0, -x + 2 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"},
       &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceBothEmpty) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : (x - 3 >= 0, -x - 1 >= 0)", "(x) : (x >= 0, -x - 1 >= 0)"},
       &context);
   expectCoalesce(0, set);
 }
 
 TEST(SetTest, coalesceFirstUniv) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : ()", "(x) : ( x >= 0, -x + 1 >= 0)"}, &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceSecondUniv) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : ( x >= 0, -x + 1 >= 0)", "(x) : ()"}, &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceBothUniv) {
   MLIRContext context;
   PresburgerSet set =
-      parsePresburgerSetFromFACStrings(1, {"(x) : ()", "(x) : ()"}, &context);
+      parsePresburgerSetFromPolyStrings(1, {"(x) : ()", "(x) : ()"}, &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceFirstUnivSecondEmpty) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : ()", "(x) : ( x >= 0, -x - 1 >= 0)"}, &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceFirstEmptySecondUniv) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : ( x >= 0, -x - 1 >= 0)", "(x) : ()"}, &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceCutOneDim) {
   MLIRContext context;
   PresburgerSet set =
-      parsePresburgerSetFromFACStrings(1,
+      parsePresburgerSetFromPolyStrings(1,
                                         {
                                             "(x) : ( x >= 0, -x + 3 >= 0)",
                                             "(x) : ( x - 2 >= 0, -x + 4 >= 0)",
                                         },
                                         &context);
   expectCoalesce(2, set);
 }
 
 TEST(SetTest, coalesceSeparateOneDim) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       1, {"(x) : ( x >= 0, -x + 2 >= 0)", "(x) : ( x - 3 >= 0, -x + 4 >= 0)"},
       &context);
   expectCoalesce(2, set);
 }
 
 TEST(SetTest, coalesceContainedTwoDim) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       2,
       {
           "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)",
           "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)",
       },
       &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceCutTwoDim) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       2,
       {
           "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)",
           "(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)",
       },
       &context);
   expectCoalesce(2, set);
 }
 
 TEST(SetTest, coalesceSeparateTwoDim) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       2,
       {
           "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)",
           "(x,y) : (x >= 0, -x + 3 >= 0, y - 2 >= 0, -y + 3 >= 0)",
       },
       &context);
   expectCoalesce(2, set);
 }
 
 TEST(SetTest, coalesceContainedEq) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       2,
       {
           "(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)",
           "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)",
       },
       &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceCuttingEq) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       2,
       {
           "(x,y) : (x - 1 >= 0, -x + 3 >= 0, x - y == 0)",
           "(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)",
       },
       &context);
   expectCoalesce(2, set);
 }
 
 TEST(SetTest, coalesceSeparateEq) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       2,
       {
           "(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)",
           "(x,y) : (x >= 0, -x + 1 >= 0, x - y == 0)",
       },
       &context);
   expectCoalesce(2, set);
 }
 
 TEST(SetTest, coalesceContainedEqAsIneq) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       2,
       {
           "(x,y) : (x >= 0, -x + 3 >= 0, x - y >= 0, -x + y >= 0)",
           "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)",
       },
       &context);
   expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceContainedEqComplex) {
   MLIRContext context;
-  PresburgerSet set = parsePresburgerSetFromFACStrings(
+  PresburgerSet set = parsePresburgerSetFromPolyStrings(
       2,
       {
           "(x,y) : (x - 2 == 0, x - y == 0)",
           "(x,y) : (x - 1 >= 0, -x + 2 >= 0, x - y == 0)",
       },
       &context);
   expectCoalesce(1, set);
 }
 
 } // namespace mlir