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

1080

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 ↗

(On Diff #289619)

Same here.

104 ↗

(On Diff #289619)

Same here.

123 ↗

(On Diff #289619)

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

246 ↗

(On Diff #289619)

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 ↗

(On Diff #289619)

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

1080

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

mlir/lib/Analysis/Presburger/Set.cpp

38 ↗

(On Diff #289820)

Missing doc comment.

41–44 ↗

(On Diff #289820)

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

53 ↗

(On Diff #289820)

an -> a

92–93 ↗

(On Diff #289820)

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

103 ↗

(On Diff #289820)

Missing doc comment.

106 ↗

(On Diff #289820)

Avoid auto.

[bondhugula]

mlir/lib/Analysis/Presburger/Set.cpp

88 ↗

(On Diff #289820)

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

88 ↗

(On Diff #289820)

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

28 ↗

(On Diff #290412)

Nit: getAll... ?

33 ↗

(On Diff #290412)

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

51–52 ↗

(On Diff #290412)

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

59 ↗

(On Diff #290412)

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

33 ↗

(On Diff #290412)

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

111 ↗

(On Diff #290984)

reserve space in the vector before populating it in the loop

123 ↗

(On Diff #290984)

same here

129 ↗

(On Diff #290984)

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

132 ↗

(On Diff #290984)

Nit: ^ for intersection, v for union ?

134 ↗

(On Diff #290984)

What is the "basic set" ?

136 ↗

(On Diff #290984)

What is s_ij, a single constraint?

145 ↗

(On Diff #290984)

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

166 ↗

(On Diff #290984)

SmallBitVector?

167 ↗

(On Diff #290984)

Do not recompute the upper bound on each iteration

173 ↗

(On Diff #290984)

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

230–234 ↗

(On Diff #290984)

Why is this even necessary?

238 ↗

(On Diff #290984)

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

256 ↗

(On Diff #290984)

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

230–234 ↗

(On Diff #290984)

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

1076

evaluate an affine expression ?

1092–1096

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

mlir/lib/Analysis/Presburger/Set.cpp

254 ↗

(On Diff #292258)

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.

294 ↗

(On Diff #292258)

const

304–308 ↗

(On Diff #292258)

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

4–8 ↗

(On Diff #292258)

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

16–52 ↗

(On Diff #292258)

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

495–506 ↗

(On Diff #292258)

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

254 ↗

(On Diff #292258)

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

254 ↗

(On Diff #292258)

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

304–308 ↗

(On Diff #292258)

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

4–8 ↗

(On Diff #292258)

Does this work?

495–506 ↗

(On Diff #292258)

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

304–308 ↗

(On Diff #292258)

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

254 ↗

(On Diff #292258)

(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

FlatAffineConstraints(unsigned numDims = 0, unsigned numSymbols = 0,
     numIds = numDims + numSymbols + numLocals;
     ids.reserve(numIds);
     if (idArgs.empty())
       ids.resize(numIds, None);
     else
       ids.append(idArgs.begin(), idArgs.end());
   }
 
+  /// Return a system with no constraints, i.e., one which is satisfied by all
+  /// points.
+  static FlatAffineConstraints getUniverse(unsigned numDims = 0,
+                                           unsigned numSymbols = 0) {
+    return FlatAffineConstraints(numDims, numSymbols);
+  }
+
   /// Create a flat affine constraint system from an AffineValueMap or a list of
   /// these. The constructed system will only include equalities.
   explicit FlatAffineConstraints(const AffineValueMap &avm);
   explicit FlatAffineConstraints(ArrayRef<const AffineValueMap *> avmRef);
 
   /// Creates an affine constraint system from an IntegerSet.
   explicit FlatAffineConstraints(IntegerSet set);
 
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. An empty list corresponds to the empty
+/// set.
+///
+/// Note that there are no invariants guaranteed on the list of FACs other than
+/// that they are all in the same space, i.e., they all have the same number of
+/// dimensions and symbols. For example, the FACs may overlap each other.
+class PresburgerSet {
+public:
+  explicit PresburgerSet(const FlatAffineConstraints &fac);
+
+  /// 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;
+
+  /// Return a reference to the list of FlatAffineConstraints.
+  ArrayRef<FlatAffineConstraints> getAllFlatAffineConstraints() const;
+
+  /// Return the FlatAffineConstraints at the specified index.
+  const FlatAffineConstraints &getFlatAffineConstraints(unsigned index) const;
+
+  /// Mutate this set, turning it into the union of this set and the given
+  /// FlatAffineConstraints.
+  void unionFACInPlace(const FlatAffineConstraints &fac);
+
+  /// Mutate this set, turning it into the union of this set and the given set.
+  void unionSetInPlace(const PresburgerSet &set);
+
+  /// Return the union of this set and the given set.
+  PresburgerSet unionSet(const PresburgerSet &set) const;
+
+  /// Return the intersection of this set and the given set.
+  PresburgerSet intersect(const PresburgerSet &set) const;
+
+  /// Return 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;
+
+  /// Return the complement of this set.
+  PresburgerSet complement() const;
+
+  /// Return the set difference of this set and the given set, i.e.,
+  /// return `this \ set`.
+  PresburgerSet subtract(const PresburgerSet &set) const;
+
+  /// Return a universe set of the specified type that contains all points.
+  static PresburgerSet getUniverse(unsigned nDim = 0, unsigned nSym = 0);
+  /// Return an empty set of the specified type that contains no points.
+  static PresburgerSet getEmptySet(unsigned nDim = 0, unsigned nSym = 0);
+
+  /// Return 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.
+  bool findIntegerSample(SmallVectorImpl<int64_t> &sample);
+
+private:
+  /// Construct an empty PresburgerSet.
+  PresburgerSet(unsigned nDim = 0, unsigned nSym = 0)
+      : nDim(nDim), nSym(nSym) {}
+
+  /// Return the set difference fac \ set.
+  static PresburgerSet getSetDifference(FlatAffineConstraints fac,
+                                        const PresburgerSet &set);
+
+  /// 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, 2> 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 intersectFlatAffineConstraints(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/include/mlir/Analysis/PresburgerSet.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_PRESBURGERSET_H
+#define MLIR_ANALYSIS_PRESBURGERSET_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. An empty list corresponds to the empty
+/// set.
+///
+/// Note that there are no invariants guaranteed on the list of FACs other than that they are all in the same
+/// space, i.e., they all have the same number of dimensions and symbols. For
+/// example, the FACs may overlap each other.
+class PresburgerSet {
+public:
+  explicit PresburgerSet(const FlatAffineConstraints &fac);
+
+  /// 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;
+
+  /// Return a reference to the list of FlatAffineConstraints.
+  ArrayRef<FlatAffineConstraints> getAllFlatAffineConstraints() const;
+
+  /// Return the FlatAffineConstraints at the specified index.
+  const FlatAffineConstraints &getFlatAffineConstraints(unsigned index) const;
+
+  /// Mutate this set, turning it into the union of this set and the given
+  /// FlatAffineConstraints.
+  void unionFACInPlace(const FlatAffineConstraints &fac);
+
+  /// Mutate this set, turning it into the union of this set and the given set.
+  void unionSetInPlace(const PresburgerSet &set);
+
+  /// Return the union of this set and the given set.
+  PresburgerSet unionSet(const PresburgerSet &set) const;
+
+  /// Return the intersection of this set and the given set.
+  PresburgerSet intersect(const PresburgerSet &set) const;
+
+  /// Return 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;
+
+  /// Return the complement of this set.
+  PresburgerSet complement() const;
+
+  /// Return the set difference of this set and the given set, i.e.,
+  /// return `this \ set`.
+  PresburgerSet subtract(const PresburgerSet &set) const;
+
+  /// Return a universe set of the specified type that contains all points.
+  static PresburgerSet getUniverse(unsigned nDim = 0, unsigned nSym = 0);
+  /// Return an empty set of the specified type that contains no points.
+  static PresburgerSet getEmptySet(unsigned nDim = 0, unsigned nSym = 0);
+
+  /// Return 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.
+  bool findIntegerSample(SmallVectorImpl<int64_t> &sample);
+
+private:
+  /// Construct an empty PresburgerSet.
+  PresburgerSet(unsigned nDim = 0, unsigned nSym = 0)
+      : nDim(nDim), nSym(nSym) {}
+
+  /// Return the set difference fac \ set.
+  static PresburgerSet getSetDifference(FlatAffineConstraints fac,
+                                        const PresburgerSet &set);
+
+  /// 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, 2> flatAffineConstraints;
+};
+
+} // namespace mlir
+
+#endif // MLIR_ANALYSIS_PRESBURGERSET_H

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();
 }
 
+/// Helper to evaluate an affine expression at a point.
+/// The expression is a list of coefficients for the dimensions followed by the
+/// constant term.
+static int64_t valueAt(ArrayRef<int64_t> expr, ArrayRef<int64_t> point) {
+  assert(expr.size() == 1 + point.size() &&
+         "Dimensionalities of point and expresion don't match!");
+  int64_t value = expr.back();
+  for (unsigned i = 0; i < point.size(); ++i)
+    value += expr[i] * point[i];
+  return value;
+}
+
+/// 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, e = getNumEqualities(); i < e; ++i) {
+    if (valueAt(getEquality(i), point) != 0)
+      return false;
+  }
+  for (unsigned i = 0, e = getNumInequalities(); i < e; ++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/CMakeLists.txt

 set(LLVM_OPTIONAL_SOURCES
   AffineAnalysis.cpp
   AffineStructures.cpp
   CallGraph.cpp
   Liveness.cpp
   LoopAnalysis.cpp
   NestedMatcher.cpp
+  PresburgerSet.cpp
   SliceAnalysis.cpp
   Utils.cpp
   )
 
 add_mlir_library(MLIRAnalysis
   CallGraph.cpp
   Liveness.cpp
   SliceAnalysis.cpp
 
   ADDITIONAL_HEADER_DIRS
   ${MLIR_MAIN_INCLUDE_DIR}/mlir/Analysis
 
   DEPENDS
   mlir-headers
 
   LINK_LIBS PUBLIC
   MLIRAffineOps
   MLIRCallInterfaces
   MLIRControlFlowInterfaces
   MLIRInferTypeOpInterface
-  MLIRPresburger
   MLIRSCF
   )
 
 add_mlir_library(MLIRLoopAnalysis
   AffineAnalysis.cpp
   AffineStructures.cpp
   LoopAnalysis.cpp
   NestedMatcher.cpp
+  PresburgerSet.cpp
   Utils.cpp
 
   ADDITIONAL_HEADER_DIRS
   ${MLIR_MAIN_INCLUDE_DIR}/mlir/Analysis
 
   DEPENDS
   mlir-headers
 
   LINK_LIBS PUBLIC
   MLIRAffineOps
   MLIRCallInterfaces
   MLIRControlFlowInterfaces
   MLIRInferTypeOpInterface
   MLIRPresburger
   MLIRSCF
   )
   
-add_subdirectory(Presburger)
+add_subdirectory(Presburger)
 No newline at end of file

mlir/lib/Analysis/Presburger/CMakeLists.txt

 add_mlir_library(MLIRPresburger
   Simplex.cpp
   Matrix.cpp
-  )
+  )
 No newline at end of file

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::intersectFlatAffineConstraints(const FlatAffineConstraints &fac) {
+  assert(fac.getNumIds() == numVariables() &&
+         "FlatAffineConstraints must have same dimensionality as simplex");
+  for (unsigned i = 0, e = fac.getNumInequalities(); i < e; ++i)
+    addInequality(fac.getInequality(i));
+  for (unsigned i = 0, e = fac.getNumEqualities(); i < e; ++i)
+    addEquality(fac.getEquality(i));
+}
+
 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/lib/Analysis/PresburgerSet.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"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SmallBitVector.h"
+
+using namespace mlir;
+
+PresburgerSet::PresburgerSet(const FlatAffineConstraints &fac)
+    : nDim(fac.getNumDimIds()), nSym(fac.getNumSymbolIds()) {
+  unionFACInPlace(fac);
+}
+
+unsigned PresburgerSet::getNumFACs() const {
+  return flatAffineConstraints.size();
+}
+
+unsigned PresburgerSet::getNumDims() const { return nDim; }
+
+unsigned PresburgerSet::getNumSyms() const { return nSym; }
+
+ArrayRef<FlatAffineConstraints>
+PresburgerSet::getAllFlatAffineConstraints() const {
+  return flatAffineConstraints;
+}
+
+const FlatAffineConstraints &
+PresburgerSet::getFlatAffineConstraints(unsigned index) const {
+  assert(index < flatAffineConstraints.size() && "index out of bounds!");
+  return flatAffineConstraints[index];
+}
+
+/// Assert that the FlatAffineConstraints and PresburgerSet live in
+/// compatible spaces.
+static void assertDimensionsCompatible(const FlatAffineConstraints &fac,
+                                       const PresburgerSet &set) {
+  assert(fac.getNumDimIds() == set.getNumDims() &&
+         "Number of dimensions of the FlatAffineConstraints and PresburgerSet"
+         "do not match!");
+  assert(fac.getNumSymbolIds() == set.getNumSyms() &&
+         "Number of symbols of the FlatAffineConstraints and PresburgerSet"
+         "do not match!");
+}
+
+/// Assert that the two PresburgerSets live in compatible spaces.
+static void assertDimensionsCompatible(const PresburgerSet &setA,
+                                       const PresburgerSet &setB) {
+  assert(setA.getNumDims() == setB.getNumDims() &&
+         "Number of dimensions of the PresburgerSets do not match!");
+  assert(setA.getNumSyms() == setB.getNumSyms() &&
+         "Number of symbols of the PresburgerSets do not match!");
+}
+
+/// Mutate this set, turning it into the union of this set and the given
+/// FlatAffineConstraints.
+void PresburgerSet::unionFACInPlace(const FlatAffineConstraints &fac) {
+  assertDimensionsCompatible(fac, *this);
+  flatAffineConstraints.push_back(fac);
+}
+
+/// Mutate this set, turning it into the union of this set and the given set.
+///
+/// This is accomplished by simply adding all the FACs of the given set to this
+/// set.
+void PresburgerSet::unionSetInPlace(const PresburgerSet &set) {
+  assertDimensionsCompatible(set, *this);
+  for (const FlatAffineConstraints &fac : set.flatAffineConstraints)
+    unionFACInPlace(fac);
+}
+
+/// Return the union of this set and the given set.
+PresburgerSet PresburgerSet::unionSet(const PresburgerSet &set) const {
+  assertDimensionsCompatible(set, *this);
+  PresburgerSet result = *this;
+  result.unionSetInPlace(set);
+  return result;
+}
+
+/// 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::getUniverse(unsigned nDim, unsigned nSym) {
+  PresburgerSet result(nDim, nSym);
+  result.unionFACInPlace(FlatAffineConstraints::getUniverse(nDim, nSym));
+  return result;
+}
+
+PresburgerSet PresburgerSet::getEmptySet(unsigned nDim, unsigned nSym) {
+  return PresburgerSet(nDim, nSym);
+}
+
+// Return the intersection of this set with the given set.
+//
+// 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 ...
+PresburgerSet PresburgerSet::intersect(const PresburgerSet &set) const {
+  assertDimensionsCompatible(set, *this);
+
+  PresburgerSet result(nDim, nSym);
+  for (const FlatAffineConstraints &csA : flatAffineConstraints) {
+    for (const FlatAffineConstraints &csB : set.flatAffineConstraints) {
+      FlatAffineConstraints intersection(csA);
+      intersection.append(csB);
+      if (!intersection.isEmpty())
+        result.unionFACInPlace(std::move(intersection));
+    }
+  }
+  return result;
+}
+
+/// Return `coeffs` with all the elements negated.
+static SmallVector<int64_t, 8> getNegatedCoeffs(ArrayRef<int64_t> coeffs) {
+  SmallVector<int64_t, 8> negatedCoeffs;
+  negatedCoeffs.reserve(coeffs.size());
+  for (int64_t coeff : coeffs)
+    negatedCoeffs.emplace_back(-coeff);
+  return negatedCoeffs;
+}
+
+/// Return the complement of the given inequality.
+///
+/// The complement of a_1 x_1 + ... + a_n x_ + c >= 0 is
+/// a_1 x_1 + ... + a_n x_ + c < 0, i.e., -a_1 x_1 - ... - a_n x_ - c - 1 >= 0.
+static SmallVector<int64_t, 8> getComplementIneq(ArrayRef<int64_t> ineq) {
+  SmallVector<int64_t, 8> coeffs;
+  coeffs.reserve(ineq.size());
+  for (int64_t coeff : ineq)
+    coeffs.emplace_back(-coeff);
+  --coeffs.back();
+  return coeffs;
+}
+
+/// Return the set difference b \ s and accumulate the result into `result`.
+/// `simplex` must correspond to b.
+///
+/// In the following, V denotes union, ^ denotes intersection, \ denotes set
+/// difference and ~ denotes complement.
+/// Let b be the FlatAffineConstraints and s = (V_i s_i) be the set. We want
+/// b \ (V_i s_i).
+///
+/// Let s_i = ^_j s_ij, where each s_ij is a single inequality. To compute
+/// b \ s_i = b ^ ~s_i, we partition s_i based on the first violated inequality:
+/// ~s_i = (~s_i1) V (s_i1 ^ ~s_i2) V (s_i1 ^ s_i2 ^ ~s_i3) V ...
+/// And the required result is (b ^ ~s_i1) V (b ^ s_i1 ^ ~s_i2) V ...
+/// We recurse by subtracting V_{j > i} S_j from each of these parts and
+/// returning the union of the results. Each equality is handled as a
+/// conjunction of two inequalities.
+///
+/// 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. These redundant constraints are ignored.
+static void subtractRecursively(FlatAffineConstraints &b, Simplex &simplex,
+                                const PresburgerSet &s, unsigned i,
+                                PresburgerSet &result) {
+  if (i == s.getNumFACs()) {
+    result.unionFACInPlace(b);
+    return;
+  }
+  const FlatAffineConstraints &sI = s.getFlatAffineConstraints(i);
+  unsigned initialSnapshot = simplex.getSnapshot();
+  unsigned offset = simplex.numConstraints();
+  simplex.intersectFlatAffineConstraints(sI);
+
+  if (simplex.isEmpty()) {
+    /// b ^ s_i is empty, so b \ s_i = b. We move directly to i + 1.
+    simplex.rollback(initialSnapshot);
+    subtractRecursively(b, simplex, s, i + 1, result);
+    return;
+  }
+
+  simplex.detectRedundant();
+  llvm::SmallBitVector isMarkedRedundant;
+  for (unsigned j = 0; j < 2 * sI.getNumEqualities() + sI.getNumInequalities();
+       j++)
+    isMarkedRedundant.push_back(simplex.isMarkedRedundant(offset + j));
+
+  simplex.rollback(initialSnapshot);
+
+  // Recurse with the part b ^ ~ineq. Note that b is modified throughout
+  // subtractRecursively. At the time this function is called, the current b is
+  // actually equal to b ^ s_i1 ^ s_i2 ^ ... ^ s_ij, and ineq is the next
+  // inequality, s_{i,j+1}. This function recurses into the next level i + 1
+  // with the part b ^ s_i1 ^ s_i2 ^ ... ^ s_ij ^ ~s_{i,j+1}.
+  auto recurseWithInequality = [&, i](ArrayRef<int64_t> ineq) {
+    size_t snapshot = simplex.getSnapshot();
+    b.addInequality(ineq);
+    simplex.addInequality(ineq);
+    subtractRecursively(b, simplex, s, i + 1, result);
+    b.removeInequality(b.getNumInequalities() - 1);
+    simplex.rollback(snapshot);
+  };
+
+  // For each inequality ineq, we first recurse with the part where ineq
+  // is not satisfied, and then add the ineq to b and simplex because
+  // ineq must be satisfied by all later parts.
+  auto processInequality = [&](ArrayRef<int64_t> ineq) {
+    recurseWithInequality(getComplementIneq(ineq));
+    b.addInequality(ineq);
+    simplex.addInequality(ineq);
+  };
+
+  // processInequality appends some additional constraints to b. We want to
+  // rollback b to its initial state before returning, which we will do by
+  // removing all constraints beyond the original number of inequalities
+  // and equalities, so we store these counts first.
+  unsigned originalNumIneqs = b.getNumInequalities();
+  unsigned originalNumEqs = b.getNumEqualities();
+
+  for (unsigned j = 0, e = sI.getNumInequalities(); j < e; j++) {
+    if (isMarkedRedundant[j])
+      continue;
+    processInequality(sI.getInequality(j));
+  }
+
+  offset = sI.getNumInequalities();
+  for (unsigned j = 0, e = sI.getNumEqualities(); j < e; ++j) {
+    const ArrayRef<int64_t> &coeffs = sI.getEquality(j);
+    // Same as the above loop for inequalities, done once each for the positive
+    // and negative inequalities that make up this equality.
+    if (!isMarkedRedundant[offset + 2 * j])
+      processInequality(coeffs);
+    if (!isMarkedRedundant[offset + 2 * j + 1])
+      processInequality(getNegatedCoeffs(coeffs));
+  }
+
+  // Rollback b and simplex to their initial states.
+  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(initialSnapshot);
+}
+
+/// Return the set difference fac \ set.
+///
+/// The FAC here is modified in subtractRecursively, so it cannot be a const
+/// reference even though it is restored to its original state before returning
+/// from that function.
+PresburgerSet PresburgerSet::getSetDifference(FlatAffineConstraints fac,
+                                              const PresburgerSet &set) {
+  assertDimensionsCompatible(fac, set);
+  if (fac.isEmptyByGCDTest())
+    return PresburgerSet::getEmptySet(fac.getNumDimIds(), fac.getNumSymbolIds());
+
+  PresburgerSet result(fac.getNumDimIds(), fac.getNumSymbolIds());
+  Simplex simplex(fac);
+  subtractRecursively(fac, simplex, set, 0, result);
+  return result;
+}
+
+/// Return the complement of this set.
+PresburgerSet PresburgerSet::complement() const {
+  return getSetDifference(
+      FlatAffineConstraints::getUniverse(getNumDims(), getNumSyms()), *this);
+}
+
+/// Return the result of subtract the given set from this set, i.e.,
+/// return `this \ set`.
+PresburgerSet PresburgerSet::subtract(const PresburgerSet &set) const {
+  assertDimensionsCompatible(set, *this);
+  PresburgerSet result(nDim, nSym);
+  /// We compute (V_i t_i) \ (V_i set_i) as V_i (t_i \ V_i set_i).
+  for (const FlatAffineConstraints &fac : flatAffineConstraints)
+    result.unionSetInPlace(getSetDifference(fac, set));
+  return 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 && "isIntegerEmpty is intended for non-symbolic sets");
+  // The set is empty iff all of the disjuncts are empty.
+  for (const FlatAffineConstraints &fac : flatAffineConstraints) {
+    if (!fac.isIntegerEmpty())
+      return false;
+  }
+  return true;
+}
+
+bool PresburgerSet::findIntegerSample(SmallVectorImpl<int64_t> &sample) {
+  assert(nSym == 0 && "findIntegerSample is intended for non-symbolic sets");
+  // A sample exists iff any of the disjuncts contains a sample.
+  for (const FlatAffineConstraints &fac : flatAffineConstraints) {
+    if (Optional<SmallVector<int64_t, 8>> opt = fac.findIntegerSample()) {
+      sample = std::move(*opt);
+      return true;
+    }
+  }
+  return false;
+}
+
+void PresburgerSet::print(raw_ostream &os) const {
+  os << getNumFACs() << " FlatAffineConstraints:\n";
+  for (const FlatAffineConstraints &fac : flatAffineConstraints) {
+    fac.print(os);
+    os << '\n';
+  }
+}
+
+void PresburgerSet::dump() const { print(llvm::errs()); }

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) {
+static 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
+static 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,
+static 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;

mlir/unittests/Analysis/CMakeLists.txt

 add_mlir_unittest(MLIRAnalysisTests
   AffineStructuresTest.cpp
+  PresburgerSetTest.cpp
 )
 
 target_link_libraries(MLIRAnalysisTests
   PRIVATE MLIRLoopAnalysis)
 
 add_subdirectory(Presburger)

mlir/unittests/Analysis/Presburger/CMakeLists.txt

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

mlir/unittests/Analysis/PresburgerSetTest.cpp

+//===- SetTest.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
+//
+//===----------------------------------------------------------------------===//
+//
+// This file contains tests for PresburgerSet. Each test works by computing
+// an operation (union, intersection, subtract, or complement) on two sets
+// and checking, for a set of points, that the resulting set contains the point
+// iff the result is supposed to contain it.
+//
+//===----------------------------------------------------------------------===//
+
+
+#include "mlir/Analysis/Presburger/Set.h"
+
+#include <gmock/gmock.h>
+#include <gtest/gtest.h>
+
+namespace mlir {
+
+/// Compute the union of s and t, and check that each of the given points
+/// belongs to the union iff it belongs to at least one of s and t.
+static void testUnionAtPoints(PresburgerSet s, PresburgerSet t,
+                       ArrayRef<SmallVector<int64_t, 4>> points) {
+  PresburgerSet unionSet = s.unionSet(t);
+  for (const auto &point : points) {
+    bool inS = s.containsPoint(point);
+    bool inT = t.containsPoint(point);
+    bool inUnion = unionSet.containsPoint(point);
+    EXPECT_EQ(inUnion, inS || inT);
+  }
+}
+
+/// Compute the intersection of s and t, and check that each of the given points
+/// belongs to the intersection iff it belongs to at both of s and t.
+static void testIntersectAtPoints(PresburgerSet s, PresburgerSet t,
+                           ArrayRef<SmallVector<int64_t, 4>> points) {
+  PresburgerSet intersection = s.intersect(t);
+  for (const auto &point : points) {
+    bool inS = s.containsPoint(point);
+    bool inT = t.containsPoint(point);
+    bool inIntersection = intersection.containsPoint(point);
+    EXPECT_EQ(inIntersection, inS && inT);
+  }
+}
+
+/// Compute the set difference s \ t, and check that each of the given points
+/// belongs to the difference iff it belongs to s and does not belong to t.
+static void testSubtractAtPoints(PresburgerSet s, PresburgerSet t,
+                          ArrayRef<SmallVector<int64_t, 4>> points) {
+  PresburgerSet diff = s.subtract(t);
+  for (const 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);
+  }
+}
+
+/// Compute the complement of s, and check that each of the given points
+/// belongs to the complement iff it does not belong to s.
+static void testComplementAtPoints(PresburgerSet s,
+                            ArrayRef<SmallVector<int64_t, 4>> points) {
+  PresburgerSet complement = s.complement();
+  complement.complement();
+  for (const auto &point : points) {
+    bool inS = s.containsPoint(point);
+    bool inComplement = complement.containsPoint(point);
+    if (inS)
+      EXPECT_FALSE(inComplement);
+    else
+      EXPECT_TRUE(inComplement);
+  }
+}
+
+/// Construct a FlatAffineConstraints from a set of inequality and
+/// equality constraints.
+static 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;
+}
+
+static FlatAffineConstraints makeFACFromIneq(unsigned dims,
+                                      ArrayRef<SmallVector<int64_t, 4>> ineqs) {
+  return makeFACFromConstraints(dims, ineqs, {});
+}
+
+static PresburgerSet makeSetFromFACs(unsigned dims,
+                              ArrayRef<FlatAffineConstraints> facs) {
+  PresburgerSet set = PresburgerSet::getEmptySet(dims);
+  for (const FlatAffineConstraints &fac : facs)
+    set.unionFACInPlace(fac);
+  return set;
+}
+
+TEST(SetTest, containsPoint) {
+  PresburgerSet setA =
+      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(setA.containsPoint({x}));
+    else
+      EXPECT_FALSE(setA.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 setB =
+      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(setB.containsPoint({x, y}));
+      else if (2 <= x && x <= 10 && 2 <= y && y <= 10)
+        EXPECT_TRUE(setB.containsPoint({x, y}));
+      else
+        EXPECT_FALSE(setB.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::getUniverse(1), set,
+                    {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // empty set union set.
+  testUnionAtPoints(PresburgerSet::getEmptySet(1), set,
+                    {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // empty set union Universe.
+  testUnionAtPoints(PresburgerSet::getEmptySet(1), PresburgerSet::getUniverse(1),
+                    {{1}, {2}, {0}, {-1}});
+
+  // Universe union empty set.
+  testUnionAtPoints(PresburgerSet::getUniverse(1), PresburgerSet::getEmptySet(1),
+                    {{1}, {2}, {0}, {-1}});
+
+  // empty set union empty set.
+  testUnionAtPoints(PresburgerSet::getEmptySet(1), PresburgerSet::getEmptySet(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.
+  testIntersectAtPoints(PresburgerSet::getUniverse(1), set,
+                        {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // empty set intersection set.
+  testIntersectAtPoints(PresburgerSet::getEmptySet(1), set,
+                        {{1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // empty set intersection Universe.
+  testIntersectAtPoints(PresburgerSet::getEmptySet(1), PresburgerSet::getUniverse(1),
+                        {{1}, {2}, {0}, {-1}});
+
+  // Universe intersection empty set.
+  testIntersectAtPoints(PresburgerSet::getUniverse(1), PresburgerSet::getEmptySet(1),
+                        {{1}, {2}, {0}, {-1}});
+
+  // Universe intersection Universe.
+  testIntersectAtPoints(PresburgerSet::getUniverse(1), PresburgerSet::getUniverse(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}});
+}
+
+TEST(SetTest, Complement) {
+  // Complement of universe.
+  testComplementAtPoints(
+      PresburgerSet::getUniverse(1),
+      {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  // Complement of empty set.
+  testComplementAtPoints(
+      PresburgerSet::getEmptySet(1),
+      {{-1}, {-2}, {-8}, {1}, {2}, {8}, {9}, {10}, {20}, {21}});
+
+  testComplementAtPoints(
+      makeSetFromFACs(2, {makeFACFromIneq(2,
+                                          {
+                                              {1, 0, -2},  // x >= 2.
+                                              {0, 1, -2},  // y >= 2.
+                                              {-1, 0, 10}, // x <= 10.
+                                              {0, -1, 10}  // y <= 10.
+                                          })}),
+      {{1, 1},
+       {2, 1},
+       {1, 2},
+       {2, 2},
+       {2, 3},
+       {3, 2},
+       {10, 10},
+       {10, 11},
+       {11, 10},
+       {2, 10},
+       {2, 11},
+       {1, 10}});
+}
+
+} // namespace mlir