Introduce subtraction for FlatAffineConstraints

[arjunp]

Summary

Subtraction is a foundational arithmetic operation that is often used when computing, for example, data transfer sets or cache hits. Since the result of subtraction need not be a convex polytope, a new class PresburgerSet is introduced to represent unions of convex polytopes.

[rriddle]

Please resolve the clang-tidy and clang-format issues.

Thanks.

mlir/lib/Analysis/AffineStructures.cpp

1065

nit: Anonymous functions should be marked static and at the top level, anonymous namespaces are only really for classes.

mlir/lib/Analysis/Presburger/Set.cpp

39

Same here.

104

Same here.

123

Comments on top-level entities should be ///.

246

nit: Just inline this variable into its use.

mlir/lib/Analysis/Presburger/Simplex.cpp

458

Cache the end iterator of loops unless the size changes dynamically.

mlir/unittests/Analysis/Presburger/SetTest.cpp

17

Please run clang-format here.

[arjunp]

Address comments.

[arjunp]

Fix header comment in SetTest.cpp.

[bondhugula]

Thanks very much for introducing this. Some initial superficial comments.

mlir/include/mlir/Analysis/Presburger/Set.h

71

const FlatAffineConstraints &c

This would lead to an extra copy also otherwise.

mlir/lib/Analysis/AffineStructures.cpp

1065

`&& "... message ..." please.

mlir/lib/Analysis/Presburger/Set.cpp

39

Missing doc comment.

42–45

Can you please split this into two assert's - one for dims and one for symbols? That would be really useful/needed for debugging.

54

an -> a

93–94

Instead of cs1, cs2, consider using csA, csB.

104

Missing doc comment.

107

Avoid auto.

[bondhugula]

mlir/lib/Analysis/Presburger/Set.cpp

89

Are there other intersect.* methods? If not, just use intersect?

[bondhugula]

mlir/include/mlir/Analysis/Presburger/Set.h

93–94

4 would a lot of stack space? Use 2 instead? A single FlatAffineConstraints is already a good amount of inline space. (Would be good to count that and take into account.)

[arjunp]

Address comments. Add some tests for complement.

[arjunp]

mlir/include/mlir/Analysis/Presburger/Set.h

71

It can't be const. I made it a non-const reference. I also added another version with an rvalue reference to support passing rvalues. It's modified internally, but its initial state eventually gets restored at the time of return, so it's safe to take it as a non-const lvalue reference as well without taking a copy.

mlir/lib/Analysis/Presburger/Set.cpp

89

No, this was more about uniformity with unionSet which can't be union.

[bondhugula]

mlir/include/mlir/Analysis/Presburger/Set.h

48

The ownership semantics is weird and the API doc doesn't mention about it - it can only be determined by looking at the implementation the way it is. You are using a move on this inside. Should this be instead a const reference on the API method and a copy happens inside? You anyway have a copy either way. The const ref would be the standard way.

70

c is undefined here. If fac is being modified, it's not reflected in the doc comment. If it's returns the set difference fac - set, why is it modifying fac?

[bondhugula]

mlir/include/mlir/Analysis/Presburger/Set.h

87

This is forcing a certain inline size on the SmallVector - consider the alternative signature:

bool findIntegerSample(SmallVectorImpl<int64_t> &sample)

This allows the caller to determine what inline size to use for SmallVector.

98

Likewise, consider the alternative instead of forcing the caller to use 2.

mlir/lib/Analysis/Presburger/CMakeLists.txt

2

I don't think you can use this - it sort of breaks modularity/layering. I'm not sure though. Instead depend on the right thing?

mlir/lib/Analysis/Presburger/Set.cpp

29

Nit: getAll... ?

34

You'll need the non const accessor as well at least for private access (even though you aren't using it yet)?

52–53

Nit: Consider using setA and setB - here and anywhere else.

60

an -> a

[arjunp]

Address comments.

[arjunp]

Thanks for reviewing this!

mlir/include/mlir/Analysis/Presburger/Set.h

70

Fixed the comment. fac is modified by the algorithm internally but gets restored to its original state by the time it returns.

mlir/lib/Analysis/Presburger/CMakeLists.txt

2

Merged MLIRPresburger into MLIRLoopAnalysis to avoid a cyclic dependency between them.

mlir/lib/Analysis/Presburger/Set.cpp

34

For private access, would it be cleaner than accessing the member variable directly?

[arjunp]

The build failure appears to be unrelated. From the log:

ERROR   exception: Cmd('git') failed due to: exit code(1)
  cmdline: git fetch --all
  stdout: 'Fetching origin
Fetching upstream'
  stderr: '[e-mail]: Permission denied (publickey).
fatal: Could not read from remote repository.
 
Please make sure you have the correct access rights
and the repository exists.
error: Could not fetch origin'

[ftynse]

mlir/include/mlir/Analysis/Presburger/Set.h

65

Why is this a static function but insertsect/union are not?

[arjunp]

mlir/include/mlir/Analysis/Presburger/Set.h

65

The implementation details are such that making intersect/union static functions that return the resultant set rather than be member functions modifying an object results in unnecessary copies.

On the other hand, the implementation of complement is such that the result set is constructed from scratch anyway. If the caller wants both the original set as well as the complement, a static function allows them to obtain that without any extra copies. If it was only a non-static member function, they would have to create a copy of the original set and then call complement on the copy, incurring an additional copy. The same is true of subtract, actually, so that could be made static too, if this reasoning makes sense.

[ftynse]

mlir/include/mlir/Analysis/Presburger/Set.h

24

Are there any intended guarantees of the "canonical" form of the set? E.g., it appears to me that the contained FAC's can overlap, which may or may not be a good idea depending on how operations will be handled.

65

Leaking implementation details to the API is very unfortunate. This means that if the implementation changes, so will the API, and it also makes it harder for uses to understand when they function they are calling is static and when it is not. In the case of already-complex abstraction such as Presburger sets, it adds even more complexity that could have been avoided.

Could you rather have something like a (non-static) getComplementSet() function that returns the complement set and indicates in its name that it produces a new value?

Have you considered having a facade class that doesn't store actual data so is cheap to copy, and use shared_ptr / uniquer / copy-on-write behind the scenes?

NRVO is a thing in modern compilers, does the copy actually happen when you return?

71

Why is this taking a mutable reference to fac?

mlir/lib/Analysis/Presburger/CMakeLists.txt

1

Why this change?

The general policy is to have one library per directory, and accordingly a cmake file.

mlir/lib/Analysis/Presburger/Set.cpp

112

reserve space in the vector before populating it in the loop

124

same here

130

Notation nit: in set theory, - is symmetric difference, e.g. (A \ B) u (B \ A), one-sided difference is usually denoted as \

133

Nit: ^ for intersection, v for union ?

135

What is the "basic set" ?

137

What is s_ij, a single constraint?

146

Do you ignore the fact that constraints are redundant, or the constraints themselves?

167

SmallBitVector?

168

Do not recompute the upper bound on each iteration

174

Non-trivial lambdas deserve a comment, similarly to top-level functions

231–235

Why is this even necessary?

239

This wouldn't need a comment if you had FlatAffineConstraints::universe(), or used PresubrgerSet::universe(0 instead.

257

copy-pasta

[bondhugula]

mlir/include/mlir/Analysis/Presburger/Set.h

65

For something returning a new value, we could use a unique_ptr return value, but that would lead to a heap allocation (in some ways defeating the purpose of using a SmallVector and contiguous storage inside a FAC)? To avoid heap allocations, we could instead use a trailing output argument (passed by reference), and this will both avoid heap allocations and copies for sure - but this makes call site code not as clean and "composing". And finally returning the FAC by value would lead to copies if "return value optimization" doesn't happen (could be sensitive to the control flow of the implementation?), and one may want to not rely on it since performance is important here. Avoid heap allocations (esp. for small ones which are actually the common case) and copies is key here.

What would be the right choices? @ftynse @arjunp

[ftynse]

mlir/include/mlir/Analysis/Presburger/Set.h

31

This will make a useless copy of fac on call, and enable implicit copy-construction. Not sure the latter is a good idea.

65

IMO, unique_ptr is a bad idea unless there is some _uniqueness_ semantics, either in ownership or in object existence. Here it does not seem to be the case, and it will lead to an even more awkward to use API.

I am slightly concerned that all this can be classified as premature optimization. Especially since we are looking into exponential-complexity algorithms, is the execution time really dominated by copies or allocations? At what point we actually stop benefiting from inline stack storage because we allocate anyway?

For this specific case, I just don't see any good reason to have static functions (other than makeUniverse, which is a factory function). Even more, I would actually prefer having only an explicit cast from FAC to PresburgerSet and only support subtraction between to instances of the latter class. This makes it clear, when reading the code, that it starts to use a more expressive and expensive abstraction.

I would strongly recommend thinking holistically about trade-offs in efficiency and usability, and coming up with a proposition of how the end result should look like and hopefully some design/implementation principles. So far it seems to be "avoid copy at all cost", and if this is the approach that is going to be taken, I would like to see a convincing rationale to support it.

Regarding the API, I would also recommend return *this from all mutating function so that they become chainable: PresburgerSet(fac).subtract(otherSet).insersect(moreSet).complement() reads quite fluently. As opposed to auto x =PresburgerSet::subtract(fac, otherSet); x.intersect(moreSet); PresburgerSet::complement(x); that is currently required.

71

Haven't seen the comment below. It's a bad smell for the API, again. As the user, I would have no way of knowing if the operand is reverted back to the original state or not, so I would have copied it just to be safe. And since the argument is not const, future changes make stop reverting it back to the original state and break all uses which expect that in subtle ways.

[arjunp]

Changed the API to return the result of set operations. Union, intersect, subtract, complement are now non-static, const member functions that return the result of the operation. This also allows chaining. Also addressed other comments and fixed an issue with the intersect tests.

[arjunp]

mlir/include/mlir/Analysis/Presburger/Set.h

24

No guarantees are intended. I can't think of any algorithmic simplifications or optimizations that could be made to the implementations of any of the operations by taking advantage of a no-overlap invariant.

65

I've changed the API to make subtract and complement non-static. I realized that I was slightly mistaken earlier -- intersect is also like subtract and complement in that it constructs the result from scratch, so returning the value seems favourable. Now unionSet, intersect, subtract and complement are all non-static, const, and return the result of the operation. This also allows chaining.

Also, only subtraction between sets is possible now and the FAC -> PresburgerSet cast has been made explicit.

71

It's just passed by value now. Also, only subtraction between PresburgerSets is possible now, so this function has been made private.

mlir/lib/Analysis/Presburger/CMakeLists.txt

1

FlatAffineConstraints depends on Simplex, while Set depends on FlatAffineConstraints, resulting in a cyclic dependency if MLIRPresburger is kept separate.

mlir/lib/Analysis/Presburger/Set.cpp

231–235

Removed. (It was previously necessary since rvalues couldn't be passed to the non-const lvalue overload. Since that overload no longer takes a reference, this is no longer needed.)

[bondhugula]

mlir/include/mlir/Analysis/Presburger/Set.h

65

Especially since we are looking into exponential-complexity algorithms, is the

These are not of exponential complexity --- most of the things using these are just quadratic/cubic and many linear. The only one exponential is also for all practical purposes of polynomial time here (Simplex). And more importantly, both n (the input size whether dimensionality of constraint) are small here - from a handful to few tens at most. In the common case, in fact, they are actually quite small. I understand things depend on use cases. But I think this is a good time to select the right data structures. Otherwise, I agree with all the points made - I don't think we should go for "avoid all copies" at this stage, but also not go in the wrong direction.

I strongly feel copies and stack allocations to be quite important if the focus remains on making sure the input sizes and use cases *by design* are all small - at least in the upstream passes/utilities, which has an impact on how passes/utilities are designed to make use of this API.

[arjunp]

Try to rebase to the new LLVM HEAD.

[arjunp]

Trying again to rebase.

[bondhugula]

mlir/include/mlir/Analysis/Presburger/Set.h

50–51

The comment can be rephrased. Something like Perform a union of fac` with this FlatAffineConstraints`?

51

Should it be addFlat.. or unionFlat...? Add can sometimes be misleading - appending constraints will lead to an intersect for a single system.

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

172–173

Likewise.

mlir/lib/Analysis/AffineStructures.cpp

1061

evaluate an affine expression ?

1077–1081

Use the i = 0, e = ...; i < e form.

mlir/lib/Analysis/Presburger/Set.cpp

255

It is odd that a PresburgerSet(..) will return an empty set while FlatAffineConstraints(.., ...) will return a universal set. Could we make things consistent? Could you just do PresburgetSet::getEmptySet(.., ...)? It's confusing otherwise.

295

const

305–309

Could you improve this slightly for debugging purposes? You could use interleaveComma while printing the list enclosed in [ -- so that we easily know where the constraint sets start and end in a debug output.

mlir/unittests/Analysis/Presburger/SetTest.cpp

5–9

Please add a comment here and/or below to say what this file is testing.

17–53

All of these methods are missing doc comments. We definitely need them at least for the first one.

496–507

Sorry, I can't immediately tell locally what these mean. I wasn't expecting points in the 2 to 10 range for x and y appear here, but there are five of them. testComplementAtPoints and all other test* methods are missing doc comments. Please add.

[ftynse]

mlir/include/mlir/Analysis/Presburger/Set.h

24

Then it is worth documenting.

65

Now unionSet, intersect, subtract and complement are all non-static, const, and return the result of the operation. This also allows chaining.

Great, now they are all consistent! Let's push this one step further and try to think if the "const member function acting on a const reference and returning a new object" applies to other operations we might want to have on PresburgerSet or not. It could also be surprising to get some operations that mutate the object they are called on and others that produce new objects.

Also, only subtraction between sets is possible now and the FAC -> PresburgerSet cast has been made explicit.

Thanks!

These are not of exponential complexity --- most of the things using these are just quadratic/cubic and many linear.

I meant simplex indeed. Also, as we start wrapping it into operations such as subtraction and building higher-level operations on top of those, it will become increasingly less clear which operations are more likely to be computationally expensive.

But I think this is a good time to select the right data structures.

You know that I am very open to doing one thing that works and reconsidering it later if needed. There are costs of such reconsideration, but they don't look terribly high at this point. If we make a properly isolated API that does not leak implementation details, this cost of change will remain manageable. But this shouldn't mean we shouldn't carefully choose the right data structures in the first place.

I strongly feel copies and stack allocations to be quite important if the focus remains on making sure the input sizes and use cases *by design* are all small - at least in the upstream passes/utilities, which has an impact on how passes/utilities are designed to make use of this API.

A data-driven approach could work well here. If we collect some performance measurements of how the implementation behaves for different kinds of inputs, we can quantify what small actually means and what are the costs of not keeping cases small.

mlir/lib/Analysis/Presburger/CMakeLists.txt

1

Then some files should move... For example, we can have lib/Analysis/PresburgerSet.cpp, keep Simplex where it is (optionally rename MLIRPresburger to MLIRSimplex) and keep the dependency of MLIRLoopAnalysis on MLIRSimplex.

Or we can go the other way around, which we should arguably do anyway, and factor the entire affine analysis out into a separate directory under Analysis.

mlir/lib/Analysis/Presburger/Set.cpp

255

Speaking about which, is there a reason why we need public default constructors? If not, I'd just go with factory functions for both empty and universe sets (in a separate patch, this patch should be consistent with what is already present in the codebase)

[arjunp]

Address comments.

mlir/include/mlir/Analysis/Presburger/Set.h

51

Changed to unionFACInPlace to disambiguate from the union operation that returns the result rather than mutating the set and added some documentation to clarify this.

I also added an analogous unionSetInPlace and used it in subtract. If we want to provide the user the option to save copies in case they want to union in-place, this can be left public. Otherwise we can make it private.

mlir/lib/Analysis/Presburger/CMakeLists.txt

1–4

Moved Set.cpp to lib/Analysis/PresburgerSet.cpp.

mlir/lib/Analysis/Presburger/Set.cpp

255

Changed to PresburgetSet::getEmptySet(.., ...).

305–309

It looks somewhat awkward printing the FACs with interleaved commas... each FAC takes up multiple lines, and the header of each FAC dump (something like Constraints (1 dims, 0 symbols, 0 locals), (1 constraints)) is much more prominent than the comma is. With commas it looks something like this

4 FlatAffineConstraints: [
Constraints (1 dims, 0 symbols, 0 locals), (1 constraints)
(None  const)
-1 -5 >= 0

,
Constraints (1 dims, 0 symbols, 0 locals), (1 constraints)
(None  const)
1 -3 = 0

,
Constraints (1 dims, 0 symbols, 0 locals), (1 constraints)
(None  const)
1 -4 = 0

,
Constraints (1 dims, 0 symbols, 0 locals), (1 constraints)
(None  const)
1 -5 = 0

]

Are the commas adding any value here?

mlir/unittests/Analysis/Presburger/SetTest.cpp

5–9

Does this work?

496–507

This is not a list of points that are supposed to be present; it is a list of points to validate correctness at. iIt checks that these points are present in the complement iff they are not present in the original set.

[bondhugula]

@ftynse comments from the previous round sound good to me too. Looks good to commit from my side once those are addressed.

mlir/lib/Analysis/Presburger/Set.cpp

305–309

They aren't really adding any value. I just meant they could be improved in some way. Feel free to do as you see fit. Thanks.

[arjunp]

clang-format.

[arjunp]

Changed auto to explicit types in PresburgerSetTest.

[arjunp]

mlir/lib/Analysis/Presburger/CMakeLists.txt

1

Moved to PresburgerSet.cpp.

mlir/lib/Analysis/Presburger/Set.cpp

255

(also made the default constructor private)

[arjunp]

clang-format again. Fix a typo in PresburgerSetTest (makeFACFromIneq -> makeFACFromIneqs)

[arjunp]

I hope all the issues have been addressed. @ftynse, do you have any further concerns?

[arjunp]

Gentle reminder :) @ftynse, did you have any further concerns?

[ftynse]

In D87068#2312200, @arjunp wrote:

Gentle reminder :) @ftynse, did you have any further concerns?

Nope, sorry, once a commit is approved by someone, it disappears from the attention set for everybody else...

[arjunp]

Great! I don't have the permissions yet -- can one of you land the patch? :)

mlir/include/mlir/Analysis/AffineStructures.h

public:
 
   /// 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;
 
+  /// Returns true if the given point satisfies the constraints, or false
+  /// otherwise.
+  bool containsPoint(ArrayRef<int64_t> point) const;
+
   // Clones this object.
   std::unique_ptr<FlatAffineConstraints> clone() const;
 
   /// Returns the value at the specified equality row and column.
   inline int64_t atEq(unsigned i, unsigned j) const {
     return equalities[i * numReservedCols + j];
   }
   inline int64_t &atEq(unsigned i, unsigned j) {

mlir/include/mlir/Analysis/Presburger/Set.h

+//===- Set.h - MLIR PresburgerSet 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
+//
+//===----------------------------------------------------------------------===//
+//
+// A class to represent unions of FlatAffineConstraints.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_ANALYSIS_PRESBURGER_SET_H
+#define MLIR_ANALYSIS_PRESBURGER_SET_H
+
+#include "mlir/Analysis/AffineStructures.h"
+
+namespace mlir {
+
+/// This class can represent a union of FlatAffineConstraints, with support for
+/// union, intersection, subtraction and complement operations, as well as
+/// sampling.
+///
+/// The FlatAffineConstraints (FACs) are stored in a vector, and the set
+/// represents the union of these FACs.
+class PresburgerSet {
+public:
+  PresburgerSet(unsigned nDim = 0, unsigned nSym = 0)
+      : nDim(nDim), nSym(nSym) {}
+  PresburgerSet(FlatAffineConstraints cs);
+
+  /// Return the number of FACs in the union.
+  unsigned getNumFACs() const;
+
+  /// Return the number of real dimensions.
+  unsigned getNumDims() const;
+
+  /// Return the number of symbolic dimensions.
+  unsigned getNumSyms() const;
+
+  /// Returns a reference to the list of FlatAffineConstraints.
+  ArrayRef<FlatAffineConstraints> getFlatAffineConstraints() const;
+
+  /// Returns the FlatAffineConsatraints at the specified index.
+  const FlatAffineConstraints &getFlatAffineConstraints(unsigned index) const;
+
+  /// Add the given FlatAffineConstraints to the union.
+  void addFlatAffineConstraints(FlatAffineConstraints cs);
+
+  /// Intersect the given set with the current set.
+  void unionSet(const PresburgerSet &set);
+
+  /// Intersect the given set with the current set.
+  void intersectSet(const PresburgerSet &set);
+
+  /// Returns true if the set contains the given point, or false otherwise.
+  bool containsPoint(ArrayRef<int64_t> point) const;
+
+  /// Print the set's internal state.
+  void print(raw_ostream &os) const;
+  void dump() const;
+
+  /// Returns the complement of the given set.
+  static PresburgerSet complement(const PresburgerSet &set);
+
+  /// Subtract the given set from the current set.
+  void subtract(const PresburgerSet &set);
+
+  /// Return the set difference c - set.
+  static PresburgerSet subtract(FlatAffineConstraints c,
+                                const PresburgerSet &set);
+
+  /// Return a universe set of the specified type that contains all points.
+  static PresburgerSet makeUniverse(unsigned nDim = 0, unsigned nSym = 0);
+
+  /// Returns true if all the sets in the union are known to be integer empty
+  /// false otherwise.
+  bool isIntegerEmpty() const;
+
+  /// Find an integer sample from the given set. This should not be called if
+  /// any of the FACs in the union are unbounded.
+  llvm::Optional<SmallVector<int64_t, 8>> findIntegerSample();
+
+private:
+  /// Number of identifiers corresponding to real dimensions.
+  unsigned nDim;
+
+  /// Number of symbolic dimensions, unknown but constant for analysis, as in
+  /// FlatAffineConstraints.
+  unsigned nSym;
+
+  /// The list of flatAffineConstraints that this set is the union of.
+  SmallVector<FlatAffineConstraints, 4> flatAffineConstraints;
+};
+
+} // namespace mlir
+
+#endif // MLIR_ANALYSIS_PRESBURGER_SET_H

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

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 addFlatAffineConstraints(const FlatAffineConstraints &fac);
+
   /// Compute the maximum or minimum value of the given row, depending on
   /// direction. The specified row is never pivoted.
   ///
   /// 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

mlir/lib/Analysis/AffineStructures.cpp

bool FlatAffineConstraints::isIntegerEmpty() const {
   return !simplex.findIntegerSample().hasValue();
 }
 
 Optional<SmallVector<int64_t, 8>>
 FlatAffineConstraints::findIntegerSample() const {
   return Simplex(*this).findIntegerSample();
 }
 
+namespace {
+/// Helper to evaluate the value of an affine expression at a 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;
+}
+} // namespace
+
+/// A point satisfies an equality iff the value of the equality at the
+/// expression is zero, and it satisfies an inequality iff the value of the
+/// inequality at that point is non-negative.
+bool FlatAffineConstraints::containsPoint(ArrayRef<int64_t> point) const {
+  for (unsigned i = 0; i < getNumEqualities(); ++i) {
+    if (valueAt(getEquality(i), point) != 0)
+      return false;
+  }
+  for (unsigned i = 0; i < getNumInequalities(); ++i) {
+    if (valueAt(getInequality(i), point) < 0)
+      return false;
+  }
+  return true;
+}
+
 /// 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.,
 ///  64*i - 100 >= 0  =>  64*i - 128 >= 0 (since 'i' is an integer). This is a
 /// fast method - linear in the number of coefficients.
 // Example on how this affects practical cases: consider the scenario:
 // 64*i >= 100, j = 64*i; without a tightening, elimination of i would yield
 // j >= 100 instead of the tighter (exact) j >= 128.

mlir/lib/Analysis/Presburger/CMakeLists.txt

 add_mlir_library(MLIRPresburger
+  ../AffineStructures.cpp
   Simplex.cpp
   Matrix.cpp
+  Set.cpp
   )

mlir/lib/Analysis/Presburger/Set.cpp

+//===- Set.cpp - MLIR PresburgerSet 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/Set.h"
+#include "mlir/Analysis/Presburger/Simplex.h"
+
+using namespace mlir;
+
+PresburgerSet::PresburgerSet(FlatAffineConstraints cs)
+    : nDim(cs.getNumDimIds()), nSym(cs.getNumSymbolIds()) {
+  addFlatAffineConstraints(cs);
+}
+
+unsigned PresburgerSet::getNumFACs() const {
+  return flatAffineConstraints.size();
+}
+
+unsigned PresburgerSet::getNumDims() const { return nDim; }
+
+unsigned PresburgerSet::getNumSyms() const { return nSym; }
+
+ArrayRef<FlatAffineConstraints>
+PresburgerSet::getFlatAffineConstraints() const {
+  return flatAffineConstraints;
+}
+
+const FlatAffineConstraints &
+PresburgerSet::getFlatAffineConstraints(unsigned index) const {
+  assert(index < flatAffineConstraints.size() && "index out of bounds!");
+  return flatAffineConstraints[index];
+}
+
+namespace {
+void assertDimensionsCompatible(FlatAffineConstraints cs, PresburgerSet set) {
+  assert(
+      cs.getNumDimIds() == set.getNumDims() &&
+      cs.getNumSymbolIds() == set.getNumSyms() &&
+      "Dimensionalities of the FlatAffineConstraints and PresburgerSet do not "
+      "match");
+}
+
+void assertDimensionsCompatible(PresburgerSet set1, PresburgerSet set2) {
+  assert(set1.getNumDims() == set2.getNumDims() &&
+         set1.getNumSyms() == set2.getNumSyms() &&
+         "Dimensionalities of the PresburgerSets do not match");
+}
+} // anonymous namespace
+
+/// Add an FAC to the union.
+void PresburgerSet::addFlatAffineConstraints(FlatAffineConstraints cs) {
+  assertDimensionsCompatible(cs, *this);
+  flatAffineConstraints.push_back(cs);
+}
+
+/// Union the current set with the given set.
+///
+/// This is accomplished by simply adding all the FACs of the given set to the
+/// current set.
+void PresburgerSet::unionSet(const PresburgerSet &set) {
+  assertDimensionsCompatible(set, *this);
+  for (const FlatAffineConstraints &cs : set.flatAffineConstraints)
+    addFlatAffineConstraints(std::move(cs));
+}
+
+/// A point is contained in the union iff any of the parts contain the point.
+bool PresburgerSet::containsPoint(ArrayRef<int64_t> point) const {
+  for (const FlatAffineConstraints &fac : flatAffineConstraints) {
+    if (fac.containsPoint(point))
+      return true;
+  }
+  return false;
+}
+
+PresburgerSet PresburgerSet::makeUniverse(unsigned nDim, unsigned nSym) {
+  PresburgerSet result(nDim, nSym);
+  result.addFlatAffineConstraints(FlatAffineConstraints(nDim, nSym));
+  return result;
+}
+
+// Compute the intersection of the two sets.
+//
+// We directly compute (S_1 or S_2 ...) and (T_1 or T_2 ...)
+// as (S_1 and T_1) or (S_1 and T_2) or ...
+void PresburgerSet::intersectSet(const PresburgerSet &set) {
+  assertDimensionsCompatible(set, *this);
+
+  PresburgerSet result(nDim, nSym);
+  for (const FlatAffineConstraints &cs1 : flatAffineConstraints) {
+    for (const FlatAffineConstraints &cs2 : set.flatAffineConstraints) {
+      FlatAffineConstraints intersection(cs1);
+      intersection.append(cs2);
+      if (!intersection.isEmpty())
+        result.addFlatAffineConstraints(std::move(intersection));
+    }
+  }
+  *this = std::move(result);
+}
+
+namespace {
+SmallVector<int64_t, 8> inequalityFromEquality(ArrayRef<int64_t> eq,
+                                               bool negated) {
+  SmallVector<int64_t, 8> coeffs;
+  for (auto coeff : eq)
+    coeffs.emplace_back(negated ? -coeff : coeff);
+  return coeffs;
+}
+
+SmallVector<int64_t, 8> complementIneq(ArrayRef<int64_t> ineq) {
+  SmallVector<int64_t, 8> coeffs;
+  for (auto coeff : ineq)
+    coeffs.emplace_back(-coeff);
+  --coeffs.back();
+  return coeffs;
+}
+} // anonymous namespace
+
+// Return the set difference b - s and accumulate the result into `result`.
+// `simplex` must correspond to b.
+//
+// In the following, U denotes union, /\ denotes intersection, - denotes set
+// subtraction and ~ denotes complement.
+// Let b be the basic set and s = (U_i s_i) be the set. We want b - (U_i s_i).
+//
+// Let s_i = /\_j s_ij. To compute b - s_i = b /\ ~s_i, we partition s_i based
+// on the first violated constraint:
+// ~s_i = (~s_i1) U (s_i1 /\ ~s_i2) U (s_i1 /\ s_i2 /\ ~s_i3) U ...
+// And the required result is (b /\ ~s_i1) U (b /\ s_i1 /\ ~s_i2) U ...
+// We recurse by subtracting U_{j > i} S_j from each of these parts and
+// returning the union of the results.
+//
+// As a heuristic, we try adding all the constraints and check if simplex
+// says that the intersection is empty. Also, in the process we find out that
+// some constraints are redundant, which we then ignore.
+void subtractRecursively(FlatAffineConstraints &b, Simplex &simplex,
+                         const PresburgerSet &s, unsigned i,
+                         PresburgerSet &result) {
+  if (i == s.getNumFACs()) {
+    result.addFlatAffineConstraints(b);
+    return;
+  }
+  const FlatAffineConstraints &sI = s.getFlatAffineConstraints()[i];
+  auto initialSnap = simplex.getSnapshot();
+  unsigned offset = simplex.numConstraints();
+  simplex.addFlatAffineConstraints(sI);
+
+  if (simplex.isEmpty()) {
+    /// b /\ s_i is empty, so b - s_i = b. We move directly to i + 1.
+    simplex.rollback(initialSnap);
+    subtractRecursively(b, simplex, s, i + 1, result);
+    return;
+  }
+
+  simplex.detectRedundant();
+  SmallVector<bool, 8> isMarkedRedundant;
+  for (unsigned j = 0; j < 2 * sI.getNumEqualities() + sI.getNumInequalities();
+       j++)
+    isMarkedRedundant.push_back(simplex.isMarkedRedundant(offset + j));
+
+  simplex.rollback(initialSnap);
+
+  auto recurseWithInequality = [&, i](ArrayRef<int64_t> ineq) {
+    size_t snap = simplex.getSnapshot();
+    b.addInequality(ineq);
+    simplex.addInequality(ineq);
+    subtractRecursively(b, simplex, s, i + 1, result);
+    b.removeInequality(b.getNumInequalities() - 1);
+    simplex.rollback(snap);
+  };
+
+  auto processInequality = [&](ArrayRef<int64_t> ineq) {
+    recurseWithInequality(complementIneq(ineq));
+    b.addInequality(ineq);
+    simplex.addInequality(ineq);
+  };
+
+  unsigned originalNumIneqs = b.getNumInequalities();
+  unsigned originalNumEqs = b.getNumEqualities();
+
+  for (unsigned j = 0; j < sI.getNumInequalities(); j++) {
+    if (isMarkedRedundant[j])
+      continue;
+    processInequality(sI.getInequality(j));
+  }
+
+  offset = sI.getNumInequalities();
+  for (unsigned j = 0, e = sI.getNumEqualities(); j < e; ++j) {
+    const auto &eq = sI.getEquality(j);
+    // Same as the above loop for inequalities, done once each for the positive
+    // and negative inequalities.
+    if (!isMarkedRedundant[offset + 2 * j])
+      processInequality(inequalityFromEquality(eq, false));
+    if (!isMarkedRedundant[offset + 2 * j + 1])
+      processInequality(inequalityFromEquality(eq, true));
+  }
+
+  for (unsigned i = b.getNumInequalities(); i > originalNumIneqs; --i)
+    b.removeInequality(i - 1);
+
+  for (unsigned i = b.getNumEqualities(); i > originalNumEqs; --i)
+    b.removeEquality(i - 1);
+
+  simplex.rollback(initialSnap);
+}
+
+/// Returns the set difference fac - set.
+PresburgerSet PresburgerSet::subtract(FlatAffineConstraints fac,
+                                      const PresburgerSet &set) {
+  assertDimensionsCompatible(fac, set);
+  if (fac.isEmptyByGCDTest())
+    return PresburgerSet(fac.getNumDimIds(), fac.getNumSymbolIds());
+
+  PresburgerSet result(fac.getNumDimIds(), fac.getNumSymbolIds());
+  Simplex simplex(fac);
+  subtractRecursively(fac, simplex, set, 0, result);
+  return result;
+}
+
+PresburgerSet PresburgerSet::complement(const PresburgerSet &set) {
+  // The complement of S is the universe of all points, minus S.
+  return subtract(FlatAffineConstraints(set.getNumDims(), set.getNumSyms()),
+                  set);
+}
+
+/// Subtracts the set from the current set.
+///
+/// We compute (U_i t_i) - (U_i set_i) as U_i (t_i - U_i set_i).
+void PresburgerSet::subtract(const PresburgerSet &set) {
+  assertDimensionsCompatible(set, *this);
+  PresburgerSet result(nDim, nSym);
+  for (const FlatAffineConstraints &c : flatAffineConstraints)
+    result.unionSet(subtract(c, set));
+  *this = result;
+}
+
+/// Return true if all the sets in the union are known to be integer empty,
+/// false otherwise.
+bool PresburgerSet::isIntegerEmpty() const {
+  assert(nSym == 0 && "findIntegerSample is intended for non-symbolic sets");
+  // The set is empty iff all of the disjuncts are empty.
+  for (const FlatAffineConstraints &fac : flatAffineConstraints) {
+    bool empty = fac.isIntegerEmpty();
+    if (!empty)
+      return false;
+  }
+  return true;
+}
+
+Optional<SmallVector<int64_t, 8>> PresburgerSet::findIntegerSample() {
+  assert(nSym == 0 && "findIntegerSample is intended for non-symbolic sets");
+  // A sample exists iff any of the disjuncts containts a sample.
+  for (FlatAffineConstraints &fac : flatAffineConstraints) {
+    if (Optional<SmallVector<int64_t, 8>> opt = fac.findIntegerSample())
+      return *opt;
+  }
+  return {};
+}
+
+void PresburgerSet::print(raw_ostream &os) const {
+  for (const FlatAffineConstraints &fac : flatAffineConstraints)
+    fac.print(os);
+}
+
+void PresburgerSet::dump() const { print(llvm::errs()); }

mlir/lib/Analysis/Presburger/Simplex.cpp

 /// is reached.
 void Simplex::rollback(unsigned snapshot) {
   while (undoLog.size() > snapshot) {
     undo(undoLog.back());
     undoLog.pop_back();
   }
 }
 
+/// Add all the constraints from the given FlatAffineConstraints.
+void Simplex::addFlatAffineConstraints(const FlatAffineConstraints &fac) {
+  assert(fac.getNumIds() == numVariables() &&
+         "FlatAffineConstraints must have same dimensionality as simplex");
+  for (unsigned i = 0; i < fac.getNumInequalities(); ++i)
+    addInequality(fac.getInequality(i));
+  for (unsigned i = 0; i < fac.getNumEqualities(); ++i)
+    addEquality(fac.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.
     if (maybePivot->row == row)
       return {};

mlir/unittests/Analysis/AffineStructuresTest.cpp

 
 #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);
+    EXPECT_TRUE(fac.containsPoint(*maybeSample));
   }
 }
 
 /// 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) {

mlir/unittests/Analysis/Presburger/CMakeLists.txt

 add_mlir_unittest(MLIRPresburgerTests
   MatrixTest.cpp
   SimplexTest.cpp
+  SetTest.cpp
 )
 
 target_link_libraries(MLIRPresburgerTests
-  PRIVATE MLIRPresburger)
+  PRIVATE MLIRPresburger MLIRAnalysis)

mlir/unittests/Analysis/Presburger/SetTest.cpp

+//===- SimplexTest.cpp - Tests for PresburgerSet---------------------------===//
+//
+// 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/Set.h"
+
+#include <gmock/gmock.h>
+#include <gtest/gtest.h>
+
+namespace mlir {
+
+void testUnionAtPoints(PresburgerSet s, PresburgerSet t,
+                          ArrayRef<SmallVector<int64_t, 4>> points) {
+  PresburgerSet unionSet = s;
+  unionSet.unionSet(t);
+  for (auto &point : points) {
+    bool inS = s.containsPoint(point);
+    bool inT = t.containsPoint(point);
+    bool inUnion = unionSet.containsPoint(point);
+    EXPECT_EQ(inUnion, inS || inT);
+  }
+}
+
+void testIntersectAtPoints(PresburgerSet s, PresburgerSet t,
+                          ArrayRef<SmallVector<int64_t, 4>> points) {
+  PresburgerSet intersection = s;
+  intersection.unionSet(t);
+  for (auto &point : points) {
+    bool inS = s.containsPoint(point);
+    bool inT = t.containsPoint(point);
+    bool inIntersection = intersection.containsPoint(point);
+    EXPECT_EQ(inIntersection, inS && inT);
+  }
+}
+
+void testSubtractAtPoints(PresburgerSet s, PresburgerSet t,
+                          ArrayRef<SmallVector<int64_t, 4>> points) {
+  PresburgerSet diff = s;
+  diff.subtract(t);
+  for (auto &point : points) {
+    bool inS = s.containsPoint(point);
+    bool inT = t.containsPoint(point);
+    bool inDiff = diff.containsPoint(point);
+    if (inT)
+      EXPECT_FALSE(inDiff);
+    else
+      EXPECT_EQ(inDiff, inS);
+  }
+}
+
+/// 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;
+}
+
+FlatAffineConstraints makeFACFromIneq(unsigned dims, ArrayRef<SmallVector<int64_t, 4>> ineqs) {
+  return makeFACFromConstraints(dims, ineqs, {});
+}
+
+PresburgerSet makeSetFromFACs(unsigned dims, ArrayRef<FlatAffineConstraints> facs) {
+  PresburgerSet set(dims);
+  for (const FlatAffineConstraints &fac : facs)
+    set.addFlatAffineConstraints(fac);
+  return set;
+}
+
+TEST(SetTest, containsPoint) {
+  PresburgerSet set1 = makeSetFromFACs(1, {
+      makeFACFromIneq(1, {
+        {1, -2},    // x >= 2.
+        {-1, 8}}),  // x <= 8.
+      makeFACFromIneq(1, {
+        {1, -10},   // x >= 10.
+        {-1, 20}}), // x <= 20.
+    });
+  for (unsigned x = 0; x <= 21; ++x) {
+    if ((2 <= x && x <= 8) || (10 <= x && x <= 20))
+      EXPECT_TRUE(set1.containsPoint({x}));
+    else 
+      EXPECT_FALSE(set1.containsPoint({x}));
+  }
+
+  // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} union
+  // a square with opposite corners (2, 2) and (10, 10).
+  PresburgerSet set2 = makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 1, -2},  // x + y >= 4.
+        {-1, -1, 30},// x + y <= 32.
+        {1, -1, 0},  // x - y >= 2.
+        {-1, 1, 10}, // x - y <= 16.
+    }), makeFACFromIneq(2, {
+        {1, 0, -2},  // x >= 2.
+        {0, 1, -2},  // y >= 2.
+        {-1, 0, 10}, // x <= 10.
+        {0, -1, 10} // y <= 10.
+      })});
+
+  for (unsigned x = 1; x <= 25; ++x) {
+    for (unsigned y = -6; y <= 16; ++y) {
+      if (4 <= x + y && x + y <= 32 &&
+          2 <= x - y && x - y <= 16)
+        EXPECT_TRUE(set2.containsPoint({x, y}));
+      else if (2 <= x && x <= 10 && 2 <= y && y <= 10)
+        EXPECT_TRUE(set2.containsPoint({x, y}));
+      else 
+        EXPECT_FALSE(set2.containsPoint({x, y}));
+    }
+  }  
+}
+
+TEST(SetTest, Union) {
+  PresburgerSet set = makeSetFromFACs(1, {
+      makeFACFromIneq(1, {
+        {1, -2},    // x >= 2.
+        {-1, 8}}),  // x <= 8.
+      makeFACFromIneq(1, {
+        {1, -10},   // x >= 10.
+        {-1, 20}}), // x <= 20.
+    });
+
+  // Universe union set.
+  testUnionAtPoints(PresburgerSet::makeUniverse(1), set,
+                    {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // Null union set.
+  testUnionAtPoints(PresburgerSet(1), set,
+                    {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // Null union Universe.
+  testUnionAtPoints(
+    PresburgerSet(1),
+    PresburgerSet::makeUniverse(1),
+    {{1}, {2}, {0}, {-1}});
+
+  // Universe union Null.
+  testUnionAtPoints(
+    PresburgerSet::makeUniverse(1),
+    PresburgerSet(1),
+    {{1}, {2}, {0}, {-1}});
+
+  // Null union Null.
+  testUnionAtPoints(
+    PresburgerSet(1),
+    PresburgerSet(1),
+    {{1}, {2}, {0}, {-1}});
+}
+
+TEST(SetTest, Intersect) {
+  PresburgerSet set = makeSetFromFACs(1, {
+      makeFACFromIneq(1, {
+        {1, -2},    // x >= 2.
+        {-1, 8}}),  // x <= 8.
+      makeFACFromIneq(1, {
+        {1, -10},   // x >= 10.
+        {-1, 20}}), // x <= 20.
+    });
+
+  // Universe intersection set.
+  testUnionAtPoints(PresburgerSet::makeUniverse(1), set,
+                    {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // Null intersection set.
+  testUnionAtPoints(PresburgerSet(1), set,
+                    {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // Null intersection Universe.
+  testUnionAtPoints(
+    PresburgerSet(1),
+    PresburgerSet::makeUniverse(1),
+    {{1}, {2}, {0}, {-1}});
+
+  // Universe intersection Null.
+  testUnionAtPoints(
+    PresburgerSet::makeUniverse(1),
+    PresburgerSet(1),
+    {{1}, {2}, {0}, {-1}});
+
+  // Universe intersection Universe.
+  testUnionAtPoints(
+    PresburgerSet::makeUniverse(1),
+    PresburgerSet::makeUniverse(1),
+    {{1}, {2}, {0}, {-1}});
+}
+
+
+TEST(SetTest, Subtract) {
+  // The interval [2, 8] minus
+  // the interval [10, 20].
+  testSubtractAtPoints(
+    makeSetFromFACs(1, {
+      makeFACFromIneq(1, {})
+    }),
+    makeSetFromFACs(1, {
+      makeFACFromIneq(1, {
+        {1, -2},    // x >= 2.
+        {-1, 8}}),  // x <= 8.
+      makeFACFromIneq(1, {
+        {1, -10},   // x >= 10.
+        {-1, 20}}), // x <= 20.
+    }),
+    {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // ((-infinity, 0] U [3, 4] U [6, 7]) - ([2, 3] U [5, 6])
+  testSubtractAtPoints(
+      makeSetFromFACs(1, {
+        makeFACFromIneq(1, {
+          {-1, 0}  // x <= 0.
+        }), makeFACFromIneq(1, {
+          {1, -3}, // x >= 3.
+          {-1, 4}  // x <= 4.
+        }), makeFACFromIneq(1, {
+          {1, -6}, // x >= 6.
+          {-1, 7}  // x <= 7.
+        }),
+      }),
+      makeSetFromFACs(1, {
+        makeFACFromIneq(1, {
+          {1, -2}, // x >= 2.
+          {-1, 3}, // x <= 3.
+        }), makeFACFromIneq(1, {
+          {1, -5}, // x >= 5.
+          {-1, 6}  // x <= 6.
+        })
+      }),
+    {{0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}});
+
+  // Expected result is {[x, y] : x > y}, i.e., {[x, y] : x >= y + 1}.
+  testSubtractAtPoints(
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, -1, 0}  // x >= y.
+      })
+    }),
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 1, 0} // x >= -y.
+      })
+    }),
+  {{0, 1}, {1, 1}, {1, 0}, {1, -1}, {0, -1}});
+
+  // A rectangle with corners at (2, 2) and (10, 10), minus
+  // a rectangle with corners at (5, -10) and (7, 100).
+  // This splits the former rectangle into two halves, (2, 2) to (5, 10) and
+  // (7, 2) to (10, 10).
+  testSubtractAtPoints(
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 0, -2},  // x >= 2.
+        {0, 1, -2},  // y >= 2.
+        {-1, 0, 10}, // x <= 10.
+        {0, -1, 10} // y <= 10.
+      })
+    }),
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 0, -5},   // x >= 5.
+        {0, 1, 10},   // y >= -10.
+        {-1, 0, 7},   // x <= 7.
+        {0, -1, 100}, // y <= 100.
+      })
+    }),
+  {{1, 2},  {2, 2},  {4, 2},   {5, 2},  {7, 2},  {8, 2},
+   {11, 2}, {1, 1},  {2, 1},   {4, 1},  {5, 1},  {7, 1},
+   {8, 1},  {11, 1}, {1, 10},  {2, 10}, {4, 10}, {5, 10},
+   {7, 10}, {8, 10}, {11, 10}, {1, 11}, {2, 11}, {4, 11},
+   {5, 11}, {7, 11}, {8, 11},  {11, 11}});
+
+  // A rectangle with corners at (2, 2) and (10, 10), minus
+  // a rectangle with corners at (5, 4) and (7, 8).
+  // This creates a hole in the middle of the former rectangle, and the
+  // resulting set can be represented as a union of four rectangles.
+  testSubtractAtPoints(
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 0, -2},  // x >= 2.
+        {0, 1, -2},  // y >= 2.
+        {-1, 0, 10}, // x <= 10.
+        {0, -1, 10} // y <= 10.
+      })
+    }),
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 0, -5}, // x >= 5.
+        {0, 1, -4}, // y >= 4.
+        {-1, 0, 7}, // x <= 7.
+        {0, -1, 8}, // y <= 8.
+      })
+    }),
+  {{1, 1}, {2, 2}, {10, 10}, {11, 11}, {5, 4}, {7, 4}, {5, 8}, {7, 8}, {4, 4},
+   {8, 4}, {4, 8}, {8, 8}});
+
+  // The second set is a superset of the first one, since on the line x + y = 0,
+  // y <= 1 is equivalent to x >= -1. So the result is empty.
+  testSubtractAtPoints(
+    makeSetFromFACs(2, {
+      makeFACFromConstraints(2, {
+        {1, 0, 0} // x >= 0.
+      }, {
+        {1, 1, 0} // x + y = 0.
+    })}),
+    makeSetFromFACs(2, {
+      makeFACFromConstraints(2, {
+        {0, -1, 1} // y <= 1.
+      }, {
+        {1, 1, 0}  // x + y = 0.
+      })
+    }),
+  {{0, 0}, {1, -1}, {2, -2}, {-1, 1}, {-2, 2}, {1, 1}, {-1, -1}, {-1, 1},
+   {1, -1}});
+
+  // The result should be {0} U {2}.
+  testSubtractAtPoints(
+    makeSetFromFACs(1, {
+      makeFACFromIneq(1, {
+        {1, 0},    // x >= 0.
+        {-1, 2}}), // x <= 2.
+    }),
+    makeSetFromFACs(1, {
+      makeFACFromConstraints(1, {}, {
+        {1, -1}    // x = 1.
+      }),
+    }),
+    {{-1}, {0}, {1}, {2}, {3}});
+
+  // Sets with lots of redundant inequalities to test the redundancy heuristic.
+  // (the heuristic is for the subtrahend, the second set which is the one being
+  // subtracted)
+
+  // A parallelogram with vertices {(3, 1), (10, -6), (24, 8), (17, 15)} minus
+  // a triangle with vertices {(2, 2), (10, 2), (10, 10)}.
+  testSubtractAtPoints(
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 1, -2},  // x + y >= 4.
+        {-1, -1, 30},// x + y <= 32.
+        {1, -1, 0},  // x - y >= 2.
+        {-1, 1, 10}, // x - y <= 16.
+    })}),
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 0, -2},  // x >= 2. [redundant]
+        {0, 1, -2},  // y >= 2.
+        {-1, 0, 10}, // x <= 10.
+        {0, -1, 10}, // y <= 10. [redundant]
+        {1, 1, -2},  // x + y >= 2. [redundant]
+        {-1, -1, 30},// x + y <= 30. [redundant]
+        {1, -1, 0},  // x - y >= 0.
+        {-1, 1, 10}, // x - y <= 10.
+      })
+    }),
+  {{1, 2}, {2, 2}, {3, 2}, {4, 2}, {1, 1}, {2, 1}, {3, 1}, {4, 1}, {2, 0},
+   {3, 0}, {4, 0}, {5, 0}, {10, 2}, {11, 2}, {10, 1}, {10, 10}, {10, 11},
+   {10, 9}, {11, 10}, {10, -6}, {11, -6}, {24, 8}, {24, 7}, {17, 15},
+   {16, 15}});
+
+  testSubtractAtPoints(
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 1, -2},  // x + y >= 4.
+        {-1, -1, 30},// x + y <= 32.
+        {1, -1, 0},  // x - y >= 2.
+        {-1, 1, 10}, // x - y <= 16.
+    })}),
+    makeSetFromFACs(2, {
+      makeFACFromIneq(2, {
+        {1, 0, -2},  // x >= 2. [redundant]
+        {0, 1, -2},  // y >= 2.
+        {-1, 0, 10}, // x <= 10.
+        {0, -1, 10}, // y <= 10. [redundant]
+        {1, 1, -2},  // x + y >= 2. [redundant]
+        {-1, -1, 30},// x + y <= 30. [redundant]
+        {1, -1, 0},  // x - y >= 0.
+        {-1, 1, 10}, // x - y <= 10.
+      })
+    }),
+  {{1, 2}, {2, 2}, {3, 2}, {4, 2}, {1, 1}, {2, 1}, {3, 1}, {4, 1}, {2, 0},
+   {3, 0}, {4, 0}, {5, 0}, {10, 2}, {11, 2}, {10, 1}, {10, 10}, {10, 11},
+   {10, 9}, {11, 10}, {10, -6}, {11, -6}, {24, 8}, {24, 7}, {17, 15},
+   {16, 15}});
+
+  // ((-infinity, -5] U [3, 3] U [4, 4] U [5, 5]) - ([-2, -10] U [3, 4] U [6, 7])
+  testSubtractAtPoints(
+      makeSetFromFACs(1, {
+        makeFACFromIneq(1, {
+          {-1, -5}, // x <= -5.
+        }), makeFACFromConstraints(1, {}, {
+          {1, -3}  // x = 3.
+        }), makeFACFromConstraints(1, {}, {
+          {1, -4}  // x = 4.
+        }), makeFACFromConstraints(1, {}, {
+          {1, -5}  // x = 5.
+        }),
+      }),
+      makeSetFromFACs(1, {
+        makeFACFromIneq(1, {
+          {-1, -2},  // x <= -2.
+          {1, -10},  // x >= -10.
+          {-1, 0},   // x <= 0. [redundant]
+          {-1, 10},  // x <= 10. [redundant]
+          {1, -100}, // x >= -100. [redundant]
+          {1, -50}   // x >= -50. [redundant]
+        }), makeFACFromIneq(1, {
+          {1, -3}, // x >= 3.
+          {-1, 4}, // x <= 4.
+          {1, 1},  // x >= -1. [redundant]
+          {1, 7},  // x >= -7. [redundant]
+          {-1, 10} // x <= 10. [redundant]
+        }), makeFACFromIneq(1, {
+          {1, -6}, // x >= 6.
+          {-1, 7}, // x <= 7.
+          {1, 1},  // x >= -1. [redundant]
+          {1, -3}, // x >= -3. [redundant]
+          {-1, 5}  // x <= 5. [redundant]
+        }),
+      }),
+    {{-6}, {-5}, {-4}, {-9}, {-10}, {-11}, {0}, {1}, {2}, {3}, {4}, {5}, {6},
+     {7}, {8}});  
+}
+
+} // namespace mlir