[MLIR][Presburger] LexSimplex: support is{Redundant,Separate}Inequality

[arjunp]

Summary

Add integer-exact checks for inequalities being separate and redundant in LexSimplex.

[Groverkss]

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

492–493

Would it make more sense to have something like:

isIneqType(IneqType type, ArrayRef<int64_t> coeffs);

instead?

[arjunp]

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

492–493

No, more ineqtypes will be added in future which I don't plan to add support for here.

[Groverkss]

LGTM.

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

492–493

Makes sense.

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

public:
   MaybeOptimum<SmallVector<Fraction, 8>> findRationalLexMin();
 
   /// Return the lexicographically minimum integer solution to the constraints.
   ///
   /// Note: this should be used only when the lexmin is really needed. To obtain
   /// 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.
   ///
   /// 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;

 
 /// Takes a snapshot of the simplex state on construction and rolls back to the
 /// snapshot on destruction.
 ///
 /// Useful for performing operations in a "transient context", all changes from
 /// 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); }
 
 private:
   SimplexBase &simplex;
   unsigned snapshot;
 };
 
 } // namespace presburger
 } // namespace mlir
 
 #endif // MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H

mlir/lib/Analysis/Presburger/Simplex.cpp

while (!empty) {
     return llvm::to_vector<8>(
         llvm::map_range(*sample, std::mem_fn(&Fraction::getAsInteger)));
   }
 
   // Polytope is integer empty.
   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;
   if (tableau(row, 2) == 0 && tableau(row, 1) < 0)
     return true;
   return false;
 }
 

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

TEST(SimplexTest, addDivisionVariable) {
   Simplex simplex(/*nVar=*/1);
   simplex.addDivisionVariable({1, 0}, 2);
   simplex.addInequality({1, 0, -3}); // x >= 3.
   simplex.addInequality({-1, 0, 9}); // x <= 9.
   Optional<SmallVector<int64_t, 8>> sample = simplex.findIntegerSample();
   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}));
+}