[MLIR] Exact integer emptiness checks for FlatAffineConstraints

This patch adds the capability to perform exact integer emptiness checks for FlatAffineConstraints using the General Basis Reduction algorithm (GBR). Previously, only a heuristic was available for emptiness checks, which was not guaranteed to always give a conclusive result.

This patch adds a `Simplex` class, which can be constructed using a `FlatAffineConstraints`, and can find an integer sample point (if one exists) using the GBR algorithm. Additionally, it adds two classes `Matrix` and `Fraction`, which are used by `Simplex`.

The integer emptiness check functionality can be accessed through the new `FlatAffineConstraints::isIntegerEmpty()` function, which runs the existing heuristic first and, if that proves to be inconclusive, runs the GBR algorithm to produce a conclusive result.

Differential Revision: https://reviews.llvm.org/D80860

mlir/include/mlir/Analysis/AffineStructures.h

@@ -126,19 +126,33 @@ public:
   /// intersection with no simplification of any sort attempted.
   void append(const FlatAffineConstraints &other);
 
-  // Checks for emptiness by performing variable elimination on all identifiers,
+  /// Checks for emptiness by performing variable elimination on all
-  // running the GCD test on each equality constraint, and checking for invalid
+  /// identifiers, running the GCD test on each equality constraint, and
-  // constraints.
+  /// checking for invalid constraints. Returns true if the GCD test fails for
-  // Returns true if the GCD test fails for any equality, or if any invalid
+  /// any equality, or if any invalid constraints are discovered on any row.
-  // constraints are discovered on any row. Returns false otherwise.
+  /// Returns false otherwise.
   bool isEmpty() const;
 
-  // Runs the GCD test on all equality constraints. Returns 'true' if this test
+  /// Runs the GCD test on all equality constraints. Returns 'true' if this test
-  // fails on any equality. Returns 'false' otherwise.
+  /// fails on any equality. Returns 'false' otherwise.
-  // This test can be used to disprove the existence of a solution. If it
+  /// This test can be used to disprove the existence of a solution. If it
-  // returns true, no integer solution to the equality constraints can exist.
+  /// returns true, no integer solution to the equality constraints can exist.
   bool isEmptyByGCDTest() const;
 
+  /// Runs the GCD test heuristic. If it proves inconclusive, falls back to
+  /// generalized basis reduction if the set is bounded.
+  ///
+  /// Returns true if the set of constraints is found to have no solution,
+  /// false if a solution exists or all tests were inconclusive.
+  bool isIntegerEmpty() const;
+
+  /// Find a sample point satisfying the constraints. This uses a branch and
+  /// bound algorithm with generalized basis reduction, which always works if
+  /// the set is bounded. This should not be called for unbounded sets.
+  ///
+  /// Returns such a point if one exists, or an empty Optional otherwise.
+  Optional<SmallVector<int64_t, 8>> findIntegerSample() const;
+
   // Clones this object.
   std::unique_ptr<FlatAffineConstraints> clone() const;
 

mlir/include/mlir/Analysis/Presburger/Fraction.h

@@ -0,0 +1,77 @@
+//===- Fraction.h - MLIR Fraction 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
+//
+//===----------------------------------------------------------------------===//
+//
+// This is a simple class to represent fractions. It supports multiplication,
+// comparison, floor, and ceiling operations.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_ANALYSIS_PRESBURGER_FRACTION_H
+#define MLIR_ANALYSIS_PRESBURGER_FRACTION_H
+
+#include "mlir/Support/MathExtras.h"
+
+namespace mlir {
+
+/// A class to represent fractions. The sign of the fraction is represented
+/// in the sign of the numerator; the denominator is always positive.
+///
+/// Note that overflows may occur if the numerator or denominator are not
+/// representable by 64-bit integers.
+struct Fraction {
+  /// Default constructor initializes the represented rational number to zero.
+  Fraction() : num(0), den(1) {}
+
+  /// Construct a Fraction from a numerator and denominator.
+  Fraction(int64_t oNum, int64_t oDen) : num(oNum), den(oDen) {
+    if (den < 0) {
+      num = -num;
+      den = -den;
+    }
+  }
+
+  /// The numerator and denominator, respectively. The denominator is always
+  /// positive.
+  int64_t num, den;
+};
+
+/// Three-way comparison between two fractions.
+/// Returns +1, 0, and -1 if the first fraction is greater than, equal to, or
+/// less than the second fraction, respectively.
+inline int compare(Fraction x, Fraction y) {
+  int64_t diff = x.num * y.den - y.num * x.den;
+  if (diff > 0)
+    return +1;
+  if (diff < 0)
+    return -1;
+  return 0;
+}
+
+inline int64_t floor(Fraction f) { return floorDiv(f.num, f.den); }
+
+inline int64_t ceil(Fraction f) { return ceilDiv(f.num, f.den); }
+
+inline Fraction operator-(Fraction x) { return Fraction(-x.num, x.den); }
+
+inline bool operator<(Fraction x, Fraction y) { return compare(x, y) < 0; }
+
+inline bool operator<=(Fraction x, Fraction y) { return compare(x, y) <= 0; }
+
+inline bool operator==(Fraction x, Fraction y) { return compare(x, y) == 0; }
+
+inline bool operator>(Fraction x, Fraction y) { return compare(x, y) > 0; }
+
+inline bool operator>=(Fraction x, Fraction y) { return compare(x, y) >= 0; }
+
+inline Fraction operator*(Fraction x, Fraction y) {
+  return Fraction(x.num * y.num, x.den * y.den);
+}
+
+} // namespace mlir
+
+#endif // MLIR_ANALYSIS_PRESBURGER_FRACTION_H

mlir/include/mlir/Analysis/Presburger/Matrix.h

@@ -0,0 +1,79 @@
+//===- Matrix.h - MLIR Matrix 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
+//
+//===----------------------------------------------------------------------===//
+//
+// This is a simple 2D matrix class that supports reading, writing, resizing,
+// swapping rows, and swapping columns.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_ANALYSIS_PRESBURGER_MATRIX_H
+#define MLIR_ANALYSIS_PRESBURGER_MATRIX_H
+
+#include "mlir/Support/LLVM.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/Support/raw_ostream.h"
+
+#include <cassert>
+
+namespace mlir {
+
+/// This is a simple class to represent a resizable matrix.
+///
+/// The data is stored in the form of a vector of vectors.
+class Matrix {
+public:
+  Matrix() = delete;
+
+  /// Construct a matrix with the specified number of rows and columns.
+  /// Initially, the values are default initialized.
+  Matrix(unsigned rows, unsigned columns);
+
+  /// Return the identity matrix of the specified dimension.
+  static Matrix identity(unsigned dimension);
+
+  /// Access the element at the specified row and column.
+  int64_t &at(unsigned row, unsigned column);
+  int64_t at(unsigned row, unsigned column) const;
+  int64_t &operator()(unsigned row, unsigned column);
+  int64_t operator()(unsigned row, unsigned column) const;
+
+  /// Swap the given columns.
+  void swapColumns(unsigned column, unsigned otherColumn);
+
+  /// Swap the given rows.
+  void swapRows(unsigned row, unsigned otherRow);
+
+  unsigned getNumRows() const;
+
+  unsigned getNumColumns() const;
+
+  /// Get an ArrayRef corresponding to the specified row.
+  ArrayRef<int64_t> getRow(unsigned row) const;
+
+  /// Add `scale` multiples of the source row to the target row.
+  void addToRow(unsigned sourceRow, unsigned targetRow, int64_t scale);
+
+  /// Resize the matrix to the specified dimensions. If a dimension is smaller,
+  /// the values are truncated; if it is bigger, the new values are default
+  /// initialized.
+  void resizeVertically(unsigned newNRows);
+
+  /// Print the matrix.
+  void print(raw_ostream &os) const;
+  void dump() const;
+
+private:
+  unsigned nRows, nColumns;
+
+  /// Stores the data. data.size() is equal to nRows * nColumns.
+  SmallVector<int64_t, 64> data;
+};
+
+} // namespace mlir
+
+#endif // MLIR_ANALYSIS_PRESBURGER_MATRIX_H

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

@@ -0,0 +1,327 @@
+//===- 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,
+// support for performing emptiness 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/Matrix.h"
+#include "mlir/Support/LogicalResult.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/Optional.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/Support/raw_ostream.h"
+
+namespace mlir {
+
+class GBRSimplex;
+
+/// This 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. Simplex can also be constructed from a FlatAffineConstraints object.
+///
+/// The implementation of this Simplex class, 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,
+/// x, y, are variables while 1 + 2x + 3y >= 0, 2x - 3y >= 0 are
+/// constraints. Unknowns are either variables or constraints, i.e., x, y,
+/// 1 + 2x + 3y >= 0, 2x - 3y >= 0 are all unknowns.
+///
+/// The implementation involves a matrix called a tableau, which can be thought
+/// of as a 2D matrix of rational numbers having number of rows equal to the
+/// number of constraints and number of columns equal to one plus the number of
+/// variables. In our implementation, instead of storing rational numbers, we
+/// store a common denominator for each row, so it is in fact a matrix of
+/// integers with number of rows equal to number of constraints and number of
+/// columns equal to _two_ plus the number of variables. For example, instead of
+/// storing a row of three rationals [1/2, 2/3, 3], we would store [6, 3, 4, 18]
+/// since 3/6 = 1/2, 4/6 = 2/3, and 18/6 = 3.
+///
+/// Every row and column except the first and second columns is associated with
+/// an unknown and every unknown is associated with a row or column. The second
+/// column represents the constant, explained in more detail below. An unknown
+/// associated with a row or column is said to be in row or column position
+/// respectively.
+///
+/// The vectors var and con store information about the variables and
+/// constraints respectively, namely, whether they are in row or column
+/// position, which row or column they are associated with, and whether they
+/// correspond to a variable or a constraint.
+///
+/// An unknown is addressed by its index. If the index i is non-negative, then
+/// the variable var[i] is being addressed. If the index i is negative, then
+/// the constraint con[~i] is being addressed. Effectively this maps
+/// 0 -> var[0], 1 -> var[1], -1 -> con[0], -2 -> con[1], etc. rowUnknown[r] and
+/// colUnknown[c] are the indexes of the unknowns associated with row r and
+/// column c, respectively.
+///
+/// The unknowns in column position are together called the basis. Initially the
+/// basis is the set of variables -- in our example above, the initial basis is
+/// x, y.
+///
+/// The unknowns in row position are represented in terms of the basis unknowns.
+/// If the basis unknowns are u_1, u_2, ... u_m, and a row in the tableau is
+/// d, c, a_1, a_2, ... a_m, this representats the unknown for that row as
+/// (c + a_1*u_1 + a_2*u_2 + ... + a_m*u_m)/d. In our running example, if the
+/// basis is the initial basis of x, y, then the constraint 1 + 2x + 3y >= 0
+/// would be represented by the row [1, 1, 2, 3].
+///
+/// The association of unknowns to rows and columns can be changed by a process
+/// called pivoting, where a row unknown and a column unknown exchange places
+/// and the remaining row variables' representation is changed accordingly
+/// by eliminating the old column unknown in favour of the new column unknown.
+/// If we had pivoted the column for x with the row for 2x - 3y >= 0,
+/// the new row for x would be [2, 1, 3] since x = (1*(2x - 3y) + 3*y)/2.
+/// See the documentation for the pivot member function for details.
+///
+/// The association of unknowns to rows and columns is called the _tableau
+/// configuration_. The _sample value_ of an unknown in a particular tableau
+/// configuration is its value if all the column unknowns were set to zero.
+/// Concretely, for unknowns in column position the sample value is zero and
+/// for unknowns in row position the sample value is the constant term divided
+/// by the common denominator.
+///
+/// The tableau configuration is called _consistent_ if the sample value of all
+/// restricted unknowns is non-negative. Initially there are no constraints, and
+/// the tableau is consistent. When a new constraint is added, its sample value
+/// in the current tableau configuration may be negative. In that case, we try
+/// to find a series of pivots to bring us to a consistent tableau
+/// configuration, i.e. we try to make the new constraint's sample value
+/// non-negative without making that of any other constraints negative. (See
+/// findPivot and findPivotRow for details.) If this is not possible, then the
+/// set of constraints is mutually contradictory and the tableau is marked
+/// _empty_, which means the set of constraints has no solution.
+///
+/// This Simplex class also supports taking snapshots of the current state
+/// and rolling back to prior snapshots. This works by maintaing an undo log
+/// of operations. Snapshots are just pointers to a particular location in the
+/// log, and rolling back to a snapshot is done by reverting each log entry's
+/// operation from the end until we reach the snapshot's location.
+///
+/// Finding an integer sample is done with the Generalized Basis Reduction
+/// algorithm. See the documentation for findIntegerSample and reduceBasis.
+class Simplex {
+public:
+  enum class Direction { Up, Down };
+
+  Simplex() = delete;
+  explicit Simplex(unsigned nVar);
+  explicit Simplex(const FlatAffineConstraints &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.
+  void addInequality(ArrayRef<int64_t> coeffs);
+
+  /// Returns the number of variables in the tableau.
+  unsigned numVariables() const;
+
+  /// Returns the number of constraints in the tableau.
+  unsigned numConstraints() const;
+
+  /// Add an equality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
+  /// is the current number of variables, then the corresponding equality is
+  /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0.
+  void addEquality(ArrayRef<int64_t> coeffs);
+
+  /// Mark the tableau as being empty.
+  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);
+
+  /// Compute the maximum or minimum value of the given row, depending on
+  /// direction.
+  ///
+  /// Returns a (num, den) pair denoting the optimum, or None if no
+  /// optimum exists, i.e., if the expression is unbounded in this direction.
+  Optional<Fraction> computeRowOptimum(Direction direction, unsigned row);
+
+  /// Compute the maximum or minimum value of the given expression, depending on
+  /// direction.
+  ///
+  /// Returns a (num, den) pair 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,
+                                    ArrayRef<int64_t> coeffs);
+
+  /// Returns a (min, max) pair denoting the minimum and maximum integer values
+  /// of the given expression.
+  std::pair<int64_t, 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.
+  static Simplex makeProduct(const Simplex &a, const Simplex &b);
+
+  /// Returns the current sample point if it is integral. Otherwise, returns an
+  /// None.
+  Optional<SmallVector<int64_t, 8>> getSamplePointIfIntegral() const;
+
+  /// Returns an integer sample point if one exists, or None
+  /// otherwise. This should only be called for bounded sets.
+  Optional<SmallVector<int64_t, 8>> findIntegerSample();
+
+  /// Print the tableau's internal state.
+  void print(raw_ostream &os) const;
+  void dump() const;
+
+private:
+  friend class GBRSimplex;
+
+  enum class Orientation { Row, Column };
+
+  /// An Unknown is either a variable or a constraint. It is always associated
+  /// with either a row or column. Whether it's a row or a column is specified
+  /// by the orientation and pos identifies the specific row or column it is
+  /// associated with. If the unknown is restricted, then it has a
+  /// non-negativity constraint associated with it, i.e., its sample value must
+  /// always be non-negative and if it cannot be made non-negative without
+  /// violating other constraints, the tableau is empty.
+  struct Unknown {
+    Unknown(Orientation oOrientation, bool oRestricted, unsigned oPos)
+        : pos(oPos), orientation(oOrientation), restricted(oRestricted) {}
+    unsigned pos;
+    Orientation orientation;
+    bool restricted : 1;
+
+    void print(raw_ostream &os) const {
+      os << (orientation == Orientation::Row ? "r" : "c");
+      os << pos;
+      if (restricted)
+        os << " [>=0]";
+    }
+  };
+
+  struct Pivot {
+    unsigned row, column;
+  };
+
+  /// Find a pivot to change the sample value of row in the specified
+  /// direction. The returned pivot row will be row if and only
+  /// if the unknown is unbounded in the specified direction.
+  ///
+  /// Returns a (row, col) pair denoting a pivot, or an empty Optional if
+  /// no valid pivot exists.
+  Optional<Pivot> findPivot(int row, Direction direction) const;
+
+  /// Swap the row with the column in the tableau's data structures but not the
+  /// tableau itself. This is used by pivot.
+  void swapRowWithCol(unsigned row, unsigned col);
+
+  /// Pivot the row with the column.
+  void pivot(unsigned row, unsigned col);
+  void pivot(Pivot pair);
+
+  /// Returns the unknown associated with index.
+  const Unknown &unknownFromIndex(int index) const;
+  /// Returns the unknown associated with col.
+  const Unknown &unknownFromColumn(unsigned col) const;
+  /// Returns the unknown associated with row.
+  const Unknown &unknownFromRow(unsigned row) const;
+  /// Returns the unknown associated with index.
+  Unknown &unknownFromIndex(int index);
+  /// Returns the unknown associated with col.
+  Unknown &unknownFromColumn(unsigned col);
+  /// Returns the unknown associated with row.
+  Unknown &unknownFromRow(unsigned row);
+
+  /// Add a new row to the tableau and the associated data structures.
+  unsigned addRow(ArrayRef<int64_t> coeffs);
+
+  /// Normalize the given row by removing common factors between the numerator
+  /// and the denominator.
+  void normalizeRow(unsigned row);
+
+  /// Swap the two rows in the tableau and associated data structures.
+  void swapRows(unsigned i, unsigned j);
+
+  /// Restore the unknown to a non-negative sample value.
+  ///
+  /// Returns true if the unknown was successfully restored to a non-negative
+  /// sample value, false otherwise.
+  LogicalResult restoreRow(Unknown &u);
+
+  enum class UndoLogEntry { RemoveLastConstraint, UnmarkEmpty };
+
+  /// Undo the operation represented by the log entry.
+  void undo(UndoLogEntry entry);
+
+  /// Find a row that can be used to pivot the column in the specified
+  /// direction. If skipRow is not null, then this row is excluded
+  /// from consideration. The returned pivot will maintain all constraints
+  /// except the column itself and skipRow, if it is set. (if these unknowns
+  /// are restricted).
+  ///
+  /// Returns the row to pivot to, or an empty Optional if the column
+  /// is unbounded in the specified direction.
+  Optional<unsigned> findPivotRow(Optional<unsigned> skipRow,
+                                  Direction direction, unsigned col) const;
+
+  /// Reduce the given basis, starting at the specified level, using general
+  /// basis reduction.
+  void reduceBasis(Matrix &basis, unsigned level);
+
+  /// The number of rows in the tableau.
+  unsigned nRow;
+
+  /// The number of columns in the tableau, including the common denominator
+  /// and the constant column.
+  unsigned nCol;
+
+  /// The matrix representing the tableau.
+  Matrix tableau;
+
+  /// This is true if the tableau has been detected to be empty, false
+  /// otherwise.
+  bool empty;
+
+  /// Holds a log of operations, used for rolling back to a previous state.
+  SmallVector<UndoLogEntry, 8> undoLog;
+
+  /// These hold the indexes of the unknown at a given row or column position.
+  /// We keep these as signed integers since that makes it convenient to check
+  /// if an index corresponds to a variable or a constraint by checking the
+  /// sign.
+  ///
+  /// colUnknown is padded with two null indexes at the front since the first
+  /// two columns don't correspond to any unknowns.
+  SmallVector<int, 8> rowUnknown, colUnknown;
+
+  /// These hold information about each unknown.
+  SmallVector<Unknown, 8> con, var;
+};
+
+} // namespace mlir
+
+#endif // MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H

mlir/lib/Analysis/AffineStructures.cpp

@@ -11,6 +11,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "mlir/Analysis/AffineStructures.h"
+#include "mlir/Analysis/Presburger/Simplex.h"
 #include "mlir/Dialect/Affine/IR/AffineOps.h"
 #include "mlir/Dialect/Affine/IR/AffineValueMap.h"
 #include "mlir/Dialect/StandardOps/IR/Ops.h"
@@ -1035,6 +1036,28 @@ bool FlatAffineConstraints::isEmptyByGCDTest() const {
   return false;
 }
 
+// First, try the GCD test heuristic.
+//
+// If that doesn't find the set empty, check if the set is unbounded. If it is,
+// we cannot use the GBR algorithm and we conservatively return false.
+//
+// If the set is bounded, we use the complete emptiness check for this case
+// provided by Simplex::findIntegerSample(), which gives a definitive answer.
+bool FlatAffineConstraints::isIntegerEmpty() const {
+  if (isEmptyByGCDTest())
+    return true;
+
+  Simplex simplex(*this);
+  if (simplex.isUnbounded())
+    return false;
+  return !simplex.findIntegerSample().hasValue();
+}
+
+Optional<SmallVector<int64_t, 8>>
+FlatAffineConstraints::findIntegerSample() const {
+  return Simplex(*this).findIntegerSample();
+}
+
 /// Tightens inequalities given that we are dealing with integer spaces. This is
 /// analogous to the GCD test but applied to inequalities. The constant term can
 /// be reduced to the preceding multiple of the GCD of the coefficients, i.e.,

mlir/lib/Analysis/CMakeLists.txt

@@ -25,6 +25,7 @@ add_mlir_library(MLIRAnalysis
   MLIRCallInterfaces
   MLIRControlFlowInterfaces
   MLIRInferTypeOpInterface
+  MLIRPresburger
   MLIRSCF
   )
 
@@ -46,5 +47,8 @@ add_mlir_library(MLIRLoopAnalysis
   MLIRCallInterfaces
   MLIRControlFlowInterfaces
   MLIRInferTypeOpInterface
+  MLIRPresburger
   MLIRSCF
   )
+  
+add_subdirectory(Presburger)

mlir/lib/Analysis/Presburger/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_mlir_library(MLIRPresburger
+  Simplex.cpp
+  Matrix.cpp
+  )

mlir/lib/Analysis/Presburger/Matrix.cpp

@@ -0,0 +1,92 @@
+//===- Matrix.cpp - MLIR Matrix Class -------------------------------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Analysis/Presburger/Matrix.h"
+
+namespace mlir {
+
+Matrix::Matrix(unsigned rows, unsigned columns)
+    : nRows(rows), nColumns(columns), data(nRows * nColumns) {}
+
+Matrix Matrix::identity(unsigned dimension) {
+  Matrix matrix(dimension, dimension);
+  for (unsigned i = 0; i < dimension; ++i)
+    matrix(i, i) = 1;
+  return matrix;
+}
+
+int64_t &Matrix::at(unsigned row, unsigned column) {
+  assert(row < getNumRows() && "Row outside of range");
+  assert(column < getNumColumns() && "Column outside of range");
+  return data[row * nColumns + column];
+}
+
+int64_t Matrix::at(unsigned row, unsigned column) const {
+  assert(row < getNumRows() && "Row outside of range");
+  assert(column < getNumColumns() && "Column outside of range");
+  return data[row * nColumns + column];
+}
+
+int64_t &Matrix::operator()(unsigned row, unsigned column) {
+  return at(row, column);
+}
+
+int64_t Matrix::operator()(unsigned row, unsigned column) const {
+  return at(row, column);
+}
+
+unsigned Matrix::getNumRows() const { return nRows; }
+
+unsigned Matrix::getNumColumns() const { return nColumns; }
+
+void Matrix::resizeVertically(unsigned newNRows) {
+  nRows = newNRows;
+  data.resize(nRows * nColumns);
+}
+
+void Matrix::swapRows(unsigned row, unsigned otherRow) {
+  assert((row < getNumRows() && otherRow < getNumRows()) &&
+         "Given row out of bounds");
+  if (row == otherRow)
+    return;
+  for (unsigned col = 0; col < nColumns; col++)
+    std::swap(at(row, col), at(otherRow, col));
+}
+
+void Matrix::swapColumns(unsigned column, unsigned otherColumn) {
+  assert((column < getNumColumns() && otherColumn < getNumColumns()) &&
+         "Given column out of bounds");
+  if (column == otherColumn)
+    return;
+  for (unsigned row = 0; row < nRows; row++)
+    std::swap(at(row, column), at(row, otherColumn));
+}
+
+ArrayRef<int64_t> Matrix::getRow(unsigned row) const {
+  return {&data[row * nColumns], nColumns};
+}
+
+void Matrix::addToRow(unsigned sourceRow, unsigned targetRow, int64_t scale) {
+  if (scale == 0)
+    return;
+  for (unsigned col = 0; col < nColumns; ++col)
+    at(targetRow, col) += scale * at(sourceRow, col);
+  return;
+}
+
+void Matrix::print(raw_ostream &os) const {
+  for (unsigned row = 0; row < nRows; ++row) {
+    for (unsigned column = 0; column < nColumns; ++column)
+      os << at(row, column) << ' ';
+    os << '\n';
+  }
+}
+
+void Matrix::dump() const { print(llvm::errs()); }
+
+} // namespace mlir

mlir/unittests/Analysis/AffineStructuresTest.cpp

@@ -0,0 +1,277 @@
+//===- AffineStructuresTest.cpp - Tests for AffineStructures ----*- 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Analysis/AffineStructures.h"
+
+#include <gmock/gmock.h>
+#include <gtest/gtest.h>
+
+#include <numeric>
+
+namespace mlir {
+
+/// Evaluate the value of the given affine expression at the specified point.
+/// The expression is a list of coefficients for the dimensions followed by the
+/// constant term.
+int64_t valueAt(ArrayRef<int64_t> expr, ArrayRef<int64_t> point) {
+  assert(expr.size() == 1 + point.size());
+  int64_t value = expr.back();
+  for (unsigned i = 0; i < point.size(); ++i)
+    value += expr[i] * point[i];
+  return value;
+}
+
+/// If 'hasValue' is true, check that findIntegerSample returns a valid sample
+/// for the FlatAffineConstraints fac.
+///
+/// If hasValue is false, check that findIntegerSample does not return None.
+void checkSample(bool hasValue, const FlatAffineConstraints &fac) {
+  Optional<SmallVector<int64_t, 8>> maybeSample = fac.findIntegerSample();
+  if (!hasValue) {
+    EXPECT_FALSE(maybeSample.hasValue());
+    if (maybeSample.hasValue()) {
+      for (auto x : *maybeSample)
+        llvm::errs() << x << ' ';
+      llvm::errs() << '\n';
+    }
+  } else {
+    ASSERT_TRUE(maybeSample.hasValue());
+    for (unsigned i = 0; i < fac.getNumEqualities(); ++i)
+      EXPECT_EQ(valueAt(fac.getEquality(i), *maybeSample), 0);
+    for (unsigned i = 0; i < fac.getNumInequalities(); ++i)
+      EXPECT_GE(valueAt(fac.getInequality(i), *maybeSample), 0);
+  }
+}
+
+/// Construct a FlatAffineConstraints from a set of inequality and
+/// equality constraints.
+FlatAffineConstraints
+makeFACFromConstraints(unsigned dims, ArrayRef<SmallVector<int64_t, 4>> ineqs,
+                       ArrayRef<SmallVector<int64_t, 4>> eqs) {
+  FlatAffineConstraints fac(ineqs.size(), eqs.size(), dims + 1, dims);
+  for (const auto &eq : eqs)
+    fac.addEquality(eq);
+  for (const auto &ineq : ineqs)
+    fac.addInequality(ineq);
+  return fac;
+}
+
+/// Check sampling for all the permutations of the dimensions for the given
+/// constraint set. Since the GBR algorithm progresses dimension-wise, different
+/// orderings may cause the algorithm to proceed differently. At least some of
+///.these permutations should make it past the heuristics and test the
+/// implementation of the GBR algorithm itself.
+void checkPermutationsSample(bool hasValue, unsigned nDim,
+                             ArrayRef<SmallVector<int64_t, 4>> ineqs,
+                             ArrayRef<SmallVector<int64_t, 4>> eqs) {
+  SmallVector<unsigned, 4> perm(nDim);
+  std::iota(perm.begin(), perm.end(), 0);
+  auto permute = [&perm](ArrayRef<int64_t> coeffs) {
+    SmallVector<int64_t, 4> permuted;
+    for (unsigned id : perm)
+      permuted.push_back(coeffs[id]);
+    permuted.push_back(coeffs.back());
+    return permuted;
+  };
+  do {
+    SmallVector<SmallVector<int64_t, 4>, 4> permutedIneqs, permutedEqs;
+    for (const auto &ineq : ineqs)
+      permutedIneqs.push_back(permute(ineq));
+    for (const auto &eq : eqs)
+      permutedEqs.push_back(permute(eq));
+
+    checkSample(hasValue,
+                makeFACFromConstraints(nDim, permutedIneqs, permutedEqs));
+  } while (std::next_permutation(perm.begin(), perm.end()));
+}
+
+TEST(FlatAffineConstraintsTest, FindSampleTest) {
+  // Bounded sets with only inequalities.
+
+  // 0 <= 7x <= 5
+  checkSample(true, makeFACFromConstraints(1, {{7, 0}, {-7, 5}}, {}));
+
+  // 1 <= 5x and 5x <= 4 (no solution).
+  checkSample(false, makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}));
+
+  // 1 <= 5x and 5x <= 9 (solution: x = 1).
+  checkSample(true, makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}));
+
+  // Bounded sets with equalities.
+  // x >= 8 and 40 >= y and x = y.
+  checkSample(
+      true, makeFACFromConstraints(2, {{1, 0, -8}, {0, -1, 40}}, {{1, -1, 0}}));
+
+  // x <= 10 and y <= 10 and 10 <= z and x + 2y = 3z.
+  // solution: x = y = z = 10.
+  checkSample(true, makeFACFromConstraints(
+                        3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -10}},
+                        {{1, 2, -3, 0}}));
+
+  // x <= 10 and y <= 10 and 11 <= z and x + 2y = 3z.
+  // This implies x + 2y >= 33 and x + 2y <= 30, which has no solution.
+  checkSample(false, makeFACFromConstraints(
+                         3, {{-1, 0, 0, 10}, {0, -1, 0, 10}, {0, 0, 1, -11}},
+                         {{1, 2, -3, 0}}));
+
+  // 0 <= r and r <= 3 and 4q + r = 7.
+  // Solution: q = 1, r = 3.
+  checkSample(true,
+              makeFACFromConstraints(2, {{0, 1, 0}, {0, -1, 3}}, {{4, 1, -7}}));
+
+  // 4q + r = 7 and r = 0.
+  // Solution: q = 1, r = 3.
+  checkSample(false, makeFACFromConstraints(2, {}, {{4, 1, -7}, {0, 1, 0}}));
+
+  // The next two sets are large sets that should take a long time to sample
+  // with a naive branch and bound algorithm but can be sampled efficiently with
+  // the GBR algroithm.
+  //
+  // This is a triangle with vertices at (1/3, 0), (2/3, 0) and (10000, 10000).
+  checkSample(
+      true,
+      makeFACFromConstraints(
+          2, {{0, 1, 0}, {300000, -299999, -100000}, {-300000, 299998, 200000}},
+          {}));
+
+  // This is a tetrahedron with vertices at
+  // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 10000), and (10000, 10000, 10000).
+  // The first three points form a triangular base on the xz plane with the
+  // apex at the fourth point, which is the only integer point.
+  checkPermutationsSample(
+      true, 3,
+      {
+          {0, 1, 0, 0},  // y >= 0
+          {0, -1, 1, 0}, // z >= y
+          {300000, -299998, -1,
+           -100000},                    // -300000x + 299998y + 100000 + z <= 0.
+          {-150000, 149999, 0, 100000}, // -150000x + 149999y + 100000 >= 0.
+      },
+      {});
+
+  // Same thing with some spurious extra dimensions equated to constants.
+  checkSample(true,
+              makeFACFromConstraints(
+                  5,
+                  {
+                      {0, 1, 0, 1, -1, 0},
+                      {0, -1, 1, -1, 1, 0},
+                      {300000, -299998, -1, -9, 21, -112000},
+                      {-150000, 149999, 0, -15, 47, 68000},
+                  },
+                  {{0, 0, 0, 1, -1, 0},       // p = q.
+                   {0, 0, 0, 1, 1, -2000}})); // p + q = 20000 => p = q = 10000.
+
+  // This is a tetrahedron with vertices at
+  // (1/3, 0, 0), (2/3, 0, 0), (2/3, 0, 100), (100, 100 - 1/3, 100).
+  checkPermutationsSample(false, 3,
+                          {
+                              {0, 1, 0, 0},
+                              {0, -300, 299, 0},
+                              {300 * 299, -89400, -299, -100 * 299},
+                              {-897, 894, 0, 598},
+                          },
+                          {});
+
+  // Two tests involving equalities that are integer empty but not rational
+  // empty.
+
+  // This is a line segment from (0, 1/3) to (100, 100 + 1/3).
+  checkSample(false, makeFACFromConstraints(
+                         2,
+                         {
+                             {1, 0, 0},   // x >= 0.
+                             {-1, 0, 100} // -x + 100 >= 0, i.e., x <= 100.
+                         },
+                         {
+                             {3, -3, 1} // 3x - 3y + 1 = 0, i.e., y = x + 1/3.
+                         }));
+
+  // A thin parallelogram. 0 <= x <= 100 and x + 1/3 <= y <= x + 2/3.
+  checkSample(false, makeFACFromConstraints(2,
+                                            {
+                                                {1, 0, 0},    // x >= 0.
+                                                {-1, 0, 100}, // x <= 100.
+                                                {3, -3, 2},   // 3x - 3y >= -2.
+                                                {-3, 3, -1},  // 3x - 3y <= -1.
+                                            },
+                                            {}));
+
+  checkSample(true, makeFACFromConstraints(2,
+                                           {
+                                               {2, 0, 0},   // 2x >= 1.
+                                               {-2, 0, 99}, // 2x <= 99.
+                                               {0, 2, 0},   // 2y >= 0.
+                                               {0, -2, 99}, // 2y <= 99.
+                                           },
+                                           {}));
+}
+
+TEST(FlatAffineConstraintsTest, IsIntegerEmptyTest) {
+  // 1 <= 5x and 5x <= 4 (no solution).
+  EXPECT_TRUE(
+      makeFACFromConstraints(1, {{5, -1}, {-5, 4}}, {}).isIntegerEmpty());
+  // 1 <= 5x and 5x <= 9 (solution: x = 1).
+  EXPECT_FALSE(
+      makeFACFromConstraints(1, {{5, -1}, {-5, 9}}, {}).isIntegerEmpty());
+
+  // An unbounded set, which isIntegerEmpty should detect as unbounded and
+  // return without calling findIntegerSample.
+  EXPECT_FALSE(makeFACFromConstraints(3,
+                                      {
+                                          {2, 0, 0, -1},
+                                          {-2, 0, 0, 1},
+                                          {0, 2, 0, -1},
+                                          {0, -2, 0, 1},
+                                          {0, 0, 2, -1},
+                                      },
+                                      {})
+                   .isIntegerEmpty());
+
+  // FlatAffineConstraints::isEmpty() does not detect the following sets to be
+  // empty.
+
+  // 3x + 7y = 1 and 0 <= x, y <= 10.
+  // Since x and y are non-negative, 3x + 7y can never be 1.
+  EXPECT_TRUE(
+      makeFACFromConstraints(
+          2, {{1, 0, 0}, {-1, 0, 10}, {0, 1, 0}, {0, -1, 10}}, {{3, 7, -1}})
+          .isIntegerEmpty());
+
+  // 2x = 3y and y = x - 1 and x + y = 6z + 2 and 0 <= x, y <= 100.
+  // Substituting y = x - 1 in 3y = 2x, we obtain x = 3 and hence y = 2.
+  // Since x + y = 5 cannot be equal to 6z + 2 for any z, the set is empty.
+  EXPECT_TRUE(
+      makeFACFromConstraints(3,
+                             {
+                                 {1, 0, 0, 0},
+                                 {-1, 0, 0, 100},
+                                 {0, 1, 0, 0},
+                                 {0, -1, 0, 100},
+                             },
+                             {{2, -3, 0, 0}, {1, -1, 0, -1}, {1, 1, -6, -2}})
+          .isIntegerEmpty());
+
+  // 2x = 3y and y = x - 1 + 6z and x + y = 6q + 2 and 0 <= x, y <= 100.
+  // 2x = 3y implies x is a multiple of 3 and y is even.
+  // Now y = x - 1 + 6z implies y = 2 mod 3. In fact, since y is even, we have
+  // y = 2 mod 6. Then since x = y + 1 + 6z, we have x = 3 mod 6, implying
+  // x + y = 5 mod 6, which contradicts x + y = 6q + 2, so the set is empty.
+  EXPECT_TRUE(makeFACFromConstraints(
+                  4,
+                  {
+                      {1, 0, 0, 0, 0},
+                      {-1, 0, 0, 0, 100},
+                      {0, 1, 0, 0, 0},
+                      {0, -1, 0, 0, 100},
+                  },
+                  {{2, -3, 0, 0, 0}, {1, -1, 6, 0, -1}, {1, 1, 0, -6, -2}})
+                  .isIntegerEmpty());
+}
+
+} // namespace mlir

mlir/unittests/Analysis/CMakeLists.txt

@@ -0,0 +1,8 @@
+add_mlir_unittest(MLIRAnalysisTests
+  AffineStructuresTest.cpp
+)
+
+target_link_libraries(MLIRAnalysisTests
+  PRIVATE MLIRLoopAnalysis)
+
+add_subdirectory(Presburger)

mlir/unittests/Analysis/Presburger/CMakeLists.txt

@@ -0,0 +1,7 @@
+add_mlir_unittest(MLIRPresburgerTests
+  MatrixTest.cpp
+  SimplexTest.cpp
+)
+
+target_link_libraries(MLIRPresburgerTests
+  PRIVATE MLIRPresburger)

mlir/unittests/Analysis/Presburger/MatrixTest.cpp

@@ -0,0 +1,92 @@
+//===- MatrixTest.cpp - Tests for Matrix ----------------------------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Analysis/Presburger/Matrix.h"
+#include <gmock/gmock.h>
+#include <gtest/gtest.h>
+
+namespace mlir {
+
+TEST(MatrixTest, ReadWrite) {
+  Matrix mat(5, 5);
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      mat(row, col) = 10 * row + col;
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      EXPECT_EQ(mat(row, col), int(10 * row + col));
+}
+
+TEST(MatrixTest, SwapColumns) {
+  Matrix mat(5, 5);
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      mat(row, col) = col == 3 ? 1 : 0;
+  mat.swapColumns(3, 1);
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      EXPECT_EQ(mat(row, col), col == 1 ? 1 : 0);
+
+  // swap around all the other columns, swap (1, 3) twice for no effect.
+  mat.swapColumns(3, 1);
+  mat.swapColumns(2, 4);
+  mat.swapColumns(1, 3);
+  mat.swapColumns(0, 4);
+  mat.swapColumns(2, 2);
+
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      EXPECT_EQ(mat(row, col), col == 1 ? 1 : 0);
+}
+
+TEST(MatrixTest, SwapRows) {
+  Matrix mat(5, 5);
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      mat(row, col) = row == 2 ? 1 : 0;
+  mat.swapRows(2, 0);
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      EXPECT_EQ(mat(row, col), row == 0 ? 1 : 0);
+
+  // swap around all the other rows, swap (2, 0) twice for no effect.
+  mat.swapRows(3, 4);
+  mat.swapRows(1, 4);
+  mat.swapRows(2, 0);
+  mat.swapRows(1, 1);
+  mat.swapRows(0, 2);
+
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      EXPECT_EQ(mat(row, col), row == 0 ? 1 : 0);
+}
+
+TEST(MatrixTest, resizeVertically) {
+  Matrix mat(5, 5);
+  EXPECT_EQ(mat.getNumRows(), 5u);
+  EXPECT_EQ(mat.getNumColumns(), 5u);
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      mat(row, col) = 10 * row + col;
+
+  mat.resizeVertically(3);
+  EXPECT_EQ(mat.getNumRows(), 3u);
+  EXPECT_EQ(mat.getNumColumns(), 5u);
+  for (unsigned row = 0; row < 3; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      EXPECT_EQ(mat(row, col), int(10 * row + col));
+
+  mat.resizeVertically(5);
+  EXPECT_EQ(mat.getNumRows(), 5u);
+  EXPECT_EQ(mat.getNumColumns(), 5u);
+  for (unsigned row = 0; row < 5; ++row)
+    for (unsigned col = 0; col < 5; ++col)
+      EXPECT_EQ(mat(row, col), row >= 3 ? 0 : int(10 * row + col));
+}
+
+} // namespace mlir

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

@@ -0,0 +1,219 @@
+//===- SimplexTest.cpp - Tests for Simplex --------------------------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Analysis/Presburger/Simplex.h"
+
+#include <gmock/gmock.h>
+#include <gtest/gtest.h>
+
+namespace mlir {
+
+/// Take a snapshot, add constraints making the set empty, and rollback.
+/// The set should not be empty after rolling back.
+TEST(SimplexTest, emptyRollback) {
+  Simplex simplex(2);
+  // (u - v) >= 0
+  simplex.addInequality({1, -1, 0});
+  EXPECT_FALSE(simplex.isEmpty());
+
+  unsigned snapshot = simplex.getSnapshot();
+  // (u - v) <= -1
+  simplex.addInequality({-1, 1, -1});
+  EXPECT_TRUE(simplex.isEmpty());
+  simplex.rollback(snapshot);
+  EXPECT_FALSE(simplex.isEmpty());
+}
+
+/// Check that the set gets marked as empty when we add contradictory
+/// constraints.
+TEST(SimplexTest, addEquality_separate) {
+  Simplex simplex(1);
+  simplex.addInequality({1, -1}); // x >= 1.
+  ASSERT_FALSE(simplex.isEmpty());
+  simplex.addEquality({1, 0}); // x == 0.
+  EXPECT_TRUE(simplex.isEmpty());
+}
+
+void expectInequalityMakesSetEmpty(Simplex &simplex, ArrayRef<int64_t> coeffs,
+                                   bool expect) {
+  ASSERT_FALSE(simplex.isEmpty());
+  unsigned snapshot = simplex.getSnapshot();
+  simplex.addInequality(coeffs);
+  EXPECT_EQ(simplex.isEmpty(), expect);
+  simplex.rollback(snapshot);
+}
+
+TEST(SimplexTest, addInequality_rollback) {
+  Simplex simplex(3);
+  SmallVector<int64_t, 4> coeffs[]{{1, 0, 0, 0},   // u >= 0.
+                                   {-1, 0, 0, 0},  // u <= 0.
+                                   {1, -1, 1, 0},  // u - v + w >= 0.
+                                   {1, 1, -1, 0}}; // u + v - w >= 0.
+  // The above constraints force u = 0 and v = w.
+  // The constraints below violate v = w.
+  SmallVector<int64_t, 4> checkCoeffs[]{{0, 1, -1, -1},  // v - w >= 1.
+                                        {0, -1, 1, -1}}; // v - w <= -1.
+
+  for (int run = 0; run < 4; run++) {
+    unsigned snapshot = simplex.getSnapshot();
+
+    expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], false);
+    expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], false);
+
+    for (int i = 0; i < 4; i++)
+      simplex.addInequality(coeffs[(run + i) % 4]);
+
+    expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], true);
+    expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], true);
+
+    simplex.rollback(snapshot);
+    EXPECT_EQ(simplex.numConstraints(), 0u);
+
+    expectInequalityMakesSetEmpty(simplex, checkCoeffs[0], false);
+    expectInequalityMakesSetEmpty(simplex, checkCoeffs[1], false);
+  }
+}
+
+Simplex simplexFromConstraints(unsigned nDim,
+                               SmallVector<SmallVector<int64_t, 8>, 8> ineqs,
+                               SmallVector<SmallVector<int64_t, 8>, 8> eqs) {
+  Simplex simplex(nDim);
+  for (const auto &ineq : ineqs)
+    simplex.addInequality(ineq);
+  for (const auto &eq : eqs)
+    simplex.addEquality(eq);
+  return simplex;
+}
+
+TEST(SimplexTest, isUnbounded) {
+  EXPECT_FALSE(simplexFromConstraints(
+                   2, {{1, 1, 0}, {-1, -1, 0}, {1, -1, 5}, {-1, 1, -5}}, {})
+                   .isUnbounded());
+
+  EXPECT_TRUE(
+      simplexFromConstraints(2, {{1, 1, 0}, {1, -1, 5}, {-1, 1, -5}}, {})
+          .isUnbounded());
+
+  EXPECT_TRUE(
+      simplexFromConstraints(2, {{-1, -1, 0}, {1, -1, 5}, {-1, 1, -5}}, {})
+          .isUnbounded());
+
+  EXPECT_TRUE(simplexFromConstraints(2, {}, {}).isUnbounded());
+
+  EXPECT_FALSE(simplexFromConstraints(3,
+                                      {
+                                          {2, 0, 0, -1},
+                                          {-2, 0, 0, 1},
+                                          {0, 2, 0, -1},
+                                          {0, -2, 0, 1},
+                                          {0, 0, 2, -1},
+                                          {0, 0, -2, 1},
+                                      },
+                                      {})
+                   .isUnbounded());
+
+  EXPECT_TRUE(simplexFromConstraints(3,
+                                     {
+                                         {2, 0, 0, -1},
+                                         {-2, 0, 0, 1},
+                                         {0, 2, 0, -1},
+                                         {0, -2, 0, 1},
+                                         {0, 0, -2, 1},
+                                     },
+                                     {})
+                  .isUnbounded());
+
+  EXPECT_TRUE(simplexFromConstraints(3,
+                                     {
+                                         {2, 0, 0, -1},
+                                         {-2, 0, 0, 1},
+                                         {0, 2, 0, -1},
+                                         {0, -2, 0, 1},
+                                         {0, 0, 2, -1},
+                                     },
+                                     {})
+                  .isUnbounded());
+
+  // Bounded set with equalities.
+  EXPECT_FALSE(simplexFromConstraints(2,
+                                      {{1, 1, 1},    // x + y >= -1.
+                                       {-1, -1, 1}}, // x + y <=  1.
+                                      {{1, -1, 0}}   // x = y.
+                                      )
+                   .isUnbounded());
+
+  // Unbounded set with equalities.
+  EXPECT_TRUE(simplexFromConstraints(3,
+                                     {{1, 1, 1, 1},     // x + y + z >= -1.
+                                      {-1, -1, -1, 1}}, // x + y + z <=  1.
+                                     {{1, -1, -1, 0}}   // x = y + z.
+                                     )
+                  .isUnbounded());
+
+  // Rational empty set.
+  EXPECT_FALSE(simplexFromConstraints(3,
+                                      {
+                                          {2, 0, 0, -1},
+                                          {-2, 0, 0, 1},
+                                          {0, 2, 2, -1},
+                                          {0, -2, -2, 1},
+                                          {3, 3, 3, -4},
+                                      },
+                                      {})
+                   .isUnbounded());
+}
+
+TEST(SimplexTest, getSamplePointIfIntegral) {
+  // Empty set.
+  EXPECT_FALSE(simplexFromConstraints(3,
+                                      {
+                                          {2, 0, 0, -1},
+                                          {-2, 0, 0, 1},
+                                          {0, 2, 2, -1},
+                                          {0, -2, -2, 1},
+                                          {3, 3, 3, -4},
+                                      },
+                                      {})
+                   .getSamplePointIfIntegral()
+                   .hasValue());
+
+  auto maybeSample = simplexFromConstraints(2,
+                                            {// x = y - 2.
+                                             {1, -1, 2},
+                                             {-1, 1, -2},
+                                             // x + y = 2.
+                                             {1, 1, -2},
+                                             {-1, -1, 2}},
+                                            {})
+                         .getSamplePointIfIntegral();
+
+  EXPECT_TRUE(maybeSample.hasValue());
+  EXPECT_THAT(*maybeSample, testing::ElementsAre(0, 2));
+
+  auto maybeSample2 = simplexFromConstraints(2,
+                                             {
+                                                 {1, 0, 0},  // x >= 0.
+                                                 {-1, 0, 0}, // x <= 0.
+                                             },
+                                             {
+                                                 {0, 1, -2} // y = 2.
+                                             })
+                          .getSamplePointIfIntegral();
+  EXPECT_TRUE(maybeSample2.hasValue());
+  EXPECT_THAT(*maybeSample2, testing::ElementsAre(0, 2));
+
+  EXPECT_FALSE(simplexFromConstraints(1,
+                                      {// 2x = 1. (no integer solutions)
+                                       {2, -1},
+                                       {-2, +1}},
+                                      {})
+                   .getSamplePointIfIntegral()
+                   .hasValue());
+}
+
+} // namespace mlir

mlir/unittests/CMakeLists.txt

@@ -5,6 +5,7 @@ function(add_mlir_unittest test_dirname)
   add_unittest(MLIRUnitTests ${test_dirname} ${ARGN})
 endfunction()
 
+add_subdirectory(Analysis)
 add_subdirectory(Dialect)
 add_subdirectory(IR)
 add_subdirectory(Pass)