Application interface functions. More...

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

Include dependency graph for cuddAPI.c:

Functions
DdNode *	Cudd_addNewVar (DdManager *dd)
	Returns a new ADD variable. More...

DdNode *	Cudd_addNewVarAtLevel (DdManager *dd, int level)
	Returns a new ADD variable at a specified level. More...

DdNode *	Cudd_bddNewVar (DdManager *dd)
	Returns a new BDD variable. More...

DdNode *	Cudd_bddNewVarAtLevel (DdManager *dd, int level)
	Returns a new BDD variable at a specified level. More...

int	Cudd_bddIsVar (DdManager dd, DdNode f)
	Returns 1 if the given node is a BDD variable; 0 otherwise. More...

DdNode *	Cudd_addIthVar (DdManager *dd, int i)
	Returns the ADD variable with index i. More...

DdNode *	Cudd_bddIthVar (DdManager *dd, int i)
	Returns the BDD variable with index i. More...

DdNode *	Cudd_zddIthVar (DdManager *dd, int i)
	Returns the ZDD variable with index i. More...

int	Cudd_zddVarsFromBddVars (DdManager *dd, int multiplicity)
	Creates one or more ZDD variables for each BDD variable. More...

unsigned int	Cudd_ReadMaxIndex (void)
	Returns the maximum possible index for a variable. More...

DdNode *	Cudd_addConst (DdManager *dd, CUDD_VALUE_TYPE c)
	Returns the ADD for constant c. More...

int	Cudd_IsConstant (DdNode *node)
	Returns 1 if the node is a constant node. More...

int	Cudd_IsNonConstant (DdNode *f)
	Returns 1 if a DD node is not constant. More...

DdNode *	Cudd_T (DdNode *node)
	Returns the then child of an internal node. More...

DdNode *	Cudd_E (DdNode *node)
	Returns the else child of an internal node. More...

CUDD_VALUE_TYPE	Cudd_V (DdNode *node)
	Returns the value of a constant node. More...

unsigned long	Cudd_ReadStartTime (DdManager *unique)
	Returns the start time of the manager. More...

unsigned long	Cudd_ReadElapsedTime (DdManager *unique)
	Returns the time elapsed since the start time of the manager. More...

void	Cudd_SetStartTime (DdManager *unique, unsigned long st)
	Sets the start time of the manager. More...

void	Cudd_ResetStartTime (DdManager *unique)
	Resets the start time of the manager. More...

unsigned long	Cudd_ReadTimeLimit (DdManager *unique)
	Returns the time limit for the manager. More...

unsigned long	Cudd_SetTimeLimit (DdManager *unique, unsigned long tl)
	Sets the time limit for the manager. More...

void	Cudd_UpdateTimeLimit (DdManager *unique)
	Updates the time limit for the manager. More...

void	Cudd_IncreaseTimeLimit (DdManager *unique, unsigned long increase)
	Increases the time limit for the manager. More...

void	Cudd_UnsetTimeLimit (DdManager *unique)
	Unsets the time limit for the manager. More...

int	Cudd_TimeLimited (DdManager *unique)
	Returns true if the time limit for the manager is set. More...

void	Cudd_RegisterTerminationCallback (DdManager unique, DD_THFP callback, void callback_arg)
	Installs a termination callback. More...

void	Cudd_UnregisterTerminationCallback (DdManager *unique)
	Unregisters a termination callback. More...

DD_OOMFP	Cudd_RegisterOutOfMemoryCallback (DdManager *unique, DD_OOMFP callback)
	Installs an out-of-memory callback. More...

void	Cudd_UnregisterOutOfMemoryCallback (DdManager *unique)
	Unregister an out-of-memory callback. More...

void	Cudd_RegisterTimeoutHandler (DdManager unique, DD_TOHFP handler, void arg)
	Register a timeout handler function. More...

DD_TOHFP	Cudd_ReadTimeoutHandler (DdManager unique, void *argp)
	Read the current timeout handler function. More...

void	Cudd_AutodynEnable (DdManager *unique, Cudd_ReorderingType method)
	Enables automatic dynamic reordering of BDDs and ADDs. More...

void	Cudd_AutodynDisable (DdManager *unique)
	Disables automatic dynamic reordering. More...

int	Cudd_ReorderingStatus (DdManager unique, Cudd_ReorderingType method)
	Reports the status of automatic dynamic reordering of BDDs and ADDs. More...

void	Cudd_AutodynEnableZdd (DdManager *unique, Cudd_ReorderingType method)
	Enables automatic dynamic reordering of ZDDs. More...

void	Cudd_AutodynDisableZdd (DdManager *unique)
	Disables automatic dynamic reordering of ZDDs. More...

int	Cudd_ReorderingStatusZdd (DdManager unique, Cudd_ReorderingType method)
	Reports the status of automatic dynamic reordering of ZDDs. More...

int	Cudd_zddRealignmentEnabled (DdManager *unique)
	Tells whether the realignment of ZDD order to BDD order is enabled. More...

void	Cudd_zddRealignEnable (DdManager *unique)
	Enables realignment of ZDD order to BDD order. More...

void	Cudd_zddRealignDisable (DdManager *unique)
	Disables realignment of ZDD order to BDD order. More...

int	Cudd_bddRealignmentEnabled (DdManager *unique)
	Tells whether the realignment of BDD order to ZDD order is enabled. More...

void	Cudd_bddRealignEnable (DdManager *unique)
	Enables realignment of BDD order to ZDD order. More...

void	Cudd_bddRealignDisable (DdManager *unique)
	Disables realignment of ZDD order to BDD order. More...

DdNode *	Cudd_ReadOne (DdManager *dd)
	Returns the one constant of the manager. More...

DdNode *	Cudd_ReadZddOne (DdManager *dd, int i)
	Returns the ZDD for the constant 1 function. More...

DdNode *	Cudd_ReadZero (DdManager *dd)
	Returns the zero constant of the manager. More...

DdNode *	Cudd_ReadLogicZero (DdManager *dd)
	Returns the logic zero constant of the manager. More...

DdNode *	Cudd_ReadPlusInfinity (DdManager *dd)
	Reads the plus-infinity constant from the manager. More...

DdNode *	Cudd_ReadMinusInfinity (DdManager *dd)
	Reads the minus-infinity constant from the manager. More...

DdNode *	Cudd_ReadBackground (DdManager *dd)
	Reads the background constant of the manager. More...

void	Cudd_SetBackground (DdManager dd, DdNode bck)
	Sets the background constant of the manager. More...

unsigned int	Cudd_ReadCacheSlots (DdManager *dd)
	Reads the number of slots in the cache. More...

double	Cudd_ReadCacheUsedSlots (DdManager *dd)
	Reads the fraction of used slots in the cache. More...

double	Cudd_ReadCacheLookUps (DdManager *dd)
	Returns the number of cache look-ups. More...

double	Cudd_ReadCacheHits (DdManager *dd)
	Returns the number of cache hits. More...

double	Cudd_ReadRecursiveCalls (DdManager *dd)
	Returns the number of recursive calls. More...

unsigned int	Cudd_ReadMinHit (DdManager *dd)
	Reads the hit rate that causes resizinig of the computed table. More...

void	Cudd_SetMinHit (DdManager *dd, unsigned int hr)
	Sets the hit rate that causes resizinig of the computed table. More...

unsigned int	Cudd_ReadLooseUpTo (DdManager *dd)
	Reads the looseUpTo parameter of the manager. More...

void	Cudd_SetLooseUpTo (DdManager *dd, unsigned int lut)
	Sets the looseUpTo parameter of the manager. More...

unsigned int	Cudd_ReadMaxCache (DdManager *dd)
	Returns the soft limit for the cache size. More...

unsigned int	Cudd_ReadMaxCacheHard (DdManager *dd)
	Reads the maxCacheHard parameter of the manager. More...

void	Cudd_SetMaxCacheHard (DdManager *dd, unsigned int mc)
	Sets the maxCacheHard parameter of the manager. More...

int	Cudd_ReadSize (DdManager *dd)
	Returns the number of BDD variables in existance. More...

int	Cudd_ReadZddSize (DdManager *dd)
	Returns the number of ZDD variables in existance. More...

unsigned int	Cudd_ReadSlots (DdManager *dd)
	Returns the total number of slots of the unique table. More...

double	Cudd_ReadUsedSlots (DdManager *dd)
	Reads the fraction of used slots in the unique table. More...

double	Cudd_ExpectedUsedSlots (DdManager *dd)
	Computes the expected fraction of used slots in the unique table. More...

unsigned int	Cudd_ReadKeys (DdManager *dd)
	Returns the number of nodes in the unique table. More...

unsigned int	Cudd_ReadDead (DdManager *dd)
	Returns the number of dead nodes in the unique table. More...

unsigned int	Cudd_ReadMinDead (DdManager *dd)
	Reads the minDead parameter of the manager. More...

unsigned int	Cudd_ReadReorderings (DdManager *dd)
	Returns the number of times reordering has occurred. More...

unsigned int	Cudd_ReadMaxReorderings (DdManager *dd)
	Returns the maximum number of times reordering may be invoked. More...

void	Cudd_SetMaxReorderings (DdManager *dd, unsigned int mr)
	Sets the maximum number of times reordering may be invoked. More...

long	Cudd_ReadReorderingTime (DdManager *dd)
	Returns the time spent in reordering. More...

int	Cudd_ReadGarbageCollections (DdManager *dd)
	Returns the number of times garbage collection has occurred. More...

long	Cudd_ReadGarbageCollectionTime (DdManager *dd)
	Returns the time spent in garbage collection. More...

double	Cudd_ReadNodesFreed (DdManager *dd)
	Returns the number of nodes freed. More...

double	Cudd_ReadNodesDropped (DdManager *dd)
	Returns the number of nodes dropped. More...

double	Cudd_ReadUniqueLookUps (DdManager *dd)
	Returns the number of look-ups in the unique table. More...

double	Cudd_ReadUniqueLinks (DdManager *dd)
	Returns the number of links followed in the unique table. More...

int	Cudd_ReadSiftMaxVar (DdManager *dd)
	Reads the siftMaxVar parameter of the manager. More...

void	Cudd_SetSiftMaxVar (DdManager *dd, int smv)
	Sets the siftMaxVar parameter of the manager. More...

int	Cudd_ReadSiftMaxSwap (DdManager *dd)
	Reads the siftMaxSwap parameter of the manager. More...

void	Cudd_SetSiftMaxSwap (DdManager *dd, int sms)
	Sets the siftMaxSwap parameter of the manager. More...

double	Cudd_ReadMaxGrowth (DdManager *dd)
	Reads the maxGrowth parameter of the manager. More...

void	Cudd_SetMaxGrowth (DdManager *dd, double mg)
	Sets the maxGrowth parameter of the manager. More...

double	Cudd_ReadMaxGrowthAlternate (DdManager *dd)
	Reads the maxGrowthAlt parameter of the manager. More...

void	Cudd_SetMaxGrowthAlternate (DdManager *dd, double mg)
	Sets the maxGrowthAlt parameter of the manager. More...

int	Cudd_ReadReorderingCycle (DdManager *dd)
	Reads the reordCycle parameter of the manager. More...

void	Cudd_SetReorderingCycle (DdManager *dd, int cycle)
	Sets the reordCycle parameter of the manager. More...

MtrNode *	Cudd_ReadTree (DdManager *dd)
	Returns the variable group tree of the manager. More...

void	Cudd_SetTree (DdManager dd, MtrNode tree)
	Sets the variable group tree of the manager. More...

void	Cudd_FreeTree (DdManager *dd)
	Frees the variable group tree of the manager. More...

MtrNode *	Cudd_ReadZddTree (DdManager *dd)
	Returns the variable group tree of the manager. More...

void	Cudd_SetZddTree (DdManager dd, MtrNode tree)
	Sets the ZDD variable group tree of the manager. More...

void	Cudd_FreeZddTree (DdManager *dd)
	Frees the variable group tree of the manager. More...

unsigned int	Cudd_NodeReadIndex (DdNode *node)
	Returns the index of the node. More...

int	Cudd_ReadPerm (DdManager *dd, int i)
	Returns the current position of the i-th variable in the order. More...

int	Cudd_ReadPermZdd (DdManager *dd, int i)
	Returns the current position of the i-th ZDD variable in the order. More...

int	Cudd_ReadInvPerm (DdManager *dd, int i)
	Returns the index of the variable currently in the i-th position of the order. More...

int	Cudd_ReadInvPermZdd (DdManager *dd, int i)
	Returns the index of the ZDD variable currently in the i-th position of the order. More...

DdNode *	Cudd_ReadVars (DdManager *dd, int i)
	Returns the i-th element of the vars array. More...

CUDD_VALUE_TYPE	Cudd_ReadEpsilon (DdManager *dd)
	Reads the epsilon parameter of the manager. More...

void	Cudd_SetEpsilon (DdManager *dd, CUDD_VALUE_TYPE ep)
	Sets the epsilon parameter of the manager to ep. More...

Cudd_AggregationType	Cudd_ReadGroupcheck (DdManager *dd)
	Reads the groupcheck parameter of the manager. More...

void	Cudd_SetGroupcheck (DdManager *dd, Cudd_AggregationType gc)
	Sets the parameter groupcheck of the manager to gc. More...

int	Cudd_GarbageCollectionEnabled (DdManager *dd)
	Tells whether garbage collection is enabled. More...

void	Cudd_EnableGarbageCollection (DdManager *dd)
	Enables garbage collection. More...

void	Cudd_DisableGarbageCollection (DdManager *dd)
	Disables garbage collection. More...

int	Cudd_DeadAreCounted (DdManager *dd)
	Tells whether dead nodes are counted towards triggering reordering. More...

void	Cudd_TurnOnCountDead (DdManager *dd)
	Causes the dead nodes to be counted towards triggering reordering. More...

void	Cudd_TurnOffCountDead (DdManager *dd)
	Causes the dead nodes not to be counted towards triggering reordering. More...

int	Cudd_ReadRecomb (DdManager *dd)
	Returns the current value of the recombination parameter used in group sifting. More...

void	Cudd_SetRecomb (DdManager *dd, int recomb)
	Sets the value of the recombination parameter used in group sifting. More...

int	Cudd_ReadSymmviolation (DdManager *dd)
	Returns the current value of the symmviolation parameter used in group sifting. More...

void	Cudd_SetSymmviolation (DdManager *dd, int symmviolation)
	Sets the value of the symmviolation parameter used in group sifting. More...

int	Cudd_ReadArcviolation (DdManager *dd)
	Returns the current value of the arcviolation parameter used in group sifting. More...

void	Cudd_SetArcviolation (DdManager *dd, int arcviolation)
	Sets the value of the arcviolation parameter used in group sifting. More...

int	Cudd_ReadPopulationSize (DdManager *dd)
	Reads the current size of the population used by the genetic algorithm for variable reordering. More...

void	Cudd_SetPopulationSize (DdManager *dd, int populationSize)
	Sets the size of the population used by the genetic algorithm for variable reordering. More...

int	Cudd_ReadNumberXovers (DdManager *dd)
	Reads the current number of crossovers used by the genetic algorithm for variable reordering. More...

void	Cudd_SetNumberXovers (DdManager *dd, int numberXovers)
	Sets the number of crossovers used by the genetic algorithm for variable reordering. More...

unsigned int	Cudd_ReadOrderRandomization (DdManager *dd)
	Returns the order randomization factor. More...

void	Cudd_SetOrderRandomization (DdManager *dd, unsigned int factor)
	Sets the order randomization factor. More...

size_t	Cudd_ReadMemoryInUse (DdManager *dd)
	Returns the memory in use by the manager measured in bytes. More...

int	Cudd_PrintInfo (DdManager dd, FILE fp)
	Prints out statistics and settings for a CUDD manager. More...

long	Cudd_ReadPeakNodeCount (DdManager *dd)
	Reports the peak number of nodes. More...

int	Cudd_ReadPeakLiveNodeCount (DdManager *dd)
	Reports the peak number of live nodes. More...

long	Cudd_ReadNodeCount (DdManager *dd)
	Reports the number of nodes in BDDs and ADDs. More...

long	Cudd_zddReadNodeCount (DdManager *dd)
	Reports the number of nodes in ZDDs. More...

int	Cudd_AddHook (DdManager *dd, DD_HFP f, Cudd_HookType where)
	Adds a function to a hook. More...

int	Cudd_RemoveHook (DdManager *dd, DD_HFP f, Cudd_HookType where)
	Removes a function from a hook. More...

int	Cudd_IsInHook (DdManager *dd, DD_HFP f, Cudd_HookType where)
	Checks whether a function is in a hook. More...

int	Cudd_StdPreReordHook (DdManager dd, const char str, void *data)
	Sample hook function to call before reordering. More...

int	Cudd_StdPostReordHook (DdManager dd, const char str, void *data)
	Sample hook function to call after reordering. More...

int	Cudd_EnableReorderingReporting (DdManager *dd)
	Enables reporting of reordering stats. More...

int	Cudd_DisableReorderingReporting (DdManager *dd)
	Disables reporting of reordering stats. More...

int	Cudd_ReorderingReporting (DdManager *dd)
	Returns 1 if reporting of reordering stats is enabled; 0 otherwise. More...

int	Cudd_PrintGroupedOrder (DdManager dd, const char str, void *data)
	Hook function to print the current variable order. More...

int	Cudd_EnableOrderingMonitoring (DdManager *dd)
	Enables monitoring of ordering. More...

int	Cudd_DisableOrderingMonitoring (DdManager *dd)
	Disables monitoring of ordering. More...

int	Cudd_OrderingMonitoring (DdManager *dd)
	Returns 1 if monitoring of ordering is enabled; 0 otherwise. More...

void	Cudd_SetApplicationHook (DdManager dd, void value)
	Sets the application hook. More...

void *	Cudd_ReadApplicationHook (DdManager *dd)
	Reads the application hook. More...

Cudd_ErrorType	Cudd_ReadErrorCode (DdManager *dd)
	Returns the code of the last error. More...

void	Cudd_ClearErrorCode (DdManager *dd)
	Clear the error code of a manager. More...

DD_OOMFP	Cudd_InstallOutOfMemoryHandler (DD_OOMFP newHandler)
	Installs a handler for failed memory allocations. More...

FILE *	Cudd_ReadStdout (DdManager *dd)
	Reads the stdout of a manager. More...

void	Cudd_SetStdout (DdManager dd, FILE fp)
	Sets the stdout of a manager. More...

FILE *	Cudd_ReadStderr (DdManager *dd)
	Reads the stderr of a manager. More...

void	Cudd_SetStderr (DdManager dd, FILE fp)
	Sets the stderr of a manager. More...

unsigned int	Cudd_ReadNextReordering (DdManager *dd)
	Returns the threshold for the next dynamic reordering. More...

void	Cudd_SetNextReordering (DdManager *dd, unsigned int next)
	Sets the threshold for the next dynamic reordering. More...

double	Cudd_ReadSwapSteps (DdManager *dd)
	Reads the number of elementary reordering steps. More...

unsigned int	Cudd_ReadMaxLive (DdManager *dd)
	Reads the maximum allowed number of live nodes. More...

void	Cudd_SetMaxLive (DdManager *dd, unsigned int maxLive)
	Sets the maximum allowed number of live nodes. More...

size_t	Cudd_ReadMaxMemory (DdManager *dd)
	Reads the maximum allowed memory. More...

size_t	Cudd_SetMaxMemory (DdManager *dd, size_t maxMemory)
	Sets the maximum allowed memory. More...

int	Cudd_bddBindVar (DdManager *dd, int index)
	Prevents sifting of a variable. More...

int	Cudd_bddUnbindVar (DdManager *dd, int index)
	Allows the sifting of a variable. More...

int	Cudd_bddVarIsBound (DdManager *dd, int index)
	Tells whether a variable can be sifted. More...

int	Cudd_bddSetPiVar (DdManager *dd, int index)
	Sets a variable type to primary input. More...

int	Cudd_bddSetPsVar (DdManager *dd, int index)
	Sets a variable type to present state. More...

int	Cudd_bddSetNsVar (DdManager *dd, int index)
	Sets a variable type to next state. More...

int	Cudd_bddIsPiVar (DdManager *dd, int index)
	Checks whether a variable is primary input. More...

int	Cudd_bddIsPsVar (DdManager *dd, int index)
	Checks whether a variable is present state. More...

int	Cudd_bddIsNsVar (DdManager *dd, int index)
	Checks whether a variable is next state. More...

int	Cudd_bddSetPairIndex (DdManager *dd, int index, int pairIndex)
	Sets a corresponding pair index for a given index. More...

int	Cudd_bddReadPairIndex (DdManager *dd, int index)
	Reads a corresponding pair index for a given index. More...

int	Cudd_bddSetVarToBeGrouped (DdManager *dd, int index)
	Sets a variable to be grouped. More...

int	Cudd_bddSetVarHardGroup (DdManager *dd, int index)
	Sets a variable to be a hard group. More...

int	Cudd_bddResetVarToBeGrouped (DdManager *dd, int index)
	Resets a variable not to be grouped. More...

int	Cudd_bddIsVarToBeGrouped (DdManager *dd, int index)
	Checks whether a variable is set to be grouped. More...

int	Cudd_bddSetVarToBeUngrouped (DdManager *dd, int index)
	Sets a variable to be ungrouped. More...

int	Cudd_bddIsVarToBeUngrouped (DdManager *dd, int index)
	Checks whether a variable is set to be ungrouped. More...

int	Cudd_bddIsVarHardGroup (DdManager *dd, int index)
	Checks whether a variable is set to be in a hard group. More...

static void	fixVarTree (MtrNode treenode, int perm, int size)
	Fixes a variable group tree. More...

static int	addMultiplicityGroups (DdManager dd, MtrNode treenode, int multiplicity, char vmask, char lmask)
	Adds multiplicity groups to a ZDD variable group tree. More...

Detailed Description

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

◆ addMultiplicityGroups()

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

◆ Cudd_addConst()

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

◆ Cudd_AddHook()

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

◆ Cudd_addIthVar()

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

◆ Cudd_addNewVar()

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

◆ 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

◆ Cudd_AutodynDisable()

void Cudd_AutodynDisable ( DdManager * unique )

Disables automatic dynamic reordering.

Side effects None

See also: Cudd_AutodynEnable Cudd_ReorderingStatus Cudd_AutodynDisableZdd

◆ Cudd_AutodynDisableZdd()

void Cudd_AutodynDisableZdd ( DdManager * unique )

Disables automatic dynamic reordering of ZDDs.

Side effects None

See also: Cudd_AutodynEnableZdd Cudd_ReorderingStatusZdd Cudd_AutodynDisable

◆ Cudd_AutodynEnable()

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

◆ 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

◆ Cudd_bddBindVar()

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

◆ Cudd_bddIsNsVar()

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

◆ Cudd_bddIsPiVar()

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

◆ Cudd_bddIsPsVar()

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

◆ Cudd_bddIsVar()

int Cudd_bddIsVar	(	DdManager *	dd,
		DdNode *	f
	)

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

Side effects None

◆ Cudd_bddIsVarHardGroup()

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

◆ Cudd_bddIsVarToBeGrouped()

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

◆ Cudd_bddIsVarToBeUngrouped()

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

◆ Cudd_bddIthVar()

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

◆ Cudd_bddNewVar()

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

◆ 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

◆ Cudd_bddReadPairIndex()

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

◆ Cudd_bddRealignDisable()

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

◆ Cudd_bddRealignEnable()

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

◆ Cudd_bddRealignmentEnabled()

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

◆ Cudd_bddResetVarToBeGrouped()

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

◆ Cudd_bddSetNsVar()

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

◆ Cudd_bddSetPairIndex()

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

◆ Cudd_bddSetPiVar()

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

◆ Cudd_bddSetPsVar()

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

◆ Cudd_bddSetVarHardGroup()

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

◆ Cudd_bddSetVarToBeGrouped()

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

◆ Cudd_bddSetVarToBeUngrouped()

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

◆ Cudd_bddUnbindVar()

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

◆ Cudd_bddVarIsBound()

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

◆ Cudd_ClearErrorCode()

void Cudd_ClearErrorCode ( DdManager * dd )

Clear the error code of a manager.

Side effects None

See also: Cudd_ReadErrorCode

◆ Cudd_DeadAreCounted()

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

◆ Cudd_DisableGarbageCollection()

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

◆ Cudd_DisableOrderingMonitoring()

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

◆ Cudd_DisableReorderingReporting()

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

◆ Cudd_E()

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

◆ Cudd_EnableGarbageCollection()

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

◆ Cudd_EnableOrderingMonitoring()

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

◆ 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

◆ Cudd_ExpectedUsedSlots()

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

◆ Cudd_FreeTree()

void Cudd_FreeTree ( DdManager * dd )

Frees the variable group tree of the manager.

Side effects None

See also: Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree

◆ 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

◆ Cudd_GarbageCollectionEnabled()

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

◆ Cudd_IncreaseTimeLimit()

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

◆ Cudd_InstallOutOfMemoryHandler()

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.

◆ Cudd_IsConstant()

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

◆ Cudd_IsInHook()

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

◆ Cudd_IsNonConstant()

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

◆ Cudd_NodeReadIndex()

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

◆ Cudd_OrderingMonitoring()

int Cudd_OrderingMonitoring ( DdManager * dd )

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

Side effects none

See also: Cudd_EnableOrderingMonitoring Cudd_DisableOrderingMonitoring

◆ Cudd_PrintGroupedOrder()

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

◆ Cudd_PrintInfo()

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

◆ Cudd_ReadApplicationHook()

void* Cudd_ReadApplicationHook ( DdManager * dd )

Reads the application hook.

Side effects None

See also: Cudd_SetApplicationHook

◆ Cudd_ReadArcviolation()

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

◆ Cudd_ReadBackground()

DdNode* Cudd_ReadBackground ( DdManager * dd )

Reads the background constant of the manager.

Side effects None

◆ Cudd_ReadCacheHits()

double Cudd_ReadCacheHits ( DdManager * dd )

Returns the number of cache hits.

Side effects None

See also: Cudd_ReadCacheLookUps

◆ Cudd_ReadCacheLookUps()

double Cudd_ReadCacheLookUps ( DdManager * dd )

Returns the number of cache look-ups.

Side effects None

See also: Cudd_ReadCacheHits

◆ Cudd_ReadCacheSlots()

unsigned int Cudd_ReadCacheSlots ( DdManager * dd )

Reads the number of slots in the cache.

Side effects None

See also: Cudd_ReadCacheUsedSlots

◆ 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

◆ Cudd_ReadDead()

unsigned int Cudd_ReadDead ( DdManager * dd )

Returns the number of dead nodes in the unique table.

Side effects None

See also: Cudd_ReadKeys

◆ Cudd_ReadElapsedTime()

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_ReadEpsilon()

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_ReadErrorCode()

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

◆ Cudd_ReadGarbageCollections()

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

◆ 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_ReadGroupcheck()

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

◆ Cudd_ReadInvPerm()

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

◆ 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

◆ Cudd_ReadKeys()

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

◆ Cudd_ReadLogicZero()

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

◆ Cudd_ReadLooseUpTo()

unsigned int Cudd_ReadLooseUpTo ( DdManager * dd )

Reads the looseUpTo parameter of the manager.

Side effects None

See also: Cudd_SetLooseUpTo Cudd_ReadMinHit Cudd_ReadMinDead

◆ Cudd_ReadMaxCache()

unsigned int Cudd_ReadMaxCache ( DdManager * dd )

Returns the soft limit for the cache size.

Side effects None

See also: Cudd_ReadMaxCacheHard

◆ Cudd_ReadMaxCacheHard()

unsigned int Cudd_ReadMaxCacheHard ( DdManager * dd )

Reads the maxCacheHard parameter of the manager.

Side effects None

See also: Cudd_SetMaxCacheHard Cudd_ReadMaxCache

◆ Cudd_ReadMaxGrowth()

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

◆ 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

◆ Cudd_ReadMaxIndex()

unsigned int Cudd_ReadMaxIndex ( void )

Returns the maximum possible index for a variable.

Side effects None

◆ Cudd_ReadMaxLive()

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

◆ Cudd_ReadMaxMemory()

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

◆ Cudd_ReadMaxReorderings()

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

◆ Cudd_ReadMemoryInUse()

size_t Cudd_ReadMemoryInUse ( DdManager * dd )

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

Side effects None

◆ Cudd_ReadMinDead()

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

◆ Cudd_ReadMinHit()

unsigned int Cudd_ReadMinHit ( DdManager * dd )

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

Side effects None

See also: Cudd_SetMinHit

◆ Cudd_ReadMinusInfinity()

DdNode* Cudd_ReadMinusInfinity ( DdManager * dd )

Reads the minus-infinity constant from the manager.

Side effects None

◆ Cudd_ReadNextReordering()

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

◆ Cudd_ReadNodeCount()

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

◆ Cudd_ReadNodesDropped()

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

◆ 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

◆ Cudd_ReadNumberXovers()

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

◆ Cudd_ReadOne()

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

◆ Cudd_ReadOrderRandomization()

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

◆ Cudd_ReadPeakLiveNodeCount()

int Cudd_ReadPeakLiveNodeCount ( DdManager * dd )

Reports the peak number of live nodes.

Side effects None

See also: Cudd_ReadNodeCount Cudd_PrintInfo Cudd_ReadPeakNodeCount

◆ 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

◆ Cudd_ReadPerm()

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

◆ 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

◆ Cudd_ReadPlusInfinity()

DdNode* Cudd_ReadPlusInfinity ( DdManager * dd )

Reads the plus-infinity constant from the manager.

Side effects None

◆ Cudd_ReadPopulationSize()

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

◆ Cudd_ReadRecomb()

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

◆ Cudd_ReadRecursiveCalls()

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

◆ Cudd_ReadReorderingCycle()

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

◆ Cudd_ReadReorderings()

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

◆ 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

◆ Cudd_ReadSiftMaxSwap()

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

◆ Cudd_ReadSiftMaxVar()

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

◆ Cudd_ReadSize()

int Cudd_ReadSize ( DdManager * dd )

Returns the number of BDD variables in existance.

Side effects None

See also: Cudd_ReadZddSize

◆ Cudd_ReadSlots()

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

◆ Cudd_ReadStartTime()

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

◆ Cudd_ReadStderr()

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

◆ 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

◆ Cudd_ReadSwapSteps()

double Cudd_ReadSwapSteps ( DdManager * dd )

Reads the number of elementary reordering steps.

Side effects none

◆ Cudd_ReadSymmviolation()

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

◆ Cudd_ReadTimeLimit()

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

◆ Cudd_ReadTimeoutHandler()

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

◆ Cudd_ReadTree()

MtrNode* Cudd_ReadTree ( DdManager * dd )

Returns the variable group tree of the manager.

Side effects None

See also: Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree

◆ Cudd_ReadUniqueLinks()

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

◆ 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

◆ Cudd_ReadUsedSlots()

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

◆ Cudd_ReadVars()

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

◆ Cudd_ReadZddOne()

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

◆ Cudd_ReadZddSize()

int Cudd_ReadZddSize ( DdManager * dd )

Returns the number of ZDD variables in existance.

Side effects None

See also: Cudd_ReadSize

◆ Cudd_ReadZddTree()

MtrNode* Cudd_ReadZddTree ( DdManager * dd )

Returns the variable group tree of the manager.

Side effects None

See also: Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree

◆ Cudd_ReadZero()

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

◆ Cudd_RegisterOutOfMemoryCallback()

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

◆ Cudd_RegisterTerminationCallback()

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

◆ Cudd_RegisterTimeoutHandler()

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

◆ Cudd_RemoveHook()

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

◆ Cudd_ReorderingReporting()

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

◆ Cudd_ReorderingStatus()

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

◆ 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

◆ Cudd_ResetStartTime()

void Cudd_ResetStartTime ( DdManager * unique )

Resets the start time of the manager.

Side effects None

See also: Cudd_ReadStartTime Cudd_SetStartTime Cudd_SetTimeLimit

◆ Cudd_SetApplicationHook()

void Cudd_SetApplicationHook	(	DdManager *	dd,
		void *	value
	)

Sets the application hook.

Side effects None

See also: Cudd_ReadApplicationHook

◆ Cudd_SetArcviolation()

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

◆ Cudd_SetBackground()

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

◆ Cudd_SetEpsilon()

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

◆ Cudd_SetGroupcheck()

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

◆ Cudd_SetLooseUpTo()

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

◆ Cudd_SetMaxCacheHard()

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

◆ Cudd_SetMaxGrowth()

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

◆ 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

◆ Cudd_SetMaxLive()

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

◆ Cudd_SetMaxMemory()

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

◆ Cudd_SetMaxReorderings()

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

◆ Cudd_SetMinHit()

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

◆ Cudd_SetNextReordering()

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

◆ Cudd_SetNumberXovers()

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

◆ Cudd_SetOrderRandomization()

void Cudd_SetOrderRandomization	(	DdManager *	dd,
		unsigned int	factor
	)

Sets the order randomization factor.

Side effects None

See also: Cudd_ReadOrderRandomization

◆ Cudd_SetPopulationSize()

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

◆ Cudd_SetRecomb()

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

◆ Cudd_SetReorderingCycle()

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

◆ Cudd_SetSiftMaxSwap()

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

◆ Cudd_SetSiftMaxVar()

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

◆ Cudd_SetStartTime()

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

◆ Cudd_SetStderr()

void Cudd_SetStderr	(	DdManager *	dd,
		FILE *	fp
	)

Sets the stderr of a manager.

Side effects None

See also: Cudd_ReadStderr Cudd_SetStdout

◆ Cudd_SetStdout()

void Cudd_SetStdout	(	DdManager *	dd,
		FILE *	fp
	)

Sets the stdout of a manager.

Side effects None

See also: Cudd_ReadStdout Cudd_SetStderr

◆ Cudd_SetSymmviolation()

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

◆ Cudd_SetTimeLimit()

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

◆ Cudd_SetTree()

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

◆ 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

◆ Cudd_StdPostReordHook()

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

◆ 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

◆ Cudd_T()

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

◆ Cudd_TimeLimited()

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

◆ Cudd_TurnOffCountDead()

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

◆ Cudd_TurnOnCountDead()

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

◆ Cudd_UnregisterOutOfMemoryCallback()

void Cudd_UnregisterOutOfMemoryCallback ( DdManager * unique )

Unregister an out-of-memory callback.

Side effects None

See also: Cudd_RegisterOutOfMemoryCallback Cudd_OutOfMem Cudd_OutOfMemSilent

◆ Cudd_UnregisterTerminationCallback()

void Cudd_UnregisterTerminationCallback ( DdManager * unique )

Unregisters a termination callback.

Side effects None

See also: Cudd_RegisterTerminationCallback

◆ Cudd_UnsetTimeLimit()

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

◆ Cudd_UpdateTimeLimit()

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_V()

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

◆ Cudd_zddIthVar()

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

◆ Cudd_zddReadNodeCount()

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

◆ Cudd_zddRealignDisable()

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

◆ Cudd_zddRealignEnable()

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

◆ Cudd_zddRealignmentEnabled()

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

◆ Cudd_zddVarsFromBddVars()

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

◆ fixVarTree()

static void fixVarTree	(	MtrNode *	treenode,
		int *	perm,
		int	size
	)

static

Fixes a variable group tree.

Side effects Changes the variable group tree.

Functions

Detailed Description

Function Documentation

◆ addMultiplicityGroups()

◆ Cudd_addConst()

◆ Cudd_AddHook()

◆ Cudd_addIthVar()

◆ Cudd_addNewVar()

◆ Cudd_addNewVarAtLevel()

◆ Cudd_AutodynDisable()

◆ Cudd_AutodynDisableZdd()

◆ Cudd_AutodynEnable()

◆ Cudd_AutodynEnableZdd()

◆ Cudd_bddBindVar()

◆ Cudd_bddIsNsVar()

◆ Cudd_bddIsPiVar()

◆ Cudd_bddIsPsVar()

◆ Cudd_bddIsVar()

◆ Cudd_bddIsVarHardGroup()

◆ Cudd_bddIsVarToBeGrouped()

◆ Cudd_bddIsVarToBeUngrouped()

◆ Cudd_bddIthVar()

◆ Cudd_bddNewVar()

◆ Cudd_bddNewVarAtLevel()

◆ Cudd_bddReadPairIndex()

◆ Cudd_bddRealignDisable()

◆ Cudd_bddRealignEnable()

◆ Cudd_bddRealignmentEnabled()

◆ Cudd_bddResetVarToBeGrouped()

◆ Cudd_bddSetNsVar()

◆ Cudd_bddSetPairIndex()

◆ Cudd_bddSetPiVar()

◆ Cudd_bddSetPsVar()

◆ Cudd_bddSetVarHardGroup()

◆ Cudd_bddSetVarToBeGrouped()

◆ Cudd_bddSetVarToBeUngrouped()

◆ Cudd_bddUnbindVar()

◆ Cudd_bddVarIsBound()

◆ Cudd_ClearErrorCode()

◆ Cudd_DeadAreCounted()

◆ Cudd_DisableGarbageCollection()

◆ Cudd_DisableOrderingMonitoring()

◆ Cudd_DisableReorderingReporting()

◆ Cudd_E()

◆ Cudd_EnableGarbageCollection()

◆ Cudd_EnableOrderingMonitoring()

◆ Cudd_EnableReorderingReporting()

◆ Cudd_ExpectedUsedSlots()

◆ Cudd_FreeTree()

◆ Cudd_FreeZddTree()

◆ Cudd_GarbageCollectionEnabled()

◆ Cudd_IncreaseTimeLimit()

◆ Cudd_InstallOutOfMemoryHandler()

◆ Cudd_IsConstant()

◆ Cudd_IsInHook()

◆ Cudd_IsNonConstant()

◆ Cudd_NodeReadIndex()

◆ Cudd_OrderingMonitoring()

◆ Cudd_PrintGroupedOrder()

◆ Cudd_PrintInfo()

◆ Cudd_ReadApplicationHook()

◆ Cudd_ReadArcviolation()

◆ Cudd_ReadBackground()

◆ Cudd_ReadCacheHits()

◆ Cudd_ReadCacheLookUps()

◆ Cudd_ReadCacheSlots()

◆ Cudd_ReadCacheUsedSlots()

◆ Cudd_ReadDead()

◆ Cudd_ReadElapsedTime()

◆ Cudd_ReadEpsilon()

◆ Cudd_ReadErrorCode()

◆ Cudd_ReadGarbageCollections()

◆ Cudd_ReadGarbageCollectionTime()

◆ Cudd_ReadGroupcheck()

◆ Cudd_ReadInvPerm()

◆ Cudd_ReadInvPermZdd()

◆ Cudd_ReadKeys()

◆ Cudd_ReadLogicZero()

◆ Cudd_ReadLooseUpTo()

◆ Cudd_ReadMaxCache()