MLIR
17.0.0git
|
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace with support for union, intersection, subtraction, and complement operations, as well as sampling. More...
#include "mlir/Analysis/Presburger/PresburgerRelation.h"
Public Member Functions | |
PresburgerRelation (const IntegerRelation &disjunct) | |
unsigned | getNumDomainVars () const |
unsigned | getNumRangeVars () const |
unsigned | getNumSymbolVars () const |
unsigned | getNumLocalVars () const |
unsigned | getNumVars () const |
unsigned | getNumDisjuncts () const |
Return the number of disjuncts in the union. More... | |
const PresburgerSpace & | getSpace () const |
void | setSpace (const PresburgerSpace &oSpace) |
Set the space to oSpace . More... | |
ArrayRef< IntegerRelation > | getAllDisjuncts () const |
Return a reference to the list of disjuncts. More... | |
const IntegerRelation & | getDisjunct (unsigned index) const |
Return the disjunct at the specified index. More... | |
void | unionInPlace (const IntegerRelation &disjunct) |
Mutate this set, turning it into the union of this set and the given disjunct. More... | |
void | unionInPlace (const PresburgerRelation &set) |
Mutate this set, turning it into the union of this set and the given set. More... | |
PresburgerRelation | unionSet (const PresburgerRelation &set) const |
Return the union of this set and the given set. More... | |
PresburgerRelation | intersect (const PresburgerRelation &set) const |
Return the intersection of this set and the given set. More... | |
bool | containsPoint (ArrayRef< MPInt > point) const |
Return true if the set contains the given point, and false otherwise. More... | |
bool | containsPoint (ArrayRef< int64_t > point) const |
PresburgerRelation | complement () const |
Return the complement of this set. More... | |
PresburgerRelation | subtract (const PresburgerRelation &set) const |
Return the set difference of this set and the given set, i.e., return this \ set . More... | |
bool | isSubsetOf (const PresburgerRelation &set) const |
Return true if this set is a subset of the given set, and false otherwise. More... | |
bool | isEqual (const PresburgerRelation &set) const |
Return true if this set is equal to the given set, and false otherwise. More... | |
bool | isIntegerEmpty () const |
Return true if all the sets in the union are known to be integer empty false otherwise. More... | |
bool | findIntegerSample (SmallVectorImpl< MPInt > &sample) |
Find an integer sample from the given set. More... | |
std::optional< MPInt > | computeVolume () const |
Compute an overapproximation of the number of integer points in the disjunct. More... | |
PresburgerRelation | coalesce () const |
Simplifies the representation of a PresburgerRelation. More... | |
bool | hasOnlyDivLocals () const |
Check whether all local ids in all disjuncts have a div representation. More... | |
PresburgerRelation | computeReprWithOnlyDivLocals () const |
Compute an equivalent representation of the same relation, such that all local ids in all disjuncts have division representations. More... | |
void | print (raw_ostream &os) const |
Print the set's internal state. More... | |
void | dump () const |
Static Public Member Functions | |
static PresburgerRelation | getUniverse (const PresburgerSpace &space) |
Return a universe set of the specified type that contains all points. More... | |
static PresburgerRelation | getEmpty (const PresburgerSpace &space) |
Return an empty set of the specified type that contains no points. More... | |
Protected Member Functions | |
PresburgerRelation (const PresburgerSpace &space) | |
Construct an empty PresburgerRelation with the specified number of dimension and symbols. More... | |
Protected Attributes | |
PresburgerSpace | space |
SmallVector< IntegerRelation, 2 > | disjuncts |
The list of disjuncts that this set is the union of. More... | |
Friends | |
class | SetCoalescer |
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace with support for union, intersection, subtraction, and complement operations, as well as sampling.
The IntegerRelations (disjuncts) are stored in a vector, and the set represents the union of these relations. An empty list corresponds to the empty set.
Note that there are no invariants guaranteed on the list of disjuncts other than that they are all in the same PresburgerSpace. For example, the relations may overlap with each other.
Definition at line 38 of file PresburgerRelation.h.
|
explicit |
Definition at line 20 of file PresburgerRelation.cpp.
References unionInPlace().
Referenced by getEmpty().
|
inlineexplicitprotected |
Construct an empty PresburgerRelation with the specified number of dimension and symbols.
Definition at line 148 of file PresburgerRelation.h.
References mlir::presburger::PresburgerSpace::getNumLocalVars(), and space.
PresburgerRelation PresburgerRelation::coalesce | ( | ) | const |
Simplifies the representation of a PresburgerRelation.
In particular, removes all disjuncts which are subsets of other disjuncts in the union.
Definition at line 813 of file PresburgerRelation.cpp.
References SetCoalescer.
Referenced by mlir::presburger::PresburgerSet::coalesce().
PresburgerRelation PresburgerRelation::complement | ( | ) | const |
Return the complement of this set.
All local variables in the set must correspond to floor divisions.
Definition at line 427 of file PresburgerRelation.cpp.
References getSetDifference(), getSpace(), and mlir::presburger::IntegerRelation::getUniverse().
Referenced by mlir::presburger::PresburgerSet::complement().
PresburgerRelation PresburgerRelation::computeReprWithOnlyDivLocals | ( | ) | const |
Compute an equivalent representation of the same relation, such that all local ids in all disjuncts have division representations.
This representation may involve local ids that correspond to divisions, and may also be a union of convex disjuncts.
Definition at line 140 of file PresburgerRelation.cpp.
References disjuncts, getSpace(), hasOnlyDivLocals(), and unionInPlace().
Referenced by getSetDifference().
std::optional< MPInt > PresburgerRelation::computeVolume | ( | ) | const |
Compute an overapproximation of the number of integer points in the disjunct.
Symbol vars are currently not supported. If the computed overapproximation is infinite, an empty optional is returned.
This currently just sums up the overapproximations of the volumes of the disjuncts, so the approximation might be far from the true volume in the case when there is a lot of overlap between disjuncts.
Definition at line 475 of file PresburgerRelation.cpp.
References disjuncts, and getNumSymbolVars().
|
inline |
Definition at line 88 of file PresburgerRelation.h.
References containsPoint(), and mlir::presburger::getMPIntVec().
Return true if the set contains the given point, and false otherwise.
A point is contained in the union iff any of the parts contain the point.
Definition at line 72 of file PresburgerRelation.cpp.
References mlir::presburger::IntegerRelation::containsPointNoLocal(), and disjuncts.
Referenced by containsPoint().
void PresburgerRelation::dump | ( | ) | const |
Definition at line 831 of file PresburgerRelation.cpp.
References print().
bool PresburgerRelation::findIntegerSample | ( | SmallVectorImpl< MPInt > & | sample | ) |
Find an integer sample from the given set.
This should not be called if any of the disjuncts in the union are unbounded.
Definition at line 463 of file PresburgerRelation.cpp.
References disjuncts.
ArrayRef< IntegerRelation > PresburgerRelation::getAllDisjuncts | ( | ) | const |
Return a reference to the list of disjuncts.
Definition at line 36 of file PresburgerRelation.cpp.
References disjuncts.
Referenced by mlir::presburger::MultiAffineFunction::isEqual().
const IntegerRelation & PresburgerRelation::getDisjunct | ( | unsigned | index | ) | const |
Return the disjunct at the specified index.
Definition at line 40 of file PresburgerRelation.cpp.
References disjuncts.
Referenced by getSetDifference().
|
static |
Return an empty set of the specified type that contains no points.
Definition at line 85 of file PresburgerRelation.cpp.
References PresburgerRelation(), and space.
Referenced by getSetDifference().
unsigned PresburgerRelation::getNumDisjuncts | ( | ) | const |
Return the number of disjuncts in the union.
Definition at line 32 of file PresburgerRelation.cpp.
References disjuncts.
Referenced by getSetDifference(), print(), and mlir::presburger::SetCoalescer::SetCoalescer().
|
inline |
Definition at line 48 of file PresburgerRelation.h.
References mlir::presburger::PresburgerSpace::getNumDomainVars(), and space.
|
inline |
Definition at line 51 of file PresburgerRelation.h.
References mlir::presburger::PresburgerSpace::getNumLocalVars(), and space.
|
inline |
Definition at line 49 of file PresburgerRelation.h.
References mlir::presburger::PresburgerSpace::getNumRangeVars(), and space.
|
inline |
Definition at line 50 of file PresburgerRelation.h.
References mlir::presburger::PresburgerSpace::getNumSymbolVars(), and space.
Referenced by computeVolume().
|
inline |
Definition at line 52 of file PresburgerRelation.h.
References mlir::presburger::PresburgerSpace::getNumVars(), and space.
|
inline |
Definition at line 57 of file PresburgerRelation.h.
References space.
Referenced by complement(), computeReprWithOnlyDivLocals(), getSetDifference(), intersect(), mlir::presburger::PWMAFunction::Piece::isConsistent(), isEqual(), subtract(), unionInPlace(), and unionSet().
|
static |
Return a universe set of the specified type that contains all points.
Definition at line 79 of file PresburgerRelation.cpp.
References mlir::presburger::IntegerRelation::getUniverse(), space, and unionInPlace().
bool PresburgerRelation::hasOnlyDivLocals | ( | ) | const |
Check whether all local ids in all disjuncts have a div representation.
Definition at line 817 of file PresburgerRelation.cpp.
References disjuncts, and mlir::presburger::IntegerRelation::hasOnlyDivLocals().
Referenced by computeReprWithOnlyDivLocals(), and getSetDifference().
PresburgerRelation PresburgerRelation::intersect | ( | const PresburgerRelation & | set | ) | const |
Return the intersection of this set and the given set.
Definition at line 97 of file PresburgerRelation.cpp.
References disjuncts, getSpace(), mlir::presburger::IntegerRelation::intersect(), mlir::presburger::PresburgerSpace::isCompatible(), mlir::presburger::IntegerRelation::isEmpty(), space, and unionInPlace().
Referenced by mlir::presburger::PresburgerSet::intersect().
bool PresburgerRelation::isEqual | ( | const PresburgerRelation & | set | ) | const |
Return true if this set is equal to the given set, and false otherwise.
Two sets are equal iff they are subsets of each other.
All local variables in both sets must correspond to floor divisions.
Definition at line 451 of file PresburgerRelation.cpp.
References getSpace(), mlir::presburger::PresburgerSpace::isCompatible(), isSubsetOf(), and space.
Referenced by mlir::presburger::IntegerRelation::isEqual().
bool PresburgerRelation::isIntegerEmpty | ( | ) | const |
Return true if all the sets in the union are known to be integer empty false otherwise.
Return true if all the sets in the union are known to be integer empty, false otherwise.
Definition at line 458 of file PresburgerRelation.cpp.
References disjuncts, and mlir::presburger::IntegerRelation::isIntegerEmpty().
Referenced by mlir::affine::ComputationSliceState::isMaximal(), mlir::affine::ComputationSliceState::isSliceValid(), and isSubsetOf().
bool PresburgerRelation::isSubsetOf | ( | const PresburgerRelation & | set | ) | const |
Return true if this set is a subset of the given set, and false otherwise.
T is a subset of S iff T \ S is empty, since if T \ S contains a point then this is a point that is contained in T but not S, and if T contains a point that is not in S, this also lies in T \ S.
Definition at line 446 of file PresburgerRelation.cpp.
References isIntegerEmpty(), and subtract().
Referenced by isEqual(), and mlir::presburger::IntegerRelation::isSubsetOf().
void PresburgerRelation::print | ( | raw_ostream & | os | ) | const |
Print the set's internal state.
Definition at line 823 of file PresburgerRelation.cpp.
References disjuncts, getNumDisjuncts(), and mlir::presburger::IntegerRelation::print().
Referenced by dump().
void PresburgerRelation::setSpace | ( | const PresburgerSpace & | oSpace | ) |
Set the space to oSpace
.
oSpace
should not contain any local ids. oSpace
need not have the same number of ids as the current space; it could have more or less. If it has less, the extra ids become locals of the disjuncts. It can also have more, in which case the disjuncts will have fewer locals. If its total number of ids exceeds that of some disjunct, an assert failure will occur.
Definition at line 25 of file PresburgerRelation.cpp.
References disjuncts, mlir::presburger::PresburgerSpace::getNumLocalVars(), and space.
Referenced by mlir::presburger::IntegerRelation::computeReprWithOnlyDivLocals().
PresburgerRelation PresburgerRelation::subtract | ( | const PresburgerRelation & | set | ) | const |
Return the set difference of this set and the given set, i.e., return this \ set
.
Return the result of subtract the given set from this set, i.e., return this \ set
.
All local variables in set
must correspond to floor divisions, but local variables in this
need not correspond to divisions.
Definition at line 434 of file PresburgerRelation.cpp.
References disjuncts, getSetDifference(), getSpace(), mlir::presburger::PresburgerSpace::isCompatible(), space, and unionInPlace().
Referenced by isSubsetOf(), mlir::presburger::IntegerRelation::subtract(), and mlir::presburger::PresburgerSet::subtract().
void PresburgerRelation::unionInPlace | ( | const IntegerRelation & | disjunct | ) |
Mutate this set, turning it into the union of this set and the given disjunct.
Mutate this set, turning it into the union of this set and the given IntegerRelation.
Definition at line 47 of file PresburgerRelation.cpp.
References disjuncts, mlir::presburger::IntegerRelation::getSpace(), mlir::presburger::PresburgerSpace::isCompatible(), and space.
Referenced by mlir::presburger::SetCoalescer::coalesce(), computeReprWithOnlyDivLocals(), mlir::presburger::PWMAFunction::getDomain(), mlir::presburger::MultiAffineFunction::getLexSet(), getSetDifference(), getUniverse(), mlir::presburger::PresburgerSet::getUniverse(), intersect(), PresburgerRelation(), subtract(), unionInPlace(), and unionSet().
void PresburgerRelation::unionInPlace | ( | const PresburgerRelation & | set | ) |
Mutate this set, turning it into the union of this set and the given set.
This is accomplished by simply adding all the disjuncts of the given set to this set.
Definition at line 56 of file PresburgerRelation.cpp.
References disjuncts, getSpace(), mlir::presburger::PresburgerSpace::isCompatible(), space, and unionInPlace().
PresburgerRelation PresburgerRelation::unionSet | ( | const PresburgerRelation & | set | ) | const |
Return the union of this set and the given set.
Definition at line 64 of file PresburgerRelation.cpp.
References getSpace(), mlir::presburger::PresburgerSpace::isCompatible(), space, and unionInPlace().
Referenced by mlir::presburger::PresburgerSet::unionSet().
|
friend |
Definition at line 158 of file PresburgerRelation.h.
Referenced by coalesce().
|
protected |
The list of disjuncts that this set is the union of.
Definition at line 156 of file PresburgerRelation.h.
Referenced by computeReprWithOnlyDivLocals(), computeVolume(), containsPoint(), findIntegerSample(), getAllDisjuncts(), getDisjunct(), getNumDisjuncts(), hasOnlyDivLocals(), intersect(), isIntegerEmpty(), print(), mlir::presburger::SetCoalescer::SetCoalescer(), setSpace(), subtract(), and unionInPlace().
|
protected |
Definition at line 153 of file PresburgerRelation.h.
Referenced by getEmpty(), mlir::presburger::PresburgerSet::getEmpty(), getNumDomainVars(), getNumLocalVars(), getNumRangeVars(), getNumSymbolVars(), getNumVars(), getSpace(), getUniverse(), mlir::presburger::PresburgerSet::getUniverse(), intersect(), isEqual(), PresburgerRelation(), mlir::presburger::PresburgerSet::PresburgerSet(), setSpace(), subtract(), unionInPlace(), and unionSet().