MLIR
20.0.0git
|
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables. More...
#include "mlir/Analysis/Presburger/PresburgerSpace.h"
Public Member Functions | |
PresburgerSpace | getDomainSpace () const |
Get the domain/range space of this space. More... | |
PresburgerSpace | getRangeSpace () const |
PresburgerSpace | getSpaceWithoutLocals () const |
Get the space without local variables. More... | |
unsigned | getNumDomainVars () const |
unsigned | getNumRangeVars () const |
unsigned | getNumSetDimVars () const |
unsigned | getNumSymbolVars () const |
unsigned | getNumLocalVars () const |
unsigned | getNumDimVars () const |
unsigned | getNumDimAndSymbolVars () const |
unsigned | getNumVars () const |
unsigned | getNumVarKind (VarKind kind) const |
Get the number of vars of the specified kind. More... | |
unsigned | getVarKindOffset (VarKind kind) const |
Return the index at which the specified kind of var starts. More... | |
unsigned | getVarKindEnd (VarKind kind) const |
Return the index at Which the specified kind of var ends. More... | |
unsigned | getVarKindOverlap (VarKind kind, unsigned varStart, unsigned varLimit) const |
Get the number of elements of the specified kind in the range [varStart, varLimit). More... | |
VarKind | getVarKindAt (unsigned pos) const |
Return the VarKind of the var at the specified position. More... | |
unsigned | insertVar (VarKind kind, unsigned pos, unsigned num=1) |
Insert num variables of the specified kind at position pos . More... | |
void | removeVarRange (VarKind kind, unsigned varStart, unsigned varLimit) |
Removes variables of the specified kind in the column range [varStart, varLimit). More... | |
void | convertVarKind (VarKind srcKind, unsigned srcPos, unsigned num, VarKind dstKind, unsigned dstPos) |
Converts variables of the specified kind in the column range [srcPos, srcPos + num) to variables of the specified kind at position dstPos. More... | |
void | setVarSymbolSeparation (unsigned newSymbolCount) |
Changes the partition between dimensions and symbols. More... | |
void | swapVar (VarKind kindA, VarKind kindB, unsigned posA, unsigned posB) |
Swaps the posA^th variable of kindA and posB^th variable of kindB. More... | |
bool | isCompatible (const PresburgerSpace &other) const |
Returns true if both the spaces are compatible i.e. More... | |
bool | isEqual (const PresburgerSpace &other) const |
Returns true if both the spaces are equal including local variables i.e. More... | |
Identifier | getId (VarKind kind, unsigned pos) const |
Get the identifier of pos^th variable of the specified kind. More... | |
ArrayRef< Identifier > | getIds (VarKind kind) const |
ArrayRef< Identifier > | getIds () const |
void | setId (VarKind kind, unsigned pos, Identifier id) |
Set the identifier of pos^th variable of the specified kind. More... | |
bool | isUsingIds () const |
Returns if identifiers are being used. More... | |
void | resetIds () |
Reset the stored identifiers in the space. More... | |
void | disableIds () |
Disable identifiers being stored in space. More... | |
bool | isAligned (const PresburgerSpace &other) const |
Check if the spaces are compatible, and the non-local variables having same identifiers are in the same positions. More... | |
bool | isAligned (const PresburgerSpace &other, VarKind kind) const |
Same as above but only check the specified VarKind. More... | |
void | mergeAndAlignSymbols (PresburgerSpace &other) |
Merge and align symbol variables of this and other with respect to identifiers. More... | |
void | print (llvm::raw_ostream &os) const |
void | dump () const |
Static Public Member Functions | |
static PresburgerSpace | getRelationSpace (unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0) |
static PresburgerSpace | getSetSpace (unsigned numDims=0, unsigned numSymbols=0, unsigned numLocals=0) |
Protected Member Functions | |
PresburgerSpace (unsigned numDomain, unsigned numRange, unsigned numSymbols, unsigned numLocals) | |
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
Each variable has one of the three types:
Dimension: Ordinary variables over which the space is represented.
Symbol: Symbol variables correspond to fixed but unknown values. Mathematically, a space with symbolic variables is like a family of spaces indexed by the symbolic variables.
Local: Local variables correspond to existentially quantified variables. For example, consider the space: (x, exists q)
where x is a dimension variable and q is a local variable. Let us put the constraints: 1 <= x <= 7, x = 2q
on this space to get the set: (x) : (exists q : q <= x <= 7, x = 2q)
. An assignment to symbolic and dimension variables is valid if there exists some assignment to the local variable q
satisfying these constraints. For this example, the set is equivalent to {2, 4, 6}. Mathematically, existential quantification can be thought of as the result of projection. In this example, q
is existentially quantified. This can be thought of as the result of projecting out q
from the previous example, i.e. we obtained {2, 4, 6} by projecting out the second dimension from {(2, 1), (4, 2), (6, 2)}.
Dimension variables are further divided into Domain and Range variables to support building relations.
Variables are stored in the following order: [Domain, Range, Symbols, Locals]
A space with no distinction between types of dimension variables can be implemented as a space with zero domain. VarKind::SetDim should be used to refer to dimensions in such spaces.
Compatibility of two spaces implies that number of variables of each kind other than Locals are equal. Equality of two spaces implies that number of variables of each kind are equal.
PresburgerSpace optionally also supports attaching an Identifier with each non-local variable in the space. This is disabled by default. resetIds
is used to enable/reset these identifiers. The user can identify each variable in the space as corresponding to some Identifier. Some example use cases are described in the Identifier
documentation above. The type attached to the Identifier can be different for different variables in the space.
Definition at line 161 of file PresburgerSpace.h.
|
inlineprotected |
Definition at line 317 of file PresburgerSpace.h.
Referenced by getRelationSpace(), and getSetSpace().
void PresburgerSpace::convertVarKind | ( | VarKind | srcKind, |
unsigned | srcPos, | ||
unsigned | num, | ||
VarKind | dstKind, | ||
unsigned | dstPos | ||
) |
Converts variables of the specified kind in the column range [srcPos, srcPos + num) to variables of the specified kind at position dstPos.
The ranges are relative to the kind of variable.
srcKind and dstKind must be different.
Definition at line 160 of file PresburgerSpace.cpp.
References getNumVarKind(), getVarKindOffset(), isUsingIds(), and mlir::presburger::Local.
Referenced by mlir::presburger::PresburgerRelation::convertVarKind(), mlir::presburger::IntegerRelation::convertVarKind(), and getDomainSpace().
|
inline |
Disable identifiers being stored in space.
Definition at line 295 of file PresburgerSpace.h.
void PresburgerSpace::dump | ( | ) | const |
Definition at line 357 of file PresburgerSpace.cpp.
References print().
PresburgerSpace PresburgerSpace::getDomainSpace | ( | ) | const |
Get the domain/range space of this space.
The returned space is a set space.
Definition at line 38 of file PresburgerSpace.cpp.
References convertVarKind(), mlir::presburger::Domain, getNumDomainVars(), getNumRangeVars(), mlir::presburger::Range, removeVarRange(), and mlir::presburger::SetDim.
Referenced by mlir::presburger::PresburgerRelation::applyDomain(), mlir::presburger::PresburgerRelation::compose(), mlir::presburger::PresburgerRelation::getDomainSet(), mlir::presburger::MultiAffineFunction::getDomainSpace(), mlir::presburger::PWMAFunction::getDomainSpace(), mlir::presburger::PWMAFunction::getOutputSpace(), and mlir::presburger::PresburgerRelation::intersectDomain().
|
inline |
Get the identifier of pos^th variable of the specified kind.
Definition at line 256 of file PresburgerSpace.h.
Referenced by mlir::FlatLinearValueConstraints::computeAlignedMap(), mlir::presburger::IntegerRelation::mergeAndAlignSymbols(), mergeAndAlignSymbols(), and mlir::presburger::IntegerRelation::mergeAndCompose().
|
inline |
Definition at line 269 of file PresburgerSpace.h.
Referenced by mergeAndAlignSymbols().
|
inline |
Definition at line 263 of file PresburgerSpace.h.
Referenced by mlir::presburger::IntegerRelation::mergeAndAlignSymbols(), and mergeAndAlignSymbols().
|
inline |
Definition at line 192 of file PresburgerSpace.h.
Referenced by mlir::presburger::IntegerRelation::getNumDimAndSymbolVars(), resetIds(), and setVarSymbolSeparation().
|
inline |
Definition at line 191 of file PresburgerSpace.h.
Referenced by mlir::presburger::IntegerRelation::getNumDimVars().
|
inline |
Definition at line 185 of file PresburgerSpace.h.
Referenced by mlir::presburger::MultiAffineFunction::getAsRelation(), getDomainSpace(), mlir::presburger::IntegerRelation::getNumDomainVars(), mlir::presburger::PresburgerRelation::getNumDomainVars(), mlir::presburger::MultiAffineFunction::getNumDomainVars(), mlir::presburger::PWMAFunction::getNumDomainVars(), mlir::presburger::QuasiPolynomial::getNumInputs(), getRangeSpace(), mlir::presburger::IntegerRelation::getSpaceWithoutLocals(), mlir::presburger::IntegerPolyhedron::IntegerPolyhedron(), isCompatible(), mlir::presburger::PresburgerSet::PresburgerSet(), and print().
|
inline |
Definition at line 189 of file PresburgerSpace.h.
Referenced by mlir::presburger::MultiAffineFunction::getAsRelation(), mlir::presburger::MultiAffineFunction::getLexSet(), mlir::presburger::MultiAffineFunction::getNumDivs(), mlir::presburger::IntegerRelation::getNumLocalVars(), mlir::presburger::PresburgerRelation::getNumLocalVars(), getSetDifference(), getSpaceWithoutLocals(), mlir::presburger::PresburgerRelation::isConvexNoLocals(), isEqual(), mlir::presburger::PresburgerRelation::PresburgerRelation(), mlir::presburger::PresburgerSet::PresburgerSet(), print(), mlir::presburger::PWMAFunction::PWMAFunction(), mlir::presburger::PresburgerRelation::setSpace(), and mlir::presburger::IntegerRelation::setSpaceExceptLocals().
|
inline |
Definition at line 186 of file PresburgerSpace.h.
Referenced by getDomainSpace(), mlir::presburger::MultiAffineFunction::getNumOutputs(), mlir::presburger::PWMAFunction::getNumOutputs(), mlir::presburger::IntegerRelation::getNumRangeVars(), mlir::presburger::PresburgerRelation::getNumRangeVars(), mlir::presburger::IntegerRelation::getSpaceWithoutLocals(), isCompatible(), and print().
|
inline |
Definition at line 187 of file PresburgerSpace.h.
|
inline |
Definition at line 188 of file PresburgerSpace.h.
Referenced by mlir::presburger::MultiAffineFunction::getAsRelation(), mlir::presburger::QuasiPolynomial::getNumInputs(), mlir::presburger::IntegerRelation::getNumSymbolVars(), mlir::presburger::PresburgerRelation::getNumSymbolVars(), mlir::presburger::MultiAffineFunction::getNumSymbolVars(), mlir::presburger::PWMAFunction::getNumSymbolVars(), mlir::presburger::IntegerRelation::getSpaceWithoutLocals(), isCompatible(), and print().
unsigned PresburgerSpace::getNumVarKind | ( | VarKind | kind | ) | const |
Get the number of vars of the specified kind.
Definition at line 58 of file PresburgerSpace.cpp.
Referenced by mlir::presburger::PresburgerRelation::convertVarKind(), convertVarKind(), and mergeAndAlignSymbols().
|
inline |
Definition at line 195 of file PresburgerSpace.h.
Referenced by mlir::presburger::IntegerRelation::getEmpty(), mlir::presburger::MultiAffineFunction::getLexSet(), mlir::presburger::IntegerRelation::getNumCols(), mlir::presburger::IntegerRelation::getNumVars(), mlir::presburger::PresburgerRelation::getNumVars(), getVarKindAt(), mlir::presburger::IntegerRelation::IntegerRelation(), mlir::presburger::IntegerRelation::setSpace(), and mlir::presburger::IntegerRelation::setSpaceExceptLocals().
PresburgerSpace PresburgerSpace::getRangeSpace | ( | ) | const |
Definition at line 46 of file PresburgerSpace.cpp.
References mlir::presburger::Domain, getNumDomainVars(), and removeVarRange().
Referenced by mlir::affine::FlatAffineRelation::compose(), mlir::presburger::MultiAffineFunction::getOutputSpace(), mlir::presburger::PresburgerRelation::getRangeSet(), and mlir::presburger::PresburgerRelation::intersectRange().
|
inlinestatic |
Definition at line 163 of file PresburgerSpace.h.
References PresburgerSpace().
Referenced by mlir::presburger::PresburgerRelation::compose(), mlir::presburger::detail::computePolytopeGeneratingFunction(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::MultiAffineFunction::getAsRelation(), mlir::presburger::IntegerRelation::getSpaceWithoutLocals(), and mlir::presburger::IntegerRelation::unionBoundingBox().
|
inlinestatic |
Definition at line 170 of file PresburgerSpace.h.
References PresburgerSpace().
Referenced by mlir::presburger::detail::computeChamberDecomposition(), mlir::presburger::IntegerRelation::computeReprWithOnlyDivLocals(), mlir::presburger::detail::defineHRep(), and mlir::presburger::IntegerRelation::findSymbolicIntegerLexMin().
PresburgerSpace PresburgerSpace::getSpaceWithoutLocals | ( | ) | const |
Get the space without local variables.
Definition at line 52 of file PresburgerSpace.cpp.
References getNumLocalVars(), mlir::presburger::Local, and removeVarRange().
Referenced by mlir::presburger::MultiAffineFunction::getLexSet().
VarKind PresburgerSpace::getVarKindAt | ( | unsigned | pos | ) | const |
Return the VarKind of the var at the specified position.
Definition at line 101 of file PresburgerSpace.cpp.
References mlir::presburger::Domain, getNumVars(), getVarKindEnd(), mlir::presburger::Local, mlir::presburger::Range, and mlir::presburger::Symbol.
Referenced by mlir::presburger::IntegerRelation::getVarKindAt(), and mlir::presburger::IntegerRelation::swapVar().
unsigned PresburgerSpace::getVarKindEnd | ( | VarKind | kind | ) | const |
Return the index at Which the specified kind of var ends.
Definition at line 82 of file PresburgerSpace.cpp.
Referenced by getVarKindAt().
unsigned PresburgerSpace::getVarKindOffset | ( | VarKind | kind | ) | const |
Return the index at which the specified kind of var starts.
Definition at line 70 of file PresburgerSpace.cpp.
Referenced by convertVarKind(), and swapVar().
unsigned PresburgerSpace::getVarKindOverlap | ( | VarKind | kind, |
unsigned | varStart, | ||
unsigned | varLimit | ||
) | const |
Get the number of elements of the specified kind in the range [varStart, varLimit).
Definition at line 86 of file PresburgerSpace.cpp.
unsigned PresburgerSpace::insertVar | ( | VarKind | kind, |
unsigned | pos, | ||
unsigned | num = 1 |
||
) |
Insert num
variables of the specified kind at position pos
.
Positions are relative to the kind of variable. Return the absolute column position (i.e., not relative to the kind of variable) of the first added variable.
If identifiers are being used, the newly added variables have no identifiers.
Definition at line 114 of file PresburgerSpace.cpp.
Referenced by mergeAndAlignSymbols(), mlir::presburger::MultiAffineFunction::mergeDivs(), and mlir::presburger::IntegerRelation::setSpaceExceptLocals().
bool PresburgerSpace::isAligned | ( | const PresburgerSpace & | other | ) | const |
Check if the spaces are compatible, and the non-local variables having same identifiers are in the same positions.
If the space is not using Identifiers, this check is same as isCompatible.
Definition at line 256 of file PresburgerSpace.cpp.
References areIdsEqual(), mlir::presburger::Domain, isCompatible(), isUsingIds(), mlir::presburger::Range, and mlir::presburger::Symbol.
bool PresburgerSpace::isAligned | ( | const PresburgerSpace & | other, |
VarKind | kind | ||
) | const |
Same as above but only check the specified VarKind.
Useful to check if the symbols in two spaces are aligned.
Definition at line 274 of file PresburgerSpace.cpp.
bool PresburgerSpace::isCompatible | ( | const PresburgerSpace & | other | ) | const |
Returns true if both the spaces are compatible i.e.
if both spaces have the same number of variables of each kind (excluding locals).
Definition at line 232 of file PresburgerSpace.cpp.
References getNumDomainVars(), getNumRangeVars(), and getNumSymbolVars().
Referenced by getSetDifference(), mlir::presburger::PresburgerRelation::intersect(), mlir::presburger::PresburgerRelation::intersectDomain(), mlir::presburger::PresburgerRelation::intersectRange(), isAligned(), mlir::presburger::PWMAFunction::Piece::isConsistent(), mlir::presburger::IntegerRelation::isEqual(), mlir::presburger::MultiAffineFunction::isEqual(), mlir::presburger::PresburgerRelation::isEqual(), isEqual(), mlir::presburger::PWMAFunction::isEqual(), mlir::presburger::PresburgerRelation::isObviouslyEqual(), mlir::presburger::IntegerRelation::isSubsetOf(), mlir::presburger::MultiAffineFunction::mergeDivs(), mlir::presburger::mergeLocalVars(), mlir::presburger::MultiAffineFunction::subtract(), mlir::presburger::PresburgerRelation::subtract(), mlir::presburger::PresburgerRelation::unionInPlace(), and mlir::presburger::PresburgerRelation::unionSet().
bool PresburgerSpace::isEqual | ( | const PresburgerSpace & | other | ) | const |
Returns true if both the spaces are equal including local variables i.e.
if both spaces have the same number of variables of each kind (including locals).
Definition at line 238 of file PresburgerSpace.cpp.
References getNumLocalVars(), and isCompatible().
Referenced by mlir::presburger::IntegerRelation::append(), mlir::presburger::IntegerRelation::isObviouslyEqual(), and mlir::presburger::IntegerRelation::unionBoundingBox().
|
inline |
Returns if identifiers are being used.
Definition at line 284 of file PresburgerSpace.h.
Referenced by convertVarKind(), mlir::affine::MemRefAccess::getAccessRelation(), isAligned(), mlir::presburger::IntegerRelation::mergeAndAlignSymbols(), print(), and swapVar().
void PresburgerSpace::mergeAndAlignSymbols | ( | PresburgerSpace & | other | ) |
Merge and align symbol variables of this
and other
with respect to identifiers.
After this operation the symbol variables of both spaces have the same identifiers in the same order.
Definition at line 300 of file PresburgerSpace.cpp.
References getId(), getIds(), getNumVarKind(), insertVar(), setId(), and mlir::presburger::Symbol.
void PresburgerSpace::print | ( | llvm::raw_ostream & | os | ) | const |
Definition at line 329 of file PresburgerSpace.cpp.
References getNumDomainVars(), getNumLocalVars(), getNumRangeVars(), getNumSymbolVars(), and isUsingIds().
Referenced by dump(), mlir::presburger::MultiAffineFunction::print(), mlir::presburger::PWMAFunction::print(), and mlir::presburger::IntegerRelation::printSpace().
void PresburgerSpace::removeVarRange | ( | VarKind | kind, |
unsigned | varStart, | ||
unsigned | varLimit | ||
) |
Removes variables of the specified kind in the column range [varStart, varLimit).
The range is relative to the kind of variable.
Definition at line 136 of file PresburgerSpace.cpp.
Referenced by mlir::presburger::IntegerRelation::computeReprWithOnlyDivLocals(), getDomainSpace(), getRangeSpace(), getSpaceWithoutLocals(), mlir::presburger::MultiAffineFunction::mergeDivs(), mlir::presburger::MultiAffineFunction::removeOutputs(), and mlir::presburger::PWMAFunction::removeOutputs().
|
inline |
Reset the stored identifiers in the space.
Enables usingIds
if it was false
before.
Definition at line 288 of file PresburgerSpace.h.
References getNumDimAndSymbolVars().
Referenced by mlir::presburger::IntegerRelation::resetIds().
|
inline |
Set the identifier of pos^th variable of the specified kind.
Calls resetIds if identifiers are not enabled.
Definition at line 276 of file PresburgerSpace.h.
Referenced by mlir::presburger::IntegerRelation::mergeAndAlignSymbols(), mergeAndAlignSymbols(), mlir::presburger::IntegerRelation::mergeAndCompose(), and swapVar().
void PresburgerSpace::setVarSymbolSeparation | ( | unsigned | newSymbolCount | ) |
Changes the partition between dimensions and symbols.
Depending on the new symbol count, either a chunk of dimensional variables immediately before the split become symbols, or some of the symbols immediately after the split become dimensions.
Definition at line 291 of file PresburgerSpace.cpp.
References getNumDimAndSymbolVars().
Referenced by mlir::presburger::IntegerRelation::setDimSymbolSeparation().
Swaps the posA^th variable of kindA and posB^th variable of kindB.
Definition at line 210 of file PresburgerSpace.cpp.
References getVarKindOffset(), isUsingIds(), mlir::presburger::Local, and setId().
Referenced by mlir::presburger::IntegerRelation::swapVar().