Unique table management functions. More...

#include "util.h"
#include "mtrInt.h"
#include "cuddInt.h"

Include dependency graph for cuddTable.c:

Data Structures
union	hack
	This is a hack for when CUDD_VALUE_TYPE is double. More...

Typedefs
typedef union hack	hack
	This is a hack for when CUDD_VALUE_TYPE is double.

Functions
unsigned int	Cudd_Prime (unsigned int p)
	Returns the next prime ≥ p. More...

int	Cudd_Reserve (DdManager *manager, int amount)
	Expand manager without creating variables. More...

DdNode *	cuddAllocNode (DdManager *unique)
	Fast storage allocation for DdNodes in the table. More...

DdManager *	cuddInitTable (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)
	Creates and initializes the unique table. More...

void	cuddFreeTable (DdManager *unique)
	Frees the resources associated to a unique table. More...

int	cuddGarbageCollect (DdManager *unique, int clearCache)
	Performs garbage collection on the BDD and ZDD unique tables. More...

DdNode *	cuddZddGetNode (DdManager zdd, int id, DdNode T, DdNode *E)
	Wrapper for cuddUniqueInterZdd. More...

DdNode *	cuddZddGetNodeIVO (DdManager dd, int index, DdNode g, DdNode *h)
	Wrapper for cuddUniqueInterZdd that is independent of variable ordering. More...

DdNode *	cuddUniqueInter (DdManager unique, int index, DdNode T, DdNode *E)
	Checks the unique table for the existence of an internal node. More...

DdNode *	cuddUniqueInterIVO (DdManager unique, int index, DdNode T, DdNode *E)
	Wrapper for cuddUniqueInter that is independent of variable ordering. More...

DdNode *	cuddUniqueInterZdd (DdManager unique, int index, DdNode T, DdNode *E)
	Checks the unique table for the existence of an internal ZDD node. More...

DdNode *	cuddUniqueConst (DdManager *unique, CUDD_VALUE_TYPE value)
	Checks the unique table for the existence of a constant node. More...

void	cuddRehash (DdManager *unique, int i)
	Rehashes a unique subtable. More...

void	cuddShrinkSubtable (DdManager *unique, int i)
	Shrinks a subtable. More...

int	cuddInsertSubtables (DdManager *unique, int n, int level)
	Inserts n new subtables in a unique table at level. More...

int	cuddDestroySubtables (DdManager *unique, int n)
	Destroys the n most recently created subtables in a unique table. More...

int	cuddResizeTableZdd (DdManager *unique, int index)
	Increases the number of ZDD subtables in a unique table so that it meets or exceeds index. More...

void	cuddSlowTableGrowth (DdManager *unique)
	Adjusts parameters of a table to slow down its growth. More...

static void	ddRehashZdd (DdManager *unique, int i)
	Rehashes a ZDD unique subtable. More...

static int	ddResizeTable (DdManager *unique, int index, int amount)
	Increases the number of subtables in a unique table so that it meets or exceeds index. More...

static int	cuddFindParent (DdManager table, DdNode node)
	Searches the subtables above node for a parent. More...

static void	ddFixLimits (DdManager *unique)
	Adjusts the values of table limits. More...

static void	ddPatchTree (DdManager dd, MtrNode treenode)
	Fixes a variable tree after the insertion of new subtables. More...

static void	ddReportRefMess (DdManager unique, int i, const char caller)
	Reports problem in garbage collection. More...

Detailed Description

Unique table management functions.

Author: Fabio Somenzi

Copyright

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Function Documentation

◆ Cudd_Prime()

unsigned int Cudd_Prime ( unsigned int p )

Returns the next prime ≥ p.

Side effects None

◆ Cudd_Reserve()

int Cudd_Reserve	(	DdManager *	manager,
		int	amount
	)

Expand manager without creating variables.

Expand a manager by a specified number of subtables without actually creating new variables. This function can be used to reduce the frequency of resizing when an estimate of the number of variables is available. One would call this function instead of passing the number of variables to Cudd_Init if variables should not be created right away of if the estimate on their number became available only after the manager has been created.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_Init

◆ cuddAllocNode()

DdNode* cuddAllocNode ( DdManager * unique )

Fast storage allocation for DdNodes in the table.

The first 4 bytes of a chunk contain a pointer to the next block; the rest contains DD_MEM_CHUNK spaces for DdNodes.

Returns: a pointer to a new node if successful; NULL is memory is full.

Side effects None

See also: cuddDynamicAllocNode

◆ cuddDestroySubtables()

int cuddDestroySubtables	(	DdManager *	unique,
		int	n
	)

Destroys the n most recently created subtables in a unique table.

n should be positive. The subtables should not contain any live nodes, except the (isolated) projection function. The projection functions are freed.

Returns: 1 if successful; 0 otherwise.

Side effects The variable map used for fast variable substitution is: destroyed if it exists. In this case the cache is also cleared.

See also: cuddInsertSubtables Cudd_SetVarMap

◆ cuddFindParent()

static int cuddFindParent	(	DdManager *	table,
		DdNode *	node
	)

static

Searches the subtables above node for a parent.

Returns 1 as soon as one parent is found. Returns 0 is the search is fruitless.

Side effects None

◆ cuddFreeTable()

void cuddFreeTable ( DdManager * unique )

Frees the resources associated to a unique table.

Side effects None

See also: cuddInitTable

◆ cuddGarbageCollect()

int cuddGarbageCollect	(	DdManager *	unique,
		int	clearCache
	)

Performs garbage collection on the BDD and ZDD unique tables.

If clearCache is 0, the cache is not cleared. This should only be specified if the cache has been cleared right before calling cuddGarbageCollect. (As in the case of dynamic reordering.)

Returns: the total number of deleted nodes.

Side effects None

◆ cuddInitTable()

DdManager* cuddInitTable	(	unsigned int	numVars,
		unsigned int	numVarsZ,
		unsigned int	numSlots,
		unsigned int	looseUpTo
	)

Creates and initializes the unique table.

Returns: a pointer to the table if successful; NULL otherwise.

Side effects None

See also: Cudd_Init cuddFreeTable

Parameters

numVars	Initial number of BDD variables (and subtables)
numVarsZ	Initial number of ZDD variables (and subtables)
numSlots	Initial size of the BDD subtables
looseUpTo	Limit for fast table growth

◆ cuddInsertSubtables()

int cuddInsertSubtables	(	DdManager *	unique,
		int	n,
		int	level
	)

Inserts n new subtables in a unique table at level.

The number n should be positive, and level should be an existing level.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: cuddDestroySubtables

◆ cuddRehash()

void cuddRehash	(	DdManager *	unique,
		int	i
	)

Rehashes a unique subtable.

Doubles the size of a unique subtable and rehashes its contents.

Side effects None

◆ cuddResizeTableZdd()

int cuddResizeTableZdd	(	DdManager *	unique,
		int	index
	)

Increases the number of ZDD subtables in a unique table so that it meets or exceeds index.

When new ZDD variables are created, it is possible to preserve the functions unchanged, or it is possible to preserve the covers unchanged, but not both. cuddResizeTableZdd preserves the covers.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: ddResizeTable

◆ cuddShrinkSubtable()

void cuddShrinkSubtable	(	DdManager *	unique,
		int	i
	)

Shrinks a subtable.

Side effects None

See also: cuddRehash

◆ cuddSlowTableGrowth()

void cuddSlowTableGrowth ( DdManager * unique )

Adjusts parameters of a table to slow down its growth.

Side effects None

◆ cuddUniqueConst()

DdNode* cuddUniqueConst	(	DdManager *	unique,
		CUDD_VALUE_TYPE	value
	)

Checks the unique table for the existence of a constant node.

If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0.

Returns: a pointer to the new node.

Side effects None

◆ cuddUniqueInter()

DdNode* cuddUniqueInter	(	DdManager *	unique,
		int	index,
		DdNode *	T,
		DdNode *	E
	)

Checks the unique table for the existence of an internal node.

If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. For a newly created node, increments the reference counts of what T and E point to.

Returns: a pointer to the new node if successful; NULL if memory is exhausted, if a termination request was detected, if a timeout expired, or if reordering took place.

Side effects None

See also: cuddUniqueInterZdd

◆ cuddUniqueInterIVO()

DdNode* cuddUniqueInterIVO	(	DdManager *	unique,
		int	index,
		DdNode *	T,
		DdNode *	E
	)

Wrapper for cuddUniqueInter that is independent of variable ordering.

Wrapper for cuddUniqueInter that is independent of variable ordering (IVO). This function does not require parameter index to precede the indices of the top nodes of T and E in the variable order.

Returns: a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.

Side effects None

See also: cuddUniqueInter Cudd_MakeBddFromZddCover

◆ cuddUniqueInterZdd()

DdNode* cuddUniqueInterZdd	(	DdManager *	unique,
		int	index,
		DdNode *	T,
		DdNode *	E
	)

Checks the unique table for the existence of an internal ZDD node.

If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. For a newly created node, increments the reference counts of what T and E point to.

Returns: a pointer to the new node if successful; NULL if memory is exhausted, if a termination request was detected, if a timeout expired, or if reordering took place.

Side effects None

See also: cuddUniqueInter

◆ cuddZddGetNode()

DdNode* cuddZddGetNode	(	DdManager *	zdd,
		int	id,
		DdNode *	T,
		DdNode *	E
	)

Wrapper for cuddUniqueInterZdd.

It applies the ZDD reduction rule.

Returns: a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.

Side effects None

See also: cuddUniqueInterZdd

◆ cuddZddGetNodeIVO()

DdNode* cuddZddGetNodeIVO	(	DdManager *	dd,
		int	index,
		DdNode *	g,
		DdNode *	h
	)

Wrapper for cuddUniqueInterZdd that is independent of variable ordering.

Wrapper for cuddUniqueInterZdd that is independent of variable ordering (IVO). This function does not require parameter index to precede the indices of the top nodes of g and h in the variable order.

Returns: a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.

Side effects None

See also: cuddZddGetNode cuddZddIsop

◆ ddFixLimits()

static void ddFixLimits ( DdManager * unique )

static

Adjusts the values of table limits.

Adjusts the values of table fields controlling the sizes of subtables and computed table. If the computed table is too small according to the new values, it is resized.

Side effects Modifies manager fields. May resize computed table.

◆ ddPatchTree()

static void ddPatchTree	(	DdManager *	dd,
		MtrNode *	treenode
	)

static

Fixes a variable tree after the insertion of new subtables.

After such an insertion, the low fields of the tree below the insertion point are inconsistent.

Side effects None

◆ ddRehashZdd()

static void ddRehashZdd	(	DdManager *	unique,
		int	i
	)

static

Rehashes a ZDD unique subtable.

Side effects None

See also: cuddRehash

◆ ddReportRefMess()

static void ddReportRefMess	(	DdManager *	unique,
		int	i,
		const char *	caller
	)

static

Reports problem in garbage collection.

Side effects None

See also: cuddGarbageCollect cuddGarbageCollectZdd

Parameters

unique	manager
i	table in which the problem occurred
caller	procedure that detected the problem

◆ ddResizeTable()

static int ddResizeTable	(	DdManager *	unique,
		int	index,
		int	amount
	)

static

Increases the number of subtables in a unique table so that it meets or exceeds index.

The parameter amount determines how much spare space is allocated to prevent too frequent resizing. If index is negative, the table is resized, but no new variables are created.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_Reserve cuddResizeTableZdd

Data Structures

Typedefs

Functions

Detailed Description

Function Documentation

◆ Cudd_Prime()

◆ Cudd_Reserve()

◆ cuddAllocNode()

◆ cuddDestroySubtables()

◆ cuddFindParent()

◆ cuddFreeTable()

◆ cuddGarbageCollect()

◆ cuddInitTable()

◆ cuddInsertSubtables()

◆ cuddRehash()

◆ cuddResizeTableZdd()

◆ cuddShrinkSubtable()

◆ cuddSlowTableGrowth()

◆ cuddUniqueConst()

◆ cuddUniqueInter()

◆ cuddUniqueInterIVO()

◆ cuddUniqueInterZdd()

◆ cuddZddGetNode()

◆ cuddZddGetNodeIVO()

◆ ddFixLimits()

◆ ddPatchTree()

◆ ddRehashZdd()

◆ ddReportRefMess()

◆ ddResizeTable()