CrocoPat: bddBdd Class Reference

Definition at line 90 of file bddBdd.h.


Public Member Functions
	bddBdd (unsigned pRoot=0)
	Creates BDD with root pRoot.
	bddBdd (const bddBdd &pBdd)
	Creates BDD as a copy of pBdd.
	bddBdd (unsigned pVarId, bool pValue)
	Creates BDD that assign the bit value 'pValue' to the variable 'pVarId'.
	bddBdd (unsigned pVarId, unsigned pBitNr, unsigned pValue)
	Creates BDD that assign bit values of 'pValue' to 'pBitNr' variables beginning at position 'pVarId'.
	bddBdd (unsigned pVarId1, unsigned pVarId2)
	Creates BDD for pVarId1 == pVarId2.
	~bddBdd ()
bddBdd &	operator= (const bddBdd &aBdd)
	Assignment operator.
bool	testVars (unsigned pVarIdFirst, unsigned pVarIdLast)
	Check if there is any BDD node within the given range of var positions.
double	getTupleNr (unsigned pMinVar, unsigned pMaxVar) const
	Returns number of represented tuples.
unsigned	getTuple (unsigned pMinVar, unsigned pMaxVar) const
	Returns the elements pMinVar ... pMaxVar of an arbitrary tuple of the BDD.
unsigned	getNodeNr () const
	Returns number of nodes (Terminal nodes are not counted).
unsigned	getFreeNodeNr () const
	Returns number of free nodes.
unsigned	getMaxNodeNr () const
	Returns maximal number of nodes in BDD package.
map< unsigned, unsigned >	getNodesPerVarId () const
	Computes the number of nodes per variable id.
void	getGraph (multimap< unsigned, bddGraphNode > &pGraph) const
	Creates output graph representation for BDD.
void	print (ostream &pS) const
	Prints BDD as reduced binary decision tree.
bool	setEqual (const bddBdd &pBdd) const
	Check if the sets represented by *this and pBdd are equal.
bool	setContains (const bddBdd &pBdd) const
	Check if pBdd represents a subset of *this.
bool	isEmpty () const
	Check if the represented set is empty.
void	complement ()
	Computes complement.
void	unite (const bddBdd &pBdd)
	Unites with pBdd.
void	intersect (const bddBdd &pBdd)
	Intersects with pBdd.
void	exists (unsigned pVar)
	Existantial quantification of the variable pVar.
void	renameVars (unsigned pFirst, unsigned pLast, int pOffset)
	Rename variable ids of all nodes from pFirst to pLast by adding pOffset to the variable ids.
Static Public Member Functions
static void	init (unsigned pMaxNodeNr, unsigned pUniqueHBitNr, unsigned pBinCBitNr, unsigned pStatCBitNr)
	Initialisation of BDD package.
static void	done ()
	Frees memory used by the static data structures.
static unsigned	getReachNodeNr ()
	Returns overall number of live nodes (Terminal nodes are not counted).
static unsigned	getExtRefNr ()
	Returns number of external (user) references in mExtrefs.
static void	analyseUniqueHash ()
	Prints list lengths in mUniqueHash.
static unsigned	bddBdd_ (unsigned pVarId, bool pValue)
	Creates BDD that assign the value pValue to the variable pVarId.
static unsigned	bddBdd_ (unsigned pVarId, unsigned pBitNr, unsigned pValue)
	Creates BDD that assign bit values of 'pValue' to 'pBitNr' variables beginning at position 'pVarId'.
static unsigned	bddBdd_ (unsigned pVarId1, unsigned pVarId2)
	Creates BDD for pVarId1 == pVarId2.
static bddBdd	mkLessEqual (unsigned pVarId, unsigned pBitNr, unsigned pValue)
	Non-standard named constructor.
static unsigned	mkLessEqual_ (unsigned pVarId, unsigned pBitNr, unsigned pValue)
	Creates BDD for 'x <= pValue' for 'pBitNr' variables of 'x' beginning at position 'pVarId'.
Private Types
enum	{ mComplement = 1, mRenameVars, mExists, mUnite, mIntersect, mSetContains }
	Identifiers of the operations in the cache (mBinCache). More...
Private Member Functions
bool	testVars_ (unsigned pRoot, unsigned pVarIdFirst, unsigned pVarIdLast)
	Check if there is any BDD node between the variables.
void	decRef ()
	Removes mRoot from mExtRefs (if mRoot is no terminal).
void	incRef ()
	Inserts mRoot into mExtRefs (if mRoot is no terminal).
Static Private Member Functions
static unsigned	hash (unsigned p1, unsigned pHashBitNr)
	Hash/cache functions with 1 and 3 arguments.
static unsigned	hash (unsigned p1, unsigned p2, unsigned p3, unsigned pHashBitNr)
static void	normalize (unsigned &p1, unsigned &p2)
	Ensures that p1 <= p2.
static void	mark (unsigned pRoot)
	Marks (mark=1) all nodes of the BDD with the root pRoot.
static void	unMark (unsigned pRoot)
	Unmarks (mark=0) all nodes of the BDD with the root pRoot.
static void	gc ()
	Garbage collection: All dead nodes (i.e.
static unsigned	insert (unsigned pVar, unsigned pLow, unsigned pHigh)
	Returns the mNodes-index of the node with the passed var-, low- and high-values.
static double	getTupleNr_ (unsigned pRoot, unsigned pVar, unsigned pMaxVar)
	Returns number of represented tuples of the BDD with root pRoot.
static unsigned	getTuple_ (unsigned pRoot, unsigned pVar, unsigned pMaxVar)
	Returns the elements pVar ... pMaxVar of an arbitrary tuple of the BDD.
static unsigned	getNodeNr_ (unsigned pRoot)
	Returns number of nodes of the BDD with root pRoot.
static void	getNodesPerVarId_ (unsigned pRoot, map< unsigned, unsigned > &pBddNodesPerVar)
	Computes the number of nodes per variable id.
static void	getGraph_ (unsigned pRoot, multimap< unsigned, bddGraphNode > &pGraph)
	Creates output graph representation for BDD with root pRoot.
static void	print_ (ostream &pS, unsigned pRoot)
	Prints BDD with root pRoot as reduced binary decision tree.
static bool	setContains_ (unsigned pRoot1, unsigned pRoot2)
	Checks if pRoot2 represents a subset of pRoot1.
static unsigned	complement_ (unsigned pRoot)
	Like the equally named non-static functions, except that the static versions do not catch exceptions.
static unsigned	unite_ (unsigned pRoot1, unsigned pRoot2)
static unsigned	intersect_ (unsigned pRoot1, unsigned pRoot2)
static unsigned	exists_ (unsigned pRoot, unsigned pVar)
static unsigned	renameVars_ (unsigned pRoot, unsigned pFirst, unsigned pLast, int pOffset)
	Rename variable ids of all nodes from pFirst to pLast by adding pOffset to the variable ids.
Private Attributes
unsigned	mRoot
	Index (in mNodes) of the Root node of the BDD.
Static Private Attributes
static bddNode *	mNodes
	Node Array.
static unsigned	mMaxNodeNr
	Number of elements of mNodes.
static unsigned	mFree
	Index of the first unused node in mNodes.
static multiset< unsigned >	mExtRefs
	Indices of externally (i.e.
static unsigned *	mUniqueHash
	Hash table of all used nodes.
static unsigned	mUniqueHBitNr
	Number of elements of mUniqueHash == 2^mUniqueHBitNr == 1<<mUniqueHBitNr.
static bddBinEntry *	mBinCache
	Cache for the results of binary operations.
static unsigned	mBinCBitNr
	Number of elements of mBinCache == 2^mBinCBitNr.
static bddStatEntry *	mStatCache
	Cache for the results of getTupleNr().
static unsigned	mStatCBitNr
	Number of elements of mStatCache == 2^mStatCBitNr.
static unsigned	mRenameCnt
	Fresh, unique cache entry operand for the next call of renameVar().

Member Enumeration Documentation

anonymous enum [private]

Identifiers of the operations in the cache (mBinCache).

Enumerator:

mComplement
mRenameVars
mExists
mUnite
mIntersect
mSetContains

Definition at line 95 of file bddBdd.h.

Constructor & Destructor Documentation

bddBdd::bddBdd ( unsigned pRoot = 0 ) [inline]

Creates BDD with root pRoot.

Definition at line 274 of file bddBdd.h.

References incRef(), and mRoot.

Referenced by mkLessEqual().

Here is the call graph for this function:

Here is the caller graph for this function:

bddBdd::bddBdd ( const bddBdd & pBdd ) [inline]

Creates BDD as a copy of pBdd.

Definition at line 281 of file bddBdd.h.

References incRef(), and mRoot.

Here is the call graph for this function:

bddBdd::bddBdd	(	unsigned	pVarId,
		bool	pValue
	)

Creates BDD that assign the bit value 'pValue' to the variable 'pVarId'.

Definition at line 854 of file bddBdd.cpp.

References bddBdd_(), gc(), incRef(), and mRoot.

Here is the call graph for this function:

bddBdd::bddBdd	(	unsigned	pVarId,
		unsigned	pBitNr,
		unsigned	pValue
	)

Creates BDD that assign bit values of 'pValue' to 'pBitNr' variables beginning at position 'pVarId'.

Definition at line 892 of file bddBdd.cpp.

References bddBdd_(), gc(), incRef(), and mRoot.

Here is the call graph for this function:

bddBdd::bddBdd	(	unsigned	pVarId1,
		unsigned	pVarId2
	)

Creates BDD for pVarId1 == pVarId2.

Definition at line 940 of file bddBdd.cpp.

References bddBdd_(), gc(), incRef(), and mRoot.

Here is the call graph for this function:

bddBdd::~bddBdd ( ) [inline]

Definition at line 303 of file bddBdd.h.

References decRef().

Here is the call graph for this function:

Member Function Documentation

unsigned bddBdd::hash	(	unsigned	p1,
		unsigned	pHashBitNr
	)			`[inline, static, private]`

Hash/cache functions with 1 and 3 arguments.

Possible return values: 0..(1<<hashBitNr)-1.

Definition at line 69 of file bddBdd.cpp.

Referenced by complement_(), exists_(), gc(), getTupleNr_(), insert(), intersect_(), renameVars_(), setContains_(), and unite_().

Here is the caller graph for this function:

unsigned bddBdd::hash	(	unsigned	p1,
		unsigned	p2,
		unsigned	p3,
		unsigned	pHashBitNr
	)			`[inline, static, private]`

Definition at line 76 of file bddBdd.cpp.

void bddBdd::normalize	(	unsigned &	p1,
		unsigned &	p2
	)			`[inline, static, private]`

Ensures that p1 <= p2.

Definition at line 58 of file bddBdd.cpp.

Referenced by intersect_(), and unite_().

Here is the caller graph for this function:

void bddBdd::mark ( unsigned pRoot ) [static, private]

Marks (mark=1) all nodes of the BDD with the root pRoot.

Definition at line 108 of file bddBdd.cpp.

References bddNode::mark, and mNodes.

Referenced by gc(), getGraph_(), getNodeNr_(), getNodesPerVarId_(), testVars_(), and unMark().

Here is the caller graph for this function:

void bddBdd::unMark ( unsigned pRoot ) [static, private]

Unmarks (mark=0) all nodes of the BDD with the root pRoot.

Terminal always remain marked.

Definition at line 121 of file bddBdd.cpp.

References bddNode::mark, mark(), and mNodes.

Referenced by getGraph(), getNodeNr(), getNodesPerVarId(), getReachNodeNr(), and testVars().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::gc ( ) [static, private]

Garbage collection: All dead nodes (i.e.

all nodes which are not reachable from a node in mExtRefs) are freed (i.e. inserted into unused-list mFree). Terminal nodes are never freed.

Definition at line 135 of file bddBdd.cpp.

References hash(), bddNode::mark, mark(), mBinCache, mBinCBitNr, mExtRefs, mFree, mMaxNodeNr, mNodes, mStatCache, mStatCBitNr, mUniqueHash, mUniqueHBitNr, and bddNode::next.

Referenced by bddBdd(), complement(), exists(), getFreeNodeNr(), intersect(), mkLessEqual(), renameVars(), and unite().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::insert	(	unsigned	pVar,
		unsigned	pLow,
		unsigned	pHigh
	)			`[static, private]`

Returns the mNodes-index of the node with the passed var-, low- and high-values.

If such node does not exists, it is inserted into mNodes and mUniqueHash. If there are no free nodes left, throws exception.

Definition at line 176 of file bddBdd.cpp.

References hash(), bddNode::high, bddNode::low, mFree, mNodes, mUniqueHash, mUniqueHBitNr, bddNode::next, and bddNode::var.

Referenced by bddBdd_(), complement_(), exists_(), intersect_(), mkLessEqual_(), renameVars_(), and unite_().

Here is the call graph for this function:

Here is the caller graph for this function:

bool bddBdd::testVars_	(	unsigned	pRoot,
		unsigned	pVarIdFirst,
		unsigned	pVarIdLast
	)			`[private]`

Check if there is any BDD node between the variables.

Returns 'true' if any such node is found.

Definition at line 221 of file bddBdd.cpp.

References bddNode::mark, mark(), and mNodes.

Referenced by testVars().

Here is the call graph for this function:

Here is the caller graph for this function:

double bddBdd::getTupleNr_	(	unsigned	pRoot,
		unsigned	pVar,
		unsigned	pMaxVar
	)			`[static, private]`

Returns number of represented tuples of the BDD with root pRoot.

The BDD must not contain nodes with other variable ids. pVar is the first and pMaxVar is the maximum id of a variable.

Definition at line 258 of file bddBdd.cpp.

References hash(), mNodes, mStatCache, mStatCBitNr, bddStatEntry::result, and bddStatEntry::root.

Referenced by getTupleNr().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::getTuple_	(	unsigned	pRoot,
		unsigned	pVar,
		unsigned	pMaxVar
	)			`[static, private]`

Returns the elements pVar ... pMaxVar of an arbitrary tuple of the BDD.

Definition at line 295 of file bddBdd.cpp.

References mNodes.

Referenced by getTuple().

Here is the caller graph for this function:

unsigned bddBdd::getNodeNr_ ( unsigned pRoot ) [static, private]

Returns number of nodes of the BDD with root pRoot.

(Terminal nodes are not counted). Side effect: counted nodes are marked.

Definition at line 333 of file bddBdd.cpp.

References bddNode::mark, mark(), and mNodes.

Referenced by getNodeNr(), and getReachNodeNr().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::getNodesPerVarId_	(	unsigned	pRoot,
		map< unsigned, unsigned > &	pBddNodesPerVar
	)			`[static, private]`

Computes the number of nodes per variable id.

Definition at line 347 of file bddBdd.cpp.

References bddNode::mark, mark(), mNodes, and bddNode::var.

Referenced by getNodesPerVarId().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::getGraph_	(	unsigned	pRoot,
		multimap< unsigned, bddGraphNode > &	pGraph
	)			`[static, private]`

Creates output graph representation for BDD with root pRoot.

Definition at line 366 of file bddBdd.cpp.

References bddNode::high, bddGraphNode::high, bddGraphNode::id, bddNode::low, bddGraphNode::low, bddNode::mark, mark(), mNodes, bddNode::var, and bddGraphNode::var.

Referenced by getGraph().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::print_	(	ostream &	pS,
		unsigned	pRoot
	)			`[static, private]`

Prints BDD with root pRoot as reduced binary decision tree.

Definition at line 388 of file bddBdd.cpp.

References mNodes, and bddNode::var.

Referenced by print().

Here is the caller graph for this function:

bool bddBdd::setContains_	(	unsigned	pRoot1,
		unsigned	pRoot2
	)			`[static, private]`

Checks if pRoot2 represents a subset of pRoot1.

Definition at line 413 of file bddBdd.cpp.

References hash(), mBinCache, mBinCBitNr, mNodes, mSetContains, bddBinEntry::op, bddBinEntry::result, bddBinEntry::root1, and bddBinEntry::root2.

Referenced by setContains().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::complement_ ( unsigned pRoot ) [static, private]

Like the equally named non-static functions, except that the static versions do not catch exceptions.

Definition at line 479 of file bddBdd.cpp.

References hash(), insert(), mBinCache, mBinCBitNr, mComplement, mNodes, bddBinEntry::op, bddBinEntry::result, and bddBinEntry::root1.

Referenced by complement().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::unite_	(	unsigned	pRoot1,
		unsigned	pRoot2
	)			`[static, private]`

Definition at line 512 of file bddBdd.cpp.

References hash(), insert(), mBinCache, mBinCBitNr, mNodes, mUnite, normalize(), bddBinEntry::op, bddBinEntry::result, bddBinEntry::root1, and bddBinEntry::root2.

Referenced by exists_(), and unite().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::intersect_	(	unsigned	pRoot1,
		unsigned	pRoot2
	)			`[static, private]`

Definition at line 576 of file bddBdd.cpp.

References hash(), insert(), mBinCache, mBinCBitNr, mIntersect, mNodes, normalize(), bddBinEntry::op, bddBinEntry::result, bddBinEntry::root1, and bddBinEntry::root2.

Referenced by intersect().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::exists_	(	unsigned	pRoot,
		unsigned	pVar
	)			`[static, private]`

Definition at line 640 of file bddBdd.cpp.

References hash(), insert(), mBinCache, mBinCBitNr, mExists, mNodes, bddBinEntry::op, bddBinEntry::result, bddBinEntry::root1, bddBinEntry::root2, and unite_().

Referenced by exists().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::renameVars_	(	unsigned	pRoot,
		unsigned	pFirst,
		unsigned	pLast,
		int	pOffset
	)			`[static, private]`

Rename variable ids of all nodes from pFirst to pLast by adding pOffset to the variable ids.

Definition at line 682 of file bddBdd.cpp.

References hash(), insert(), mBinCache, mBinCBitNr, mNodes, mRenameCnt, mRenameVars, bddBinEntry::op, bddBinEntry::result, bddBinEntry::root1, and bddBinEntry::root2.

Referenced by renameVars().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::init	(	unsigned	pMaxNodeNr,
		unsigned	pUniqueHBitNr,
		unsigned	pBinCBitNr,
		unsigned	pStatCBitNr
	)			`[static]`

Initialisation of BDD package.

Must be called before any other function of the package is used. Parameters: Values for the m... variables. number of elements of mNodes == pNodes, number of elements of mUniqueHash == 2^pUniqueHBitNr, number of elements of mBinCache == 2^pBinCBitNr. number of elements of mStatCache == 2^pStatCBitNr.

Definition at line 743 of file bddBdd.cpp.

References bddNode::mark, mBinCache, mBinCBitNr, mFree, mMaxNodeNr, mNodes, mStatCache, mStatCBitNr, mUniqueHash, mUniqueHBitNr, and bddNode::var.

Referenced by crocopat().

Here is the caller graph for this function:

void bddBdd::done ( ) [static]

Frees memory used by the static data structures.

To be called after use of the BDD package.

Definition at line 789 of file bddBdd.cpp.

References mBinCache, mNodes, mStatCache, and mUniqueHash.

Referenced by crocopat().

Here is the caller graph for this function:

unsigned bddBdd::getReachNodeNr ( ) [static]

Returns overall number of live nodes (Terminal nodes are not counted).

Definition at line 798 of file bddBdd.cpp.

References getNodeNr_(), mExtRefs, and unMark().

Here is the call graph for this function:

unsigned bddBdd::getExtRefNr ( ) [static]

Returns number of external (user) references in mExtrefs.

Definition at line 822 of file bddBdd.cpp.

References mExtRefs.

void bddBdd::analyseUniqueHash ( ) [static]

Prints list lengths in mUniqueHash.

Definition at line 829 of file bddBdd.cpp.

References mNodes, mUniqueHash, and mUniqueHBitNr.

void bddBdd::decRef ( ) [inline, private]

Removes mRoot from mExtRefs (if mRoot is no terminal).

Definition at line 251 of file bddBdd.h.

References mExtRefs, and mRoot.

Referenced by complement(), exists(), intersect(), operator=(), renameVars(), unite(), and ~bddBdd().

Here is the caller graph for this function:

void bddBdd::incRef ( ) [inline, private]

Inserts mRoot into mExtRefs (if mRoot is no terminal).

Definition at line 263 of file bddBdd.h.

References mExtRefs, and mRoot.

Referenced by bddBdd(), complement(), exists(), intersect(), operator=(), renameVars(), and unite().

Here is the caller graph for this function:

unsigned bddBdd::bddBdd_	(	unsigned	pVarId,
		bool	pValue
	)			`[static]`

Creates BDD that assign the value pValue to the variable pVarId.

Definition at line 878 of file bddBdd.cpp.

References insert().

Referenced by bddBdd().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::bddBdd_	(	unsigned	pVarId,
		unsigned	pBitNr,
		unsigned	pValue
	)			`[static]`

Creates BDD that assign bit values of 'pValue' to 'pBitNr' variables beginning at position 'pVarId'.

Definition at line 917 of file bddBdd.cpp.

References insert().

Here is the call graph for this function:

unsigned bddBdd::bddBdd_	(	unsigned	pVarId1,
		unsigned	pVarId2
	)			`[static]`

Creates BDD for pVarId1 == pVarId2.

Definition at line 964 of file bddBdd.cpp.

References insert().

Here is the call graph for this function:

bddBdd & bddBdd::operator= ( const bddBdd & aBdd )

Assignment operator.

Definition at line 980 of file bddBdd.cpp.

References decRef(), incRef(), and mRoot.

Here is the call graph for this function:

bddBdd bddBdd::mkLessEqual	(	unsigned	pVarId,
		unsigned	pBitNr,
		unsigned	pValue
	)			`[static]`

Non-standard named constructor.

Creates BDD for 'x <= pValue' for 'pBitNr' variables of 'x' beginning at position 'pVarId'.

Definition at line 991 of file bddBdd.cpp.

References bddBdd(), gc(), and mkLessEqual_().

Referenced by bddRelation::mkRange().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::mkLessEqual_	(	unsigned	pVarId,
		unsigned	pBitNr,
		unsigned	pValue
	)			`[static]`

Creates BDD for 'x <= pValue' for 'pBitNr' variables of 'x' beginning at position 'pVarId'.

Definition at line 1020 of file bddBdd.cpp.

References insert().

Referenced by mkLessEqual().

Here is the call graph for this function:

Here is the caller graph for this function:

bool bddBdd::testVars	(	unsigned	pVarIdFirst,
		unsigned	pVarIdLast
	)			`[inline]`

Check if there is any BDD node within the given range of var positions.

Returns 'true' if any such node is found.

Definition at line 325 of file bddBdd.h.

References mRoot, testVars_(), and unMark().

Referenced by bddRelation::getTupleNr(), bddRelation::rename(), and bddRelation::testVars().

Here is the call graph for this function:

Here is the caller graph for this function:

double bddBdd::getTupleNr	(	unsigned	pMinVar,
		unsigned	pMaxVar
	)			const `[inline]`

Returns number of represented tuples.

The BDD must not contain nodes with other variables. pMinVar is the minimum and pMaxVar is the maximum id of a variable.

Definition at line 336 of file bddBdd.h.

References getTupleNr_(), and mRoot.

Referenced by bddRelation::getTupleNr().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::getTuple	(	unsigned	pMinVar,
		unsigned	pMaxVar
	)			const `[inline]`

Returns the elements pMinVar ... pMaxVar of an arbitrary tuple of the BDD.

Definition at line 341 of file bddBdd.h.

References getTuple_(), isEmpty(), and mRoot.

Referenced by bddRelation::getElement(), bddRelation::getTupleOf(), and bddRelation::printRelation().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::getNodeNr ( ) const

Returns number of nodes (Terminal nodes are not counted).

Definition at line 1044 of file bddBdd.cpp.

References getNodeNr_(), mRoot, and unMark().

Referenced by bddRelation::printBddInfo().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::getFreeNodeNr ( ) const

Returns number of free nodes.

Includes garbage collection to get real values.

Definition at line 1053 of file bddBdd.cpp.

References gc(), bddNode::low, mFree, and mNodes.

Referenced by bddRelation::printBddInfo().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned bddBdd::getMaxNodeNr ( ) const [inline]

Returns maximal number of nodes in BDD package.

Definition at line 358 of file bddBdd.h.

References mMaxNodeNr.

Referenced by bddRelation::printBddInfo().

Here is the caller graph for this function:

map<unsigned, unsigned> bddBdd::getNodesPerVarId ( ) const [inline]

Computes the number of nodes per variable id.

Definition at line 363 of file bddBdd.h.

References getNodesPerVarId_(), mRoot, and unMark().

Referenced by bddRelation::printNodesPerVarId().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::getGraph ( multimap< unsigned, bddGraphNode > & pGraph ) const [inline]

Creates output graph representation for BDD.

Definition at line 371 of file bddBdd.h.

References getGraph_(), mRoot, and unMark().

Referenced by bddRelation::printGraph().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::print ( ostream & pS ) const [inline]

Prints BDD as reduced binary decision tree.

Definition at line 377 of file bddBdd.h.

References mRoot, and print_().

Referenced by bddRelation::printBDT().

Here is the call graph for this function:

Here is the caller graph for this function:

bool bddBdd::setEqual ( const bddBdd & pBdd ) const [inline]

Check if the sets represented by *this and pBdd are equal.

Definition at line 385 of file bddBdd.h.

References mRoot.

Referenced by bddRelation::setEqual().

Here is the caller graph for this function:

bool bddBdd::setContains ( const bddBdd & pBdd ) const [inline]

Check if pBdd represents a subset of *this.

Definition at line 390 of file bddBdd.h.

References mRoot, and setContains_().

Referenced by bddRelation::setContains().

Here is the call graph for this function:

Here is the caller graph for this function:

bool bddBdd::isEmpty ( ) const [inline]

Check if the represented set is empty.

Definition at line 395 of file bddBdd.h.

References mRoot.

Referenced by getTuple(), and bddRelation::isEmpty().

Here is the caller graph for this function:

void bddBdd::complement ( )

Computes complement.

If the second try does not work too, the program is aborted.

Definition at line 1072 of file bddBdd.cpp.

References complement_(), decRef(), gc(), incRef(), and mRoot.

Referenced by bddRelation::complement().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::unite ( const bddBdd & pBdd )

Unites with pBdd.

Definition at line 1100 of file bddBdd.cpp.

References decRef(), gc(), incRef(), mRoot, and unite_().

Referenced by bddRelation::unite().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::intersect ( const bddBdd & pBdd )

Intersects with pBdd.

Definition at line 1127 of file bddBdd.cpp.

References decRef(), gc(), incRef(), intersect_(), and mRoot.

Referenced by bddRelation::intersect(), and bddRelation::renameSafe().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::exists ( unsigned pVar )

Existantial quantification of the variable pVar.

Definition at line 1154 of file bddBdd.cpp.

References decRef(), exists_(), gc(), incRef(), and mRoot.

Referenced by bddRelation::exists(), and bddRelation::renameSafe().

Here is the call graph for this function:

Here is the caller graph for this function:

void bddBdd::renameVars	(	unsigned	pFirst,
		unsigned	pLast,
		int	pOffset
	)

Rename variable ids of all nodes from pFirst to pLast by adding pOffset to the variable ids.

Precondition: pLast - pFirst has to be the same for all calls of this method, because the cache entries contain only pFirst and pOffset.

Definition at line 1182 of file bddBdd.cpp.

References decRef(), gc(), incRef(), mRenameCnt, mRoot, and renameVars_().

Referenced by bddRelation::rename().

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

bddNode * bddBdd::mNodes [static, private]

Node Array.

mNodes[0] is the 0-terminal, mNodes[1] is the 1-terminal. Both are always marked (mark == 1) and have the variable id -1.

Definition at line 103 of file bddBdd.h.

Referenced by analyseUniqueHash(), complement_(), done(), exists_(), gc(), getFreeNodeNr(), getGraph_(), getNodeNr_(), getNodesPerVarId_(), getTuple_(), getTupleNr_(), init(), insert(), intersect_(), mark(), print_(), renameVars_(), setContains_(), testVars_(), unite_(), and unMark().

unsigned bddBdd::mMaxNodeNr [static, private]

Number of elements of mNodes.

Definition at line 105 of file bddBdd.h.

Referenced by gc(), getMaxNodeNr(), and init().

unsigned bddBdd::mFree [static, private]

Index of the first unused node in mNodes.

Unused nodes are linked using their low-element.

Definition at line 108 of file bddBdd.h.

Referenced by gc(), getFreeNodeNr(), init(), and insert().

multiset< unsigned > bddBdd::mExtRefs [static, private]

Indices of externally (i.e.

by the package user) reference nodes. Updated by constructors and destructors. Does not contain terminals. Used in garbage collections to recognise live nodes.

Definition at line 113 of file bddBdd.h.

Referenced by decRef(), gc(), getExtRefNr(), getReachNodeNr(), and incRef().

unsigned * bddBdd::mUniqueHash [static, private]

Hash table of all used nodes.

Used by insert to ensure that mNodes contains no two equal nodes. mUniqueHash[i] contains the index of first node of a list of all nodes with hash value i. Lists are linked by the next-element of the nodes.

Definition at line 119 of file bddBdd.h.

Referenced by analyseUniqueHash(), done(), gc(), init(), and insert().