[MLIR] Use IntegerPolyhedron in Simplex instead of FlatAffineConstraints

[Groverkss]

Summary

This patch replaces usage of FlatAffineConstraints in Simplex with
IntegerPolyhedron. This removes dependency of Simplex on FlatAffineConstraints
and puts it on IntegerPolyhedron, which is part of Presburger library.

[arjunp]

There are still some IntegerPolyhedron objects called fac. Please change them to poly as well.

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

9

42

[arjunp]

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

9

Or better: "on an IntegerPolyhedron"

[Groverkss]

• Address Arjun's comments.

[Groverkss]

• Fix doc comment for Simplex.h

[Groverkss]

Send correct commits.

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

 //===- Simplex.h - MLIR Simplex Class ---------------------------*- C++ -*-===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
-// Functionality to perform analysis on FlatAffineConstraints. In particular,
+// Functionality to perform analysis on an IntegerPolyhedron. In particular,
 // support for performing emptiness checks and redundancy checks.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
 #define MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
 
-#include "mlir/Analysis/AffineStructures.h"
 #include "mlir/Analysis/Presburger/Fraction.h"
+#include "mlir/Analysis/Presburger/IntegerPolyhedron.h"
 #include "mlir/Analysis/Presburger/Matrix.h"
 #include "mlir/IR/Location.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 {
 
 class GBRSimplex;
 
 /// The Simplex class implements a version of the Simplex and Generalized Basis
 /// Reduction algorithms, which can perform analysis of integer sets with affine
 /// inequalities and equalities. A Simplex can be constructed
 /// by specifying the dimensionality of the set. It supports adding affine
 /// inequalities and equalities, and can perform emptiness checks, i.e., it can
 /// find a solution to the set of constraints if one exists, or say that the
 /// set is empty if no solution exists. Currently, this only works for bounded
 /// sets. Furthermore, it can find a subset of these constraints that are
 /// redundant, i.e. a subset of constraints that doesn't constrain the affine
 /// set further after adding the non-redundant constraints. Simplex can also be
-/// constructed from a FlatAffineConstraints object.
+/// constructed from an IntegerPolyhedron object.
 ///
 /// The implementation of the Simplex and SimplexBase classes, other than the
 /// functionality for sampling, is based on the paper
 /// "Simplify: A Theorem Prover for Program Checking"
 /// by D. Detlefs, G. Nelson, J. B. Saxe.
 ///
 /// We define variables, constraints, and unknowns. Consider the example of a
 /// two-dimensional set defined by 1 + 2x + 3y >= 0 and 2x - 3y >= 0. Here,

 /// in `Simplex`.
 
 class SimplexBase {
 public:
   enum class Direction { Up, Down };
 
   SimplexBase() = delete;
   explicit SimplexBase(unsigned nVar);
-  explicit SimplexBase(const FlatAffineConstraints &constraints);
+  explicit SimplexBase(const IntegerPolyhedron &constraints);
 
   /// Returns true if the tableau is empty (has conflicting constraints),
   /// false otherwise.
   bool isEmpty() const;
 
   /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
   /// is the current number of variables, then the corresponding inequality is
   /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0.
public:
   void markEmpty();
 
   /// Get a snapshot of the current state. This is used for rolling back.
   unsigned getSnapshot() const;
 
   /// Rollback to a snapshot. This invalidates all later snapshots.
   void rollback(unsigned snapshot);
 
-  /// Add all the constraints from the given FlatAffineConstraints.
-  void intersectFlatAffineConstraints(const FlatAffineConstraints &fac);
+  /// Add all the constraints from the given IntegerPolyhedron.
+  void intersectIntegerPolyhedron(const IntegerPolyhedron &fac);
 
   /// Returns a rational sample point. This should not be called when Simplex is
   /// empty.
   SmallVector<Fraction, 8> getRationalSample() const;
 
   /// Returns the current sample point if it is integral. Otherwise, returns
   /// None.
   Optional<SmallVector<int64_t, 8>> getSamplePointIfIntegral() const;
protected:
   /// These hold information about each unknown.
   SmallVector<Unknown, 8> con, var;
 };
 
 class Simplex : public SimplexBase {
 public:
   Simplex() = delete;
   explicit Simplex(unsigned nVar) : SimplexBase(nVar) {}
-  explicit Simplex(const FlatAffineConstraints &constraints)
+  explicit Simplex(const IntegerPolyhedron &constraints)
       : SimplexBase(constraints) {}
 
   /// 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.
public:
   /// Check if the specified inequality already holds in the polytope.
   bool isRedundantInequality(ArrayRef<int64_t> coeffs);
 
   /// Check if the specified equality already holds in the polytope.
   bool isRedundantEquality(ArrayRef<int64_t> coeffs);
 
   /// Returns true if this Simplex's polytope is a rational subset of `fac`.
   /// Otherwise, returns false.
-  bool isRationalSubsetOf(const FlatAffineConstraints &fac);
+  bool isRationalSubsetOf(const IntegerPolyhedron &fac);
 
 private:
   friend class GBRSimplex;
 
   /// 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.

mlir/lib/Analysis/Presburger/Simplex.cpp

SimplexBase::SimplexBase(unsigned nVar)
   colUnknown.push_back(nullIndex);
   for (unsigned i = 0; i < nVar; ++i) {
     var.emplace_back(Orientation::Column, /*restricted=*/false, /*pos=*/nCol);
     colUnknown.push_back(i);
     nCol++;
   }
 }
 
-SimplexBase::SimplexBase(const FlatAffineConstraints &constraints)
+SimplexBase::SimplexBase(const IntegerPolyhedron &constraints)
     : SimplexBase(constraints.getNumIds()) {
   for (unsigned i = 0, numIneqs = constraints.getNumInequalities();
        i < numIneqs; ++i)
     addInequality(constraints.getInequality(i));
   for (unsigned i = 0, numEqs = constraints.getNumEqualities(); i < numEqs; ++i)
     addEquality(constraints.getEquality(i));
 }
 
for (unsigned i = 0; i < count; ++i) {
     var.emplace_back(Orientation::Column, /*restricted=*/false,
                      /*pos=*/nCol - 1);
     colUnknown.push_back(var.size() - 1);
   }
   tableau.resizeHorizontally(nCol);
   undoLog.insert(undoLog.end(), count, UndoLogEntry::RemoveLastVariable);
 }
 
-/// Add all the constraints from the given FlatAffineConstraints.
-void SimplexBase::intersectFlatAffineConstraints(
-    const FlatAffineConstraints &fac) {
-  assert(fac.getNumIds() == getNumVariables() &&
-         "FlatAffineConstraints must have same dimensionality as simplex");
-  for (unsigned i = 0, e = fac.getNumInequalities(); i < e; ++i)
-    addInequality(fac.getInequality(i));
-  for (unsigned i = 0, e = fac.getNumEqualities(); i < e; ++i)
-    addEquality(fac.getEquality(i));
+/// Add all the constraints from the given IntegerPolyhedron.
+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,
                                               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.
for (unsigned col = 0; col < nCol; ++col)
       os << tableau(row, col) << '\t';
     os << '\n';
   }
   os << '\n';
 }
 
 void SimplexBase::dump() const { print(llvm::errs()); }
 
-bool Simplex::isRationalSubsetOf(const FlatAffineConstraints &fac) {
+bool Simplex::isRationalSubsetOf(const IntegerPolyhedron &poly) {
   if (isEmpty())
     return true;
 
-  for (unsigned i = 0, e = fac.getNumInequalities(); i < e; ++i)
-    if (!isRedundantInequality(fac.getInequality(i)))
+  for (unsigned i = 0, e = poly.getNumInequalities(); i < e; ++i)
+    if (!isRedundantInequality(poly.getInequality(i)))
       return false;
 
-  for (unsigned i = 0, e = fac.getNumEqualities(); i < e; ++i)
-    if (!isRedundantEquality(fac.getEquality(i)))
+  for (unsigned i = 0, e = poly.getNumEqualities(); i < e; ++i)
+    if (!isRedundantEquality(poly.getEquality(i)))
       return false;
 
   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`.

mlir/lib/Analysis/PresburgerSet.cpp

for (Optional<std::pair<unsigned, unsigned>> &maybePair : repr) {
     isDivInequality[maybePair->second] = true;
   }
 
   unsigned offset = simplex.getNumConstraints();
   unsigned numLocalsAdded = b.getNumLocalIds() - bInitNumLocals;
   simplex.appendVariable(numLocalsAdded);
 
   unsigned snapshotBeforeIntersect = simplex.getSnapshot();
-  simplex.intersectFlatAffineConstraints(sI);
+  simplex.intersectIntegerPolyhedron(sI);
 
   if (simplex.isEmpty()) {
     /// b ^ s_i is empty, so b \ s_i = b. We move directly to i + 1.
     /// We are ignoring level i completely, so we restore the state
     /// *before* going to level i + 1.
     restoreState();
     subtractRecursively(b, simplex, s, i + 1, result);
     return;

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

TEST(SimplexTest, isRedundantEquality) {
 
   EXPECT_FALSE(simplex.isRedundantEquality({0, 1, -1})); // y = 1.
 
   simplex.addEquality({0, -1, 2}); // y = 2.
 
   EXPECT_TRUE(simplex.isRedundantEquality({-1, 0, 2})); // x = 2.
 }
 
-static FlatAffineConstraints parseFAC(StringRef str, MLIRContext *context) {
-  FailureOr<FlatAffineConstraints> fac = parseIntegerSetToFAC(str, context);
+static IntegerPolyhedron parsePoly(StringRef str, MLIRContext *context) {
+  FailureOr<IntegerPolyhedron> poly = parseIntegerSetToFAC(str, context);
 
-  EXPECT_TRUE(succeeded(fac));
+  EXPECT_TRUE(succeeded(poly));
 
-  return *fac;
+  return *poly;
 }
 
 TEST(SimplexTest, IsRationalSubsetOf) {
 
   MLIRContext context;
 
-  FlatAffineConstraints univ = FlatAffineConstraints::getUniverse(1, 0);
-  FlatAffineConstraints empty =
-      parseFAC("(x) : (x + 0 >= 0, -x - 1 >= 0)", &context);
-  FlatAffineConstraints s1 = parseFAC("(x) : ( x >= 0, -x + 4 >= 0)", &context);
-  FlatAffineConstraints s2 =
-      parseFAC("(x) : (x - 1 >= 0, -x + 3 >= 0)", &context);
+  IntegerPolyhedron univ = parsePoly("(x) : ()", &context);
+  IntegerPolyhedron empty =
+      parsePoly("(x) : (x + 0 >= 0, -x - 1 >= 0)", &context);
+  IntegerPolyhedron s1 = parsePoly("(x) : ( x >= 0, -x + 4 >= 0)", &context);
+  IntegerPolyhedron s2 = parsePoly("(x) : (x - 1 >= 0, -x + 3 >= 0)", &context);
 
   Simplex simUniv(univ);
   Simplex simEmpty(empty);
   Simplex sim1(s1);
   Simplex sim2(s2);
 
   EXPECT_TRUE(simUniv.isRationalSubsetOf(univ));
   EXPECT_TRUE(simEmpty.isRationalSubsetOf(empty));