mlir::presburger::PresburgerSpace Class Reference

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	setVarSymbolSeperation (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)
	Get the identifier of the specified variable. More...
Identifier	getId (VarKind kind, unsigned pos) const
ArrayRef< Identifier >	getIds (VarKind kind) const
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	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)

Detailed Description

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 159 of file PresburgerSpace.h.

Constructor & Destructor Documentation

PresburgerSpace()

mlir::presburger::PresburgerSpace::PresburgerSpace ( unsigned  numDomain, unsigned  numRange, unsigned  numSymbols, unsigned  numLocals  )

inlineprotected

Definition at line 297 of file PresburgerSpace.h.

Referenced by getRelationSpace(), and getSetSpace().

Member Function Documentation

convertVarKind()

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 157 of file PresburgerSpace.cpp.

References getNumVarKind(), getVarKindOffset(), isUsingIds(), and mlir::presburger::Local.

Referenced by mlir::presburger::PresburgerRelation::convertVarKind(), and getDomainSpace().

disableIds()

void mlir::presburger::PresburgerSpace::disableIds ( )

inline

Disable identifiers being stored in space.

Definition at line 280 of file PresburgerSpace.h.

dump()

void PresburgerSpace::dump

(

)

const

Definition at line 324 of file PresburgerSpace.cpp.

References print().

getDomainSpace()

PresburgerSpace PresburgerSpace::getDomainSpace

(

)

const

Get the domain/range space of this space.

The returned space is a set space.

Definition at line 35 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().

getId() [1/2]

Identifier& mlir::presburger::PresburgerSpace::getId ( VarKind  kind, unsigned  pos  )

inline

Get the identifier of the specified variable.

Definition at line 254 of file PresburgerSpace.h.

Referenced by swapVar().

getId() [2/2]

Identifier mlir::presburger::PresburgerSpace::getId ( VarKind  kind, unsigned  pos  ) const

inline

Definition at line 258 of file PresburgerSpace.h.

getIds()

ArrayRef<Identifier> mlir::presburger::PresburgerSpace::getIds ( VarKind  kind ) const

inline

Definition at line 263 of file PresburgerSpace.h.

getNumDimAndSymbolVars()

unsigned mlir::presburger::PresburgerSpace::getNumDimAndSymbolVars ( ) const

inline

Definition at line 190 of file PresburgerSpace.h.

Referenced by mlir::presburger::IntegerRelation::getNumDimAndSymbolVars(), resetIds(), and setVarSymbolSeperation().

getNumDimVars()

unsigned mlir::presburger::PresburgerSpace::getNumDimVars ( ) const

inline

Definition at line 189 of file PresburgerSpace.h.

Referenced by mlir::presburger::IntegerRelation::getNumDimVars().

getNumDomainVars()

unsigned mlir::presburger::PresburgerSpace::getNumDomainVars ( ) const

inline

Definition at line 183 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(), getRangeSpace(), mlir::presburger::IntegerRelation::getSpaceWithoutLocals(), mlir::presburger::IntegerPolyhedron::IntegerPolyhedron(), isCompatible(), mlir::presburger::PresburgerSet::PresburgerSet(), and print().

getNumLocalVars()

unsigned mlir::presburger::PresburgerSpace::getNumLocalVars ( ) const

inline

Definition at line 187 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().

getNumRangeVars()

unsigned mlir::presburger::PresburgerSpace::getNumRangeVars ( ) const

inline

Definition at line 184 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().

getNumSetDimVars()

unsigned mlir::presburger::PresburgerSpace::getNumSetDimVars ( ) const

inline

Definition at line 185 of file PresburgerSpace.h.

getNumSymbolVars()

unsigned mlir::presburger::PresburgerSpace::getNumSymbolVars ( ) const

inline

Definition at line 186 of file PresburgerSpace.h.

Referenced by mlir::presburger::MultiAffineFunction::getAsRelation(), mlir::presburger::IntegerRelation::getNumSymbolVars(), mlir::presburger::PresburgerRelation::getNumSymbolVars(), mlir::presburger::MultiAffineFunction::getNumSymbolVars(), mlir::presburger::PWMAFunction::getNumSymbolVars(), mlir::presburger::IntegerRelation::getSpaceWithoutLocals(), isCompatible(), and print().

getNumVarKind()

unsigned PresburgerSpace::getNumVarKind

(

VarKind

kind

)

const

Get the number of vars of the specified kind.

Definition at line 55 of file PresburgerSpace.cpp.

Referenced by mlir::presburger::PresburgerRelation::convertVarKind(), and convertVarKind().

getNumVars()

unsigned mlir::presburger::PresburgerSpace::getNumVars ( ) const

inline

Definition at line 193 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().

getRangeSpace()

PresburgerSpace PresburgerSpace::getRangeSpace

(

)

const

Definition at line 43 of file PresburgerSpace.cpp.

References mlir::presburger::Domain, getNumDomainVars(), and removeVarRange().

Referenced by mlir::presburger::MultiAffineFunction::getOutputSpace(), mlir::presburger::PresburgerRelation::getRangeSet(), and mlir::presburger::PresburgerRelation::intersectRange().

getRelationSpace()

static PresburgerSpace mlir::presburger::PresburgerSpace::getRelationSpace ( unsigned  numDomain = 0, unsigned  numRange = 0, unsigned  numSymbols = 0, unsigned  numLocals = 0  )

inlinestatic

Definition at line 161 of file PresburgerSpace.h.

References PresburgerSpace().

Referenced by mlir::presburger::PresburgerRelation::compose(), mlir::presburger::SymbolicLexSimplex::computeSymbolicIntegerLexMin(), mlir::presburger::MultiAffineFunction::getAsRelation(), mlir::presburger::IntegerRelation::getSpaceWithoutLocals(), and mlir::presburger::IntegerRelation::unionBoundingBox().

getSetSpace()

static PresburgerSpace mlir::presburger::PresburgerSpace::getSetSpace ( unsigned  numDims = 0, unsigned  numSymbols = 0, unsigned  numLocals = 0  )

inlinestatic

Definition at line 168 of file PresburgerSpace.h.

References PresburgerSpace().

Referenced by mlir::presburger::IntegerRelation::computeReprWithOnlyDivLocals(), and mlir::presburger::IntegerRelation::findSymbolicIntegerLexMin().

getSpaceWithoutLocals()

PresburgerSpace PresburgerSpace::getSpaceWithoutLocals

(

)

const

Get the space without local variables.

Definition at line 49 of file PresburgerSpace.cpp.

References getNumLocalVars(), mlir::presburger::Local, and removeVarRange().

Referenced by mlir::presburger::MultiAffineFunction::getLexSet().

getVarKindAt()

VarKind PresburgerSpace::getVarKindAt

(

unsigned

pos

)

const

Return the VarKind of the var at the specified position.

Definition at line 98 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::fourierMotzkinEliminate(), and mlir::presburger::IntegerRelation::getVarKindAt().

getVarKindEnd()

unsigned PresburgerSpace::getVarKindEnd

(

VarKind

kind

)

const

Return the index at Which the specified kind of var ends.

Definition at line 79 of file PresburgerSpace.cpp.

Referenced by getVarKindAt().

getVarKindOffset()

unsigned PresburgerSpace::getVarKindOffset

(

VarKind

kind

)

const

Return the index at which the specified kind of var starts.

Definition at line 67 of file PresburgerSpace.cpp.

Referenced by convertVarKind(), and mlir::presburger::IntegerRelation::fourierMotzkinEliminate().

getVarKindOverlap()

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 83 of file PresburgerSpace.cpp.

insertVar()

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 111 of file PresburgerSpace.cpp.

Referenced by mlir::presburger::MultiAffineFunction::mergeDivs(), and mlir::presburger::IntegerRelation::setSpaceExceptLocals().

isAligned() [1/2]

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 252 of file PresburgerSpace.cpp.

References areIdsEqual(), mlir::presburger::Domain, isCompatible(), isUsingIds(), mlir::presburger::Range, and mlir::presburger::Symbol.

isAligned() [2/2]

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 270 of file PresburgerSpace.cpp.

isCompatible()

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 228 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().

isEqual()

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 234 of file PresburgerSpace.cpp.

References getNumLocalVars(), and isCompatible().

Referenced by mlir::presburger::IntegerRelation::append(), mlir::presburger::IntegerRelation::isObviouslyEqual(), and mlir::presburger::IntegerRelation::unionBoundingBox().

isUsingIds()

bool mlir::presburger::PresburgerSpace::isUsingIds ( ) const

inline

Returns if identifiers are being used.

Definition at line 269 of file PresburgerSpace.h.

Referenced by convertVarKind(), isAligned(), print(), and swapVar().

print()

void PresburgerSpace::print

(

llvm::raw_ostream &

os

)

const

Definition at line 296 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().

removeVarRange()

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 133 of file PresburgerSpace.cpp.

Referenced by mlir::presburger::IntegerRelation::computeReprWithOnlyDivLocals(), mlir::presburger::IntegerRelation::fourierMotzkinEliminate(), getDomainSpace(), getRangeSpace(), getSpaceWithoutLocals(), mlir::presburger::MultiAffineFunction::mergeDivs(), mlir::presburger::MultiAffineFunction::removeOutputs(), and mlir::presburger::PWMAFunction::removeOutputs().

resetIds()

void mlir::presburger::PresburgerSpace::resetIds ( )

inline

Reset the stored identifiers in the space.

Enables usingIds if it was false before.

Definition at line 273 of file PresburgerSpace.h.

References getNumDimAndSymbolVars().

setVarSymbolSeperation()

void PresburgerSpace::setVarSymbolSeperation

(

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 287 of file PresburgerSpace.cpp.

References getNumDimAndSymbolVars().

Referenced by mlir::presburger::IntegerRelation::setDimSymbolSeparation().

swapVar()

void PresburgerSpace::swapVar	(	VarKind	kindA,
		VarKind	kindB,
		unsigned	posA,
		unsigned	posB
	)

Swaps the posA^th variable of kindA and posB^th variable of kindB.

Definition at line 207 of file PresburgerSpace.cpp.

References getId(), isUsingIds(), and mlir::presburger::Local.

---

The documentation for this class was generated from the following files:

• include/mlir/Analysis/Presburger/PresburgerSpace.h
• lib/Analysis/Presburger/PresburgerSpace.cpp