MLIR  16.0.0git
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Friends | List of all members
mlir::presburger::PresburgerRelation Class Reference

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"

+ Inheritance diagram for mlir::presburger::PresburgerRelation:
+ Collaboration diagram for mlir::presburger::PresburgerRelation:

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 PresburgerSpacegetSpace () const
 
void setSpace (const PresburgerSpace &oSpace)
 Set the space to oSpace. More...
 
ArrayRef< IntegerRelationgetAllDisjuncts () const
 Return a reference to the list of disjuncts. More...
 
const IntegerRelationgetDisjunct (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...
 
Optional< MPIntcomputeVolume () 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
 

Detailed Description

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 37 of file PresburgerRelation.h.

Constructor & Destructor Documentation

◆ PresburgerRelation() [1/2]

PresburgerRelation::PresburgerRelation ( const IntegerRelation disjunct)
explicit

Definition at line 19 of file PresburgerRelation.cpp.

References unionInPlace().

Referenced by getEmpty().

◆ PresburgerRelation() [2/2]

mlir::presburger::PresburgerRelation::PresburgerRelation ( const PresburgerSpace space)
inlineexplicitprotected

Construct an empty PresburgerRelation with the specified number of dimension and symbols.

Definition at line 147 of file PresburgerRelation.h.

References mlir::presburger::PresburgerSpace::getNumLocalVars().

Member Function Documentation

◆ coalesce()

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 811 of file PresburgerRelation.cpp.

References mlir::presburger::SetCoalescer::SetCoalescer().

Referenced by mlir::presburger::PresburgerSet::coalesce(), and containsPoint().

◆ complement()

PresburgerRelation PresburgerRelation::complement ( ) const

Return the complement of this set.

All local variables in the set must correspond to floor divisions.

Definition at line 426 of file PresburgerRelation.cpp.

References getSetDifference(), getSpace(), and mlir::presburger::IntegerRelation::getUniverse().

Referenced by mlir::presburger::PresburgerSet::complement(), and containsPoint().

◆ computeReprWithOnlyDivLocals()

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 139 of file PresburgerRelation.cpp.

References disjuncts, getSpace(), hasOnlyDivLocals(), and unionInPlace().

Referenced by containsPoint(), and getSetDifference().

◆ computeVolume()

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 473 of file PresburgerRelation.cpp.

References disjuncts, and getNumSymbolVars().

Referenced by containsPoint().

◆ containsPoint() [1/2]

bool PresburgerRelation::containsPoint ( ArrayRef< MPInt point) const

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 71 of file PresburgerRelation.cpp.

References mlir::presburger::IntegerRelation::containsPointNoLocal(), and disjuncts.

Referenced by containsPoint(), and getSpace().

◆ containsPoint() [2/2]

bool mlir::presburger::PresburgerRelation::containsPoint ( ArrayRef< int64_t >  point) const
inline

◆ dump()

void PresburgerRelation::dump ( ) const

Definition at line 829 of file PresburgerRelation.cpp.

References print().

Referenced by containsPoint().

◆ findIntegerSample()

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 462 of file PresburgerRelation.cpp.

References disjuncts.

Referenced by containsPoint().

◆ getAllDisjuncts()

ArrayRef< IntegerRelation > PresburgerRelation::getAllDisjuncts ( ) const

Return a reference to the list of disjuncts.

Definition at line 35 of file PresburgerRelation.cpp.

References disjuncts.

Referenced by getSpace(), and mlir::presburger::MultiAffineFunction::isEqual().

◆ getDisjunct()

const IntegerRelation & PresburgerRelation::getDisjunct ( unsigned  index) const

Return the disjunct at the specified index.

Definition at line 39 of file PresburgerRelation.cpp.

References disjuncts.

Referenced by getSetDifference(), and getSpace().

◆ getEmpty()

PresburgerRelation PresburgerRelation::getEmpty ( const PresburgerSpace space)
static

Return an empty set of the specified type that contains no points.

Definition at line 84 of file PresburgerRelation.cpp.

References PresburgerRelation().

Referenced by getSetDifference().

◆ getNumDisjuncts()

unsigned PresburgerRelation::getNumDisjuncts ( ) const

Return the number of disjuncts in the union.

Definition at line 31 of file PresburgerRelation.cpp.

References disjuncts.

Referenced by getNumVars(), getSetDifference(), and mlir::presburger::SetCoalescer::SetCoalescer().

◆ getNumDomainVars()

unsigned mlir::presburger::PresburgerRelation::getNumDomainVars ( ) const
inline

◆ getNumLocalVars()

unsigned mlir::presburger::PresburgerRelation::getNumLocalVars ( ) const
inline

◆ getNumRangeVars()

unsigned mlir::presburger::PresburgerRelation::getNumRangeVars ( ) const
inline

◆ getNumSymbolVars()

unsigned mlir::presburger::PresburgerRelation::getNumSymbolVars ( ) const
inline

Definition at line 49 of file PresburgerRelation.h.

References mlir::presburger::PresburgerSpace::getNumSymbolVars().

Referenced by computeVolume().

◆ getNumVars()

unsigned mlir::presburger::PresburgerRelation::getNumVars ( ) const
inline

◆ getSpace()

const PresburgerSpace& mlir::presburger::PresburgerRelation::getSpace ( ) const
inline

◆ getUniverse()

PresburgerRelation PresburgerRelation::getUniverse ( const PresburgerSpace space)
static

Return a universe set of the specified type that contains all points.

Definition at line 78 of file PresburgerRelation.cpp.

References mlir::presburger::IntegerRelation::getUniverse(), and unionInPlace().

◆ hasOnlyDivLocals()

bool PresburgerRelation::hasOnlyDivLocals ( ) const

Check whether all local ids in all disjuncts have a div representation.

Definition at line 815 of file PresburgerRelation.cpp.

References mlir::presburger::IntegerRelation::hasOnlyDivLocals().

Referenced by computeReprWithOnlyDivLocals(), containsPoint(), and getSetDifference().

◆ intersect()

PresburgerRelation PresburgerRelation::intersect ( const PresburgerRelation set) const

◆ isEqual()

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 450 of file PresburgerRelation.cpp.

References mlir::presburger::PresburgerSpace::isCompatible(), isSubsetOf(), and space.

Referenced by containsPoint(), and mlir::presburger::IntegerRelation::isEqual().

◆ isIntegerEmpty()

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 457 of file PresburgerRelation.cpp.

References disjuncts, and mlir::presburger::IntegerRelation::isIntegerEmpty().

Referenced by containsPoint(), mlir::ComputationSliceState::isMaximal(), mlir::ComputationSliceState::isSliceValid(), and isSubsetOf().

◆ 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 445 of file PresburgerRelation.cpp.

References isIntegerEmpty(), and subtract().

Referenced by containsPoint(), isEqual(), and mlir::presburger::IntegerRelation::isSubsetOf().

◆ print()

void PresburgerRelation::print ( raw_ostream &  os) const

Print the set's internal state.

Definition at line 821 of file PresburgerRelation.cpp.

References mlir::presburger::IntegerRelation::print().

Referenced by containsPoint().

◆ setSpace()

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 24 of file PresburgerRelation.cpp.

References disjuncts, mlir::presburger::PresburgerSpace::getNumLocalVars(), and space.

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

◆ subtract()

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 433 of file PresburgerRelation.cpp.

References disjuncts, getSetDifference(), getSpace(), mlir::presburger::PresburgerSpace::isCompatible(), space, and unionInPlace().

Referenced by containsPoint(), isSubsetOf(), mlir::presburger::PresburgerSet::subtract(), and mlir::presburger::IntegerRelation::subtract().

◆ unionInPlace() [1/2]

void PresburgerRelation::unionInPlace ( const IntegerRelation disjunct)

◆ unionInPlace() [2/2]

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 55 of file PresburgerRelation.cpp.

References disjuncts, mlir::presburger::PresburgerSpace::isCompatible(), space, and unionInPlace().

◆ unionSet()

PresburgerRelation PresburgerRelation::unionSet ( const PresburgerRelation set) const

Return the union of this set and the given set.

Definition at line 63 of file PresburgerRelation.cpp.

References mlir::presburger::PresburgerSpace::isCompatible(), space, and unionInPlace().

Referenced by getSpace(), and mlir::presburger::PresburgerSet::unionSet().

Friends And Related Function Documentation

◆ SetCoalescer

friend class SetCoalescer
friend

Definition at line 157 of file PresburgerRelation.h.

Member Data Documentation

◆ disjuncts

SmallVector<IntegerRelation, 2> mlir::presburger::PresburgerRelation::disjuncts
protected

◆ space

PresburgerSpace mlir::presburger::PresburgerRelation::space
protected

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