MLIR  17.0.0git
PresburgerRelation.h
Go to the documentation of this file.
1 //===- PresburgerRelation.h - MLIR PresburgerRelation Class -----*- C++ -*-===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // A class to represent unions of IntegerRelations.
10 //
11 //===----------------------------------------------------------------------===//
12 
13 #ifndef MLIR_ANALYSIS_PRESBURGER_PRESBURGERRELATION_H
14 #define MLIR_ANALYSIS_PRESBURGER_PRESBURGERRELATION_H
15 
17 #include <optional>
18 
19 namespace mlir {
20 namespace presburger {
21 
22 /// The SetCoalescer class contains all functionality concerning the coalesce
23 /// heuristic. It is built from a `PresburgerRelation` and has the `coalesce()`
24 /// function as its main API.
25 class SetCoalescer;
26 
27 /// A PresburgerRelation represents a union of IntegerRelations that live in
28 /// the same PresburgerSpace with support for union, intersection, subtraction,
29 /// and complement operations, as well as sampling.
30 ///
31 /// The IntegerRelations (disjuncts) are stored in a vector, and the set
32 /// represents the union of these relations. An empty list corresponds to
33 /// the empty set.
34 ///
35 /// Note that there are no invariants guaranteed on the list of disjuncts
36 /// other than that they are all in the same PresburgerSpace. For example, the
37 /// relations may overlap with each other.
39 public:
40  /// Return a universe set of the specified type that contains all points.
42 
43  /// Return an empty set of the specified type that contains no points.
45 
46  explicit PresburgerRelation(const IntegerRelation &disjunct);
47 
48  unsigned getNumDomainVars() const { return space.getNumDomainVars(); }
49  unsigned getNumRangeVars() const { return space.getNumRangeVars(); }
50  unsigned getNumSymbolVars() const { return space.getNumSymbolVars(); }
51  unsigned getNumLocalVars() const { return space.getNumLocalVars(); }
52  unsigned getNumVars() const { return space.getNumVars(); }
53 
54  /// Return the number of disjuncts in the union.
55  unsigned getNumDisjuncts() const;
56 
57  const PresburgerSpace &getSpace() const { return space; }
58 
59  /// Set the space to `oSpace`. `oSpace` should not contain any local ids.
60  /// `oSpace` need not have the same number of ids as the current space;
61  /// it could have more or less. If it has less, the extra ids become
62  /// locals of the disjuncts. It can also have more, in which case the
63  /// disjuncts will have fewer locals. If its total number of ids
64  /// exceeds that of some disjunct, an assert failure will occur.
65  void setSpace(const PresburgerSpace &oSpace);
66 
67  /// Return a reference to the list of disjuncts.
69 
70  /// Return the disjunct at the specified index.
71  const IntegerRelation &getDisjunct(unsigned index) const;
72 
73  /// Mutate this set, turning it into the union of this set and the given
74  /// disjunct.
75  void unionInPlace(const IntegerRelation &disjunct);
76 
77  /// Mutate this set, turning it into the union of this set and the given set.
78  void unionInPlace(const PresburgerRelation &set);
79 
80  /// Return the union of this set and the given set.
82 
83  /// Return the intersection of this set and the given set.
85 
86  /// Return true if the set contains the given point, and false otherwise.
87  bool containsPoint(ArrayRef<MPInt> point) const;
88  bool containsPoint(ArrayRef<int64_t> point) const {
89  return containsPoint(getMPIntVec(point));
90  }
91 
92  /// Return the complement of this set. All local variables in the set must
93  /// correspond to floor divisions.
95 
96  /// Return the set difference of this set and the given set, i.e.,
97  /// return `this \ set`. All local variables in `set` must correspond
98  /// to floor divisions, but local variables in `this` need not correspond to
99  /// divisions.
101 
102  /// Return true if this set is a subset of the given set, and false otherwise.
103  bool isSubsetOf(const PresburgerRelation &set) const;
104 
105  /// Return true if this set is equal to the given set, and false otherwise.
106  /// All local variables in both sets must correspond to floor divisions.
107  bool isEqual(const PresburgerRelation &set) const;
108 
109  /// Return true if all the sets in the union are known to be integer empty
110  /// false otherwise.
111  bool isIntegerEmpty() const;
112 
113  /// Find an integer sample from the given set. This should not be called if
114  /// any of the disjuncts in the union are unbounded.
116 
117  /// Compute an overapproximation of the number of integer points in the
118  /// disjunct. Symbol vars are currently not supported. If the computed
119  /// overapproximation is infinite, an empty optional is returned.
120  ///
121  /// This currently just sums up the overapproximations of the volumes of the
122  /// disjuncts, so the approximation might be far from the true volume in the
123  /// case when there is a lot of overlap between disjuncts.
124  std::optional<MPInt> computeVolume() const;
125 
126  /// Simplifies the representation of a PresburgerRelation.
127  ///
128  /// In particular, removes all disjuncts which are subsets of other
129  /// disjuncts in the union.
131 
132  /// Check whether all local ids in all disjuncts have a div representation.
133  bool hasOnlyDivLocals() const;
134 
135  /// Compute an equivalent representation of the same relation, such that all
136  /// local ids in all disjuncts have division representations. This
137  /// representation may involve local ids that correspond to divisions, and may
138  /// also be a union of convex disjuncts.
140 
141  /// Print the set's internal state.
142  void print(raw_ostream &os) const;
143  void dump() const;
144 
145 protected:
146  /// Construct an empty PresburgerRelation with the specified number of
147  /// dimension and symbols.
149  assert(space.getNumLocalVars() == 0 &&
150  "PresburgerRelation cannot have local vars.");
151  }
152 
154 
155  /// The list of disjuncts that this set is the union of.
157 
158  friend class SetCoalescer;
159 };
160 
162 public:
163  /// Return a universe set of the specified type that contains all points.
165 
166  /// Return an empty set of the specified type that contains no points.
168 
169  /// Create a set from a relation.
170  explicit PresburgerSet(const IntegerPolyhedron &disjunct);
171  explicit PresburgerSet(const PresburgerRelation &set);
172 
173  /// These operations are the same as the ones in PresburgeRelation, they just
174  /// forward the arguement and return the result as a set instead of a
175  /// relation.
176  PresburgerSet unionSet(const PresburgerRelation &set) const;
177  PresburgerSet intersect(const PresburgerRelation &set) const;
178  PresburgerSet complement() const;
179  PresburgerSet subtract(const PresburgerRelation &set) const;
180  PresburgerSet coalesce() const;
181 
182 protected:
183  /// Construct an empty PresburgerRelation with the specified number of
184  /// dimension and symbols.
187  assert(space.getNumDomainVars() == 0 &&
188  "Set type cannot have domain vars.");
189  assert(space.getNumLocalVars() == 0 &&
190  "PresburgerRelation cannot have local vars.");
191  }
192 };
193 
194 } // namespace presburger
195 } // namespace mlir
196 
197 #endif // MLIR_ANALYSIS_PRESBURGER_PRESBURGERRELATION_H
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...
bool containsPoint(ArrayRef< MPInt > point) const
Return true if the set contains the given point, and false otherwise.
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace.
PresburgerRelation(const PresburgerSpace &space)
Construct an empty PresburgerRelation with the specified number of dimension and symbols.
PresburgerRelation intersect(const PresburgerRelation &set) const
Return the intersection of this set and the given set.
bool hasOnlyDivLocals() const
Check whether all local ids in all disjuncts have a div representation.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
PresburgerRelation(const IntegerRelation &disjunct)
PresburgerRelation computeReprWithOnlyDivLocals() const
Compute an equivalent representation of the same relation, such that all local ids in all disjuncts h...
bool isSubsetOf(const PresburgerRelation &set) const
Return true if this set is a subset of the given set, and false otherwise.
bool containsPoint(ArrayRef< int64_t > point) const
bool isIntegerEmpty() const
Return true if all the sets in the union are known to be integer empty false otherwise.
void unionInPlace(const IntegerRelation &disjunct)
Mutate this set, turning it into the union of this set and the given disjunct.
std::optional< MPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the disjunct.
bool isEqual(const PresburgerRelation &set) const
Return true if this set is equal to the given set, and false otherwise.
static PresburgerRelation getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
unsigned getNumDisjuncts() const
Return the number of disjuncts in the union.
PresburgerRelation coalesce() const
Simplifies the representation of a PresburgerRelation.
static PresburgerRelation getUniverse(const PresburgerSpace &space)
Return a universe set of the specified type that contains all points.
const IntegerRelation & getDisjunct(unsigned index) const
Return the disjunct at the specified index.
ArrayRef< IntegerRelation > getAllDisjuncts() const
Return a reference to the list of disjuncts.
SmallVector< IntegerRelation, 2 > disjuncts
The list of disjuncts that this set is the union of.
const PresburgerSpace & getSpace() const
void print(raw_ostream &os) const
Print the set's internal state.
PresburgerRelation unionSet(const PresburgerRelation &set) const
Return the union of this set and the given set.
bool findIntegerSample(SmallVectorImpl< MPInt > &sample)
Find an integer sample from the given set.
PresburgerRelation complement() const
Return the complement of this set.
PresburgerSet intersect(const PresburgerRelation &set) const
PresburgerSet(const IntegerPolyhedron &disjunct)
Create a set from a relation.
PresburgerSet unionSet(const PresburgerRelation &set) const
These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...
PresburgerSet subtract(const PresburgerRelation &set) const
static PresburgerSet getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
PresburgerSet(const PresburgerSpace &space)
Construct an empty PresburgerRelation with the specified number of dimension and symbols.
static PresburgerSet getUniverse(const PresburgerSpace &space)
Return a universe set of the specified type that contains all points.
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
The SetCoalescer class contains all functionality concerning the coalesce heuristic.
SmallVector< MPInt, 8 > getMPIntVec(ArrayRef< int64_t > range)
Check if the pos^th variable can be expressed as a floordiv of an affine function of other variables ...
Definition: Utils.cpp:503
Include the generated interface declarations.