cudd/cuddTable.c File Reference

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...

Functions

unsigned int Cudd_Prime (unsigned int p)
 Returns the next prime p.
int Cudd_Reserve (DdManager *manager, int amount)
 Expand manager without creating variables.
DdNodecuddAllocNode (DdManager *unique)
 Fast storage allocation for DdNodes in the table.
DdManagercuddInitTable (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)
 Creates and initializes the unique table.
void cuddFreeTable (DdManager *unique)
 Frees the resources associated to a unique table.
int cuddGarbageCollect (DdManager *unique, int clearCache)
 Performs garbage collection on the BDD and ZDD unique tables.
DdNodecuddZddGetNode (DdManager *zdd, int id, DdNode *T, DdNode *E)
 Wrapper for cuddUniqueInterZdd.
DdNodecuddZddGetNodeIVO (DdManager *dd, int index, DdNode *g, DdNode *h)
 Wrapper for cuddUniqueInterZdd that is independent of variable ordering.
DdNodecuddUniqueInter (DdManager *unique, int index, DdNode *T, DdNode *E)
 Checks the unique table for the existence of an internal node.
DdNodecuddUniqueInterIVO (DdManager *unique, int index, DdNode *T, DdNode *E)
 Wrapper for cuddUniqueInter that is independent of variable ordering.
DdNodecuddUniqueInterZdd (DdManager *unique, int index, DdNode *T, DdNode *E)
 Checks the unique table for the existence of an internal ZDD node.
DdNodecuddUniqueConst (DdManager *unique, CUDD_VALUE_TYPE value)
 Checks the unique table for the existence of a constant node.
void cuddRehash (DdManager *unique, int i)
 Rehashes a unique subtable.
void cuddShrinkSubtable (DdManager *unique, int i)
 Shrinks a subtable.
int cuddInsertSubtables (DdManager *unique, int n, int level)
 Inserts n new subtables in a unique table at level.
int cuddDestroySubtables (DdManager *unique, int n)
 Destroys the n most recently created subtables in a unique table.
int cuddResizeTableZdd (DdManager *unique, int index)
 Increases the number of ZDD subtables in a unique table so that it meets or exceeds index.
void cuddSlowTableGrowth (DdManager *unique)
 Adjusts parameters of a table to slow down its growth.
static void ddRehashZdd (DdManager *unique, int i)
 Rehashes a ZDD unique subtable.
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.
static int cuddFindParent (DdManager *table, DdNode *node)
 Searches the subtables above node for a parent.
static void ddFixLimits (DdManager *unique)
 Adjusts the values of table limits.
static void ddPatchTree (DdManager *dd, MtrNode *treenode)
 Fixes a variable tree after the insertion of new subtables.
static void ddReportRefMess (DdManager *unique, int i, const char *caller)
 Reports problem in garbage collection.

Detailed Description

Unique table management functions.

Author:
Fabio Somenzi

Copyright (c) 1995-2015, Regents of the University of Colorado

All rights reserved.

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

unsigned int Cudd_Prime ( unsigned int  p  ) 

Returns the next prime p.

Side effects
None
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
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
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
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
void cuddFreeTable ( DdManager unique  ) 

Frees the resources associated to a unique table.

Side effects
None
See also:
cuddInitTable
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
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
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
void cuddRehash ( DdManager unique,
int  i 
)

Rehashes a unique subtable.

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

Side effects
None
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
void cuddShrinkSubtable ( DdManager unique,
int  i 
)

Shrinks a subtable.

Side effects
None
See also:
cuddRehash
void cuddSlowTableGrowth ( DdManager unique  ) 

Adjusts parameters of a table to slow down its growth.

Side effects
None
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
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
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
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
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
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
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.
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
static void ddRehashZdd ( DdManager unique,
int  i 
) [static]

Rehashes a ZDD unique subtable.

Side effects
None
See also:
cuddRehash
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
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
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1