[MLIR][Presburger] Introduce MaybeOptimum type to represent computed optima

[arjunp]

Summary

This allows to differentiate between the cases where the optimum does not
exist due to being unbounded and due to the polytope being empty.

[arjunp]

clang-format

[Groverkss]

mlir/include/mlir/Analysis/Presburger/Utils.h

84

Any reason for MaybeOptimum to not be in presburger_utils?

[arjunp]

mlir/include/mlir/Analysis/Presburger/Utils.h

84

It's part of Simplex really, logically. It should be in the same namespace as it. We should move Simplex into a presburger namespace maybe.

[arjunp]

mlir/include/mlir/Analysis/Presburger/Utils.h

84

For now I don't mind putting it in presburger_utils. We can move them both into a presburger namespace as you suggested. We can do that later in another patch

[Groverkss]

mlir/include/mlir/Analysis/Presburger/Utils.h

84

You can keep it in presburger_utils for now and I will send a patch later today moving things to presburger namespace.

[arjunp]

Move MaybeOptimum into presburger_utils

[arjunp]

Rebase on main

[arjunp]

clang-format

[Groverkss]

LGTM.

mlir/include/mlir/Analysis/Presburger/IntegerPolyhedron.h

public:
   /// Remove the (in)equalities at positions [start, end).
   void removeEqualityRange(unsigned start, unsigned end);
   void removeInequalityRange(unsigned start, unsigned end);
 
   /// Get the lexicographically minimum rational point satisfying the
   /// 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<SmallVector<Fraction, 8>> getRationalLexMin() const;
+  MaybeOptimum<SmallVector<Fraction, 8>> getRationalLexMin() const;
 
   /// Swap the posA^th identifier with the posB^th identifier.
   virtual void swapId(unsigned posA, unsigned posB);
 
   /// Removes all equalities and inequalities.
   void clearConstraints();
 
   /// Sets the `values.size()` identifiers starting at `po`s to the specified

mlir/include/mlir/Analysis/Presburger/Simplex.h

 //===----------------------------------------------------------------------===//
 
 #ifndef MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
 #define MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
 
 #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"
 #include "llvm/ADT/SmallVector.h"
 #include "llvm/Support/StringSaver.h"
 #include "llvm/Support/raw_ostream.h"
 
 namespace mlir {
public:
   unsigned getSnapshotBasis();
 
   /// Rollback to a snapshot. This invalidates all later snapshots.
   void rollback(unsigned snapshot);
 
   /// 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<SmallVector<Fraction, 8>> getRationalSample() const;
-
   /// Print the tableau's internal state.
   void print(raw_ostream &os) const;
   void dump() const;
 
 protected:
   enum class Orientation { Row, Column };
 
   /// An Unknown is either a variable or a constraint. It is always associated
public:
   void addInequality(ArrayRef<int64_t> coeffs) final {
     addRow(coeffs, /*makeRestricted=*/true);
   }
 
   /// Get a snapshot of the current state. This is used for rolling back.
   unsigned getSnapshot() { return SimplexBase::getSnapshotBasis(); }
 
   /// Return the lexicographically minimum rational solution to the constraints.
-  Optional<SmallVector<Fraction, 8>> getRationalLexMin();
+  MaybeOptimum<SmallVector<Fraction, 8>> 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.
+  MaybeOptimum<SmallVector<Fraction, 8>> getRationalSample() const;
+
   /// Undo the addition of the last constraint. This is only called while
   /// rolling back.
   void undoLastConstraint() final;
 
   /// Make the tableau configuration consistent.
   void restoreRationalConsistency();
 
   /// Return whether the specified row is violated;
public:
   void addInequality(ArrayRef<int64_t> coeffs) final;
 
   /// Compute the maximum or minimum value of the given row, depending on
   /// direction. The specified row is never pivoted. On return, the row may
   /// have a negative sample value if the direction is down.
   ///
   /// 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<Fraction> computeRowOptimum(Direction direction, unsigned row);
+  MaybeOptimum<Fraction> 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<Fraction> computeOptimum(Direction direction,
+  MaybeOptimum<Fraction> computeOptimum(Direction direction,
                                         ArrayRef<int64_t> coeffs);
 
   /// Returns whether the perpendicular of the specified constraint is a
   /// is a direction along which the polytope is bounded.
   bool isBoundedAlongConstraint(unsigned constraintIndex);
 
   /// Returns whether the specified constraint has been marked as redundant.
   /// Constraints are numbered from 0 starting at the first added inequality.
   /// Equalities are added as a pair of inequalities and so correspond to two
   /// inequalities with successive indices.
   bool isMarkedRedundant(unsigned constraintIndex) const;
 
   /// Finds a subset of constraints that is redundant, i.e., such that
   /// the set of solutions does not change if these constraints are removed.
   /// Marks these constraints as redundant. Whether a specific constraint has
   /// been marked redundant can be queried using isMarkedRedundant.
   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<int64_t>, Optional<int64_t>>
+  /// of the given expression. If no integer value exists, both results will be
+  /// of kind Empty.
+  std::pair<MaybeOptimum<int64_t>, MaybeOptimum<int64_t>>
   computeIntegerBounds(ArrayRef<int64_t> coeffs);
 
   /// Returns true if the polytope is unbounded, i.e., extends to infinity in
   /// some direction. Otherwise, returns false.
   bool isUnbounded();
 
   /// Make a tableau to represent a pair of points in the given tableaus, one in
   /// tableau A and one in B.
public:
   /// Returns true if this Simplex's polytope is a rational subset of `poly`.
   /// Otherwise, returns false.
   bool isRationalSubsetOf(const IntegerPolyhedron &poly);
 
   /// Returns the current sample point if it is integral. Otherwise, returns
   /// None.
   Optional<SmallVector<int64_t, 8>> getSamplePointIfIntegral() const;
 
+  /// Returns the current sample point, which may contain non-integer (rational)
+  /// coordinates. Returns an empty optional when the tableau is empty.
+  Optional<SmallVector<Fraction, 8>> getRationalSample() const;
+
 private:
   friend class GBRSimplex;
 
   /// Restore the unknown to a non-negative sample value.
   ///
   /// Returns success if the unknown was successfully restored to a non-negative
   /// sample value, failure otherwise.
   LogicalResult restoreRow(Unknown &u);
private:
 
   /// Compute the maximum or minimum of the specified Unknown, depending on
   /// direction. The specified unknown may be pivoted. If the unknown is
   /// restricted, it will have a non-negative sample value on return.
   /// Should not be called if 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<Fraction> computeOptimum(Direction direction, Unknown &u);
+  MaybeOptimum<Fraction> 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
   /// orientation.
   void markRowRedundant(Unknown &u);
 
   /// Reduce the given basis, starting at the specified level, using general
   /// basis reduction.
   void reduceBasis(Matrix &basis, unsigned level);
 };
 
 } // namespace mlir
 
 #endif // MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H

mlir/include/mlir/Analysis/Presburger/Utils.h

 
 #include "mlir/Support/LLVM.h"
 #include "llvm/ADT/STLExtras.h"
 
 namespace mlir {
 
 class IntegerPolyhedron;
 
-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 <typename T>
+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<T> 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<T> &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<T>` to
+  // a `MaybeOptimum<U>` by applying `f` to the bounded optimum if it exists, or
+  // returning a MaybeOptimum of the same kind otherwise.
+  template <class Function>
+  auto map(const Function &f) const & -> MaybeOptimum<decltype(f(optimum))> {
+    if (kind == OptimumKind::Bounded)
+      return f(optimum);
+    return kind;
+  }
+};
 
+namespace presburger_utils {
 /// `ReprKind` enum is used to set the constraint type in `MaybeLocalRepr`.
 enum class ReprKind { Inequality, Equality, None };
 
 /// `MaybeLocalRepr` contains the indices of the contraints that can be
 /// expressed as a floordiv of an affine function. If it's an `equality`
 /// contraint `equalityIdx` is set, in case of `inequality` the `lowerBoundIdx`
 /// and `upperBoundIdx` is set. By default the kind attribute is set to None.
 struct MaybeLocalRepr {

mlir/lib/Analysis/Presburger/IntegerPolyhedron.cpp

 bool IntegerPolyhedron::isEqual(const IntegerPolyhedron &other) const {
   return PresburgerSet(*this).isEqual(PresburgerSet(other));
 }
 
 bool IntegerPolyhedron::isSubsetOf(const IntegerPolyhedron &other) const {
   return PresburgerSet(*this).isSubsetOf(PresburgerSet(other));
 }
 
-Optional<SmallVector<Fraction, 8>>
+MaybeOptimum<SmallVector<Fraction, 8>>
 IntegerPolyhedron::getRationalLexMin() const {
   assert(getNumSymbolIds() == 0 && "Symbols are not supported!");
-  Optional<SmallVector<Fraction, 8>> maybeLexMin =
+  MaybeOptimum<SmallVector<Fraction, 8>> 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
   // result. Since the locals are placed last in the list of identifiers, they
   // will be minimized last in the lexmin. So simply truncating out the locals
   // from the end of the answer gives the desired lexmin over the dimensions.
   assert(maybeLexMin->size() == getNumIds() &&
          "Incorrect number of vars in lexMin!");
Optional<uint64_t> IntegerPolyhedron::computeVolume() const {
   //
   // If there is no such empty dimension, if any dimension is unbounded we
   // just return the result as unbounded.
   uint64_t count = 1;
   SmallVector<int64_t, 8> dim(getNumIds() + 1);
   bool hasUnboundedId = false;
   for (unsigned i = 0, e = getNumDimAndSymbolIds(); i < e; ++i) {
     dim[i] = 1;
-    Optional<int64_t> min, max;
+    MaybeOptimum<int64_t> 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);
   }
 
   if (count == 0)
     return 0;
   if (hasUnboundedId)
void IntegerPolyhedron::mergeLocalIds(IntegerPolyhedron &other) {
 
   IntegerPolyhedron &polyA = *this;
   IntegerPolyhedron &polyB = other;
 
   // Merge local ids of polyA and polyB without using division information,
   // i.e. append local ids of `polyB` to `polyA` and insert local ids of `polyA`
   // to `polyB` at start of its local ids.
   unsigned initLocals = polyA.getNumLocalIds();
   insertLocalId(polyA.getNumLocalIds(), polyB.getNumLocalIds());
   polyB.insertLocalId(0, initLocals);
 
   // Get division representations from each poly.
   std::vector<SmallVector<int64_t, 8>> divsA, divsB;
   SmallVector<unsigned, 4> denomsA, denomsB;
   polyA.getLocalReprs(divsA, denomsA);
   polyB.getLocalReprs(divsB, denomsB);
 

mlir/lib/Analysis/Presburger/Simplex.cpp

bool signMatchesDirection(int64_t elem, Direction direction) {
   return direction == Direction::Up ? elem > 0 : elem < 0;
 }
 
 Direction flippedDirection(Direction direction) {
   return direction == Direction::Up ? Direction::Down : Simplex::Direction::Up;
 }
 } // namespace
 
-Optional<SmallVector<Fraction, 8>> LexSimplex::getRationalLexMin() {
+MaybeOptimum<SmallVector<Fraction, 8>> LexSimplex::getRationalLexMin() {
   restoreRationalConsistency();
   return getRationalSample();
 }
 
 bool LexSimplex::rowIsViolated(unsigned row) const {
   if (tableau(row, 2) < 0)
     return true;
   if (tableau(row, 2) == 0 && tableau(row, 1) < 0)
void SimplexBase::intersectIntegerPolyhedron(const IntegerPolyhedron &poly) {
   assert(poly.getNumIds() == getNumVariables() &&
          "IntegerPolyhedron must have same dimensionality as simplex");
   for (unsigned i = 0, e = poly.getNumInequalities(); i < e; ++i)
     addInequality(poly.getInequality(i));
   for (unsigned i = 0, e = poly.getNumEqualities(); i < e; ++i)
     addEquality(poly.getEquality(i));
 }
 
-Optional<Fraction> Simplex::computeRowOptimum(Direction direction,
+MaybeOptimum<Fraction> Simplex::computeRowOptimum(Direction direction,
                                                   unsigned row) {
   // Keep trying to find a pivot for the row in the specified direction.
   while (Optional<Pivot> 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);
   }
 
   // The row has reached its optimal sample value, which we return.
   // The sample value is the entry in the constant column divided by the common
   // denominator for this row.
   return Fraction(tableau(row, 1), tableau(row, 0));
 }
 
 /// Compute the optimum of the specified expression in the specified direction,
 /// or None if it is unbounded.
-Optional<Fraction> Simplex::computeOptimum(Direction direction,
+MaybeOptimum<Fraction> Simplex::computeOptimum(Direction direction,
                                                ArrayRef<int64_t> coeffs) {
-  assert(!empty && "Simplex should not be empty");
-
+  if (empty)
+    return OptimumKind::Empty;
   unsigned snapshot = getSnapshot();
   unsigned conIndex = addRow(coeffs);
   unsigned row = con[conIndex].pos;
-  Optional<Fraction> optimum = computeRowOptimum(direction, row);
+  MaybeOptimum<Fraction> optimum = computeRowOptimum(direction, row);
   rollback(snapshot);
   return optimum;
 }
 
-Optional<Fraction> Simplex::computeOptimum(Direction direction, Unknown &u) {
-  assert(!empty && "Simplex should not be empty!");
+MaybeOptimum<Fraction> Simplex::computeOptimum(Direction direction,
+                                               Unknown &u) {
+  if (empty)
+    return OptimumKind::Empty;
   if (u.orientation == Orientation::Column) {
     unsigned column = u.pos;
     Optional<unsigned> 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<Fraction> optimum = computeRowOptimum(direction, row);
+  MaybeOptimum<Fraction> 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!");
   }
   return optimum;
 }
 
 bool Simplex::isBoundedAlongConstraint(unsigned constraintIndex) {
   assert(!empty && "It is not meaningful to ask whether a direction is bounded "
                    "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
 /// rows 0 to nRedundant - 1.
 bool Simplex::isMarkedRedundant(unsigned constraintIndex) const {
   const Unknown &u = con[constraintIndex];
   return u.orientation == Orientation::Row && u.pos < nRedundant;
 }
if (u.orientation == Orientation::Column) {
       // If no downward pivot is returned, the constraint is unbounded below
       // and hence not redundant.
       if (!pivotRow)
         continue;
       pivot(*pivotRow, column);
     }
 
     unsigned row = u.pos;
-    Optional<Fraction> minimum = computeRowOptimum(Direction::Down, row);
-    if (!minimum || *minimum < Fraction(0, 1)) {
+    MaybeOptimum<Fraction> 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)))
         llvm_unreachable("Could not restore non-redundant row!");
       continue;
     }
 
     markRowRedundant(u);
   }
 }
 
 bool Simplex::isUnbounded() {
   if (empty)
     return false;
 
   SmallVector<int64_t, 8> dir(var.size() + 1);
   for (unsigned i = 0; i < var.size(); ++i) {
     dir[i] = 1;
 
-    Optional<Fraction> maybeMax = computeOptimum(Direction::Up, dir);
-    if (!maybeMax)
+    if (computeOptimum(Direction::Up, dir).isUnbounded())
       return true;
 
-    Optional<Fraction> maybeMin = computeOptimum(Direction::Down, dir);
-    if (!maybeMin)
+    if (computeOptimum(Direction::Down, dir).isUnbounded())
       return true;
 
     dir[i] = 0;
   }
   return false;
 }
 
 /// Make a tableau to represent a pair of points in the original tableau.
Simplex Simplex::makeProduct(const Simplex &a, const Simplex &b) {
   for (unsigned row = a.nRedundant; row < a.nRow; ++row)
     appendRowFromA(row);
   for (unsigned row = b.nRedundant; row < b.nRow; ++row)
     appendRowFromB(row);
 
   return result;
 }
 
-Optional<SmallVector<Fraction, 8>> SimplexBase::getRationalSample() const {
+Optional<SmallVector<Fraction, 8>> Simplex::getRationalSample() const {
   if (empty)
     return {};
 
   SmallVector<Fraction, 8> sample;
   sample.reserve(var.size());
   // Push the sample value for each variable into the vector.
   for (const Unknown &u : var) {
     if (u.orientation == Orientation::Column) {
       // 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<SmallVector<Fraction, 8>> LexSimplex::getRationalSample() const {
+  if (empty)
+    return OptimumKind::Empty;
+
+  SmallVector<Fraction, 8> sample;
+  sample.reserve(var.size());
+  // Push the sample value for each variable into the vector.
+  for (const Unknown &u : var) {
+    // 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;
+    }
 
-      // 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);
-    }
-  }
+    // If the variable is in row position, its sample value is the
+    int64_t denom = tableau(u.pos, 0);
+    if (usingBigM)
+      if (tableau(u.pos, 2) != denom)
+        return OptimumKind::Unbounded;
   return sample;
 }
 
 Optional<SmallVector<int64_t, 8>> Simplex::getSamplePointIfIntegral() const {
   // If the tableau is empty, no sample point exists.
   if (empty)
     return {};
 
void addEqualityForDirection(ArrayRef<int64_t> dir) {
     assert(
         std::any_of(dir.begin(), dir.end(), [](int64_t x) { return x != 0; }) &&
         "Direction passed is the zero vector!");
     snapshotStack.push_back(simplex.getSnapshot());
     simplex.addEquality(getCoeffsForDirection(dir));
   }
   /// Compute max(dotProduct(dir, x - y)).
   Fraction computeWidth(ArrayRef<int64_t> dir) {
-    Optional<Fraction> maybeWidth =
+    MaybeOptimum<Fraction> maybeWidth =
         simplex.computeOptimum(Direction::Up, getCoeffsForDirection(dir));
-    assert(maybeWidth.hasValue() && "Width should not be unbounded!");
+    assert(maybeWidth.isBounded() && "Width should be bounded!");
     return *maybeWidth;
   }
 
   /// Compute max(dotProduct(dir, x - y)) and save the dual variables for only
   /// the direction equalities to `dual`.
   Fraction computeWidthAndDuals(ArrayRef<int64_t> dir,
                                 SmallVectorImpl<int64_t> &dual,
                                 int64_t &dualDenom) {
     // We can't just call into computeWidth or computeOptimum since we need to
     // access the state of the tableau after computing the optimum, and these
     // functions rollback the insertion of the objective function into the
     // tableau before returning. We instead add a row for the objective function
     // ourselves, call into computeOptimum, compute the duals from the tableau
     // state, and finally rollback the addition of the row before returning.
     unsigned snap = simplex.getSnapshot();
     unsigned conIndex = simplex.addRow(getCoeffsForDirection(dir));
     unsigned row = simplex.con[conIndex].pos;
-    Optional<Fraction> maybeWidth =
+    MaybeOptimum<Fraction> 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();
 
     // The increment is i += 2 because equalities are added as two inequalities,
     // one positive and one negative. Each iteration processes one equality.
     for (unsigned i = simplexConstraintOffset; i < conIndex; i += 2) {
       // The dual variable for an inequality in column orientation is the
       // negative of its coefficient at the objective row. If the inequality is
if (level >= upperBoundStack.size()) {
       // We haven't populated the stack values for this level yet, so we have
       // just come down a level ("recursed"). Find the lower and upper bounds.
       // If there is more than one integer point in the range, perform
       // generalized basis reduction.
       SmallVector<int64_t, 8> basisCoeffs =
           llvm::to_vector<8>(basis.getRow(level));
       basisCoeffs.push_back(0);
 
-      Optional<int64_t> minRoundedUp, maxRoundedDown;
+      MaybeOptimum<int64_t> 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);
         std::tie(minRoundedUp, maxRoundedDown) =
             computeIntegerBounds(basisCoeffs);
       }
 
       snapshotStack.push_back(getSnapshot());
while (level != -1u) {
     level++;
   }
 
   return {};
 }
 
 /// Compute the minimum and maximum integer values the expression can take. We
 /// compute each separately.
-std::pair<Optional<int64_t>, Optional<int64_t>>
+std::pair<MaybeOptimum<int64_t>, MaybeOptimum<int64_t>>
 Simplex::computeIntegerBounds(ArrayRef<int64_t> coeffs) {
-  Optional<int64_t> minRoundedUp;
-  if (Optional<Fraction> maybeMin =
-          computeOptimum(Simplex::Direction::Down, coeffs))
-    minRoundedUp = ceil(*maybeMin);
-
-  Optional<int64_t> maxRoundedDown;
-  if (Optional<Fraction> maybeMax =
-          computeOptimum(Simplex::Direction::Up, coeffs))
-    maxRoundedDown = floor(*maybeMax);
-
+  MaybeOptimum<int64_t> minRoundedUp(
+      computeOptimum(Simplex::Direction::Down, coeffs).map(ceil));
+  MaybeOptimum<int64_t> maxRoundedDown(
+      computeOptimum(Simplex::Direction::Up, coeffs).map(floor));
   return {minRoundedUp, maxRoundedDown};
 }
 
 void SimplexBase::print(raw_ostream &os) const {
   os << "rows = " << nRow << ", columns = " << nCol << "\n";
   if (empty)
     os << "Simplex marked empty!\n";
   os << "var: ";
bool Simplex::isRationalSubsetOf(const IntegerPolyhedron &poly) {
 
   return true;
 }
 
 /// Computes the minimum value `coeffs` can take. If the value is greater than
 /// or equal to zero, the polytope entirely lies in the half-space defined by
 /// `coeffs >= 0`.
 bool Simplex::isRedundantInequality(ArrayRef<int64_t> coeffs) {
-  Optional<Fraction> 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<Fraction> 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
 /// the existing constraints. This is redundant when `coeffs` is already
 /// 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<int64_t> coeffs) {
-  Optional<Fraction> minimum = computeOptimum(Direction::Down, coeffs);
-  Optional<Fraction> maximum = computeOptimum(Direction::Up, coeffs);
-  return minimum && maximum && *maximum == Fraction(0, 1) &&
+  assert(!empty &&
+         "It is not meaningful to ask about redundancy in an empty set!");
+  MaybeOptimum<Fraction> minimum = computeOptimum(Direction::Down, coeffs);
+  MaybeOptimum<Fraction> 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

mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp

TEST(IntegerPolyhedronTest, negativeDividends) {
   IntegerPolyhedron poly2(1);
   // Normalization test.
   poly2.addLocalFloorDiv({-2, 2}, 4);     // y = [-2x + 2 / 4] -> [-x + 1 / 2].
   poly2.addLocalFloorDiv({-1, 0, -2}, 3); // z = [-x - 2 / 3].
   poly2.addInequality({1, -1, -1, 0});    // y + z <= x.
 
   poly1.mergeLocalIds(poly2);
 
   // Merging triggers normalization.
   std::vector<SmallVector<int64_t, 8>> divisions = {{-1, 0, 0, 1},
                                                     {-1, 0, 0, -2}};
   SmallVector<unsigned, 8> denoms = {2, 3};
   checkDivisionRepresentation(poly1, divisions, denoms);
 }
 
 void expectRationalLexMin(const IntegerPolyhedron &poly,
                           ArrayRef<Fraction> min) {
   auto lexMin = poly.getRationalLexMin();
-  ASSERT_TRUE(lexMin.hasValue());
+  ASSERT_TRUE(lexMin.isBounded());
   EXPECT_EQ(ArrayRef<Fraction>(*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) {
   expectRationalLexMin(
       parsePoly("(x, y, z) : (x + 10 >= 0, y + 40 >= 0, z + 30 >= 0)"),
       {{-10, 1}, {-40, 1}, {-30, 1}});
   expectRationalLexMin(
       parsePoly(
expectRationalLexMin(parsePoly("(x, y) : (3*x + 2*y + 10 >= 0,"
                                  "-4*x + 7*y + 10 >= 0, -3*y + 10 >= 0)"),
                        {{-50, 9}, {10, 3}});
 
   // Cartesian product of above with itself.
   expectRationalLexMin(
       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 + 10 >= 0, -4*z + 7*w + 10 >= 0,"
                 "-3*w + 10 >= 0)"),
       {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}});
 
   // Same as above but for the constraints on z and w, we express "10" in terms
   // of x and y. We know that x and y still have to take the values
   // -50/9 and 10/3 since their constraints are the same and their values are
   // minimized first. Accordingly, the values -9x - 12y,  -9x - 0y - 10,
   // and -9x - 15y + 10 are all equal to 10.
   expectRationalLexMin(
       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, -3*w - 9*x - 15*y + 10 >= 0)"),
       {{-50, 9}, {10, 3}, {-50, 9}, {10, 3}});
 
   // Same as above with one constraint removed, making the lexmin unbounded.
-  expectNoRationalLexMin(
+  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)"));
 
   // Again, the lexmin is unbounded.
-  expectNoRationalLexMin(
+  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)"));
 
   // The set is empty.
-  expectNoRationalLexMin(parsePoly("(x) : (2*x >= 0, -x - 1 >= 0)"));
+  expectNoRationalLexMin(OptimumKind::Empty, parsePoly("(x) : (2*x >= 0, -x - 1 >= 0)"));
 }
 
 static void
 expectComputedVolumeIsValidOverapprox(const IntegerPolyhedron &poly,
                                       Optional<uint64_t> trueVolume,
                                       Optional<uint64_t> resultBound) {
   expectComputedVolumeIsValidOverapprox(poly.computeVolume(), trueVolume,
                                         resultBound);

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

TEST(Simplextest, pivotRedundantRegressionTest) {
   // non-redundant rows as well, otherwise these pivots result in an incorrect
   // tableau state. In particular, after the rollback below, some rows that are
   // NOT marked redundant will have an incorrect state.
   simplex.detectRedundant();
 
   // After the rollback, the only remaining constraint is x <= -1.
   // The maximum value of x should be -1.
   simplex.rollback(snapshot);
-  Optional<Fraction> maxX =
+  MaybeOptimum<Fraction> 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) {
   Simplex simplex(1);
   simplex.addInequality({1, -1}); // x >= 1.
   simplex.addInequality({1, 0});  // x >= 0.
   simplex.detectRedundant();
   ASSERT_FALSE(simplex.isEmpty());
TEST(SimplexTest, appendVariable) {
 
   unsigned snapshot2 = simplex.getSnapshot();
   simplex.appendVariable(2);
   EXPECT_EQ(simplex.getNumVariables(), 4u);
   simplex.rollback(snapshot2);
 
   EXPECT_EQ(simplex.getNumVariables(), 2u);
   EXPECT_EQ(simplex.getNumConstraints(), 2u);
   EXPECT_EQ(simplex.computeIntegerBounds({0, 1, 0}),
-            std::make_pair(Optional<int64_t>(yMin), Optional<int64_t>(yMax)));
+            std::make_pair(MaybeOptimum<int64_t>(yMin), MaybeOptimum<int64_t>(yMax)));
 
   simplex.rollback(snapshot1);
   EXPECT_EQ(simplex.getNumVariables(), 1u);
   EXPECT_EQ(simplex.getNumConstraints(), 0u);
 }
 
 TEST(SimplexTest, isRedundantInequality) {
   Simplex simplex(2);