cudd/cuddAPI.c File Reference

Application interface functions. More...

#include "util.h"
#include "mtrInt.h"
#include "cuddInt.h"
Include dependency graph for cuddAPI.c:

Functions

DdNodeCudd_addNewVar (DdManager *dd)
 Returns a new ADD variable.
DdNodeCudd_addNewVarAtLevel (DdManager *dd, int level)
 Returns a new ADD variable at a specified level.
DdNodeCudd_bddNewVar (DdManager *dd)
 Returns a new BDD variable.
DdNodeCudd_bddNewVarAtLevel (DdManager *dd, int level)
 Returns a new BDD variable at a specified level.
int Cudd_bddIsVar (DdManager *dd, DdNode *f)
 Returns 1 if the given node is a BDD variable; 0 otherwise.
DdNodeCudd_addIthVar (DdManager *dd, int i)
 Returns the ADD variable with index i.
DdNodeCudd_bddIthVar (DdManager *dd, int i)
 Returns the BDD variable with index i.
DdNodeCudd_zddIthVar (DdManager *dd, int i)
 Returns the ZDD variable with index i.
int Cudd_zddVarsFromBddVars (DdManager *dd, int multiplicity)
 Creates one or more ZDD variables for each BDD variable.
unsigned int Cudd_ReadMaxIndex (void)
 Returns the maximum possible index for a variable.
DdNodeCudd_addConst (DdManager *dd, CUDD_VALUE_TYPE c)
 Returns the ADD for constant c.
int Cudd_IsConstant (DdNode *node)
 Returns 1 if the node is a constant node.
int Cudd_IsNonConstant (DdNode *f)
 Returns 1 if a DD node is not constant.
DdNodeCudd_T (DdNode *node)
 Returns the then child of an internal node.
DdNodeCudd_E (DdNode *node)
 Returns the else child of an internal node.
CUDD_VALUE_TYPE Cudd_V (DdNode *node)
 Returns the value of a constant node.
unsigned long Cudd_ReadStartTime (DdManager *unique)
 Returns the start time of the manager.
unsigned long Cudd_ReadElapsedTime (DdManager *unique)
 Returns the time elapsed since the start time of the manager.
void Cudd_SetStartTime (DdManager *unique, unsigned long st)
 Sets the start time of the manager.
void Cudd_ResetStartTime (DdManager *unique)
 Resets the start time of the manager.
unsigned long Cudd_ReadTimeLimit (DdManager *unique)
 Returns the time limit for the manager.
unsigned long Cudd_SetTimeLimit (DdManager *unique, unsigned long tl)
 Sets the time limit for the manager.
void Cudd_UpdateTimeLimit (DdManager *unique)
 Updates the time limit for the manager.
void Cudd_IncreaseTimeLimit (DdManager *unique, unsigned long increase)
 Increases the time limit for the manager.
void Cudd_UnsetTimeLimit (DdManager *unique)
 Unsets the time limit for the manager.
int Cudd_TimeLimited (DdManager *unique)
 Returns true if the time limit for the manager is set.
void Cudd_RegisterTerminationCallback (DdManager *unique, DD_THFP callback, void *callback_arg)
 Installs a termination callback.
void Cudd_UnregisterTerminationCallback (DdManager *unique)
 Unregisters a termination callback.
DD_OOMFP Cudd_RegisterOutOfMemoryCallback (DdManager *unique, DD_OOMFP callback)
 Installs an out-of-memory callback.
void Cudd_UnregisterOutOfMemoryCallback (DdManager *unique)
 Unregister an out-of-memory callback.
void Cudd_RegisterTimeoutHandler (DdManager *unique, DD_TOHFP handler, void *arg)
 Register a timeout handler function.
DD_TOHFP Cudd_ReadTimeoutHandler (DdManager *unique, void **argp)
 Read the current timeout handler function.
void Cudd_AutodynEnable (DdManager *unique, Cudd_ReorderingType method)
 Enables automatic dynamic reordering of BDDs and ADDs.
void Cudd_AutodynDisable (DdManager *unique)
 Disables automatic dynamic reordering.
int Cudd_ReorderingStatus (DdManager *unique, Cudd_ReorderingType *method)
 Reports the status of automatic dynamic reordering of BDDs and ADDs.
void Cudd_AutodynEnableZdd (DdManager *unique, Cudd_ReorderingType method)
 Enables automatic dynamic reordering of ZDDs.
void Cudd_AutodynDisableZdd (DdManager *unique)
 Disables automatic dynamic reordering of ZDDs.
int Cudd_ReorderingStatusZdd (DdManager *unique, Cudd_ReorderingType *method)
 Reports the status of automatic dynamic reordering of ZDDs.
int Cudd_zddRealignmentEnabled (DdManager *unique)
 Tells whether the realignment of ZDD order to BDD order is enabled.
void Cudd_zddRealignEnable (DdManager *unique)
 Enables realignment of ZDD order to BDD order.
void Cudd_zddRealignDisable (DdManager *unique)
 Disables realignment of ZDD order to BDD order.
int Cudd_bddRealignmentEnabled (DdManager *unique)
 Tells whether the realignment of BDD order to ZDD order is enabled.
void Cudd_bddRealignEnable (DdManager *unique)
 Enables realignment of BDD order to ZDD order.
void Cudd_bddRealignDisable (DdManager *unique)
 Disables realignment of ZDD order to BDD order.
DdNodeCudd_ReadOne (DdManager *dd)
 Returns the one constant of the manager.
DdNodeCudd_ReadZddOne (DdManager *dd, int i)
 Returns the ZDD for the constant 1 function.
DdNodeCudd_ReadZero (DdManager *dd)
 Returns the zero constant of the manager.
DdNodeCudd_ReadLogicZero (DdManager *dd)
 Returns the logic zero constant of the manager.
DdNodeCudd_ReadPlusInfinity (DdManager *dd)
 Reads the plus-infinity constant from the manager.
DdNodeCudd_ReadMinusInfinity (DdManager *dd)
 Reads the minus-infinity constant from the manager.
DdNodeCudd_ReadBackground (DdManager *dd)
 Reads the background constant of the manager.
void Cudd_SetBackground (DdManager *dd, DdNode *bck)
 Sets the background constant of the manager.
unsigned int Cudd_ReadCacheSlots (DdManager *dd)
 Reads the number of slots in the cache.
double Cudd_ReadCacheUsedSlots (DdManager *dd)
 Reads the fraction of used slots in the cache.
double Cudd_ReadCacheLookUps (DdManager *dd)
 Returns the number of cache look-ups.
double Cudd_ReadCacheHits (DdManager *dd)
 Returns the number of cache hits.
double Cudd_ReadRecursiveCalls (DdManager *dd)
 Returns the number of recursive calls.
unsigned int Cudd_ReadMinHit (DdManager *dd)
 Reads the hit rate that causes resizinig of the computed table.
void Cudd_SetMinHit (DdManager *dd, unsigned int hr)
 Sets the hit rate that causes resizinig of the computed table.
unsigned int Cudd_ReadLooseUpTo (DdManager *dd)
 Reads the looseUpTo parameter of the manager.
void Cudd_SetLooseUpTo (DdManager *dd, unsigned int lut)
 Sets the looseUpTo parameter of the manager.
unsigned int Cudd_ReadMaxCache (DdManager *dd)
 Returns the soft limit for the cache size.
unsigned int Cudd_ReadMaxCacheHard (DdManager *dd)
 Reads the maxCacheHard parameter of the manager.
void Cudd_SetMaxCacheHard (DdManager *dd, unsigned int mc)
 Sets the maxCacheHard parameter of the manager.
int Cudd_ReadSize (DdManager *dd)
 Returns the number of BDD variables in existance.
int Cudd_ReadZddSize (DdManager *dd)
 Returns the number of ZDD variables in existance.
unsigned int Cudd_ReadSlots (DdManager *dd)
 Returns the total number of slots of the unique table.
double Cudd_ReadUsedSlots (DdManager *dd)
 Reads the fraction of used slots in the unique table.
double Cudd_ExpectedUsedSlots (DdManager *dd)
 Computes the expected fraction of used slots in the unique table.
unsigned int Cudd_ReadKeys (DdManager *dd)
 Returns the number of nodes in the unique table.
unsigned int Cudd_ReadDead (DdManager *dd)
 Returns the number of dead nodes in the unique table.
unsigned int Cudd_ReadMinDead (DdManager *dd)
 Reads the minDead parameter of the manager.
unsigned int Cudd_ReadReorderings (DdManager *dd)
 Returns the number of times reordering has occurred.
unsigned int Cudd_ReadMaxReorderings (DdManager *dd)
 Returns the maximum number of times reordering may be invoked.
void Cudd_SetMaxReorderings (DdManager *dd, unsigned int mr)
 Sets the maximum number of times reordering may be invoked.
long Cudd_ReadReorderingTime (DdManager *dd)
 Returns the time spent in reordering.
int Cudd_ReadGarbageCollections (DdManager *dd)
 Returns the number of times garbage collection has occurred.
long Cudd_ReadGarbageCollectionTime (DdManager *dd)
 Returns the time spent in garbage collection.
double Cudd_ReadNodesFreed (DdManager *dd)
 Returns the number of nodes freed.
double Cudd_ReadNodesDropped (DdManager *dd)
 Returns the number of nodes dropped.
double Cudd_ReadUniqueLookUps (DdManager *dd)
 Returns the number of look-ups in the unique table.
double Cudd_ReadUniqueLinks (DdManager *dd)
 Returns the number of links followed in the unique table.
int Cudd_ReadSiftMaxVar (DdManager *dd)
 Reads the siftMaxVar parameter of the manager.
void Cudd_SetSiftMaxVar (DdManager *dd, int smv)
 Sets the siftMaxVar parameter of the manager.
int Cudd_ReadSiftMaxSwap (DdManager *dd)
 Reads the siftMaxSwap parameter of the manager.
void Cudd_SetSiftMaxSwap (DdManager *dd, int sms)
 Sets the siftMaxSwap parameter of the manager.
double Cudd_ReadMaxGrowth (DdManager *dd)
 Reads the maxGrowth parameter of the manager.
void Cudd_SetMaxGrowth (DdManager *dd, double mg)
 Sets the maxGrowth parameter of the manager.
double Cudd_ReadMaxGrowthAlternate (DdManager *dd)
 Reads the maxGrowthAlt parameter of the manager.
void Cudd_SetMaxGrowthAlternate (DdManager *dd, double mg)
 Sets the maxGrowthAlt parameter of the manager.
int Cudd_ReadReorderingCycle (DdManager *dd)
 Reads the reordCycle parameter of the manager.
void Cudd_SetReorderingCycle (DdManager *dd, int cycle)
 Sets the reordCycle parameter of the manager.
MtrNodeCudd_ReadTree (DdManager *dd)
 Returns the variable group tree of the manager.
void Cudd_SetTree (DdManager *dd, MtrNode *tree)
 Sets the variable group tree of the manager.
void Cudd_FreeTree (DdManager *dd)
 Frees the variable group tree of the manager.
MtrNodeCudd_ReadZddTree (DdManager *dd)
 Returns the variable group tree of the manager.
void Cudd_SetZddTree (DdManager *dd, MtrNode *tree)
 Sets the ZDD variable group tree of the manager.
void Cudd_FreeZddTree (DdManager *dd)
 Frees the variable group tree of the manager.
unsigned int Cudd_NodeReadIndex (DdNode *node)
 Returns the index of the node.
int Cudd_ReadPerm (DdManager *dd, int i)
 Returns the current position of the i-th variable in the order.
int Cudd_ReadPermZdd (DdManager *dd, int i)
 Returns the current position of the i-th ZDD variable in the order.
int Cudd_ReadInvPerm (DdManager *dd, int i)
 Returns the index of the variable currently in the i-th position of the order.
int Cudd_ReadInvPermZdd (DdManager *dd, int i)
 Returns the index of the ZDD variable currently in the i-th position of the order.
DdNodeCudd_ReadVars (DdManager *dd, int i)
 Returns the i-th element of the vars array.
CUDD_VALUE_TYPE Cudd_ReadEpsilon (DdManager *dd)
 Reads the epsilon parameter of the manager.
void Cudd_SetEpsilon (DdManager *dd, CUDD_VALUE_TYPE ep)
 Sets the epsilon parameter of the manager to ep.
Cudd_AggregationType Cudd_ReadGroupcheck (DdManager *dd)
 Reads the groupcheck parameter of the manager.
void Cudd_SetGroupcheck (DdManager *dd, Cudd_AggregationType gc)
 Sets the parameter groupcheck of the manager to gc.
int Cudd_GarbageCollectionEnabled (DdManager *dd)
 Tells whether garbage collection is enabled.
void Cudd_EnableGarbageCollection (DdManager *dd)
 Enables garbage collection.
void Cudd_DisableGarbageCollection (DdManager *dd)
 Disables garbage collection.
int Cudd_DeadAreCounted (DdManager *dd)
 Tells whether dead nodes are counted towards triggering reordering.
void Cudd_TurnOnCountDead (DdManager *dd)
 Causes the dead nodes to be counted towards triggering reordering.
void Cudd_TurnOffCountDead (DdManager *dd)
 Causes the dead nodes not to be counted towards triggering reordering.
int Cudd_ReadRecomb (DdManager *dd)
 Returns the current value of the recombination parameter used in group sifting.
void Cudd_SetRecomb (DdManager *dd, int recomb)
 Sets the value of the recombination parameter used in group sifting.
int Cudd_ReadSymmviolation (DdManager *dd)
 Returns the current value of the symmviolation parameter used in group sifting.
void Cudd_SetSymmviolation (DdManager *dd, int symmviolation)
 Sets the value of the symmviolation parameter used in group sifting.
int Cudd_ReadArcviolation (DdManager *dd)
 Returns the current value of the arcviolation parameter used in group sifting.
void Cudd_SetArcviolation (DdManager *dd, int arcviolation)
 Sets the value of the arcviolation parameter used in group sifting.
int Cudd_ReadPopulationSize (DdManager *dd)
 Reads the current size of the population used by the genetic algorithm for variable reordering.
void Cudd_SetPopulationSize (DdManager *dd, int populationSize)
 Sets the size of the population used by the genetic algorithm for variable reordering.
int Cudd_ReadNumberXovers (DdManager *dd)
 Reads the current number of crossovers used by the genetic algorithm for variable reordering.
void Cudd_SetNumberXovers (DdManager *dd, int numberXovers)
 Sets the number of crossovers used by the genetic algorithm for variable reordering.
unsigned int Cudd_ReadOrderRandomization (DdManager *dd)
 Returns the order randomization factor.
void Cudd_SetOrderRandomization (DdManager *dd, unsigned int factor)
 Sets the order randomization factor.
size_t Cudd_ReadMemoryInUse (DdManager *dd)
 Returns the memory in use by the manager measured in bytes.
int Cudd_PrintInfo (DdManager *dd, FILE *fp)
 Prints out statistics and settings for a CUDD manager.
long Cudd_ReadPeakNodeCount (DdManager *dd)
 Reports the peak number of nodes.
int Cudd_ReadPeakLiveNodeCount (DdManager *dd)
 Reports the peak number of live nodes.
long Cudd_ReadNodeCount (DdManager *dd)
 Reports the number of nodes in BDDs and ADDs.
long Cudd_zddReadNodeCount (DdManager *dd)
 Reports the number of nodes in ZDDs.
int Cudd_AddHook (DdManager *dd, DD_HFP f, Cudd_HookType where)
 Adds a function to a hook.
int Cudd_RemoveHook (DdManager *dd, DD_HFP f, Cudd_HookType where)
 Removes a function from a hook.
int Cudd_IsInHook (DdManager *dd, DD_HFP f, Cudd_HookType where)
 Checks whether a function is in a hook.
int Cudd_StdPreReordHook (DdManager *dd, const char *str, void *data)
 Sample hook function to call before reordering.
int Cudd_StdPostReordHook (DdManager *dd, const char *str, void *data)
 Sample hook function to call after reordering.
int Cudd_EnableReorderingReporting (DdManager *dd)
 Enables reporting of reordering stats.
int Cudd_DisableReorderingReporting (DdManager *dd)
 Disables reporting of reordering stats.
int Cudd_ReorderingReporting (DdManager *dd)
 Returns 1 if reporting of reordering stats is enabled; 0 otherwise.
int Cudd_PrintGroupedOrder (DdManager *dd, const char *str, void *data)
 Hook function to print the current variable order.
int Cudd_EnableOrderingMonitoring (DdManager *dd)
 Enables monitoring of ordering.
int Cudd_DisableOrderingMonitoring (DdManager *dd)
 Disables monitoring of ordering.
int Cudd_OrderingMonitoring (DdManager *dd)
 Returns 1 if monitoring of ordering is enabled; 0 otherwise.
void Cudd_SetApplicationHook (DdManager *dd, void *value)
 Sets the application hook.
void * Cudd_ReadApplicationHook (DdManager *dd)
 Reads the application hook.
Cudd_ErrorType Cudd_ReadErrorCode (DdManager *dd)
 Returns the code of the last error.
void Cudd_ClearErrorCode (DdManager *dd)
 Clear the error code of a manager.
DD_OOMFP Cudd_InstallOutOfMemoryHandler (DD_OOMFP newHandler)
 Installs a handler for failed memory allocations.
FILE * Cudd_ReadStdout (DdManager *dd)
 Reads the stdout of a manager.
void Cudd_SetStdout (DdManager *dd, FILE *fp)
 Sets the stdout of a manager.
FILE * Cudd_ReadStderr (DdManager *dd)
 Reads the stderr of a manager.
void Cudd_SetStderr (DdManager *dd, FILE *fp)
 Sets the stderr of a manager.
unsigned int Cudd_ReadNextReordering (DdManager *dd)
 Returns the threshold for the next dynamic reordering.
void Cudd_SetNextReordering (DdManager *dd, unsigned int next)
 Sets the threshold for the next dynamic reordering.
double Cudd_ReadSwapSteps (DdManager *dd)
 Reads the number of elementary reordering steps.
unsigned int Cudd_ReadMaxLive (DdManager *dd)
 Reads the maximum allowed number of live nodes.
void Cudd_SetMaxLive (DdManager *dd, unsigned int maxLive)
 Sets the maximum allowed number of live nodes.
size_t Cudd_ReadMaxMemory (DdManager *dd)
 Reads the maximum allowed memory.
size_t Cudd_SetMaxMemory (DdManager *dd, size_t maxMemory)
 Sets the maximum allowed memory.
int Cudd_bddBindVar (DdManager *dd, int index)
 Prevents sifting of a variable.
int Cudd_bddUnbindVar (DdManager *dd, int index)
 Allows the sifting of a variable.
int Cudd_bddVarIsBound (DdManager *dd, int index)
 Tells whether a variable can be sifted.
int Cudd_bddSetPiVar (DdManager *dd, int index)
 Sets a variable type to primary input.
int Cudd_bddSetPsVar (DdManager *dd, int index)
 Sets a variable type to present state.
int Cudd_bddSetNsVar (DdManager *dd, int index)
 Sets a variable type to next state.
int Cudd_bddIsPiVar (DdManager *dd, int index)
 Checks whether a variable is primary input.
int Cudd_bddIsPsVar (DdManager *dd, int index)
 Checks whether a variable is present state.
int Cudd_bddIsNsVar (DdManager *dd, int index)
 Checks whether a variable is next state.
int Cudd_bddSetPairIndex (DdManager *dd, int index, int pairIndex)
 Sets a corresponding pair index for a given index.
int Cudd_bddReadPairIndex (DdManager *dd, int index)
 Reads a corresponding pair index for a given index.
int Cudd_bddSetVarToBeGrouped (DdManager *dd, int index)
 Sets a variable to be grouped.
int Cudd_bddSetVarHardGroup (DdManager *dd, int index)
 Sets a variable to be a hard group.
int Cudd_bddResetVarToBeGrouped (DdManager *dd, int index)
 Resets a variable not to be grouped.
int Cudd_bddIsVarToBeGrouped (DdManager *dd, int index)
 Checks whether a variable is set to be grouped.
int Cudd_bddSetVarToBeUngrouped (DdManager *dd, int index)
 Sets a variable to be ungrouped.
int Cudd_bddIsVarToBeUngrouped (DdManager *dd, int index)
 Checks whether a variable is set to be ungrouped.
int Cudd_bddIsVarHardGroup (DdManager *dd, int index)
 Checks whether a variable is set to be in a hard group.
static void fixVarTree (MtrNode *treenode, int *perm, int size)
 Fixes a variable group tree.
static int addMultiplicityGroups (DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask)
 Adds multiplicity groups to a ZDD variable group tree.

Detailed Description

Application interface 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

static int addMultiplicityGroups ( DdManager dd,
MtrNode treenode,
int  multiplicity,
char *  vmask,
char *  lmask 
) [static]

Adds multiplicity groups to a ZDD variable group tree.

This function creates the groups for set of ZDD variables (whose cardinality is given by parameter multiplicity) that are created for each BDD variable in Cudd_zddVarsFromBddVars. The crux of the matter is to determine the index each new group. (The index of the first variable in the group.) We first build all the groups for the children of a node, and then deal with the ZDD variables that are directly attached to the node. The problem for these is that the tree itself does not provide information on their position inside the group. While we deal with the children of the node, therefore, we keep track of all the positions they occupy. The remaining positions in the tree can be freely used. Also, we keep track of all the variables placed in the children. All the remaining variables are directly attached to the group. We can then place any pair of variables not yet grouped in any pair of available positions in the node.

Returns:
1 if successful; 0 otherwise.
Side effects
Changes the variable group tree.
See also:
Cudd_zddVarsFromBddVars
Parameters:
dd manager
treenode current tree node
multiplicity how many ZDD vars per BDD var
vmask variable pairs for which a group has been already built
lmask levels for which a group has already been built
DdNode* Cudd_addConst ( DdManager dd,
CUDD_VALUE_TYPE  c 
)

Returns the ADD for constant c.

Retrieves the ADD for constant c if it already exists, or creates a new ADD.

Returns:
a pointer to the ADD if successful; NULL otherwise.
Side effects
None
See also:
Cudd_addNewVar Cudd_addIthVar
int Cudd_AddHook ( DdManager dd,
DD_HFP  f,
Cudd_HookType  where 
)

Adds a function to a hook.

A hook is a list of application-provided functions called on certain occasions by the package.

Returns:
1 if the function is successfully added; 2 if the function was already in the list; 0 otherwise.
Side effects
None
See also:
Cudd_RemoveHook
DdNode* Cudd_addIthVar ( DdManager dd,
int  i 
)

Returns the ADD variable with index i.

Retrieves the ADD variable with index i if it already exists, or creates a new ADD variable. An ADD variable differs from a BDD variable because it points to the arithmetic zero, instead of having a complement pointer to 1.

Returns:
a pointer to the variable if successful; NULL otherwise.
Side effects
None
See also:
Cudd_addNewVar Cudd_bddIthVar Cudd_addConst Cudd_addNewVarAtLevel
DdNode* Cudd_addNewVar ( DdManager dd  ) 

Returns a new ADD variable.

The new variable has an index equal to the largest previous index plus 1. An ADD variable differs from a BDD variable because it points to the arithmetic zero, instead of having a complement pointer to 1.

Returns:
a pointer to the new variable if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddNewVar Cudd_addIthVar Cudd_addConst Cudd_addNewVarAtLevel
DdNode* Cudd_addNewVarAtLevel ( DdManager dd,
int  level 
)

Returns a new ADD variable at a specified level.

The new variable has an index equal to the largest previous index plus 1 and is positioned at the specified level in the order.

Returns:
a pointer to the new variable if successful; NULL otherwise.
Side effects
None
See also:
Cudd_addNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel
void Cudd_AutodynDisable ( DdManager unique  ) 

Disables automatic dynamic reordering.

Side effects
None
See also:
Cudd_AutodynEnable Cudd_ReorderingStatus Cudd_AutodynDisableZdd
void Cudd_AutodynDisableZdd ( DdManager unique  ) 

Disables automatic dynamic reordering of ZDDs.

Side effects
None
See also:
Cudd_AutodynEnableZdd Cudd_ReorderingStatusZdd Cudd_AutodynDisable
void Cudd_AutodynEnable ( DdManager unique,
Cudd_ReorderingType  method 
)

Enables automatic dynamic reordering of BDDs and ADDs.

Parameter method is used to determine the method used for reordering. If CUDD_REORDER_SAME is passed, the method is unchanged.

Side effects
None
See also:
Cudd_AutodynDisable Cudd_ReorderingStatus Cudd_AutodynEnableZdd
void Cudd_AutodynEnableZdd ( DdManager unique,
Cudd_ReorderingType  method 
)

Enables automatic dynamic reordering of ZDDs.

Parameter method is used to determine the method used for reordering ZDDs. If CUDD_REORDER_SAME is passed, the method is unchanged.

Side effects
None
See also:
Cudd_AutodynDisableZdd Cudd_ReorderingStatusZdd Cudd_AutodynEnable
int Cudd_bddBindVar ( DdManager dd,
int  index 
)

Prevents sifting of a variable.

This function sets a flag to prevent sifting of a variable.

Returns:
1 if successful; 0 otherwise (i.e., invalid variable index).
Side effects
Changes the "bindVar" flag in DdSubtable.
See also:
Cudd_bddUnbindVar
Parameters:
dd manager
index variable index
int Cudd_bddIsNsVar ( DdManager dd,
int  index 
)

Checks whether a variable is next state.

Returns:
1 if the variable's type is present state; 0 if the variable exists but is not a present state; -1 if the variable does not exist.
Side effects
none
See also:
Cudd_bddSetNsVar Cudd_bddIsPiVar Cudd_bddIsPsVar
int Cudd_bddIsPiVar ( DdManager dd,
int  index 
)

Checks whether a variable is primary input.

Returns:
1 if the variable's type is primary input; 0 if the variable exists but is not a primary input; -1 if the variable does not exist.
Side effects
none
See also:
Cudd_bddSetPiVar Cudd_bddIsPsVar Cudd_bddIsNsVar
Parameters:
dd manager
index variable index
int Cudd_bddIsPsVar ( DdManager dd,
int  index 
)

Checks whether a variable is present state.

Returns:
1 if the variable's type is present state; 0 if the variable exists but is not a present state; -1 if the variable does not exist.
Side effects
none
See also:
Cudd_bddSetPsVar Cudd_bddIsPiVar Cudd_bddIsNsVar
int Cudd_bddIsVar ( DdManager dd,
DdNode f 
)

Returns 1 if the given node is a BDD variable; 0 otherwise.

Side effects
None
int Cudd_bddIsVarHardGroup ( DdManager dd,
int  index 
)

Checks whether a variable is set to be in a hard group.

This function is used for lazy sifting.

Returns:
1 if the variable is marked to be in a hard group; 0 if the variable exists, but it is not marked to be in a hard group; -1 if the variable does not exist.
Side effects
none
See also:
Cudd_bddSetVarHardGroup
int Cudd_bddIsVarToBeGrouped ( DdManager dd,
int  index 
)

Checks whether a variable is set to be grouped.

This function is used for lazy sifting.

Side effects
none
int Cudd_bddIsVarToBeUngrouped ( DdManager dd,
int  index 
)

Checks whether a variable is set to be ungrouped.

This function is used for lazy sifting.

Returns:
1 if the variable is marked to be ungrouped; 0 if the variable exists, but it is not marked to be ungrouped; -1 if the variable does not exist.
Side effects
none
See also:
Cudd_bddSetVarToBeUngrouped
DdNode* Cudd_bddIthVar ( DdManager dd,
int  i 
)

Returns the BDD variable with index i.

Retrieves the BDD variable with index i if it already exists, or creates a new BDD variable.

Returns:
a pointer to the variable if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel Cudd_ReadVars
DdNode* Cudd_bddNewVar ( DdManager dd  ) 

Returns a new BDD variable.

The new variable has an index equal to the largest previous index plus 1.

Returns:
a pointer to the new variable if successful; NULL otherwise.
Side effects
None
See also:
Cudd_addNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel
DdNode* Cudd_bddNewVarAtLevel ( DdManager dd,
int  level 
)

Returns a new BDD variable at a specified level.

The new variable has an index equal to the largest previous index plus 1 and is positioned at the specified level in the order.

Returns:
a pointer to the new variable if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddNewVar Cudd_bddIthVar Cudd_addNewVarAtLevel
int Cudd_bddReadPairIndex ( DdManager dd,
int  index 
)

Reads a corresponding pair index for a given index.

These pair indices are present and next state variable.

Returns:
the corresponding variable index if the variable exists; -1 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddSetPairIndex
void Cudd_bddRealignDisable ( DdManager unique  ) 

Disables realignment of ZDD order to BDD order.

Side effects
None
See also:
Cudd_bddRealignEnable Cudd_bddRealignmentEnabled Cudd_zddRealignEnable Cudd_zddRealignmentEnabled
void Cudd_bddRealignEnable ( DdManager unique  ) 

Enables realignment of BDD order to ZDD order.

Enables realignment of the BDD variable order to the ZDD variable order after the ZDDs have been reordered. The number of ZDD variables must be a multiple of the number of BDD variables for realignment to make sense. If this condition is not met, Cudd_zddReduceHeap will return 0. Let M be the ratio of the two numbers. For the purpose of realignment, the ZDD variables from M*i to (M+1)*i-1 are reagarded as corresponding to BDD variable i. Realignment is initially disabled.

Side effects
None
See also:
Cudd_zddReduceHeap Cudd_bddRealignDisable Cudd_bddRealignmentEnabled Cudd_zddRealignDisable Cudd_zddRealignmentEnabled
int Cudd_bddRealignmentEnabled ( DdManager unique  ) 

Tells whether the realignment of BDD order to ZDD order is enabled.

Returns:
1 if the realignment of BDD order to ZDD order is enabled; 0 otherwise.
Side effects
None
See also:
Cudd_bddRealignEnable Cudd_bddRealignDisable Cudd_zddRealignEnable Cudd_zddRealignDisable
int Cudd_bddResetVarToBeGrouped ( DdManager dd,
int  index 
)

Resets a variable not to be grouped.

This function is used for lazy sifting.

Returns:
1 if successful; 0 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddSetVarToBeGrouped Cudd_bddSetVarHardGroup
int Cudd_bddSetNsVar ( DdManager dd,
int  index 
)

Sets a variable type to next state.

The variable type is used by lazy sifting.

Returns:
1 if successful; 0 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddSetPiVar Cudd_bddSetPsVar Cudd_bddIsNsVar
Parameters:
dd manager
index variable index
int Cudd_bddSetPairIndex ( DdManager dd,
int  index,
int  pairIndex 
)

Sets a corresponding pair index for a given index.

These pair indices are present and next state variable.

Returns:
1 if successful; 0 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddReadPairIndex
Parameters:
dd manager
index variable index
pairIndex corresponding variable index
int Cudd_bddSetPiVar ( DdManager dd,
int  index 
)

Sets a variable type to primary input.

The variable type is used by lazy sifting.

Returns:
1 if successful; 0 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddSetPsVar Cudd_bddSetNsVar Cudd_bddIsPiVar
Parameters:
dd manager
index variable index
int Cudd_bddSetPsVar ( DdManager dd,
int  index 
)

Sets a variable type to present state.

The variable type is used by lazy sifting.

Returns:
1 if successful; 0 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddSetPiVar Cudd_bddSetNsVar Cudd_bddIsPsVar
Parameters:
dd manager
index variable index
int Cudd_bddSetVarHardGroup ( DdManager dd,
int  index 
)

Sets a variable to be a hard group.

This function is used for lazy sifting.

Returns:
1 if successful; 0 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddSetVarToBeGrouped Cudd_bddResetVarToBeGrouped Cudd_bddIsVarHardGroup
int Cudd_bddSetVarToBeGrouped ( DdManager dd,
int  index 
)

Sets a variable to be grouped.

This function is used for lazy sifting.

Returns:
1 if successful; 0 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddSetVarHardGroup Cudd_bddResetVarToBeGrouped
int Cudd_bddSetVarToBeUngrouped ( DdManager dd,
int  index 
)

Sets a variable to be ungrouped.

This function is used for lazy sifting.

Returns:
1 if successful; 0 otherwise.
Side effects
modifies the manager
See also:
Cudd_bddIsVarToBeUngrouped
int Cudd_bddUnbindVar ( DdManager dd,
int  index 
)

Allows the sifting of a variable.

This function resets the flag that prevents the sifting of a variable. In successive variable reorderings, the variable will NOT be skipped, that is, sifted. Initially all variables can be sifted. It is necessary to call this function only to re-enable sifting after a call to Cudd_bddBindVar.

Returns:
1 if successful; 0 otherwise (i.e., invalid variable index).
Side effects
Changes the "bindVar" flag in DdSubtable.
See also:
Cudd_bddBindVar
Parameters:
dd manager
index variable index
int Cudd_bddVarIsBound ( DdManager dd,
int  index 
)

Tells whether a variable can be sifted.

This function returns 1 if a variable is enabled for sifting. Initially all variables can be sifted. This function returns 0 if there has been a previous call to Cudd_bddBindVar for that variable not followed by a call to Cudd_bddUnbindVar. The function returns 0 also in the case in which the index of the variable is out of bounds.

Side effects
none
See also:
Cudd_bddBindVar Cudd_bddUnbindVar
Parameters:
dd manager
index variable index
void Cudd_ClearErrorCode ( DdManager dd  ) 

Clear the error code of a manager.

Side effects
None
See also:
Cudd_ReadErrorCode
int Cudd_DeadAreCounted ( DdManager dd  ) 

Tells whether dead nodes are counted towards triggering reordering.

Returns:
1 if dead nodes are counted; 0 otherwise.
Side effects
None
See also:
Cudd_TurnOnCountDead Cudd_TurnOffCountDead
void Cudd_DisableGarbageCollection ( DdManager dd  ) 

Disables garbage collection.

Garbage collection is initially enabled. This function may be called to disable it. However, garbage collection will still occur when a new node must be created and no memory is left, or when garbage collection is required for correctness. (E.g., before reordering.)

Side effects
None
See also:
Cudd_EnableGarbageCollection Cudd_GarbageCollectionEnabled
int Cudd_DisableOrderingMonitoring ( DdManager dd  ) 

Disables monitoring of ordering.

Returns:
1 if successful; 0 otherwise.
Side effects
Removes functions from the pre-reordering and post-reordering hooks.
See also:
Cudd_EnableOrderingMonitoring
int Cudd_DisableReorderingReporting ( DdManager dd  ) 

Disables reporting of reordering stats.

Returns:
1 if successful; 0 otherwise.
Side effects
Removes functions from the pre-reordering and post-reordering hooks.
See also:
Cudd_EnableReorderingReporting Cudd_ReorderingReporting
DdNode* Cudd_E ( DdNode node  ) 

Returns the else child of an internal node.

If node is a constant node, the result is unpredictable.

Side effects
none
See also:
Cudd_T Cudd_V
void Cudd_EnableGarbageCollection ( DdManager dd  ) 

Enables garbage collection.

Garbage collection is initially enabled. Therefore it is necessary to call this function only if garbage collection has been explicitly disabled.

Side effects
None
See also:
Cudd_DisableGarbageCollection Cudd_GarbageCollectionEnabled
int Cudd_EnableOrderingMonitoring ( DdManager dd  ) 

Enables monitoring of ordering.

Returns:
1 if successful; 0 otherwise.
Side effects
Installs functions in the pre-reordering and post-reordering hooks.
See also:
Cudd_EnableReorderingReporting
int Cudd_EnableReorderingReporting ( DdManager dd  ) 

Enables reporting of reordering stats.

Returns:
1 if successful; 0 otherwise.
Side effects
Installs functions in the pre-reordering and post-reordering hooks.
See also:
Cudd_DisableReorderingReporting Cudd_ReorderingReporting
double Cudd_ExpectedUsedSlots ( DdManager dd  ) 

Computes the expected fraction of used slots in the unique table.

This expected value is based on the assumption that the hash function distributes the keys randomly; it can be compared with the result of Cudd_ReadUsedSlots to monitor the performance of the unique table hash function.

Side effects
None
See also:
Cudd_ReadSlots Cudd_ReadUsedSlots
void Cudd_FreeTree ( DdManager dd  ) 

Frees the variable group tree of the manager.

Side effects
None
See also:
Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree
void Cudd_FreeZddTree ( DdManager dd  ) 

Frees the variable group tree of the manager.

Side effects
None
See also:
Cudd_SetZddTree Cudd_ReadZddTree Cudd_FreeTree
int Cudd_GarbageCollectionEnabled ( DdManager dd  ) 

Tells whether garbage collection is enabled.

Returns:
1 if garbage collection is enabled; 0 otherwise.
Side effects
None
See also:
Cudd_EnableGarbageCollection Cudd_DisableGarbageCollection
void Cudd_IncreaseTimeLimit ( DdManager unique,
unsigned long  increase 
)

Increases the time limit for the manager.

The time increase must be expressed in milliseconds.

Side effects
None
See also:
Cudd_ReadTimeLimit Cudd_SetTimeLimit Cudd_UnsetTimeLimit Cudd_UpdateTimeLimit Cudd_TimeLimited Cudd_SetStartTime
DD_OOMFP Cudd_InstallOutOfMemoryHandler ( DD_OOMFP  newHandler  ) 

Installs a handler for failed memory allocations.

Changing the handler only has an effect if the wrappers in safe_mem.c are in use.

Returns:
the current handler.
int Cudd_IsConstant ( DdNode node  ) 

Returns 1 if the node is a constant node.

A constant node is not an internal node. The pointer passed to Cudd_IsConstant may be either regular or complemented.

Side effects
none
int Cudd_IsInHook ( DdManager dd,
DD_HFP  f,
Cudd_HookType  where 
)

Checks whether a function is in a hook.

A hook is a list of application-provided functions called on certain occasions by the package.

Returns:
1 if the function is found; 0 otherwise.
Side effects
None
See also:
Cudd_AddHook Cudd_RemoveHook
int Cudd_IsNonConstant ( DdNode f  ) 

Returns 1 if a DD node is not constant.

This function is useful to test the results of Cudd_bddIteConstant, Cudd_addIteConstant, Cudd_addEvalConst. These results may be a special value signifying non-constant. In the other cases Cudd_IsConstant can be used.

Side effects
None
See also:
Cudd_IsConstant Cudd_bddIteConstant Cudd_addIteConstant Cudd_addEvalConst
unsigned int Cudd_NodeReadIndex ( DdNode node  ) 

Returns the index of the node.

The node pointer can be either regular or complemented.

Side effects
None
See also:
Cudd_ReadIndex
int Cudd_OrderingMonitoring ( DdManager dd  ) 

Returns 1 if monitoring of ordering is enabled; 0 otherwise.

Side effects
none
See also:
Cudd_EnableOrderingMonitoring Cudd_DisableOrderingMonitoring
int Cudd_PrintGroupedOrder ( DdManager dd,
const char *  str,
void *  data 
)

Hook function to print the current variable order.

It may be called before or after reordering. Prints on the manager's stdout a parenthesized list that describes the variable groups.

Returns:
1 if successful; 0 otherwise.
Side effects
None
See also:
Cudd_StdPreReordHook
int Cudd_PrintInfo ( DdManager dd,
FILE *  fp 
)

Prints out statistics and settings for a CUDD manager.

Returns:
1 if successful; 0 otherwise.
Side effects
None
void* Cudd_ReadApplicationHook ( DdManager dd  ) 

Reads the application hook.

Side effects
None
See also:
Cudd_SetApplicationHook
int Cudd_ReadArcviolation ( DdManager dd  ) 

Returns the current value of the arcviolation parameter used in group sifting.

This parameter is used to decide how many arcs into y not coming from x are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.

Side effects
None
See also:
Cudd_SetArcviolation
DdNode* Cudd_ReadBackground ( DdManager dd  ) 

Reads the background constant of the manager.

Side effects
None
double Cudd_ReadCacheHits ( DdManager dd  ) 

Returns the number of cache hits.

Side effects
None
See also:
Cudd_ReadCacheLookUps
double Cudd_ReadCacheLookUps ( DdManager dd  ) 

Returns the number of cache look-ups.

Side effects
None
See also:
Cudd_ReadCacheHits
unsigned int Cudd_ReadCacheSlots ( DdManager dd  ) 

Reads the number of slots in the cache.

Side effects
None
See also:
Cudd_ReadCacheUsedSlots
double Cudd_ReadCacheUsedSlots ( DdManager dd  ) 

Reads the fraction of used slots in the cache.

The unused slots are those in which no valid data is stored. Garbage collection, variable reordering, and cache resizing may cause used slots to become unused.

Side effects
None
See also:
Cudd_ReadCacheSlots
unsigned int Cudd_ReadDead ( DdManager dd  ) 

Returns the number of dead nodes in the unique table.

Side effects
None
See also:
Cudd_ReadKeys
unsigned long Cudd_ReadElapsedTime ( DdManager unique  ) 

Returns the time elapsed since the start time of the manager.

The time is expressed in milliseconds.

Side effects
None
See also:
Cudd_ReadStartTime Cudd_SetStartTime
CUDD_VALUE_TYPE Cudd_ReadEpsilon ( DdManager dd  ) 

Reads the epsilon parameter of the manager.

The epsilon parameter control the comparison between floating point numbers.

Side effects
None
See also:
Cudd_SetEpsilon
Cudd_ErrorType Cudd_ReadErrorCode ( DdManager dd  ) 

Returns the code of the last error.

The error codes are defined in cudd.h.

Side effects
None
See also:
Cudd_ClearErrorCode
int Cudd_ReadGarbageCollections ( DdManager dd  ) 

Returns the number of times garbage collection has occurred.

The number includes both the calls from reordering procedures and those caused by requests to create new nodes.

Side effects
None
See also:
Cudd_ReadGarbageCollectionTime
long Cudd_ReadGarbageCollectionTime ( DdManager dd  ) 

Returns the time spent in garbage collection.

Returns the number of milliseconds spent doing garbage collection since the manager was initialized.

Side effects
None
See also:
Cudd_ReadGarbageCollections
Cudd_AggregationType Cudd_ReadGroupcheck ( DdManager dd  ) 

Reads the groupcheck parameter of the manager.

The groupcheck parameter determines the aggregation criterion in group sifting.

Side effects
None
See also:
Cudd_SetGroupcheck
int Cudd_ReadInvPerm ( DdManager dd,
int  i 
)

Returns the index of the variable currently in the i-th position of the order.

If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.

Side effects
None
See also:
Cudd_ReadPerm Cudd_ReadInvPermZdd
int Cudd_ReadInvPermZdd ( DdManager dd,
int  i 
)

Returns the index of the ZDD variable currently in the i-th position of the order.

If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.

Side effects
None
See also:
Cudd_ReadPerm Cudd_ReadInvPermZdd
unsigned int Cudd_ReadKeys ( DdManager dd  ) 

Returns the number of nodes in the unique table.

Returns the total number of nodes currently in the unique table, including the dead nodes.

Side effects
None
See also:
Cudd_ReadDead
DdNode* Cudd_ReadLogicZero ( DdManager dd  ) 

Returns the logic zero constant of the manager.

The logic zero constant is the complement of the one constant, and is distinct from the arithmetic zero.

Side effects
None
See also:
Cudd_ReadOne Cudd_ReadZero
unsigned int Cudd_ReadLooseUpTo ( DdManager dd  ) 

Reads the looseUpTo parameter of the manager.

Side effects
None
See also:
Cudd_SetLooseUpTo Cudd_ReadMinHit Cudd_ReadMinDead
unsigned int Cudd_ReadMaxCache ( DdManager dd  ) 

Returns the soft limit for the cache size.

Side effects
None
See also:
Cudd_ReadMaxCacheHard
unsigned int Cudd_ReadMaxCacheHard ( DdManager dd  ) 

Reads the maxCacheHard parameter of the manager.

Side effects
None
See also:
Cudd_SetMaxCacheHard Cudd_ReadMaxCache
double Cudd_ReadMaxGrowth ( DdManager dd  ) 

Reads the maxGrowth parameter of the manager.

This parameter determines how much the number of nodes can grow during sifting of a variable. Overall, sifting never increases the size of the decision diagrams. This parameter only refers to intermediate results. A lower value will speed up sifting, possibly at the expense of quality.

Side effects
None
See also:
Cudd_SetMaxGrowth Cudd_ReadMaxGrowthAlternate
double Cudd_ReadMaxGrowthAlternate ( DdManager dd  ) 

Reads the maxGrowthAlt parameter of the manager.

This parameter is analogous to the maxGrowth paramter, and is used every given number of reorderings instead of maxGrowth. The number of reorderings is set with Cudd_SetReorderingCycle. If the number of reorderings is 0 (default) maxGrowthAlt is never used.

Side effects
None
See also:
Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate Cudd_SetReorderingCycle Cudd_ReadReorderingCycle
unsigned int Cudd_ReadMaxIndex ( void   ) 

Returns the maximum possible index for a variable.

Side effects
None
unsigned int Cudd_ReadMaxLive ( DdManager dd  ) 

Reads the maximum allowed number of live nodes.

When this number is exceeded, the package returns NULL.

Side effects
none
See also:
Cudd_SetMaxLive
size_t Cudd_ReadMaxMemory ( DdManager dd  ) 

Reads the maximum allowed memory.

When this number is exceeded, the package returns NULL.

Side effects
none
See also:
Cudd_SetMaxMemory
unsigned int Cudd_ReadMaxReorderings ( DdManager dd  ) 

Returns the maximum number of times reordering may be invoked.

Side effects
None
See also:
Cudd_ReadReorderings Cudd_SetMaxReorderings Cudd_ReduceHeap
size_t Cudd_ReadMemoryInUse ( DdManager dd  ) 

Returns the memory in use by the manager measured in bytes.

Side effects
None
unsigned int Cudd_ReadMinDead ( DdManager dd  ) 

Reads the minDead parameter of the manager.

The minDead parameter is used by the package to decide whether to collect garbage or resize a subtable of the unique table when the subtable becomes too full. The application can indirectly control the value of minDead by setting the looseUpTo parameter.

Side effects
None
See also:
Cudd_ReadDead Cudd_ReadLooseUpTo Cudd_SetLooseUpTo
unsigned int Cudd_ReadMinHit ( DdManager dd  ) 

Reads the hit rate that causes resizinig of the computed table.

Side effects
None
See also:
Cudd_SetMinHit
DdNode* Cudd_ReadMinusInfinity ( DdManager dd  ) 

Reads the minus-infinity constant from the manager.

Side effects
None
unsigned int Cudd_ReadNextReordering ( DdManager dd  ) 

Returns the threshold for the next dynamic reordering.

The threshold is in terms of number of nodes and is in effect only if reordering is enabled. The count does not include the dead nodes, unless the countDead parameter of the manager has been changed from its default setting.

Side effects
None
See also:
Cudd_SetNextReordering
long Cudd_ReadNodeCount ( DdManager dd  ) 

Reports the number of nodes in BDDs and ADDs.

This number does not include the isolated projection functions and the unused constants. These nodes that are not counted are not part of the DDs manipulated by the application.

Side effects
None
See also:
Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount
double Cudd_ReadNodesDropped ( DdManager dd  ) 

Returns the number of nodes dropped.

Returns the number of nodes killed by dereferencing if the keeping of this statistic is enabled; -1 otherwise. This statistic is enabled only if the package is compiled with DD_STATS defined.

Side effects
None
See also:
Cudd_ReadNodesFreed
double Cudd_ReadNodesFreed ( DdManager dd  ) 

Returns the number of nodes freed.

Returns the number of nodes returned to the free list if the keeping of this statistic is enabled; -1 otherwise. This statistic is enabled only if the package is compiled with DD_STATS defined.

Side effects
None
See also:
Cudd_ReadNodesDropped
int Cudd_ReadNumberXovers ( DdManager dd  ) 

Reads the current number of crossovers used by the genetic algorithm for variable reordering.

A larger number of crossovers will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as number of crossovers, with a maximum of 60.

Side effects
None
See also:
Cudd_SetNumberXovers
DdNode* Cudd_ReadOne ( DdManager dd  ) 

Returns the one constant of the manager.

The one constant is common to ADDs and BDDs.

Side effects
None
See also:
Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne
unsigned int Cudd_ReadOrderRandomization ( DdManager dd  ) 

Returns the order randomization factor.

If non-zero this factor is used to determine a perturbation of the next reordering threshold. Larger factors cause larger perturbations.

Side effects
None
See also:
Cudd_SetOrderRandomization
int Cudd_ReadPeakLiveNodeCount ( DdManager dd  ) 

Reports the peak number of live nodes.

Side effects
None
See also:
Cudd_ReadNodeCount Cudd_PrintInfo Cudd_ReadPeakNodeCount
long Cudd_ReadPeakNodeCount ( DdManager dd  ) 

Reports the peak number of nodes.

This number includes node on the free list. At the peak, the number of nodes on the free list is guaranteed to be less than DD_MEM_CHUNK.

Side effects
None
See also:
Cudd_ReadNodeCount Cudd_PrintInfo
int Cudd_ReadPerm ( DdManager dd,
int  i 
)

Returns the current position of the i-th variable in the order.

If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.

Side effects
None
See also:
Cudd_ReadInvPerm Cudd_ReadPermZdd
int Cudd_ReadPermZdd ( DdManager dd,
int  i 
)

Returns the current position of the i-th ZDD variable in the order.

If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.

Side effects
None
See also:
Cudd_ReadInvPermZdd Cudd_ReadPerm
DdNode* Cudd_ReadPlusInfinity ( DdManager dd  ) 

Reads the plus-infinity constant from the manager.

Side effects
None
int Cudd_ReadPopulationSize ( DdManager dd  ) 

Reads the current size of the population used by the genetic algorithm for variable reordering.

A larger population size will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as population size, with a maximum of 120.

Side effects
None
See also:
Cudd_SetPopulationSize
int Cudd_ReadRecomb ( DdManager dd  ) 

Returns the current value of the recombination parameter used in group sifting.

A larger (positive) value makes the aggregation of variables due to the second difference criterion more likely. A smaller (negative) value makes aggregation less likely.

Side effects
None
See also:
Cudd_SetRecomb
double Cudd_ReadRecursiveCalls ( DdManager dd  ) 

Returns the number of recursive calls.

Returns the number of recursive calls if the package is compiled with DD_COUNT defined.

Side effects
None
int Cudd_ReadReorderingCycle ( DdManager dd  ) 

Reads the reordCycle parameter of the manager.

This parameter determines how often the alternate threshold on maximum growth is used in reordering.

Side effects
None
See also:
Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate Cudd_SetReorderingCycle
unsigned int Cudd_ReadReorderings ( DdManager dd  ) 

Returns the number of times reordering has occurred.

The number includes both the calls to Cudd_ReduceHeap from the application program and those automatically performed by the package. However, calls that do not even initiate reordering are not counted. A call may not initiate reordering if there are fewer than minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified as reordering method. The calls to Cudd_ShuffleHeap are not counted.

Side effects
None
See also:
Cudd_ReduceHeap Cudd_ReadReorderingTime
long Cudd_ReadReorderingTime ( DdManager dd  ) 

Returns the time spent in reordering.

Returns the number of milliseconds spent reordering variables since the manager was initialized. The time spent in collecting garbage before reordering is included.

Side effects
None
See also:
Cudd_ReadReorderings
int Cudd_ReadSiftMaxSwap ( DdManager dd  ) 

Reads the siftMaxSwap parameter of the manager.

This parameter gives the maximum number of swaps that will be attempted for each invocation of sifting. The real number of swaps may exceed the set limit because the package will always complete the sifting of the variable that causes the limit to be reached.

Side effects
None
See also:
Cudd_ReadSiftMaxVar Cudd_SetSiftMaxSwap
int Cudd_ReadSiftMaxVar ( DdManager dd  ) 

Reads the siftMaxVar parameter of the manager.

This parameter gives the maximum number of variables that will be sifted for each invocation of sifting.

Side effects
None
See also:
Cudd_ReadSiftMaxSwap Cudd_SetSiftMaxVar
int Cudd_ReadSize ( DdManager dd  ) 

Returns the number of BDD variables in existance.

Side effects
None
See also:
Cudd_ReadZddSize
unsigned int Cudd_ReadSlots ( DdManager dd  ) 

Returns the total number of slots of the unique table.

This number is mainly for diagnostic purposes.

Side effects
None
unsigned long Cudd_ReadStartTime ( DdManager unique  ) 

Returns the start time of the manager.

This is initially set to the number of milliseconds since the program started, but may be reset by the application.

Side effects
None
See also:
Cudd_SetStartTime Cudd_ResetStartTime Cudd_ReadTimeLimit
FILE* Cudd_ReadStderr ( DdManager dd  ) 

Reads the stderr of a manager.

This is the file pointer to which messages normally going to stderr are written. It is initialized to stderr. Cudd_SetStderr allows the application to redirect it.

Side effects
None
See also:
Cudd_SetStderr Cudd_ReadStdout
FILE* Cudd_ReadStdout ( DdManager dd  ) 

Reads the stdout of a manager.

This is the file pointer to which messages normally going to stdout are written. It is initialized to stdout. Cudd_SetStdout allows the application to redirect it.

Side effects
None
See also:
Cudd_SetStdout Cudd_ReadStderr
double Cudd_ReadSwapSteps ( DdManager dd  ) 

Reads the number of elementary reordering steps.

Side effects
none
int Cudd_ReadSymmviolation ( DdManager dd  ) 

Returns the current value of the symmviolation parameter used in group sifting.

This parameter is used in group sifting to decide how many violations to the symmetry conditions f10 = f01 or f11 = f00 are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.

Side effects
None
See also:
Cudd_SetSymmviolation
unsigned long Cudd_ReadTimeLimit ( DdManager unique  ) 

Returns the time limit for the manager.

This is initially set to a very large number, but may be reset by the application. The time is expressed in milliseconds.

Side effects
None
See also:
Cudd_SetTimeLimit Cudd_UpdateTimeLimit Cudd_UnsetTimeLimit Cudd_IncreaseTimeLimit Cudd_TimeLimited Cudd_ReadStartTime
DD_TOHFP Cudd_ReadTimeoutHandler ( DdManager unique,
void **  argp 
)

Read the current timeout handler function.

Side effects
If argp is non-null, the second argument to the handler is written to the location it points to.
See also:
Cudd_RegisterTimeoutHandler
MtrNode* Cudd_ReadTree ( DdManager dd  ) 

Returns the variable group tree of the manager.

Side effects
None
See also:
Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree
double Cudd_ReadUniqueLinks ( DdManager dd  ) 

Returns the number of links followed in the unique table.

Returns the number of links followed during look-ups in the unique table if the keeping of this statistic is enabled; -1 otherwise. If an item is found in the first position of its collision list, the number of links followed is taken to be 0. If it is in second position, the number of links is 1, and so on. This statistic is enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.

Side effects
None
See also:
Cudd_ReadUniqueLookUps
double Cudd_ReadUniqueLookUps ( DdManager dd  ) 

Returns the number of look-ups in the unique table.

Returns the number of look-ups in the unique table if the keeping of this statistic is enabled; -1 otherwise. This statistic is enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.

Side effects
None
See also:
Cudd_ReadUniqueLinks
double Cudd_ReadUsedSlots ( DdManager dd  ) 

Reads the fraction of used slots in the unique table.

The unused slots are those in which no valid data is stored. Garbage collection, variable reordering, and subtable resizing may cause used slots to become unused.

Side effects
None
See also:
Cudd_ReadSlots
DdNode* Cudd_ReadVars ( DdManager dd,
int  i 
)

Returns the i-th element of the vars array.

Returns the i-th element of the vars array if it falls within the array bounds; NULL otherwise. If i is the index of an existing variable, this function produces the same result as Cudd_bddIthVar. However, if the i-th var does not exist yet, Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.

Side effects
None
See also:
Cudd_bddIthVar
DdNode* Cudd_ReadZddOne ( DdManager dd,
int  i 
)

Returns the ZDD for the constant 1 function.

The representation of the constant 1 function as a ZDD depends on how many variables it (nominally) depends on. The index of the topmost variable in the support is given as argument i.

Side effects
None
See also:
Cudd_ReadOne
int Cudd_ReadZddSize ( DdManager dd  ) 

Returns the number of ZDD variables in existance.

Side effects
None
See also:
Cudd_ReadSize
MtrNode* Cudd_ReadZddTree ( DdManager dd  ) 

Returns the variable group tree of the manager.

Side effects
None
See also:
Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree
DdNode* Cudd_ReadZero ( DdManager dd  ) 

Returns the zero constant of the manager.

The zero constant is the arithmetic zero, rather than the logic zero. The latter is the complement of the one constant.

Side effects
None
See also:
Cudd_ReadOne Cudd_ReadLogicZero
DD_OOMFP Cudd_RegisterOutOfMemoryCallback ( DdManager unique,
DD_OOMFP  callback 
)

Installs an out-of-memory callback.

Registers a callback function that is called when a discretionary memory allocation fails.

Returns:
the old callback function.
Side effects
None
See also:
Cudd_UnregisterOutOfMemoryCallback Cudd_OutOfMem Cudd_OutOfMemSilent
void Cudd_RegisterTerminationCallback ( DdManager unique,
DD_THFP  callback,
void *  callback_arg 
)

Installs a termination callback.

Registers a callback function that is called from time to time to decide whether computation should be abandoned.

Side effects
None
See also:
Cudd_UnregisterTerminationCallback
void Cudd_RegisterTimeoutHandler ( DdManager unique,
DD_TOHFP  handler,
void *  arg 
)

Register a timeout handler function.

To unregister a handler, register a NULL pointer.

Side effects
None
See also:
Cudd_ReadTimeoutHandler
int Cudd_RemoveHook ( DdManager dd,
DD_HFP  f,
Cudd_HookType  where 
)

Removes a function from a hook.

A hook is a list of application-provided functions called on certain occasions by the package.

Returns:
1 if successful; 0 the function was not in the list.
Side effects
None
See also:
Cudd_AddHook
int Cudd_ReorderingReporting ( DdManager dd  ) 

Returns 1 if reporting of reordering stats is enabled; 0 otherwise.

Side effects
none
See also:
Cudd_EnableReorderingReporting Cudd_DisableReorderingReporting
int Cudd_ReorderingStatus ( DdManager unique,
Cudd_ReorderingType method 
)

Reports the status of automatic dynamic reordering of BDDs and ADDs.

The location pointed by parameter method is set to the reordering method currently selected if method is non-null.

Returns:
1 if automatic reordering is enabled; 0 otherwise.
Side effects
The location pointed by parameter method is set to the reordering method currently selected if method is non-null.
See also:
Cudd_AutodynEnable Cudd_AutodynDisable Cudd_ReorderingStatusZdd
int Cudd_ReorderingStatusZdd ( DdManager unique,
Cudd_ReorderingType method 
)

Reports the status of automatic dynamic reordering of ZDDs.

Parameter method is set to the ZDD reordering method currently selected.

Returns:
1 if automatic reordering is enabled; 0 otherwise.
Side effects
Parameter method is set to the ZDD reordering method currently selected.
See also:
Cudd_AutodynEnableZdd Cudd_AutodynDisableZdd Cudd_ReorderingStatus
void Cudd_ResetStartTime ( DdManager unique  ) 

Resets the start time of the manager.

Side effects
None
See also:
Cudd_ReadStartTime Cudd_SetStartTime Cudd_SetTimeLimit
void Cudd_SetApplicationHook ( DdManager dd,
void *  value 
)

Sets the application hook.

Side effects
None
See also:
Cudd_ReadApplicationHook
void Cudd_SetArcviolation ( DdManager dd,
int  arcviolation 
)

Sets the value of the arcviolation parameter used in group sifting.

This parameter is used to decide how many arcs into y not coming from x are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.

Side effects
None
See also:
Cudd_ReadArcviolation
void Cudd_SetBackground ( DdManager dd,
DdNode bck 
)

Sets the background constant of the manager.

It assumes that the DdNode pointer bck is already referenced.

Side effects
None
void Cudd_SetEpsilon ( DdManager dd,
CUDD_VALUE_TYPE  ep 
)

Sets the epsilon parameter of the manager to ep.

The epsilon parameter control the comparison between floating point numbers.

Side effects
None
See also:
Cudd_ReadEpsilon
void Cudd_SetGroupcheck ( DdManager dd,
Cudd_AggregationType  gc 
)

Sets the parameter groupcheck of the manager to gc.

The groupcheck parameter determines the aggregation criterion in group sifting.

Side effects
None
See also:
Cudd_ReadGroupCheck
void Cudd_SetLooseUpTo ( DdManager dd,
unsigned int  lut 
)

Sets the looseUpTo parameter of the manager.

This parameter of the manager controls the threshold beyond which no fast growth of the unique table is allowed. The threshold is given as a number of slots. If the value passed to this function is 0, the function determines a suitable value based on the available memory.

Side effects
None
See also:
Cudd_ReadLooseUpTo Cudd_SetMinHit
void Cudd_SetMaxCacheHard ( DdManager dd,
unsigned int  mc 
)

Sets the maxCacheHard parameter of the manager.

The cache cannot grow larger than maxCacheHard entries. This parameter allows an application to control the trade-off of memory versus speed. If the value passed to this function is 0, the function determines a suitable maximum cache size based on the available memory.

Side effects
None
See also:
Cudd_ReadMaxCacheHard Cudd_SetMaxCache
void Cudd_SetMaxGrowth ( DdManager dd,
double  mg 
)

Sets the maxGrowth parameter of the manager.

This parameter determines how much the number of nodes can grow during sifting of a variable. Overall, sifting never increases the size of the decision diagrams. This parameter only refers to intermediate results. A lower value will speed up sifting, possibly at the expense of quality.

Side effects
None
See also:
Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate
void Cudd_SetMaxGrowthAlternate ( DdManager dd,
double  mg 
)

Sets the maxGrowthAlt parameter of the manager.

This parameter is analogous to the maxGrowth paramter, and is used every given number of reorderings instead of maxGrowth. The number of reorderings is set with Cudd_SetReorderingCycle. If the number of reorderings is 0 (default) maxGrowthAlt is never used.

Side effects
None
See also:
Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowth Cudd_SetReorderingCycle Cudd_ReadReorderingCycle
void Cudd_SetMaxLive ( DdManager dd,
unsigned int  maxLive 
)

Sets the maximum allowed number of live nodes.

When this number is exceeded, the package returns NULL.

Side effects
none
See also:
Cudd_ReadMaxLive
size_t Cudd_SetMaxMemory ( DdManager dd,
size_t  maxMemory 
)

Sets the maximum allowed memory.

When this number is exceeded, the package returns NULL.

Returns:
the previous limit.
Side effects
none
See also:
Cudd_ReadMaxMemory
void Cudd_SetMaxReorderings ( DdManager dd,
unsigned int  mr 
)

Sets the maximum number of times reordering may be invoked.

The default value is (practically) infinite.

Side effects
None
See also:
Cudd_ReadReorderings Cudd_ReadMaxReorderings Cudd_ReduceHeap
void Cudd_SetMinHit ( DdManager dd,
unsigned int  hr 
)

Sets the hit rate that causes resizinig of the computed table.

Sets the minHit parameter of the manager. This parameter controls the resizing of the computed table. If the hit rate is larger than the specified value, and the cache is not already too large, then its size is doubled.

Side effects
None
See also:
Cudd_ReadMinHit
void Cudd_SetNextReordering ( DdManager dd,
unsigned int  next 
)

Sets the threshold for the next dynamic reordering.

The threshold is in terms of number of nodes and is in effect only if reordering is enabled. The count does not include the dead nodes, unless the countDead parameter of the manager has been changed from its default setting.

Side effects
None
See also:
Cudd_ReadNextReordering
void Cudd_SetNumberXovers ( DdManager dd,
int  numberXovers 
)

Sets the number of crossovers used by the genetic algorithm for variable reordering.

A larger number of crossovers will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as number of crossovers, with a maximum of 60.

Side effects
None
See also:
Cudd_ReadNumberXovers
void Cudd_SetOrderRandomization ( DdManager dd,
unsigned int  factor 
)

Sets the order randomization factor.

Side effects
None
See also:
Cudd_ReadOrderRandomization
void Cudd_SetPopulationSize ( DdManager dd,
int  populationSize 
)

Sets the size of the population used by the genetic algorithm for variable reordering.

A larger population size will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as population size, with a maximum of 120.

Side effects
Changes the manager.
See also:
Cudd_ReadPopulationSize
void Cudd_SetRecomb ( DdManager dd,
int  recomb 
)

Sets the value of the recombination parameter used in group sifting.

A larger (positive) value makes the aggregation of variables due to the second difference criterion more likely. A smaller (negative) value makes aggregation less likely. The default value is 0.

Side effects
Changes the manager.
See also:
Cudd_ReadRecomb
void Cudd_SetReorderingCycle ( DdManager dd,
int  cycle 
)

Sets the reordCycle parameter of the manager.

This parameter determines how often the alternate threshold on maximum growth is used in reordering.

Side effects
None
See also:
Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate Cudd_ReadReorderingCycle
void Cudd_SetSiftMaxSwap ( DdManager dd,
int  sms 
)

Sets the siftMaxSwap parameter of the manager.

This parameter gives the maximum number of swaps that will be attempted for each invocation of sifting. The real number of swaps may exceed the set limit because the package will always complete the sifting of the variable that causes the limit to be reached.

Side effects
None
See also:
Cudd_SetSiftMaxVar Cudd_ReadSiftMaxSwap
void Cudd_SetSiftMaxVar ( DdManager dd,
int  smv 
)

Sets the siftMaxVar parameter of the manager.

This parameter gives the maximum number of variables that will be sifted for each invocation of sifting.

Side effects
None
See also:
Cudd_SetSiftMaxSwap Cudd_ReadSiftMaxVar
void Cudd_SetStartTime ( DdManager unique,
unsigned long  st 
)

Sets the start time of the manager.

The time must be expressed in milliseconds.

Side effects
None
See also:
Cudd_ReadStartTime Cudd_ResetStartTime Cudd_ReadElapsedTime Cudd_SetTimeLimit
void Cudd_SetStderr ( DdManager dd,
FILE *  fp 
)

Sets the stderr of a manager.

Side effects
None
See also:
Cudd_ReadStderr Cudd_SetStdout
void Cudd_SetStdout ( DdManager dd,
FILE *  fp 
)

Sets the stdout of a manager.

Side effects
None
See also:
Cudd_ReadStdout Cudd_SetStderr
void Cudd_SetSymmviolation ( DdManager dd,
int  symmviolation 
)

Sets the value of the symmviolation parameter used in group sifting.

This parameter is used in group sifting to decide how many violations to the symmetry conditions f10 = f01 or f11 = f00 are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.

Side effects
Changes the manager.
See also:
Cudd_ReadSymmviolation
unsigned long Cudd_SetTimeLimit ( DdManager unique,
unsigned long  tl 
)

Sets the time limit for the manager.

The time must be expressed in milliseconds.

Returns:
the old time limit.
Side effects
None
See also:
Cudd_ReadTimeLimit Cudd_UnsetTimeLimit Cudd_UpdateTimeLimit Cudd_IncreaseTimeLimit Cudd_TimeLimited Cudd_SetStartTime
void Cudd_SetTree ( DdManager dd,
MtrNode tree 
)

Sets the variable group tree of the manager.

Side effects
None
See also:
Cudd_FreeTree Cudd_ReadTree Cudd_SetZddTree
void Cudd_SetZddTree ( DdManager dd,
MtrNode tree 
)

Sets the ZDD variable group tree of the manager.

Side effects
None
See also:
Cudd_FreeZddTree Cudd_ReadZddTree Cudd_SetTree
int Cudd_StdPostReordHook ( DdManager dd,
const char *  str,
void *  data 
)

Sample hook function to call after reordering.

Prints on the manager's stdout final size and reordering time.

Returns:
1 if successful; 0 otherwise.
Side effects
None
See also:
Cudd_StdPreReordHook
int Cudd_StdPreReordHook ( DdManager dd,
const char *  str,
void *  data 
)

Sample hook function to call before reordering.

Prints on the manager's stdout reordering method and initial size.

Returns:
1 if successful; 0 otherwise.
Side effects
None
See also:
Cudd_StdPostReordHook
DdNode* Cudd_T ( DdNode node  ) 

Returns the then child of an internal node.

If node is a constant node, the result is unpredictable.

Side effects
none
See also:
Cudd_E Cudd_V
int Cudd_TimeLimited ( DdManager unique  ) 

Returns true if the time limit for the manager is set.

Side effects
None
See also:
Cudd_ReadTimeLimit Cudd_SetTimeLimit Cudd_UpdateTimeLimit Cudd_UnsetTimeLimit Cudd_IncreaseTimeLimit
void Cudd_TurnOffCountDead ( DdManager dd  ) 

Causes the dead nodes not to be counted towards triggering reordering.

This causes less frequent reorderings. By default dead nodes are not counted. Therefore there is no need to call this function unless Cudd_TurnOnCountDead has been previously called.

Side effects
Changes the manager.
See also:
Cudd_TurnOnCountDead Cudd_DeadAreCounted
void Cudd_TurnOnCountDead ( DdManager dd  ) 

Causes the dead nodes to be counted towards triggering reordering.

This causes more frequent reorderings. By default dead nodes are not counted.

Side effects
Changes the manager.
See also:
Cudd_TurnOffCountDead Cudd_DeadAreCounted
void Cudd_UnregisterOutOfMemoryCallback ( DdManager unique  ) 

Unregister an out-of-memory callback.

Side effects
None
See also:
Cudd_RegisterOutOfMemoryCallback Cudd_OutOfMem Cudd_OutOfMemSilent
void Cudd_UnregisterTerminationCallback ( DdManager unique  ) 

Unregisters a termination callback.

Side effects
None
See also:
Cudd_RegisterTerminationCallback
void Cudd_UnsetTimeLimit ( DdManager unique  ) 

Unsets the time limit for the manager.

Actually, sets it to a very large value.

Side effects
None
See also:
Cudd_ReadTimeLimit Cudd_SetTimeLimit Cudd_UpdateTimeLimit Cudd_IncreaseTimeLimit Cudd_TimeLimited Cudd_SetStartTime
void Cudd_UpdateTimeLimit ( DdManager unique  ) 

Updates the time limit for the manager.

Updates the time limit for the manager by subtracting the elapsed time from it.

Side effects
None
See also:
Cudd_ReadTimeLimit Cudd_SetTimeLimit Cudd_UnsetTimeLimit Cudd_IncreaseTimeLimit Cudd_TimeLimited Cudd_SetStartTime
CUDD_VALUE_TYPE Cudd_V ( DdNode node  ) 

Returns the value of a constant node.

If node is an internal node, the result is unpredictable.

Side effects
none
See also:
Cudd_T Cudd_E
DdNode* Cudd_zddIthVar ( DdManager dd,
int  i 
)

Returns the ZDD variable with index i.

Retrieves the ZDD variable with index i if it already exists, or creates a new ZDD variable.

Returns:
a pointer to the variable if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddIthVar Cudd_addIthVar
long Cudd_zddReadNodeCount ( DdManager dd  ) 

Reports the number of nodes in ZDDs.

This number always includes the two constants 1 and 0.

Side effects
None
See also:
Cudd_ReadPeakNodeCount Cudd_ReadNodeCount
void Cudd_zddRealignDisable ( DdManager unique  ) 

Disables realignment of ZDD order to BDD order.

Side effects
None
See also:
Cudd_zddRealignEnable Cudd_zddRealignmentEnabled Cudd_bddRealignEnable Cudd_bddRealignmentEnabled
void Cudd_zddRealignEnable ( DdManager unique  ) 

Enables realignment of ZDD order to BDD order.

Enables realignment of the ZDD variable order to the BDD variable order after the BDDs and ADDs have been reordered. The number of ZDD variables must be a multiple of the number of BDD variables for realignment to make sense. If this condition is not met, Cudd_ReduceHeap will return 0. Let M be the ratio of the two numbers. For the purpose of realignment, the ZDD variables from M*i to (M+1)*i-1 are reagarded as corresponding to BDD variable i. Realignment is initially disabled.

Side effects
None
See also:
Cudd_ReduceHeap Cudd_zddRealignDisable Cudd_zddRealignmentEnabled Cudd_bddRealignDisable Cudd_bddRealignmentEnabled
int Cudd_zddRealignmentEnabled ( DdManager unique  ) 

Tells whether the realignment of ZDD order to BDD order is enabled.

Returns:
1 if the realignment of ZDD order to BDD order is enabled; 0 otherwise.
Side effects
None
See also:
Cudd_zddRealignEnable Cudd_zddRealignDisable Cudd_bddRealignEnable Cudd_bddRealignDisable
int Cudd_zddVarsFromBddVars ( DdManager dd,
int  multiplicity 
)

Creates one or more ZDD variables for each BDD variable.

If some ZDD variables already exist, only the missing variables are created. Parameter multiplicity allows the caller to control how many variables are created for each BDD variable in existence. For instance, if ZDDs are used to represent covers, two ZDD variables are required for each BDD variable. The order of the BDD variables is transferred to the ZDD variables. If a variable group tree exists for the BDD variables, a corresponding ZDD variable group tree is created by expanding the BDD variable tree. In any case, the ZDD variables derived from the same BDD variable are merged in a ZDD variable group. If a ZDD variable group tree exists, it is freed.

Returns:
1 if successful; 0 otherwise.
Side effects
None
See also:
Cudd_bddNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel
Parameters:
dd DD manager
multiplicity how many ZDD variables are created for each BDD variable
static void fixVarTree ( MtrNode treenode,
int *  perm,
int  size 
) [static]

Fixes a variable group tree.

Side effects
Changes the variable group tree.
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1