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
@@ -484,6 +484,14 @@
   /// any integer sample, use Simplex::findIntegerSample as that is more robust.
   MaybeOptimum<SmallVector<int64_t, 8>> findIntegerLexMin();
 
+  /// Return whether the specified inequality is redundant/separate for the
+  /// polytope. Redundant means every point satisfies the given inequality, and
+  /// separate means no point satisfies it.
+  ///
+  /// These checks are integer-exact.
+  bool isSeparateInequality(ArrayRef<int64_t> coeffs);
+  bool isRedundantInequality(ArrayRef<int64_t> coeffs);
+
 private:
   /// Returns the current sample point, which may contain non-integer (rational)
   /// coordinates. Returns an empty optimum when the tableau is empty.
@@ -685,7 +693,7 @@
 /// which get rolled back on scope exit.
 class SimplexRollbackScopeExit {
 public:
-  SimplexRollbackScopeExit(Simplex &simplex) : simplex(simplex) {
+  SimplexRollbackScopeExit(SimplexBase &simplex) : simplex(simplex) {
     snapshot = simplex.getSnapshot();
   };
   ~SimplexRollbackScopeExit() { simplex.rollback(snapshot); }
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
@@ -219,6 +219,15 @@
   return OptimumKind::Empty;
 }
 
+bool LexSimplex::isSeparateInequality(ArrayRef<int64_t> coeffs) {
+  SimplexRollbackScopeExit scopeExit(*this);
+  addInequality(coeffs);
+  return findIntegerLexMin().isEmpty();
+}
+
+bool LexSimplex::isRedundantInequality(ArrayRef<int64_t> coeffs) {
+  return isSeparateInequality(getComplementIneq(coeffs));
+}
 bool LexSimplex::rowIsViolated(unsigned row) const {
   if (tableau(row, 2) < 0)
     return true;
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
@@ -548,3 +548,20 @@
   ASSERT_TRUE(sample.hasValue());
   EXPECT_EQ((*sample)[0] / 2, (*sample)[1]);
 }
+
+TEST(SimplexTest, LexIneqType) {
+  LexSimplex simplex(/*nVar=*/1);
+  simplex.addInequality({2, -1}); // x >= 1/2.
+
+  // Redundant inequality x >= 2/3.
+  EXPECT_TRUE(simplex.isRedundantInequality({3, -2}));
+  EXPECT_FALSE(simplex.isSeparateInequality({3, -2}));
+
+  // Separate inequality x <= 2/3.
+  EXPECT_FALSE(simplex.isRedundantInequality({-3, 2}));
+  EXPECT_TRUE(simplex.isSeparateInequality({-3, 2}));
+
+  // Cut inequality x <= 1.
+  EXPECT_FALSE(simplex.isRedundantInequality({-1, 1}));
+  EXPECT_FALSE(simplex.isSeparateInequality({-1, 1}));
+}