diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h --- a/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h +++ b/mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h @@ -209,7 +209,8 @@ /// constraints. Returns an empty optional if the polyhedron is empty or if /// the lexmin is unbounded. Symbols are not supported and will result in /// assert-failure. - Optional> getRationalLexMin() const; + presburger_utils::MaybeOptimum> + getRationalLexMin() const; /// Swap the posA^th identifier with the posB^th identifier. virtual void swapId(unsigned posA, unsigned posB); diff --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h b/mlir/include/mlir/Analysis/Presburger/Simplex.h --- a/mlir/include/mlir/Analysis/Presburger/Simplex.h +++ b/mlir/include/mlir/Analysis/Presburger/Simplex.h @@ -18,6 +18,7 @@ #include "mlir/Analysis/Presburger/Fraction.h" #include "mlir/Analysis/Presburger/IntegerPolyhedron.h" #include "mlir/Analysis/Presburger/Matrix.h" +#include "mlir/Analysis/Presburger/Utils.h" #include "mlir/Support/LogicalResult.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/Optional.h" @@ -202,14 +203,6 @@ /// Add all the constraints from the given IntegerPolyhedron. void intersectIntegerPolyhedron(const IntegerPolyhedron &poly); - /// Returns the current sample point, which may contain non-integer (rational) - /// coordinates. Returns an empty optional when the tableau is empty. - /// - /// Also returns empty when the big M parameter is used and a variable - /// has a non-zero big M coefficient, meaning its value is infinite or - /// unbounded. - Optional> getRationalSample() const; - /// Print the tableau's internal state. void print(raw_ostream &os) const; void dump() const; @@ -441,9 +434,18 @@ unsigned getSnapshot() { return SimplexBase::getSnapshotBasis(); } /// Return the lexicographically minimum rational solution to the constraints. - Optional> getRationalLexMin(); + presburger_utils::MaybeOptimum> getRationalLexMin(); protected: + /// Returns the current sample point, which may contain non-integer (rational) + /// coordinates. Returns an empty optimum when the tableau is empty. + /// + /// Returns an unbounded optimum when the big M parameter is used and a + /// variable has a non-zero big M coefficient, meaning its value is infinite + /// or unbounded. + presburger_utils::MaybeOptimum> + getRationalSample() const; + /// Undo the addition of the last constraint. This is only called while /// rolling back. void undoLastConstraint() final; @@ -510,15 +512,16 @@ /// /// Returns a Fraction denoting the optimum, or a null value if no optimum /// exists, i.e., if the expression is unbounded in this direction. - Optional computeRowOptimum(Direction direction, unsigned row); + presburger_utils::MaybeOptimum + computeRowOptimum(Direction direction, unsigned row); /// Compute the maximum or minimum value of the given expression, depending on /// direction. Should not be called when the Simplex is empty. /// /// Returns a Fraction denoting the optimum, or a null value if no optimum /// exists, i.e., if the expression is unbounded in this direction. - Optional computeOptimum(Direction direction, - ArrayRef coeffs); + presburger_utils::MaybeOptimum + computeOptimum(Direction direction, ArrayRef coeffs); /// Returns whether the perpendicular of the specified constraint is a /// is a direction along which the polytope is bounded. @@ -537,10 +540,10 @@ void detectRedundant(); /// Returns a (min, max) pair denoting the minimum and maximum integer values - /// of the given expression. If either of the values is unbounded, an empty - /// optional is returned in its place. If the result has min > max then no - /// integer value exists. - std::pair, Optional> + /// of the given expression. If no integer value exists, both results will be + /// of kind Empty. + std::pair, + presburger_utils::MaybeOptimum> computeIntegerBounds(ArrayRef coeffs); /// Returns true if the polytope is unbounded, i.e., extends to infinity in @@ -569,6 +572,10 @@ /// None. Optional> getSamplePointIfIntegral() const; + /// Returns the current sample point, which may contain non-integer (rational) + /// coordinates. Returns an empty optional when the tableau is empty. + Optional> getRationalSample() const; + private: friend class GBRSimplex; @@ -610,7 +617,8 @@ /// /// Returns a Fraction denoting the optimum, or a null value if no optimum /// exists, i.e., if the expression is unbounded in this direction. - Optional computeOptimum(Direction direction, Unknown &u); + presburger_utils::MaybeOptimum computeOptimum(Direction direction, + Unknown &u); /// Mark the specified unknown redundant. This operation is added to the undo /// log and will be undone by rollbacks. The specified unknown must be in row diff --git a/mlir/include/mlir/Analysis/Presburger/Utils.h b/mlir/include/mlir/Analysis/Presburger/Utils.h --- a/mlir/include/mlir/Analysis/Presburger/Utils.h +++ b/mlir/include/mlir/Analysis/Presburger/Utils.h @@ -22,6 +22,67 @@ namespace presburger_utils { +/// This class represents the result of operations optimizing something subject +/// to some constraints. If the constraints were not satisfiable the, kind will +/// be Empty. If the optimum is unbounded, the kind is Unbounded, and if the +/// optimum is bounded, the kind will be Bounded and `optimum` holds the optimal +/// value. +enum class OptimumKind { Empty, Unbounded, Bounded }; +template +class MaybeOptimum { +public: +private: + OptimumKind kind = OptimumKind::Empty; + T optimum; + +public: + MaybeOptimum() = default; + MaybeOptimum(OptimumKind kind) : kind(kind) { + assert(kind != OptimumKind::Bounded && + "Bounded optima should be constructed by specifying the optimum!"); + } + MaybeOptimum(const T &optimum) + : kind(OptimumKind::Bounded), optimum(optimum) {} + + OptimumKind getKind() const { return kind; } + bool isBounded() const { return kind == OptimumKind::Bounded; } + bool isUnbounded() const { return kind == OptimumKind::Unbounded; } + bool isEmpty() const { return kind == OptimumKind::Empty; } + + Optional getOptimumIfBounded() const { return optimum; } + const T &getBoundedOptimum() const { + assert(kind == OptimumKind::Bounded && + "This should be called only for bounded optima"); + return optimum; + } + T &getBoundedOptimum() { + assert(kind == OptimumKind::Bounded && + "This should be called only for bounded optima"); + return optimum; + } + const T &operator*() const { return getBoundedOptimum(); } + T &operator*() { return getBoundedOptimum(); } + const T *operator->() const { return &getBoundedOptimum(); } + T *operator->() { return &getBoundedOptimum(); } + bool operator==(const MaybeOptimum &other) const { + if (kind != other.kind) + return false; + if (kind != OptimumKind::Bounded) + return true; + return optimum == other.optimum; + } + + // Given f that takes a T and returns a U, convert this `MaybeOptimum` to + // a `MaybeOptimum` by applying `f` to the bounded optimum if it exists, or + // returning a MaybeOptimum of the same kind otherwise. + template + auto map(const Function &f) const & -> MaybeOptimum { + if (kind == OptimumKind::Bounded) + return f(optimum); + return kind; + } +}; + /// `ReprKind` enum is used to set the constraint type in `MaybeLocalRepr`. enum class ReprKind { Inequality, Equality, None }; diff --git a/mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp b/mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp --- a/mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp +++ b/mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp @@ -72,14 +72,14 @@ return PresburgerSet(*this).isSubsetOf(PresburgerSet(other)); } -Optional> +MaybeOptimum> IntegerPolyhedron::getRationalLexMin() const { assert(getNumSymbolIds() == 0 && "Symbols are not supported!"); - Optional> maybeLexMin = + MaybeOptimum> maybeLexMin = LexSimplex(*this).getRationalLexMin(); - if (!maybeLexMin) - return {}; + if (!maybeLexMin.isBounded()) + return maybeLexMin; // The Simplex returns the lexmin over all the variables including locals. But // locals are not actually part of the space and should not be returned in the @@ -1033,20 +1033,23 @@ bool hasUnboundedId = false; for (unsigned i = 0, e = getNumDimAndSymbolIds(); i < e; ++i) { dim[i] = 1; - Optional min, max; + MaybeOptimum min, max; std::tie(min, max) = simplex.computeIntegerBounds(dim); dim[i] = 0; + assert((!min.isEmpty() && !max.isEmpty()) && + "Polytope should be rationally non-empty!"); + // One of the dimensions is unbounded. Note this fact. We will return // unbounded if none of the other dimensions makes the volume zero. - if (!min || !max) { + if (min.isUnbounded() || max.isUnbounded()) { hasUnboundedId = true; continue; } // In this case there are no valid integer points and the volume is // definitely zero. - if (*min > *max) + if (min.getBoundedOptimum() > max.getBoundedOptimum()) return 0; count *= (*max - *min + 1); diff --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp --- a/mlir/lib/Analysis/Presburger/Simplex.cpp +++ b/mlir/lib/Analysis/Presburger/Simplex.cpp @@ -12,6 +12,8 @@ #include "llvm/ADT/Optional.h" namespace mlir { + +using namespace presburger_utils; using Direction = Simplex::Direction; const int nullIndex = std::numeric_limits::max(); @@ -157,7 +159,7 @@ } } // namespace -Optional> LexSimplex::getRationalLexMin() { +MaybeOptimum> LexSimplex::getRationalLexMin() { restoreRationalConsistency(); return getRationalSample(); } @@ -786,14 +788,14 @@ addEquality(poly.getEquality(i)); } -Optional Simplex::computeRowOptimum(Direction direction, - unsigned row) { +MaybeOptimum Simplex::computeRowOptimum(Direction direction, + unsigned row) { // Keep trying to find a pivot for the row in the specified direction. while (Optional maybePivot = findPivot(row, direction)) { // If findPivot returns a pivot involving the row itself, then the optimum // is unbounded, so we return None. if (maybePivot->row == row) - return {}; + return OptimumKind::Unbounded; pivot(*maybePivot); } @@ -805,34 +807,36 @@ /// Compute the optimum of the specified expression in the specified direction, /// or None if it is unbounded. -Optional Simplex::computeOptimum(Direction direction, - ArrayRef coeffs) { - assert(!empty && "Simplex should not be empty"); - +MaybeOptimum Simplex::computeOptimum(Direction direction, + ArrayRef coeffs) { + if (empty) + return OptimumKind::Empty; unsigned snapshot = getSnapshot(); unsigned conIndex = addRow(coeffs); unsigned row = con[conIndex].pos; - Optional optimum = computeRowOptimum(direction, row); + MaybeOptimum optimum = computeRowOptimum(direction, row); rollback(snapshot); return optimum; } -Optional Simplex::computeOptimum(Direction direction, Unknown &u) { - assert(!empty && "Simplex should not be empty!"); +MaybeOptimum Simplex::computeOptimum(Direction direction, + Unknown &u) { + if (empty) + return OptimumKind::Empty; if (u.orientation == Orientation::Column) { unsigned column = u.pos; Optional pivotRow = findPivotRow({}, direction, column); // If no pivot is returned, the constraint is unbounded in the specified // direction. if (!pivotRow) - return {}; + return OptimumKind::Unbounded; pivot(*pivotRow, column); } unsigned row = u.pos; - Optional optimum = computeRowOptimum(direction, row); + MaybeOptimum optimum = computeRowOptimum(direction, row); if (u.restricted && direction == Direction::Down && - (!optimum || *optimum < Fraction(0, 1))) { + (optimum.isUnbounded() || *optimum < Fraction(0, 1))) { if (failed(restoreRow(u))) llvm_unreachable("Could not restore row!"); } @@ -844,7 +848,7 @@ "in an empty set."); // The constraint's perpendicular is already bounded below, since it is a // constraint. If it is also bounded above, we can return true. - return computeOptimum(Direction::Up, con[constraintIndex]).hasValue(); + return computeOptimum(Direction::Up, con[constraintIndex]).isBounded(); } /// Redundant constraints are those that are in row orientation and lie in @@ -895,8 +899,8 @@ } unsigned row = u.pos; - Optional minimum = computeRowOptimum(Direction::Down, row); - if (!minimum || *minimum < Fraction(0, 1)) { + MaybeOptimum minimum = computeRowOptimum(Direction::Down, row); + if (minimum.isUnbounded() || *minimum < Fraction(0, 1)) { // Constraint is unbounded below or can attain negative sample values and // hence is not redundant. if (failed(restoreRow(u))) @@ -916,12 +920,10 @@ for (unsigned i = 0; i < var.size(); ++i) { dir[i] = 1; - Optional maybeMax = computeOptimum(Direction::Up, dir); - if (!maybeMax) + if (computeOptimum(Direction::Up, dir).isUnbounded()) return true; - Optional maybeMin = computeOptimum(Direction::Down, dir); - if (!maybeMin) + if (computeOptimum(Direction::Down, dir).isUnbounded()) return true; dir[i] = 0; @@ -1010,7 +1012,7 @@ return result; } -Optional> SimplexBase::getRationalSample() const { +Optional> Simplex::getRationalSample() const { if (empty) return {}; @@ -1022,20 +1024,41 @@ // If the variable is in column position, its sample value is zero. sample.emplace_back(0, 1); } else { + // If the variable is in row position, its sample value is the + // entry in the constant column divided by the denominator. int64_t denom = tableau(u.pos, 0); + sample.emplace_back(tableau(u.pos, 1), denom); + } + } + return sample; +} - // When the big M parameter is being used, each variable x is represented - // as M + x, so its sample value is finite only if it is of the form - // 1*M + c. If the coefficient of M is not one then the sample value is - // infinite, and we return an empty optional. - if (usingBigM) - if (tableau(u.pos, 2) != denom) - return {}; +MaybeOptimum> LexSimplex::getRationalSample() const { + if (empty) + return OptimumKind::Empty; - // Otherwise, If the variable is in row position, its sample value is the - // entry in the constant column divided by the denominator. - sample.emplace_back(tableau(u.pos, 1), denom); + SmallVector sample; + sample.reserve(var.size()); + // Push the sample value for each variable into the vector. + for (const Unknown &u : var) { + // When the big M parameter is being used, each variable x is represented + // as M + x, so its sample value is finite if and only if it is of the + // form 1*M + c. If the coefficient of M is not one then the sample value + // is infinite, and we return an empty optional. + + if (u.orientation == Orientation::Column) { + // If the variable is in column position, the sample value of M + x is + // zero, so x = -M which is unbounded. + return OptimumKind::Unbounded; } + + // If the variable is in row position, its sample value is the + // entry in the constant column divided by the denominator. + int64_t denom = tableau(u.pos, 0); + if (usingBigM) + if (tableau(u.pos, 2) != denom) + return OptimumKind::Unbounded; + sample.emplace_back(tableau(u.pos, 1), denom); } return sample; } @@ -1088,9 +1111,9 @@ } /// Compute max(dotProduct(dir, x - y)). Fraction computeWidth(ArrayRef dir) { - Optional maybeWidth = + MaybeOptimum maybeWidth = simplex.computeOptimum(Direction::Up, getCoeffsForDirection(dir)); - assert(maybeWidth.hasValue() && "Width should not be unbounded!"); + assert(maybeWidth.isBounded() && "Width should be bounded!"); return *maybeWidth; } @@ -1108,9 +1131,9 @@ unsigned snap = simplex.getSnapshot(); unsigned conIndex = simplex.addRow(getCoeffsForDirection(dir)); unsigned row = simplex.con[conIndex].pos; - Optional maybeWidth = + MaybeOptimum maybeWidth = simplex.computeRowOptimum(Simplex::Direction::Up, row); - assert(maybeWidth.hasValue() && "Width should not be unbounded!"); + assert(maybeWidth.isBounded() && "Width should be bounded!"); dualDenom = simplex.tableau(row, 0); dual.clear(); @@ -1456,16 +1479,32 @@ llvm::to_vector<8>(basis.getRow(level)); basisCoeffs.push_back(0); - Optional minRoundedUp, maxRoundedDown; + MaybeOptimum minRoundedUp, maxRoundedDown; std::tie(minRoundedUp, maxRoundedDown) = computeIntegerBounds(basisCoeffs); + // We don't have any integer values in the range. + // Pop the stack and return up a level. + if (minRoundedUp.isEmpty() || maxRoundedDown.isEmpty()) { + assert((minRoundedUp.isEmpty() && maxRoundedDown.isEmpty()) && + "If one bound is empty, both should be."); + snapshotStack.pop_back(); + nextValueStack.pop_back(); + upperBoundStack.pop_back(); + level--; + continue; + } + + // We already checked the empty case above. + assert((minRoundedUp.isBounded() && maxRoundedDown.isBounded()) && + "Polyhedron should be bounded!"); + // Heuristic: if the sample point is integral at this point, just return // it. if (auto maybeSample = getSamplePointIfIntegral()) return *maybeSample; - if (minRoundedUp < maxRoundedDown) { + if (*minRoundedUp < *maxRoundedDown) { reduceBasis(basis, level); basisCoeffs = llvm::to_vector<8>(basis.getRow(level)); basisCoeffs.push_back(0); @@ -1515,18 +1554,12 @@ /// Compute the minimum and maximum integer values the expression can take. We /// compute each separately. -std::pair, Optional> +std::pair, MaybeOptimum> Simplex::computeIntegerBounds(ArrayRef coeffs) { - Optional minRoundedUp; - if (Optional maybeMin = - computeOptimum(Simplex::Direction::Down, coeffs)) - minRoundedUp = ceil(*maybeMin); - - Optional maxRoundedDown; - if (Optional maybeMax = - computeOptimum(Simplex::Direction::Up, coeffs)) - maxRoundedDown = floor(*maybeMax); - + MaybeOptimum minRoundedUp( + computeOptimum(Simplex::Direction::Down, coeffs).map(ceil)); + MaybeOptimum maxRoundedDown( + computeOptimum(Simplex::Direction::Up, coeffs).map(floor)); return {minRoundedUp, maxRoundedDown}; } @@ -1586,8 +1619,12 @@ /// or equal to zero, the polytope entirely lies in the half-space defined by /// `coeffs >= 0`. bool Simplex::isRedundantInequality(ArrayRef coeffs) { - Optional minimum = computeOptimum(Direction::Down, coeffs); - return minimum && *minimum >= Fraction(0, 1); + assert(!empty && + "It is not meaningful to ask about redundancy in an empty set!"); + MaybeOptimum minimum = computeOptimum(Direction::Down, coeffs); + assert(!minimum.isEmpty() && + "Optima should be non-empty for a non-empty set"); + return minimum.isBounded() && *minimum >= Fraction(0, 1); } /// Check whether the equality given by `coeffs == 0` is redundant given @@ -1595,10 +1632,14 @@ /// always zero under the existing constraints. `coeffs` is always zero /// when the minimum and maximum value that `coeffs` can take are both zero. bool Simplex::isRedundantEquality(ArrayRef coeffs) { - Optional minimum = computeOptimum(Direction::Down, coeffs); - Optional maximum = computeOptimum(Direction::Up, coeffs); - return minimum && maximum && *maximum == Fraction(0, 1) && - *minimum == Fraction(0, 1); + assert(!empty && + "It is not meaningful to ask about redundancy in an empty set!"); + MaybeOptimum minimum = computeOptimum(Direction::Down, coeffs); + MaybeOptimum maximum = computeOptimum(Direction::Up, coeffs); + assert((!minimum.isEmpty() && !maximum.isEmpty()) && + "Optima should be non-empty for a non-empty set"); + return minimum.isBounded() && maximum.isBounded() && + *maximum == Fraction(0, 1) && *minimum == Fraction(0, 1); } } // namespace mlir diff --git a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp --- a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp +++ b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp @@ -16,7 +16,7 @@ #include namespace mlir { - +using namespace presburger_utils; using testing::ElementsAre; enum class TestFunction { Sample, Empty }; @@ -1057,12 +1057,14 @@ void expectRationalLexMin(const IntegerPolyhedron &poly, ArrayRef min) { auto lexMin = poly.getRationalLexMin(); - ASSERT_TRUE(lexMin.hasValue()); + ASSERT_TRUE(lexMin.isBounded()); EXPECT_EQ(ArrayRef(*lexMin), min); } -void expectNoRationalLexMin(const IntegerPolyhedron &poly) { - EXPECT_FALSE(poly.getRationalLexMin().hasValue()); +void expectNoRationalLexMin(OptimumKind kind, const IntegerPolyhedron &poly) { + ASSERT_NE(kind, OptimumKind::Bounded) + << "Use expectRationalLexMin for bounded min"; + EXPECT_EQ(poly.getRationalLexMin().getKind(), kind); } TEST(IntegerPolyhedronTest, getRationalLexMin) { @@ -1118,6 +1120,7 @@ // Same as above with one constraint removed, making the lexmin unbounded. expectNoRationalLexMin( + OptimumKind::Unbounded, parsePoly("(x, y, z, w) : (3*x + 2*y + 10 >= 0, -4*x + 7*y + 10 >= 0," "-3*y + 10 >= 0, 3*z + 2*w - 9*x - 12*y >= 0," "-4*z + 7*w + - 9*x - 9*y - 10>= 0)", @@ -1125,12 +1128,14 @@ // Again, the lexmin is unbounded. expectNoRationalLexMin( + OptimumKind::Unbounded, parsePoly("(x, y, z) : (2*x + 5*y + 8*z - 10 >= 0," "2*x + 10*y + 8*z - 10 >= 0, 2*x + 5*y + 10*z - 10 >= 0)", &context)); // The set is empty. - expectNoRationalLexMin(parsePoly("(x) : (2*x >= 0, -x - 1 >= 0)", &context)); + expectNoRationalLexMin(OptimumKind::Empty, + parsePoly("(x) : (2*x >= 0, -x - 1 >= 0)", &context)); } static void diff --git a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp --- a/mlir/unittests/Analysis/Presburger/SimplexTest.cpp +++ b/mlir/unittests/Analysis/Presburger/SimplexTest.cpp @@ -15,6 +15,7 @@ #include namespace mlir { +using namespace presburger_utils; /// Take a snapshot, add constraints making the set empty, and rollback. /// The set should not be empty after rolling back. We add additional @@ -406,9 +407,9 @@ // After the rollback, the only remaining constraint is x <= -1. // The maximum value of x should be -1. simplex.rollback(snapshot); - Optional maxX = + MaybeOptimum maxX = simplex.computeOptimum(Simplex::Direction::Up, {1, 0, 0}); - EXPECT_TRUE(maxX.hasValue() && *maxX == Fraction(-1, 1)); + EXPECT_TRUE(maxX.isBounded() && *maxX == Fraction(-1, 1)); } TEST(SimplexTest, addInequality_already_redundant) { @@ -440,8 +441,9 @@ EXPECT_EQ(simplex.getNumVariables(), 2u); EXPECT_EQ(simplex.getNumConstraints(), 2u); - EXPECT_EQ(simplex.computeIntegerBounds({0, 1, 0}), - std::make_pair(Optional(yMin), Optional(yMax))); + EXPECT_EQ( + simplex.computeIntegerBounds({0, 1, 0}), + std::make_pair(MaybeOptimum(yMin), MaybeOptimum(yMax))); simplex.rollback(snapshot1); EXPECT_EQ(simplex.getNumVariables(), 1u);