diff --git a/mlir/include/mlir/Analysis/PresburgerSet.h b/mlir/include/mlir/Analysis/Presburger/PresburgerSet.h rename from mlir/include/mlir/Analysis/PresburgerSet.h rename to mlir/include/mlir/Analysis/Presburger/PresburgerSet.h --- a/mlir/include/mlir/Analysis/PresburgerSet.h +++ b/mlir/include/mlir/Analysis/Presburger/PresburgerSet.h @@ -6,34 +6,34 @@ // //===----------------------------------------------------------------------===// // -// 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; @@ -41,15 +41,15 @@ /// Return the number of symbolic dimensions. unsigned getNumSyms() const; - /// Return a reference to the list of FlatAffineConstraints. - ArrayRef getAllFlatAffineConstraints() const; + /// Return a reference to the list of IntegerPolyhedron. + ArrayRef 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); @@ -91,12 +91,12 @@ 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 &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; @@ -105,19 +105,19 @@ 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; + /// The list of integerPolyhedrons that this set is the union of. + SmallVector integerPolyhedrons; }; } // namespace mlir diff --git a/mlir/lib/Analysis/CMakeLists.txt b/mlir/lib/Analysis/CMakeLists.txt --- a/mlir/lib/Analysis/CMakeLists.txt +++ b/mlir/lib/Analysis/CMakeLists.txt @@ -10,7 +10,6 @@ LoopAnalysis.cpp NestedMatcher.cpp NumberOfExecutions.cpp - PresburgerSet.cpp SliceAnalysis.cpp Utils.cpp @@ -49,7 +48,6 @@ AffineStructures.cpp LoopAnalysis.cpp NestedMatcher.cpp - PresburgerSet.cpp Utils.cpp ADDITIONAL_HEADER_DIRS diff --git a/mlir/lib/Analysis/Presburger/CMakeLists.txt b/mlir/lib/Analysis/Presburger/CMakeLists.txt --- a/mlir/lib/Analysis/Presburger/CMakeLists.txt +++ b/mlir/lib/Analysis/Presburger/CMakeLists.txt @@ -2,6 +2,7 @@ IntegerPolyhedron.cpp LinearTransform.cpp Matrix.cpp + PresburgerSet.cpp Simplex.cpp Utils.cpp diff --git a/mlir/lib/Analysis/PresburgerSet.cpp b/mlir/lib/Analysis/Presburger/PresburgerSet.cpp rename from mlir/lib/Analysis/PresburgerSet.cpp rename to mlir/lib/Analysis/Presburger/PresburgerSet.cpp --- a/mlir/lib/Analysis/PresburgerSet.cpp +++ b/mlir/lib/Analysis/Presburger/PresburgerSet.cpp @@ -6,46 +6,43 @@ // //===----------------------------------------------------------------------===// -#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 -PresburgerSet::getAllFlatAffineConstraints() const { - return flatAffineConstraints; +ArrayRef 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!"); } @@ -59,20 +56,20 @@ } /// 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. @@ -85,15 +82,14 @@ /// A point is contained in the union iff any of the parts contain the point. bool PresburgerSet::containsPoint(ArrayRef 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; } @@ -112,13 +108,13 @@ 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; @@ -152,7 +148,7 @@ /// /// 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 @@ -175,20 +171,20 @@ /// 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 @@ -202,7 +198,7 @@ // 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()); @@ -314,28 +310,28 @@ 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., @@ -344,8 +340,8 @@ 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; } @@ -366,8 +362,8 @@ /// 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; @@ -375,8 +371,8 @@ bool PresburgerSet::findIntegerSample(SmallVectorImpl &sample) { // A sample exists iff any of the disjuncts contains a sample. - for (const FlatAffineConstraints &fac : flatAffineConstraints) { - if (Optional> opt = fac.findIntegerSample()) { + for (const IntegerPolyhedron &poly : integerPolyhedrons) { + if (Optional> opt = poly.findIntegerSample()) { sample = std::move(*opt); return true; } @@ -386,12 +382,12 @@ 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. @@ -400,30 +396,30 @@ 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'; } } diff --git a/mlir/lib/Analysis/Utils.cpp b/mlir/lib/Analysis/Utils.cpp --- a/mlir/lib/Analysis/Utils.cpp +++ b/mlir/lib/Analysis/Utils.cpp @@ -14,7 +14,7 @@ #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" diff --git a/mlir/unittests/Analysis/AffineStructuresParserTest.cpp b/mlir/unittests/Analysis/AffineStructuresParserTest.cpp --- a/mlir/unittests/Analysis/AffineStructuresParserTest.cpp +++ b/mlir/unittests/Analysis/AffineStructuresParserTest.cpp @@ -14,7 +14,7 @@ //===----------------------------------------------------------------------===// #include "./AffineStructuresParser.h" -#include "mlir/Analysis/PresburgerSet.h" +#include "mlir/Analysis/Presburger/PresburgerSet.h" #include diff --git a/mlir/unittests/Analysis/CMakeLists.txt b/mlir/unittests/Analysis/CMakeLists.txt --- a/mlir/unittests/Analysis/CMakeLists.txt +++ b/mlir/unittests/Analysis/CMakeLists.txt @@ -1,7 +1,6 @@ add_mlir_unittest(MLIRAnalysisTests AffineStructuresParser.cpp AffineStructuresParserTest.cpp - PresburgerSetTest.cpp ) target_link_libraries(MLIRAnalysisTests diff --git a/mlir/unittests/Analysis/Presburger/CMakeLists.txt b/mlir/unittests/Analysis/Presburger/CMakeLists.txt --- a/mlir/unittests/Analysis/Presburger/CMakeLists.txt +++ b/mlir/unittests/Analysis/Presburger/CMakeLists.txt @@ -2,6 +2,7 @@ IntegerPolyhedronTest.cpp LinearTransformTest.cpp MatrixTest.cpp + PresburgerSetTest.cpp SimplexTest.cpp ../AffineStructuresParser.cpp ) diff --git a/mlir/unittests/Analysis/PresburgerSetTest.cpp b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp rename from mlir/unittests/Analysis/PresburgerSetTest.cpp rename to mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp --- a/mlir/unittests/Analysis/PresburgerSetTest.cpp +++ b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp @@ -14,35 +14,35 @@ // //===----------------------------------------------------------------------===// -#include "mlir/Analysis/PresburgerSet.h" -#include "./AffineStructuresParser.h" +#include "mlir/Analysis/Presburger/PresburgerSet.h" +#include "../AffineStructuresParser.h" #include #include 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 fac = parseIntegerSetToFAC(str, context); +static IntegerPolyhedron parsePoly(StringRef str, MLIRContext *context) { + FailureOr 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, - ArrayRef strs, - MLIRContext *context) { +static PresburgerSet parsePresburgerSetFromPolyStrings(unsigned numDims, + ArrayRef strs, + MLIRContext *context) { PresburgerSet set = PresburgerSet::getEmptySet(numDims); for (StringRef str : strs) - set.unionFACInPlace(parseFAC(str, context)); + set.unionPolyInPlace(parsePoly(str, context)); return set; } @@ -106,21 +106,21 @@ } /// 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 facs) { +static PresburgerSet makeSetFromPoly(unsigned numDims, + ArrayRef 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); @@ -133,7 +133,7 @@ // 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)", @@ -155,7 +155,7 @@ 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); @@ -184,7 +184,7 @@ 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); @@ -213,38 +213,38 @@ 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, - {"(x) : (x - 2 >= 0, -x + 8 >= 0)", - "(x) : (x - 10 >= 0, -x + 20 >= 0)"}, - &context), + 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, - {"(x) : (-x >= 0)", - "(x) : (x - 3 >= 0, -x + 4 >= 0)", - "(x) : (x - 6 >= 0, -x + 7 >= 0)"}, - &context), - parsePresburgerSetFromFACStrings(1, - {"(x) : (x - 2 >= 0, -x + 3 >= 0)", - "(x) : (x - 5 >= 0, -x + 6 >= 0)"}, - &context), + parsePresburgerSetFromPolyStrings(1, + {"(x) : (-x >= 0)", + "(x) : (x - 3 >= 0, -x + 4 >= 0)", + "(x) : (x - 6 >= 0, -x + 7 >= 0)"}, + &context), + 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 @@ -252,13 +252,13 @@ // 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)", @@ -274,10 +274,10 @@ // 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)", @@ -298,9 +298,9 @@ // 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}, @@ -314,9 +314,9 @@ // The result should be {0} U {2}. testSubtractAtPoints( - parsePresburgerSetFromFACStrings(1, {"(x) : (x >= 0, -x + 2 >= 0)"}, - &context), - parsePresburgerSetFromFACStrings(1, {"(x) : (x - 1 == 0)"}, &context), + parsePresburgerSetFromPolyStrings(1, {"(x) : (x >= 0, -x + 2 >= 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. @@ -326,14 +326,14 @@ // 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, " @@ -347,12 +347,12 @@ // ((-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)", @@ -392,10 +392,10 @@ {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}}); testComplementAtPoints( - parsePresburgerSetFromFACStrings(2, - {"(x,y) : (x - 2 >= 0, y - 2 >= 0, " - "-x + 10 >= 0, -y + 10 >= 0)"}, - &context), + parsePresburgerSetFromPolyStrings(2, + {"(x,y) : (x - 2 >= 0, y - 2 >= 0, " + "-x + 10 >= 0, -y + 10 >= 0)"}, + &context), {{1, 1}, {2, 1}, {1, 2}, @@ -416,7 +416,7 @@ // 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); @@ -455,10 +455,10 @@ 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)); @@ -481,19 +481,19 @@ // 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))); @@ -504,28 +504,28 @@ // 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); @@ -533,7 +533,7 @@ 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); @@ -541,7 +541,7 @@ 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); @@ -549,7 +549,7 @@ 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); @@ -557,14 +557,14 @@ 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); } @@ -572,20 +572,20 @@ 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); } @@ -593,18 +593,18 @@ TEST(SetTest, coalesceCutOneDim) { MLIRContext context; PresburgerSet set = - parsePresburgerSetFromFACStrings(1, - { - "(x) : ( x >= 0, -x + 3 >= 0)", - "(x) : ( x - 2 >= 0, -x + 4 >= 0)", - }, - &context); + 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); @@ -612,7 +612,7 @@ TEST(SetTest, coalesceContainedTwoDim) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = parsePresburgerSetFromPolyStrings( 2, { "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 3 >= 0)", @@ -624,7 +624,7 @@ TEST(SetTest, coalesceCutTwoDim) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = parsePresburgerSetFromPolyStrings( 2, { "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)", @@ -636,7 +636,7 @@ TEST(SetTest, coalesceSeparateTwoDim) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = parsePresburgerSetFromPolyStrings( 2, { "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 1 >= 0)", @@ -648,7 +648,7 @@ TEST(SetTest, coalesceContainedEq) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = parsePresburgerSetFromPolyStrings( 2, { "(x,y) : (x >= 0, -x + 3 >= 0, x - y == 0)", @@ -660,7 +660,7 @@ TEST(SetTest, coalesceCuttingEq) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = parsePresburgerSetFromPolyStrings( 2, { "(x,y) : (x - 1 >= 0, -x + 3 >= 0, x - y == 0)", @@ -672,7 +672,7 @@ TEST(SetTest, coalesceSeparateEq) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = parsePresburgerSetFromPolyStrings( 2, { "(x,y) : (x - 3 >= 0, -x + 4 >= 0, x - y == 0)", @@ -684,7 +684,7 @@ 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)", @@ -696,7 +696,7 @@ TEST(SetTest, coalesceContainedEqComplex) { MLIRContext context; - PresburgerSet set = parsePresburgerSetFromFACStrings( + PresburgerSet set = parsePresburgerSetFromPolyStrings( 2, { "(x,y) : (x - 2 == 0, x - y == 0)",