#include "misc/util/util_hack.h"
#include "cuddInt.h"

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

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

DdNode *	Cudd_addNewVar (DdManager *dd)

DdNode *	Cudd_addNewVarAtLevel (DdManager *dd, int level)

DdNode *	Cudd_bddNewVar (DdManager *dd)

DdNode *	Cudd_bddNewVarAtLevel (DdManager *dd, int level)

DdNode *	Cudd_addIthVar (DdManager *dd, int i)

DdNode *	Cudd_bddIthVar (DdManager *dd, int i)

DdNode *	Cudd_zddIthVar (DdManager *dd, int i)

int	Cudd_zddVarsFromBddVars (DdManager *dd, int multiplicity)

DdNode *	Cudd_addConst (DdManager *dd, CUDD_VALUE_TYPE c)

int	Cudd_IsNonConstant (DdNode *f)

void	Cudd_AutodynEnable (DdManager *unique, Cudd_ReorderingType method)

void	Cudd_AutodynDisable (DdManager *unique)

int	Cudd_ReorderingStatus (DdManager unique, Cudd_ReorderingType method)

void	Cudd_AutodynEnableZdd (DdManager *unique, Cudd_ReorderingType method)

void	Cudd_AutodynDisableZdd (DdManager *unique)

int	Cudd_ReorderingStatusZdd (DdManager unique, Cudd_ReorderingType method)

int	Cudd_zddRealignmentEnabled (DdManager *unique)

void	Cudd_zddRealignEnable (DdManager *unique)

void	Cudd_zddRealignDisable (DdManager *unique)

int	Cudd_bddRealignmentEnabled (DdManager *unique)

void	Cudd_bddRealignEnable (DdManager *unique)

void	Cudd_bddRealignDisable (DdManager *unique)

DdNode *	Cudd_ReadOne (DdManager *dd)

DdNode *	Cudd_ReadZddOne (DdManager *dd, int i)

DdNode *	Cudd_ReadZero (DdManager *dd)

DdNode *	Cudd_ReadLogicZero (DdManager *dd)

DdNode *	Cudd_ReadPlusInfinity (DdManager *dd)

DdNode *	Cudd_ReadMinusInfinity (DdManager *dd)

DdNode *	Cudd_ReadBackground (DdManager *dd)

void	Cudd_SetBackground (DdManager dd, DdNode bck)

unsigned int	Cudd_ReadCacheSlots (DdManager *dd)

double	Cudd_ReadCacheUsedSlots (DdManager *dd)

double	Cudd_ReadCacheLookUps (DdManager *dd)

double	Cudd_ReadCacheHits (DdManager *dd)

double	Cudd_ReadRecursiveCalls (DdManager *dd)

unsigned int	Cudd_ReadMinHit (DdManager *dd)

void	Cudd_SetMinHit (DdManager *dd, unsigned int hr)

unsigned int	Cudd_ReadLooseUpTo (DdManager *dd)

void	Cudd_SetLooseUpTo (DdManager *dd, unsigned int lut)

unsigned int	Cudd_ReadMaxCache (DdManager *dd)

unsigned int	Cudd_ReadMaxCacheHard (DdManager *dd)

void	Cudd_SetMaxCacheHard (DdManager *dd, unsigned int mc)

int	Cudd_ReadSize (DdManager *dd)

int	Cudd_ReadZddSize (DdManager *dd)

unsigned int	Cudd_ReadSlots (DdManager *dd)

double	Cudd_ReadUsedSlots (DdManager *dd)

double	Cudd_ExpectedUsedSlots (DdManager *dd)

unsigned int	Cudd_ReadKeys (DdManager *dd)

unsigned int	Cudd_ReadDead (DdManager *dd)

unsigned int	Cudd_ReadMinDead (DdManager *dd)

int	Cudd_ReadReorderings (DdManager *dd)

long	Cudd_ReadReorderingTime (DdManager *dd)

int	Cudd_ReadGarbageCollections (DdManager *dd)

long	Cudd_ReadGarbageCollectionTime (DdManager *dd)

double	Cudd_ReadNodesFreed (DdManager *dd)

double	Cudd_ReadNodesDropped (DdManager *dd)

double	Cudd_ReadUniqueLookUps (DdManager *dd)

double	Cudd_ReadUniqueLinks (DdManager *dd)

int	Cudd_ReadSiftMaxVar (DdManager *dd)

void	Cudd_SetSiftMaxVar (DdManager *dd, int smv)

int	Cudd_ReadSiftMaxSwap (DdManager *dd)

void	Cudd_SetSiftMaxSwap (DdManager *dd, int sms)

double	Cudd_ReadMaxGrowth (DdManager *dd)

void	Cudd_SetMaxGrowth (DdManager *dd, double mg)

double	Cudd_ReadMaxGrowthAlternate (DdManager *dd)

void	Cudd_SetMaxGrowthAlternate (DdManager *dd, double mg)

int	Cudd_ReadReorderingCycle (DdManager *dd)

void	Cudd_SetReorderingCycle (DdManager *dd, int cycle)

MtrNode *	Cudd_ReadTree (DdManager *dd)

void	Cudd_SetTree (DdManager dd, MtrNode tree)

void	Cudd_FreeTree (DdManager *dd)

MtrNode *	Cudd_ReadZddTree (DdManager *dd)

void	Cudd_SetZddTree (DdManager dd, MtrNode tree)

void	Cudd_FreeZddTree (DdManager *dd)

unsigned int	Cudd_NodeReadIndex (DdNode *node)

int	Cudd_ReadPerm (DdManager *dd, int i)

int	Cudd_ReadPermZdd (DdManager *dd, int i)

int	Cudd_ReadInvPerm (DdManager *dd, int i)

int	Cudd_ReadInvPermZdd (DdManager *dd, int i)

DdNode *	Cudd_ReadVars (DdManager *dd, int i)

CUDD_VALUE_TYPE	Cudd_ReadEpsilon (DdManager *dd)

void	Cudd_SetEpsilon (DdManager *dd, CUDD_VALUE_TYPE ep)

Cudd_AggregationType	Cudd_ReadGroupcheck (DdManager *dd)

void	Cudd_SetGroupcheck (DdManager *dd, Cudd_AggregationType gc)

int	Cudd_GarbageCollectionEnabled (DdManager *dd)

void	Cudd_EnableGarbageCollection (DdManager *dd)

void	Cudd_DisableGarbageCollection (DdManager *dd)

int	Cudd_DeadAreCounted (DdManager *dd)

void	Cudd_TurnOnCountDead (DdManager *dd)

void	Cudd_TurnOffCountDead (DdManager *dd)

int	Cudd_ReadRecomb (DdManager *dd)

void	Cudd_SetRecomb (DdManager *dd, int recomb)

int	Cudd_ReadSymmviolation (DdManager *dd)

void	Cudd_SetSymmviolation (DdManager *dd, int symmviolation)

int	Cudd_ReadArcviolation (DdManager *dd)

void	Cudd_SetArcviolation (DdManager *dd, int arcviolation)

int	Cudd_ReadPopulationSize (DdManager *dd)

void	Cudd_SetPopulationSize (DdManager *dd, int populationSize)

int	Cudd_ReadNumberXovers (DdManager *dd)

void	Cudd_SetNumberXovers (DdManager *dd, int numberXovers)

unsigned long	Cudd_ReadMemoryInUse (DdManager *dd)

int	Cudd_PrintInfo (DdManager dd, FILE fp)

long	Cudd_ReadPeakNodeCount (DdManager *dd)

int	Cudd_ReadPeakLiveNodeCount (DdManager *dd)

long	Cudd_ReadNodeCount (DdManager *dd)

long	Cudd_zddReadNodeCount (DdManager *dd)

int	Cudd_AddHook (DdManager *dd, DD_HFP f, Cudd_HookType where)

int	Cudd_RemoveHook (DdManager *dd, DD_HFP f, Cudd_HookType where)

int	Cudd_IsInHook (DdManager *dd, DD_HFP f, Cudd_HookType where)

int	Cudd_StdPreReordHook (DdManager dd, const char str, void *data)

int	Cudd_StdPostReordHook (DdManager dd, const char str, void *data)

int	Cudd_EnableReorderingReporting (DdManager *dd)

int	Cudd_DisableReorderingReporting (DdManager *dd)

int	Cudd_ReorderingReporting (DdManager *dd)

Cudd_ErrorType	Cudd_ReadErrorCode (DdManager *dd)

void	Cudd_ClearErrorCode (DdManager *dd)

FILE *	Cudd_ReadStdout (DdManager *dd)

void	Cudd_SetStdout (DdManager dd, FILE fp)

FILE *	Cudd_ReadStderr (DdManager *dd)

void	Cudd_SetStderr (DdManager dd, FILE fp)

unsigned int	Cudd_ReadNextReordering (DdManager *dd)

void	Cudd_SetNextReordering (DdManager *dd, unsigned int next)

double	Cudd_ReadSwapSteps (DdManager *dd)

unsigned int	Cudd_ReadMaxLive (DdManager *dd)

void	Cudd_SetMaxLive (DdManager *dd, unsigned int maxLive)

unsigned long	Cudd_ReadMaxMemory (DdManager *dd)

void	Cudd_SetMaxMemory (DdManager *dd, unsigned long maxMemory)

int	Cudd_bddBindVar (DdManager *dd, int index)

int	Cudd_bddUnbindVar (DdManager *dd, int index)

int	Cudd_bddVarIsBound (DdManager *dd, int index)

int	Cudd_bddSetPiVar (DdManager *dd, int index)

int	Cudd_bddSetPsVar (DdManager *dd, int index)

int	Cudd_bddSetNsVar (DdManager *dd, int index)

int	Cudd_bddIsPiVar (DdManager *dd, int index)

int	Cudd_bddIsPsVar (DdManager *dd, int index)

int	Cudd_bddIsNsVar (DdManager *dd, int index)

int	Cudd_bddSetPairIndex (DdManager *dd, int index, int pairIndex)

int	Cudd_bddReadPairIndex (DdManager *dd, int index)

int	Cudd_bddSetVarToBeGrouped (DdManager *dd, int index)

int	Cudd_bddSetVarHardGroup (DdManager *dd, int index)

int	Cudd_bddResetVarToBeGrouped (DdManager *dd, int index)

int	Cudd_bddIsVarToBeGrouped (DdManager *dd, int index)

int	Cudd_bddSetVarToBeUngrouped (DdManager *dd, int index)

int	Cudd_bddIsVarToBeUngrouped (DdManager *dd, int index)

int	Cudd_bddIsVarHardGroup (DdManager *dd, int index)

Variables
static ABC_NAMESPACE_IMPL_START char rcsid[]	DD_UNUSED = "$Id: cuddAPI.c,v 1.59 2009/02/19 16:14:14 fabio Exp $"

Function Documentation

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

static

Function********************************************************************

Synopsis [Adds multiplicity groups to a ZDD variable group tree.]

Description [Adds multiplicity groups to a ZDD variable group tree. Returns 1 if successful; 0 otherwise. 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.]

SideEffects [Changes the variable group tree.]

SeeAlso [Cudd_zddVarsFromBddVars]

Definition at line 4402 of file cuddAPI.c.

 {
     int startV, stopV, startL;
     int i, j;
     MtrNode *auxnode = treenode;
 
     while (auxnode != NULL) {
         if (auxnode->child != NULL) {
             addMultiplicityGroups(dd,auxnode->child,multiplicity,vmask,lmask);
         }
         /* Build remaining groups. */
         startV = dd->permZ[auxnode->index] / multiplicity;
         startL = auxnode->low / multiplicity;
         stopV = startV + auxnode->size / multiplicity;
         /* Walk down vmask starting at startV and build missing groups. */
         for (i = startV, j = startL; i < stopV; i++) {
             if (vmask[i] == 0) {
                 MtrNode *node;
                 while (lmask[j] == 1) j++;
                 node = Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity,
                                      MTR_FIXED);
                 if (node == NULL) {
                     return(0);
                 }
                 node->index = dd->invpermZ[i * multiplicity];
                 vmask[i] = 1;
                 lmask[j] = 1;
             }
         }
         auxnode = auxnode->younger;
     }
     return(1);
 
 } /* end of addMultiplicityGroups */

DdNode* Cudd_addConst	(	DdManager *	dd,
		CUDD_VALUE_TYPE	c
	)

Function********************************************************************

Synopsis [Returns the ADD for constant c.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_addNewVar Cudd_addIthVar]

Definition at line 620 of file cuddAPI.c.

 {
     return(cuddUniqueConst(dd,c));
 
 } /* end of Cudd_addConst */

int Cudd_AddHook	(	DdManager *	dd,
		DD_HFP	f,
		Cudd_HookType	where
	)

Function********************************************************************

Synopsis [Adds a function to a hook.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_RemoveHook]

Definition at line 3244 of file cuddAPI.c.

 {
     DdHook **hook, *nextHook, *newHook;
 
     switch (where) {
     case CUDD_PRE_GC_HOOK:
         hook = &(dd->preGCHook);
         break;
     case CUDD_POST_GC_HOOK:
         hook = &(dd->postGCHook);
         break;
     case CUDD_PRE_REORDERING_HOOK:
         hook = &(dd->preReorderingHook);
         break;
     case CUDD_POST_REORDERING_HOOK:
         hook = &(dd->postReorderingHook);
         break;
     default:
         return(0);
     }
     /* Scan the list and find whether the function is already there.
     ** If so, just return. */
     nextHook = *hook;
     while (nextHook != NULL) {
         if (nextHook->f == f) {
             return(2);
         }
         hook = &(nextHook->next);
         nextHook = nextHook->next;
     }
     /* The function was not in the list. Create a new item and append it
     ** to the end of the list. */
     newHook = ABC_ALLOC(DdHook,1);
     if (newHook == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
     newHook->next = NULL;
     newHook->f = f;
     *hook = newHook;
     return(1);
 
 } /* end of Cudd_AddHook */

DdNode* Cudd_addIthVar	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

Synopsis [Returns the ADD variable with index i.]

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

SideEffects [None]

SeeAlso [Cudd_addNewVar Cudd_bddIthVar Cudd_addConst Cudd_addNewVarAtLevel]

Definition at line 384 of file cuddAPI.c.

 {
     DdNode *res;
 
     if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
     do {
         dd->reordered = 0;
         res = cuddUniqueInter(dd,i,DD_ONE(dd),DD_ZERO(dd));
     } while (dd->reordered == 1);
 
     return(res);
 
 } /* end of Cudd_addIthVar */

DdNode* Cudd_addNewVar ( DdManager * dd )

AutomaticEnd Function********************************************************************

Synopsis [Returns a new ADD variable.]

Description [Creates a new ADD 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. An ADD variable differs from a BDD variable because it points to the arithmetic zero, instead of having a complement pointer to 1. ]

SideEffects [None]

SeeAlso [Cudd_bddNewVar Cudd_addIthVar Cudd_addConst Cudd_addNewVarAtLevel]

Definition at line 259 of file cuddAPI.c.

 {
     DdNode *res;
 
     if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
     do {
         dd->reordered = 0;
         res = cuddUniqueInter(dd,dd->size,DD_ONE(dd),DD_ZERO(dd));
     } while (dd->reordered == 1);
 
     return(res);
 
 } /* end of Cudd_addNewVar */

DdNode* Cudd_addNewVarAtLevel	(	DdManager *	dd,
		int	level
	)

Function********************************************************************

Synopsis [Returns a new ADD variable at a specified level.]

Description [Creates a new ADD variable. 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.]

SideEffects [None]

SeeAlso [Cudd_addNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel]

Definition at line 290 of file cuddAPI.c.

 {
     DdNode *res;
 
     if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
     if (level >= dd->size) return(Cudd_addIthVar(dd,level));
     if (!cuddInsertSubtables(dd,1,level)) return(NULL);
     do {
         dd->reordered = 0;
         res = cuddUniqueInter(dd,dd->size - 1,DD_ONE(dd),DD_ZERO(dd));
     } while (dd->reordered == 1);
 
     return(res);
 
 } /* end of Cudd_addNewVarAtLevel */

void Cudd_AutodynDisable ( DdManager * unique )

Function********************************************************************

Synopsis [Disables automatic dynamic reordering.]

Description []

SideEffects [None]

SeeAlso [Cudd_AutodynEnable Cudd_ReorderingStatus Cudd_AutodynDisableZdd]

Definition at line 708 of file cuddAPI.c.

 {
     unique->autoDyn = 0;
     return;
 
 } /* end of Cudd_AutodynDisable */

void Cudd_AutodynDisableZdd ( DdManager * unique )

Function********************************************************************

Synopsis [Disables automatic dynamic reordering of ZDDs.]

Description []

SideEffects [None]

SeeAlso [Cudd_AutodynEnableZdd Cudd_ReorderingStatusZdd Cudd_AutodynDisable]

Definition at line 786 of file cuddAPI.c.

 {
     unique->autoDynZ = 0;
     return;
 
 } /* end of Cudd_AutodynDisableZdd */

void Cudd_AutodynEnable	(	DdManager *	unique,
		Cudd_ReorderingType	method
	)

Function********************************************************************

Synopsis [Enables automatic dynamic reordering of BDDs and ADDs.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_AutodynDisable Cudd_ReorderingStatus Cudd_AutodynEnableZdd]

Definition at line 669 of file cuddAPI.c.

 {
     unique->autoDyn = 1;
     if (method != CUDD_REORDER_SAME) {
         unique->autoMethod = method;
     }
 #ifndef DD_NO_DEATH_ROW
     /* If reordering is enabled, using the death row causes too many
     ** invocations. Hence, we shrink the death row to just one entry.
     */
     cuddClearDeathRow(unique);
     unique->deathRowDepth = 1;
     unique->deadMask = unique->deathRowDepth - 1;
     if ((unsigned) unique->nextDead > unique->deadMask) {
         unique->nextDead = 0;
     }
     unique->deathRow = ABC_REALLOC(DdNodePtr, unique->deathRow,
         unique->deathRowDepth);
 #endif
     return;
 
 } /* end of Cudd_AutodynEnable */

void Cudd_AutodynEnableZdd	(	DdManager *	unique,
		Cudd_ReorderingType	method
	)

Function********************************************************************

Synopsis [Enables automatic dynamic reordering of ZDDs.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_AutodynDisableZdd Cudd_ReorderingStatusZdd Cudd_AutodynEnable]

Definition at line 760 of file cuddAPI.c.

 {
     unique->autoDynZ = 1;
     if (method != CUDD_REORDER_SAME) {
         unique->autoMethodZ = method;
     }
     return;
 
 } /* end of Cudd_AutodynEnableZdd */

int Cudd_bddBindVar	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Prevents sifting of a variable.]

Description [This function sets a flag to prevent sifting of a variable. Returns 1 if successful; 0 otherwise (i.e., invalid variable index).]

SideEffects [Changes the "bindVar" flag in DdSubtable.]

SeeAlso [Cudd_bddUnbindVar]

Definition at line 3899 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(0);
     dd->subtables[dd->perm[index]].bindVar = 1;
     return(1);
 
 } /* end of Cudd_bddBindVar */

int Cudd_bddIsNsVar	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Checks whether a variable is next state.]

Description [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.]

SideEffects [none]

SeeAlso [Cudd_bddSetNsVar Cudd_bddIsPiVar Cudd_bddIsPsVar]

Definition at line 4098 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return -1;
     return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_NEXT_STATE);
 
 } /* end of Cudd_bddIsNsVar */

int Cudd_bddIsPiVar	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Checks whether a variable is primary input.]

Description [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.]

SideEffects [none]

SeeAlso [Cudd_bddSetPiVar Cudd_bddIsPsVar Cudd_bddIsNsVar]

Definition at line 4050 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return -1;
     return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRIMARY_INPUT);
 
 } /* end of Cudd_bddIsPiVar */

int Cudd_bddIsPsVar	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Checks whether a variable is present state.]

Description [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.]

SideEffects [none]

SeeAlso [Cudd_bddSetPsVar Cudd_bddIsPiVar Cudd_bddIsNsVar]

Definition at line 4074 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return -1;
     return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRESENT_STATE);
 
 } /* end of Cudd_bddIsPsVar */

int Cudd_bddIsVarHardGroup	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

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

Description [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.]

SideEffects [none]

SeeAlso [Cudd_bddSetVarHardGroup]

Definition at line 4326 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(-1);
     if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_HARD_GROUP)
         return(1);
     return(0);
 
 } /* end of Cudd_bddIsVarToBeGrouped */

int Cudd_bddIsVarToBeGrouped	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Checks whether a variable is set to be grouped.]

Description [Checks whether a variable is set to be grouped. This function is used for lazy sifting.]

SideEffects [none]

SeeAlso []

Definition at line 4249 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(-1);
     if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP)
         return(0);
     else
         return(dd->subtables[dd->perm[index]].varToBeGrouped);
 
 } /* end of Cudd_bddIsVarToBeGrouped */

int Cudd_bddIsVarToBeUngrouped	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Checks whether a variable is set to be ungrouped.]

Description [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.]

SideEffects [none]

SeeAlso [Cudd_bddSetVarToBeUngrouped]

Definition at line 4301 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(-1);
     return dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP;
 
 } /* end of Cudd_bddIsVarToBeGrouped */

DdNode* Cudd_bddIthVar	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

Synopsis [Returns the BDD variable with index i.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_bddNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel Cudd_ReadVars]

Definition at line 416 of file cuddAPI.c.

 {
     DdNode *res;
 
     if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
     if (i < dd->size) {
         res = dd->vars[i];
     } else {
         res = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
     }
 
     return(res);
 
 } /* end of Cudd_bddIthVar */

DdNode* Cudd_bddNewVar ( DdManager * dd )

Function********************************************************************

Synopsis [Returns a new BDD variable.]

Description [Creates 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.]

SideEffects [None]

SeeAlso [Cudd_addNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]

Definition at line 323 of file cuddAPI.c.

 {
     DdNode *res;
 
     if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
     res = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));
 
     return(res);
 
 } /* end of Cudd_bddNewVar */

DdNode* Cudd_bddNewVarAtLevel	(	DdManager *	dd,
		int	level
	)

Function********************************************************************

Synopsis [Returns a new BDD variable at a specified level.]

Description [Creates a new BDD variable. 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.]

SideEffects [None]

SeeAlso [Cudd_bddNewVar Cudd_bddIthVar Cudd_addNewVarAtLevel]

Definition at line 351 of file cuddAPI.c.

 {
     DdNode *res;
 
     if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
     if (level >= dd->size) return(Cudd_bddIthVar(dd,level));
     if (!cuddInsertSubtables(dd,1,level)) return(NULL);
     res = dd->vars[dd->size - 1];
 
     return(res);
 
 } /* end of Cudd_bddNewVarAtLevel */

int Cudd_bddReadPairIndex	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Reads a corresponding pair index for a given index.]

Description [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.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddSetPairIndex]

Definition at line 4148 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return -1;
     return dd->subtables[dd->perm[index]].pairIndex;
 
 } /* end of Cudd_bddReadPairIndex */

void Cudd_bddRealignDisable ( DdManager * unique )

Function********************************************************************

Synopsis [Disables realignment of ZDD order to BDD order.]

Description []

SideEffects [None]

SeeAlso [Cudd_bddRealignEnable Cudd_bddRealignmentEnabled Cudd_zddRealignEnable Cudd_zddRealignmentEnabled]

Definition at line 965 of file cuddAPI.c.

 {
     unique->realignZ = 0;
     return;
 
 } /* end of Cudd_bddRealignDisable */

void Cudd_bddRealignEnable ( DdManager * unique )

Function********************************************************************

Synopsis [Enables realignment of BDD order to ZDD order.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_zddReduceHeap Cudd_bddRealignDisable Cudd_bddRealignmentEnabled Cudd_zddRealignDisable Cudd_zddRealignmentEnabled]

Definition at line 943 of file cuddAPI.c.

 {
     unique->realignZ = 1;
     return;
 
 } /* end of Cudd_bddRealignEnable */

int Cudd_bddRealignmentEnabled ( DdManager * unique )

Function********************************************************************

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

Description [Returns 1 if the realignment of BDD order to ZDD order is enabled; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddRealignEnable Cudd_bddRealignDisable Cudd_zddRealignEnable Cudd_zddRealignDisable]

Definition at line 913 of file cuddAPI.c.

 {
     return(unique->realignZ);
 
 } /* end of Cudd_bddRealignmentEnabled */

int Cudd_bddResetVarToBeGrouped	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Resets a variable not to be grouped.]

Description [Resets a variable not to be grouped. This function is used for lazy sifting. Returns 1 if successful; 0 otherwise.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddSetVarToBeGrouped Cudd_bddSetVarHardGroup]

Definition at line 4222 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(0);
     if (dd->subtables[dd->perm[index]].varToBeGrouped <=
         CUDD_LAZY_SOFT_GROUP) {
         dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_NONE;
     }
     return(1);
 
 } /* end of Cudd_bddResetVarToBeGrouped */

int Cudd_bddSetNsVar	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Sets a variable type to next state.]

Description [Sets a variable type to next state. The variable type is used by lazy sifting. Returns 1 if successful; 0 otherwise.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddSetPiVar Cudd_bddSetPsVar Cudd_bddIsNsVar]

Definition at line 4025 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return (0);
     dd->subtables[dd->perm[index]].varType = CUDD_VAR_NEXT_STATE;
     return(1);
 
 } /* end of Cudd_bddSetNsVar */

int Cudd_bddSetPairIndex	(	DdManager *	dd,
		int	index,
		int	pairIndex
	)

Function********************************************************************

Synopsis [Sets a corresponding pair index for a given index.]

Description [Sets a corresponding pair index for a given index. These pair indices are present and next state variable. Returns 1 if successful; 0 otherwise.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddReadPairIndex]

Definition at line 4122 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(0);
     dd->subtables[dd->perm[index]].pairIndex = pairIndex;
     return(1);
 
 } /* end of Cudd_bddSetPairIndex */

int Cudd_bddSetPiVar	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Sets a variable type to primary input.]

Description [Sets a variable type to primary input. The variable type is used by lazy sifting. Returns 1 if successful; 0 otherwise.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddSetPsVar Cudd_bddSetNsVar Cudd_bddIsPiVar]

Definition at line 3977 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return (0);
     dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRIMARY_INPUT;
     return(1);
 
 } /* end of Cudd_bddSetPiVar */

int Cudd_bddSetPsVar	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Sets a variable type to present state.]

Description [Sets a variable type to present state. The variable type is used by lazy sifting. Returns 1 if successful; 0 otherwise.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddSetPiVar Cudd_bddSetNsVar Cudd_bddIsPsVar]

Definition at line 4001 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return (0);
     dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRESENT_STATE;
     return(1);
 
 } /* end of Cudd_bddSetPsVar */

int Cudd_bddSetVarHardGroup	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Sets a variable to be a hard group.]

Description [Sets a variable to be a hard group. This function is used for lazy sifting. Returns 1 if successful; 0 otherwise.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddSetVarToBeGrouped Cudd_bddResetVarToBeGrouped Cudd_bddIsVarHardGroup]

Definition at line 4198 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(0);
     dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_HARD_GROUP;
     return(1);
 
 } /* end of Cudd_bddSetVarHardGrouped */

int Cudd_bddSetVarToBeGrouped	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Sets a variable to be grouped.]

Description [Sets a variable to be grouped. This function is used for lazy sifting. Returns 1 if successful; 0 otherwise.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddSetVarHardGroup Cudd_bddResetVarToBeGrouped]

Definition at line 4171 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(0);
     if (dd->subtables[dd->perm[index]].varToBeGrouped <= CUDD_LAZY_SOFT_GROUP) {
         dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_SOFT_GROUP;
     }
     return(1);
 
 } /* end of Cudd_bddSetVarToBeGrouped */

int Cudd_bddSetVarToBeUngrouped	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Sets a variable to be ungrouped.]

Description [Sets a variable to be ungrouped. This function is used for lazy sifting. Returns 1 if successful; 0 otherwise.]

SideEffects [modifies the manager]

SeeAlso [Cudd_bddIsVarToBeUngrouped]

Definition at line 4275 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(0);
     dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_UNGROUP;
     return(1);
 
 } /* end of Cudd_bddSetVarToBeGrouped */

int Cudd_bddUnbindVar	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Allows the sifting of a variable.]

Description [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).]

SideEffects [Changes the "bindVar" flag in DdSubtable.]

SeeAlso [Cudd_bddBindVar]

Definition at line 3927 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(0);
     dd->subtables[dd->perm[index]].bindVar = 0;
     return(1);
 
 } /* end of Cudd_bddUnbindVar */

int Cudd_bddVarIsBound	(	DdManager *	dd,
		int	index
	)

Function********************************************************************

Synopsis [Tells whether a variable can be sifted.]

Description [This function returns 1 if a variable is enabled for sifting. Initially all variables can be sifted. This function returns 0 only 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.]

SideEffects [none]

SeeAlso [Cudd_bddBindVar Cudd_bddUnbindVar]

Definition at line 3954 of file cuddAPI.c.

 {
     if (index >= dd->size || index < 0) return(0);
     return(dd->subtables[dd->perm[index]].bindVar);
 
 } /* end of Cudd_bddVarIsBound */

void Cudd_ClearErrorCode ( DdManager * dd )

Function********************************************************************

Synopsis [Clear the error code of a manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_ReadErrorCode]

Definition at line 3632 of file cuddAPI.c.

 {
     dd->errorCode = CUDD_NO_ERROR;
 
 } /* end of Cudd_ClearErrorCode */

int Cudd_DeadAreCounted ( DdManager * dd )

Function********************************************************************

Synopsis [Tells whether dead nodes are counted towards triggering reordering.]

Description [Tells whether dead nodes are counted towards triggering reordering. Returns 1 if dead nodes are counted; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_TurnOnCountDead Cudd_TurnOffCountDead]

Definition at line 2585 of file cuddAPI.c.

 {
     return(dd->countDead == 0 ? 1 : 0);
 
 } /* end of Cudd_DeadAreCounted */

void Cudd_DisableGarbageCollection ( DdManager * dd )

Function********************************************************************

Synopsis [Disables garbage collection.]

Description [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.)]

SideEffects [None]

SeeAlso [Cudd_EnableGarbageCollection Cudd_GarbageCollectionEnabled]

Definition at line 2563 of file cuddAPI.c.

 {
     dd->gcEnabled = 0;
 
 } /* end of Cudd_DisableGarbageCollection */

int Cudd_DisableReorderingReporting ( DdManager * dd )

Function********************************************************************

Synopsis [Disables reporting of reordering stats.]

Description [Disables reporting of reordering stats. Returns 1 if successful; 0 otherwise.]

SideEffects [Removes functions from the pre-reordering and post-reordering hooks.]

SeeAlso [Cudd_EnableReorderingReporting Cudd_ReorderingReporting]

Definition at line 3564 of file cuddAPI.c.

 {
     if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
         return(0);
     }
     if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
         return(0);
     }
     return(1);
 
 } /* end of Cudd_DisableReorderingReporting */

void Cudd_EnableGarbageCollection ( DdManager * dd )

Function********************************************************************

Synopsis [Enables garbage collection.]

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

SideEffects [None]

SeeAlso [Cudd_DisableGarbageCollection Cudd_GarbageCollectionEnabled]

Definition at line 2539 of file cuddAPI.c.

 {
     dd->gcEnabled = 1;
 
 } /* end of Cudd_EnableGarbageCollection */

int Cudd_EnableReorderingReporting ( DdManager * dd )

Function********************************************************************

Synopsis [Enables reporting of reordering stats.]

Description [Enables reporting of reordering stats. Returns 1 if successful; 0 otherwise.]

SideEffects [Installs functions in the pre-reordering and post-reordering hooks.]

SeeAlso [Cudd_DisableReorderingReporting Cudd_ReorderingReporting]

Definition at line 3536 of file cuddAPI.c.

 {
     if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
         return(0);
     }
     if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
         return(0);
     }
     return(1);
 
 } /* end of Cudd_EnableReorderingReporting */

double Cudd_ExpectedUsedSlots ( DdManager * dd )

Function********************************************************************

Synopsis [Computes the expected fraction of used slots in the unique table.]

Description [Computes the fraction of slots in the unique table that should be in use. 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.]

SideEffects [None]

SeeAlso [Cudd_ReadSlots Cudd_ReadUsedSlots]

Definition at line 1572 of file cuddAPI.c.

 {
     int i;
     int size = dd->size;
     DdSubtable *subtable;
     double empty = 0.0;
 
     /* To each subtable we apply the corollary to Theorem 8.5 (occupancy
     ** distribution) from Sedgewick and Flajolet's Analysis of Algorithms.
     ** The corollary says that for a table with M buckets and a load ratio
     ** of r, the expected number of empty buckets is asymptotically given
     ** by M * exp(-r).
     */
 
     /* Scan each BDD/ADD subtable. */
     for (i = 0; i < size; i++) {
         subtable = &(dd->subtables[i]);
         empty += (double) subtable->slots *
             exp(-(double) subtable->keys / (double) subtable->slots);
     }
 
     /* Scan the ZDD subtables. */
     size = dd->sizeZ;
 
     for (i = 0; i < size; i++) {
         subtable = &(dd->subtableZ[i]);
         empty += (double) subtable->slots *
             exp(-(double) subtable->keys / (double) subtable->slots);
     }
 
     /* Constant table. */
     subtable = &(dd->constants);
     empty += (double) subtable->slots *
         exp(-(double) subtable->keys / (double) subtable->slots);
 
     return(1.0 - empty / (double) dd->slots);
 
 } /* end of Cudd_ExpectedUsedSlots */

void Cudd_FreeTree ( DdManager * dd )

Function********************************************************************

Synopsis [Frees the variable group tree of the manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree]

Definition at line 2180 of file cuddAPI.c.

 {
     if (dd->tree != NULL) {
         Mtr_FreeTree(dd->tree);
         dd->tree = NULL;
     }
     return;
 
 } /* end of Cudd_FreeTree */

void Cudd_FreeZddTree ( DdManager * dd )

Function********************************************************************

Synopsis [Frees the variable group tree of the manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_SetZddTree Cudd_ReadZddTree Cudd_FreeTree]

Definition at line 2252 of file cuddAPI.c.

 {
     if (dd->treeZ != NULL) {
         Mtr_FreeTree(dd->treeZ);
         dd->treeZ = NULL;
     }
     return;
 
 } /* end of Cudd_FreeZddTree */

int Cudd_GarbageCollectionEnabled ( DdManager * dd )

Function********************************************************************

Synopsis [Tells whether garbage collection is enabled.]

Description [Returns 1 if garbage collection is enabled; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_EnableGarbageCollection Cudd_DisableGarbageCollection]

Definition at line 2517 of file cuddAPI.c.

 {
     return(dd->gcEnabled);
 
 } /* end of Cudd_GarbageCollectionEnabled */

int Cudd_IsInHook	(	DdManager *	dd,
		DD_HFP	f,
		Cudd_HookType	where
	)

Function********************************************************************

Synopsis [Checks whether a function is in a hook.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_AddHook Cudd_RemoveHook]

Definition at line 3359 of file cuddAPI.c.

 {
     DdHook *hook;
 
     switch (where) {
     case CUDD_PRE_GC_HOOK:
         hook = dd->preGCHook;
         break;
     case CUDD_POST_GC_HOOK:
         hook = dd->postGCHook;
         break;
     case CUDD_PRE_REORDERING_HOOK:
         hook = dd->preReorderingHook;
         break;
     case CUDD_POST_REORDERING_HOOK:
         hook = dd->postReorderingHook;
         break;
     default:
         return(0);
     }
     /* Scan the list and find whether the function is already there. */
     while (hook != NULL) {
         if (hook->f == f) {
             return(1);
         }
         hook = hook->next;
     }
     return(0);
 
 } /* end of Cudd_IsInHook */

int Cudd_IsNonConstant ( DdNode * f )

Function********************************************************************

Synopsis [Returns 1 if a DD node is not constant.]

Description [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 the macro Cudd_IsConstant can be used.]

SideEffects [None]

SeeAlso [Cudd_IsConstant Cudd_bddIteConstant Cudd_addIteConstant Cudd_addEvalConst]

Definition at line 645 of file cuddAPI.c.

 {
     return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f));
 
 } /* end of Cudd_IsNonConstant */

unsigned int Cudd_NodeReadIndex ( DdNode * node )

Function********************************************************************

Synopsis [Returns the index of the node.]

Description [Returns the index of the node. The node pointer can be either regular or complemented.]

SideEffects [None]

SeeAlso [Cudd_ReadIndex]

Definition at line 2277 of file cuddAPI.c.

 {
     return((unsigned int) Cudd_Regular(node)->index);
 
 } /* end of Cudd_NodeReadIndex */

int Cudd_PrintInfo	(	DdManager *	dd,
		FILE *	fp
	)

Function********************************************************************

Synopsis [Prints out statistics and settings for a CUDD manager.]

Description [Prints out statistics and settings for a CUDD manager. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 2937 of file cuddAPI.c.

 {
     int retval;
     Cudd_ReorderingType autoMethod, autoMethodZ;
 
     /* Modifiable parameters. */
     retval = fprintf(fp,"**** CUDD modifiable parameters ****\n");
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Hard limit for cache size: %u\n",
                      Cudd_ReadMaxCacheHard(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Cache hit threshold for resizing: %u%%\n",
                      Cudd_ReadMinHit(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Garbage collection enabled: %s\n",
                      Cudd_GarbageCollectionEnabled(dd) ? "yes" : "no");
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Limit for fast unique table growth: %u\n",
                      Cudd_ReadLooseUpTo(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,
                      "Maximum number of variables sifted per reordering: %d\n",
                      Cudd_ReadSiftMaxVar(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,
                      "Maximum number of variable swaps per reordering: %d\n",
                      Cudd_ReadSiftMaxSwap(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Maximum growth while sifting a variable: %g\n",
                      Cudd_ReadMaxGrowth(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Dynamic reordering of BDDs enabled: %s\n",
                      Cudd_ReorderingStatus(dd,&autoMethod) ? "yes" : "no");
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Default BDD reordering method: %d\n",
                      (int) autoMethod);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Dynamic reordering of ZDDs enabled: %s\n",
                      Cudd_ReorderingStatusZdd(dd,&autoMethodZ) ? "yes" : "no");
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Default ZDD reordering method: %d\n",
                      (int) autoMethodZ);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Realignment of ZDDs to BDDs enabled: %s\n",
                      Cudd_zddRealignmentEnabled(dd) ? "yes" : "no");
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Realignment of BDDs to ZDDs enabled: %s\n",
                      Cudd_bddRealignmentEnabled(dd) ? "yes" : "no");
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Dead nodes counted in triggering reordering: %s\n",
                      Cudd_DeadAreCounted(dd) ? "yes" : "no");
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Group checking criterion: %d\n",
                      (int) Cudd_ReadGroupcheck(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Recombination threshold: %d\n", Cudd_ReadRecomb(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Symmetry violation threshold: %d\n",
                      Cudd_ReadSymmviolation(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Arc violation threshold: %d\n",
                      Cudd_ReadArcviolation(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"GA population size: %d\n",
                      Cudd_ReadPopulationSize(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of crossovers for GA: %d\n",
                      Cudd_ReadNumberXovers(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Next reordering threshold: %u\n",
                      Cudd_ReadNextReordering(dd));
     if (retval == EOF) return(0);
 
     /* Non-modifiable parameters. */
     retval = fprintf(fp,"**** CUDD non-modifiable parameters ****\n");
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Memory in use: %lu\n", Cudd_ReadMemoryInUse(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Peak number of nodes: %ld\n",
                      Cudd_ReadPeakNodeCount(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Peak number of live nodes: %d\n",
                      Cudd_ReadPeakLiveNodeCount(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of BDD variables: %d\n", dd->size);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of ZDD variables: %d\n", dd->sizeZ);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of cache entries: %u\n", dd->cacheSlots);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of cache look-ups: %.0f\n",
                      Cudd_ReadCacheLookUps(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of cache hits: %.0f\n",
                      Cudd_ReadCacheHits(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of cache insertions: %.0f\n",
                      dd->cacheinserts);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of cache collisions: %.0f\n",
                      dd->cachecollisions);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of cache deletions: %.0f\n",
                      dd->cachedeletions);
     if (retval == EOF) return(0);
     retval = cuddCacheProfile(dd,fp);
     if (retval == 0) return(0);
     retval = fprintf(fp,"Soft limit for cache size: %u\n",
                      Cudd_ReadMaxCache(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of buckets in unique table: %u\n", dd->slots);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Used buckets in unique table: %.2f%% (expected %.2f%%)\n",
                      100.0 * Cudd_ReadUsedSlots(dd),
                      100.0 * Cudd_ExpectedUsedSlots(dd));
     if (retval == EOF) return(0);
 #ifdef DD_UNIQUE_PROFILE
     retval = fprintf(fp,"Unique lookups: %.0f\n", dd->uniqueLookUps);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Unique links: %.0f (%g per lookup)\n",
             dd->uniqueLinks, dd->uniqueLinks / dd->uniqueLookUps);
     if (retval == EOF) return(0);
 #endif
     retval = fprintf(fp,"Number of BDD and ADD nodes: %u\n", dd->keys);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of ZDD nodes: %u\n", dd->keysZ);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of dead BDD and ADD nodes: %u\n", dd->dead);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Total number of nodes allocated: %d\n", (int)dd->allocated);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n",
                      dd->reclaimed);
     if (retval == EOF) return(0);
 #ifdef DD_STATS
     retval = fprintf(fp,"Nodes freed: %.0f\n", dd->nodesFreed);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Nodes dropped: %.0f\n", dd->nodesDropped);
     if (retval == EOF) return(0);
 #endif
 #ifdef DD_COUNT
     retval = fprintf(fp,"Number of recursive calls: %.0f\n",
                      Cudd_ReadRecursiveCalls(dd));
     if (retval == EOF) return(0);
 #endif
     retval = fprintf(fp,"Garbage collections so far: %d\n",
                      Cudd_ReadGarbageCollections(dd));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Time for garbage collection: %.2f sec\n",
                      ((double)Cudd_ReadGarbageCollectionTime(dd)/1000.0));
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Reorderings so far: %d\n", dd->reorderings);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Time for reordering: %.2f sec\n",
                      ((double)Cudd_ReadReorderingTime(dd)/1000.0));
     if (retval == EOF) return(0);
 #ifdef DD_COUNT
     retval = fprintf(fp,"Node swaps in reordering: %.0f\n",
         Cudd_ReadSwapSteps(dd));
     if (retval == EOF) return(0);
 #endif
 
     return(1);
 
 } /* end of Cudd_PrintInfo */

int Cudd_ReadArcviolation ( DdManager * dd )

Function********************************************************************

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

Description [Returns the current value of the arcviolation parameter. This parameter is used in group sifting 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.]

SideEffects [None]

SeeAlso [Cudd_SetArcviolation]

Definition at line 2764 of file cuddAPI.c.

 {
     return(dd->arcviolation);
 
 } /* end of Cudd_ReadArcviolation */

DdNode* Cudd_ReadBackground ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the background constant of the manager.]

Description []

SideEffects [None]

Definition at line 1112 of file cuddAPI.c.

 {
     return(dd->background);
 
 } /* end of Cudd_ReadBackground */

double Cudd_ReadCacheHits ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of cache hits.]

Description []

SideEffects [None]

SeeAlso [Cudd_ReadCacheLookUps]

Definition at line 1225 of file cuddAPI.c.

 {
     return(dd->cacheHits + dd->totCachehits);
 
 } /* end of Cudd_ReadCacheHits */

double Cudd_ReadCacheLookUps ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of cache look-ups.]

Description [Returns the number of cache look-ups.]

SideEffects [None]

SeeAlso [Cudd_ReadCacheHits]

Definition at line 1204 of file cuddAPI.c.

 {
     return(dd->cacheHits + dd->cacheMisses +
            dd->totCachehits + dd->totCacheMisses);
 
 } /* end of Cudd_ReadCacheLookUps */

unsigned int Cudd_ReadCacheSlots ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the number of slots in the cache.]

Description []

SideEffects [None]

SeeAlso [Cudd_ReadCacheUsedSlots]

Definition at line 1152 of file cuddAPI.c.

 {
     return(dd->cacheSlots);
 
 } /* end of Cudd_ReadCacheSlots */

double Cudd_ReadCacheUsedSlots ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the fraction of used slots in the cache.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadCacheSlots]

Definition at line 1175 of file cuddAPI.c.

 {
     unsigned long used = 0;
     int slots = dd->cacheSlots;
     DdCache *cache = dd->cache;
     int i;
 
     for (i = 0; i < slots; i++) {
         used += cache[i].h != 0;
     }
 
     return((double)used / (double) dd->cacheSlots);
 
 } /* end of Cudd_ReadCacheUsedSlots */

unsigned int Cudd_ReadDead ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of dead nodes in the unique table.]

Description []

SideEffects [None]

SeeAlso [Cudd_ReadKeys]

Definition at line 1646 of file cuddAPI.c.

 {
     return(dd->dead);
 
 } /* end of Cudd_ReadDead */

CUDD_VALUE_TYPE Cudd_ReadEpsilon ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the epsilon parameter of the manager.]

Description [Reads the epsilon parameter of the manager. The epsilon parameter control the comparison between floating point numbers.]

SideEffects [None]

SeeAlso [Cudd_SetEpsilon]

Definition at line 2430 of file cuddAPI.c.

 {
     return(dd->epsilon);
 
 } /* end of Cudd_ReadEpsilon */

Cudd_ErrorType Cudd_ReadErrorCode ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the code of the last error.]

Description [Returns the code of the last error. The error codes are defined in cudd.h.]

SideEffects [None]

SeeAlso [Cudd_ClearErrorCode]

Definition at line 3612 of file cuddAPI.c.

 {
     return(dd->errorCode);
 
 } /* end of Cudd_ReadErrorCode */

int Cudd_ReadGarbageCollections ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of times garbage collection has occurred.]

Description [Returns the number of times garbage collection has occurred in the manager. The number includes both the calls from reordering procedures and those caused by requests to create new nodes.]

SideEffects [None]

SeeAlso [Cudd_ReadGarbageCollectionTime]

Definition at line 1741 of file cuddAPI.c.

 {
     return(dd->garbageCollections);
 
 } /* end of Cudd_ReadGarbageCollections */

long Cudd_ReadGarbageCollectionTime ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the time spent in garbage collection.]

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

SideEffects [None]

SeeAlso [Cudd_ReadGarbageCollections]

Definition at line 1762 of file cuddAPI.c.

 {
     return(dd->GCTime);
 
 } /* end of Cudd_ReadGarbageCollectionTime */

Cudd_AggregationType Cudd_ReadGroupcheck ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the groupcheck parameter of the manager.]

Description [Reads the groupcheck parameter of the manager. The groupcheck parameter determines the aggregation criterion in group sifting.]

SideEffects [None]

SeeAlso [Cudd_SetGroupcheck]

Definition at line 2474 of file cuddAPI.c.

 {
     return(dd->groupcheck);
 
 } /* end of Cudd_ReadGroupCheck */

int Cudd_ReadInvPerm	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

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

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadPerm Cudd_ReadInvPermZdd]

Definition at line 2354 of file cuddAPI.c.

 {
     if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
     if (i < 0 || i >= dd->size) return(-1);
     return(dd->invperm[i]);
 
 } /* end of Cudd_ReadInvPerm */

int Cudd_ReadInvPermZdd	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

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

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadPerm Cudd_ReadInvPermZdd]

Definition at line 2380 of file cuddAPI.c.

 {
     if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
     if (i < 0 || i >= dd->sizeZ) return(-1);
     return(dd->invpermZ[i]);
 
 } /* end of Cudd_ReadInvPermZdd */

unsigned int Cudd_ReadKeys ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of nodes in the unique table.]

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

SideEffects [None]

SeeAlso [Cudd_ReadDead]

Definition at line 1626 of file cuddAPI.c.

 {
     return(dd->keys);
 
 } /* end of Cudd_ReadKeys */

DdNode* Cudd_ReadLogicZero ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the logic zero constant of the manager.]

Description [Returns the zero constant of the manager. The logic zero constant is the complement of the one constant, and is distinct from the arithmetic zero.]

SideEffects [None]

SeeAlso [Cudd_ReadOne Cudd_ReadZero]

Definition at line 1058 of file cuddAPI.c.

 {
     return(Cudd_Not(DD_ONE(dd)));
 
 } /* end of Cudd_ReadLogicZero */

unsigned int Cudd_ReadLooseUpTo ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the looseUpTo parameter of the manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_SetLooseUpTo Cudd_ReadMinHit Cudd_ReadMinDead]

Definition at line 1321 of file cuddAPI.c.

 {
     return(dd->looseUpTo);
 
 } /* end of Cudd_ReadLooseUpTo */

unsigned int Cudd_ReadMaxCache ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the soft limit for the cache size.]

Description [Returns the soft limit for the cache size. The soft limit]

SideEffects [None]

SeeAlso [Cudd_ReadMaxCache]

Definition at line 1371 of file cuddAPI.c.

 {
     return(2 * dd->cacheSlots + dd->cacheSlack);
 
 } /* end of Cudd_ReadMaxCache */

unsigned int Cudd_ReadMaxCacheHard ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the maxCacheHard parameter of the manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_SetMaxCacheHard Cudd_ReadMaxCache]

Definition at line 1391 of file cuddAPI.c.

 {
     return(dd->maxCacheHard);
 
 } /* end of Cudd_ReadMaxCache */

double Cudd_ReadMaxGrowth ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the maxGrowth parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_SetMaxGrowth Cudd_ReadMaxGrowthAlternate]

Definition at line 1988 of file cuddAPI.c.

 {
     return(dd->maxGrowth);
 
 } /* end of Cudd_ReadMaxGrowth */

double Cudd_ReadMaxGrowthAlternate ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the maxGrowthAlt parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]

Definition at line 2039 of file cuddAPI.c.

 {
     return(dd->maxGrowthAlt);
 
 } /* end of Cudd_ReadMaxGrowthAlternate */

unsigned int Cudd_ReadMaxLive ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the maximum allowed number of live nodes.]

Description [Reads the maximum allowed number of live nodes. When this number is exceeded, the package returns NULL.]

SideEffects [none]

SeeAlso [Cudd_SetMaxLive]

Definition at line 3812 of file cuddAPI.c.

 {
     return(dd->maxLive);
 
 } /* end of Cudd_ReadMaxLive */

unsigned long Cudd_ReadMaxMemory ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the maximum allowed memory.]

Description [Reads the maximum allowed memory. When this number is exceeded, the package returns NULL.]

SideEffects [none]

SeeAlso [Cudd_SetMaxMemory]

Definition at line 3855 of file cuddAPI.c.

 {
     return(dd->maxmemhard);
 
 } /* end of Cudd_ReadMaxMemory */

unsigned long Cudd_ReadMemoryInUse ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the memory in use by the manager measured in bytes.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 2916 of file cuddAPI.c.

 {
     return(dd->memused);
 
 } /* end of Cudd_ReadMemoryInUse */

unsigned int Cudd_ReadMinDead ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the minDead parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadDead Cudd_ReadLooseUpTo Cudd_SetLooseUpTo]

Definition at line 1670 of file cuddAPI.c.

 {
     return(dd->minDead);
 
 } /* end of Cudd_ReadMinDead */

unsigned int Cudd_ReadMinHit ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the hit rate that causes resizinig of the computed table.]

Description []

SideEffects [None]

SeeAlso [Cudd_SetMinHit]

Definition at line 1272 of file cuddAPI.c.

 {
     /* Internally, the package manipulates the ratio of hits to
     ** misses instead of the ratio of hits to accesses. */
     return((unsigned int) (0.5 + 100 * dd->minHit / (1 + dd->minHit)));
 
 } /* end of Cudd_ReadMinHit */

DdNode* Cudd_ReadMinusInfinity ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the minus-infinity constant from the manager.]

Description []

SideEffects [None]

Definition at line 1094 of file cuddAPI.c.

 {
     return(dd->minusinfinity);
 
 } /* end of Cudd_ReadMinusInfinity */

unsigned int Cudd_ReadNextReordering ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the threshold for the next dynamic reordering.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_SetNextReordering]

Definition at line 3742 of file cuddAPI.c.

 {
     return(dd->nextDyn);
 
 } /* end of Cudd_ReadNextReordering */

long Cudd_ReadNodeCount ( DdManager * dd )

Function********************************************************************

Synopsis [Reports the number of nodes in BDDs and ADDs.]

Description [Reports the number of live 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.]

SideEffects [None]

SeeAlso [Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount]

Definition at line 3179 of file cuddAPI.c.

 {
     long count;
     int i;
 
 #ifndef DD_NO_DEATH_ROW
     cuddClearDeathRow(dd);
 #endif
 
     count = (long) (dd->keys - dd->dead);
 
     /* Count isolated projection functions. Their number is subtracted
     ** from the node count because they are not part of the BDDs.
     */
     for (i=0; i < dd->size; i++) {
         if (dd->vars[i]->ref == 1) count--;
     }
     /* Subtract from the count the unused constants. */
     if (DD_ZERO(dd)->ref == 1) count--;
     if (DD_PLUS_INFINITY(dd)->ref == 1) count--;
     if (DD_MINUS_INFINITY(dd)->ref == 1) count--;
 
     return(count);
 
 } /* end of Cudd_ReadNodeCount */

double Cudd_ReadNodesDropped ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of nodes dropped.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadNodesFreed]

Definition at line 1810 of file cuddAPI.c.

 {
 #ifdef DD_STATS
     return(dd->nodesDropped);
 #else
     return(-1.0);
 #endif
 
 } /* end of Cudd_ReadNodesDropped */

double Cudd_ReadNodesFreed ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of nodes freed.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadNodesDropped]

Definition at line 1784 of file cuddAPI.c.

 {
 #ifdef DD_STATS
     return(dd->nodesFreed);
 #else
     return(-1.0);
 #endif
 
 } /* end of Cudd_ReadNodesFreed */

int Cudd_ReadNumberXovers ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the current number of crossovers used by the genetic algorithm for reordering.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_SetNumberXovers]

Definition at line 2870 of file cuddAPI.c.

 {
     return(dd->numberXovers);
 
 } /* end of Cudd_ReadNumberXovers */

DdNode* Cudd_ReadOne ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the one constant of the manager.]

Description [Returns the one constant of the manager. The one constant is common to ADDs and BDDs.]

SideEffects [None]

SeeAlso [Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne]

Definition at line 987 of file cuddAPI.c.

 {
     return(dd->one);
 
 } /* end of Cudd_ReadOne */

int Cudd_ReadPeakLiveNodeCount ( DdManager * dd )

Function********************************************************************

Synopsis [Reports the peak number of live nodes.]

Description [Reports the peak number of live nodes. This count is kept only if CUDD is compiled with DD_STATS defined. If DD_STATS is not defined, this function returns -1.]

SideEffects [None]

SeeAlso [Cudd_ReadNodeCount Cudd_PrintInfo Cudd_ReadPeakNodeCount]

Definition at line 3151 of file cuddAPI.c.

 {
     unsigned int live = dd->keys - dd->dead;
 
     if (live > dd->peakLiveNodes) {
         dd->peakLiveNodes = live;
     }
     return((int)dd->peakLiveNodes);
 
 } /* end of Cudd_ReadPeakLiveNodeCount */

long Cudd_ReadPeakNodeCount ( DdManager * dd )

Function********************************************************************

Synopsis [Reports the peak number of nodes.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadNodeCount Cudd_PrintInfo]

Definition at line 3122 of file cuddAPI.c.

 {
     long count = 0;
     DdNodePtr *scan = dd->memoryList;
 
     while (scan != NULL) {
         count += DD_MEM_CHUNK;
         scan = (DdNodePtr *) *scan;
     }
     return(count);
 
 } /* end of Cudd_ReadPeakNodeCount */

int Cudd_ReadPerm	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

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

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadInvPerm Cudd_ReadPermZdd]

Definition at line 2301 of file cuddAPI.c.

 {
     if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
     if (i < 0 || i >= dd->size) return(-1);
     return(dd->perm[i]);
 
 } /* end of Cudd_ReadPerm */

int Cudd_ReadPermZdd	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

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

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadInvPermZdd Cudd_ReadPerm]

Definition at line 2328 of file cuddAPI.c.

 {
     if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
     if (i < 0 || i >= dd->sizeZ) return(-1);
     return(dd->permZ[i]);
 
 } /* end of Cudd_ReadPermZdd */

DdNode* Cudd_ReadPlusInfinity ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the plus-infinity constant from the manager.]

Description []

SideEffects [None]

Definition at line 1076 of file cuddAPI.c.

 {
     return(dd->plusinfinity);
 
 } /* end of Cudd_ReadPlusInfinity */

int Cudd_ReadPopulationSize ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the current size of the population used by the genetic algorithm for reordering.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_SetPopulationSize]

Definition at line 2817 of file cuddAPI.c.

 {
     return(dd->populationSize);
 
 } /* end of Cudd_ReadPopulationSize */

int Cudd_ReadRecomb ( DdManager * dd )

Function********************************************************************

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

Description [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.]

SideEffects [None]

SeeAlso [Cudd_SetRecomb]

Definition at line 2657 of file cuddAPI.c.

 {
     return(dd->recomb);
 
 } /* end of Cudd_ReadRecomb */

double Cudd_ReadRecursiveCalls ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of recursive calls.]

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

SideEffects [None]

SeeAlso []

Definition at line 1246 of file cuddAPI.c.

 {
 #ifdef DD_COUNT
     return(dd->recursiveCalls);
 #else
     return(-1.0);
 #endif
 
 } /* end of Cudd_ReadRecursiveCalls */

int Cudd_ReadReorderingCycle ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the reordCycle parameter of the manager.]

Description [Reads the reordCycle parameter of the manager. This parameter determines how often the alternate threshold on maximum growth is used in reordering.]

SideEffects [None]

SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate Cudd_SetReorderingCycle]

Definition at line 2088 of file cuddAPI.c.

 {
     return(dd->reordCycle);
 
 } /* end of Cudd_ReadReorderingCycle */

int Cudd_ReadReorderings ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of times reordering has occurred.]

Description [Returns the number of times reordering has occurred in the manager. 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.]

SideEffects [None]

SeeAlso [Cudd_ReduceHeap Cudd_ReadReorderingTime]

Definition at line 1696 of file cuddAPI.c.

 {
     return(dd->reorderings);
 
 } /* end of Cudd_ReadReorderings */

long Cudd_ReadReorderingTime ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the time spent in reordering.]

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

SideEffects [None]

SeeAlso [Cudd_ReadReorderings]

Definition at line 1718 of file cuddAPI.c.

 {
     return(dd->reordTime);
 
 } /* end of Cudd_ReadReorderingTime */

int Cudd_ReadSiftMaxSwap ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the siftMaxSwap parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadSiftMaxVar Cudd_SetSiftMaxSwap]

Definition at line 1938 of file cuddAPI.c.

 {
     return(dd->siftMaxSwap);
 
 } /* end of Cudd_ReadSiftMaxSwap */

int Cudd_ReadSiftMaxVar ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the siftMaxVar parameter of the manager.]

Description [Reads the siftMaxVar parameter of the manager. This parameter gives the maximum number of variables that will be sifted for each invocation of sifting.]

SideEffects [None]

SeeAlso [Cudd_ReadSiftMaxSwap Cudd_SetSiftMaxVar]

Definition at line 1891 of file cuddAPI.c.

 {
     return(dd->siftMaxVar);
 
 } /* end of Cudd_ReadSiftMaxVar */

int Cudd_ReadSize ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of BDD variables in existance.]

Description []

SideEffects [None]

SeeAlso [Cudd_ReadZddSize]

Definition at line 1441 of file cuddAPI.c.

 {
     return(dd->size);
 
 } /* end of Cudd_ReadSize */

unsigned int Cudd_ReadSlots ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the total number of slots of the unique table.]

Description [Returns the total number of slots of the unique table. This number ismainly for diagnostic purposes.]

SideEffects [None]

Definition at line 1480 of file cuddAPI.c.

 {
     return(dd->slots);
 
 } /* end of Cudd_ReadSlots */

FILE* Cudd_ReadStderr ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the stderr of a manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_SetStderr Cudd_ReadStdout]

Definition at line 3697 of file cuddAPI.c.

 {
     return(dd->err);
 
 } /* end of Cudd_ReadStderr */

FILE* Cudd_ReadStdout ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the stdout of a manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_SetStdout Cudd_ReadStderr]

Definition at line 3654 of file cuddAPI.c.

 {
     return(dd->out);
 
 } /* end of Cudd_ReadStdout */

double Cudd_ReadSwapSteps ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the number of elementary reordering steps.]

Description []

SideEffects [none]

SeeAlso []

Definition at line 3787 of file cuddAPI.c.

 {
 #ifdef DD_COUNT
     return(dd->swapSteps);
 #else
     return(-1);
 #endif
 
 } /* end of Cudd_ReadSwapSteps */

int Cudd_ReadSymmviolation ( DdManager * dd )

Function********************************************************************

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

Description [Returns the current value of the symmviolation parameter. 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.]

SideEffects [None]

SeeAlso [Cudd_SetSymmviolation]

Definition at line 2710 of file cuddAPI.c.

 {
     return(dd->symmviolation);
 
 } /* end of Cudd_ReadSymmviolation */

MtrNode* Cudd_ReadTree ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the variable group tree of the manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree]

Definition at line 2132 of file cuddAPI.c.

 {
     return(dd->tree);
 
 } /* end of Cudd_ReadTree */

double Cudd_ReadUniqueLinks ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of links followed in the unique table.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadUniqueLookUps]

Definition at line 1865 of file cuddAPI.c.

 {
 #ifdef DD_UNIQUE_PROFILE
     return(dd->uniqueLinks);
 #else
     return(-1.0);
 #endif
 
 } /* end of Cudd_ReadUniqueLinks */

double Cudd_ReadUniqueLookUps ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of look-ups in the unique table.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadUniqueLinks]

Definition at line 1836 of file cuddAPI.c.

 {
 #ifdef DD_UNIQUE_PROFILE
     return(dd->uniqueLookUps);
 #else
     return(-1.0);
 #endif
 
 } /* end of Cudd_ReadUniqueLookUps */

double Cudd_ReadUsedSlots ( DdManager * dd )

Function********************************************************************

Synopsis [Reads the fraction of used slots in the unique table.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadSlots]

Definition at line 1503 of file cuddAPI.c.

 {
     unsigned long used = 0;
     int i, j;
     int size = dd->size;
     DdNodePtr *nodelist;
     DdSubtable *subtable;
     DdNode *node;
     DdNode *sentinel = &(dd->sentinel);
 
     /* Scan each BDD/ADD subtable. */
     for (i = 0; i < size; i++) {
         subtable = &(dd->subtables[i]);
         nodelist = subtable->nodelist;
         for (j = 0; (unsigned) j < subtable->slots; j++) {
             node = nodelist[j];
             if (node != sentinel) {
                 used++;
             }
         }
     }
 
     /* Scan the ZDD subtables. */
     size = dd->sizeZ;
 
     for (i = 0; i < size; i++) {
         subtable = &(dd->subtableZ[i]);
         nodelist = subtable->nodelist;
         for (j = 0; (unsigned) j < subtable->slots; j++) {
             node = nodelist[j];
             if (node != NULL) {
                 used++;
             }
         }
     }
 
     /* Constant table. */
     subtable = &(dd->constants);
     nodelist = subtable->nodelist;
     for (j = 0; (unsigned) j < subtable->slots; j++) {
         node = nodelist[j];
         if (node != NULL) {
             used++;
         }
     }
 
     return((double)used / (double) dd->slots);
 
 } /* end of Cudd_ReadUsedSlots */

DdNode* Cudd_ReadVars	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

Synopsis [Returns the i-th element of the vars array.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_bddIthVar]

Definition at line 2407 of file cuddAPI.c.

 {
     if (i < 0 || i > dd->size) return(NULL);
     return(dd->vars[i]);
 
 } /* end of Cudd_ReadVars */

DdNode* Cudd_ReadZddOne	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

Synopsis [Returns the ZDD for the constant 1 function.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadOne]

Definition at line 1010 of file cuddAPI.c.

 {
     if (i < 0)
         return(NULL);
     return(i < dd->sizeZ ? dd->univ[i] : DD_ONE(dd));
 
 } /* end of Cudd_ReadZddOne */

int Cudd_ReadZddSize ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the number of ZDD variables in existance.]

Description []

SideEffects [None]

SeeAlso [Cudd_ReadSize]

Definition at line 1461 of file cuddAPI.c.

 {
     return(dd->sizeZ);
 
 } /* end of Cudd_ReadZddSize */

MtrNode* Cudd_ReadZddTree ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the variable group tree of the manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree]

Definition at line 2204 of file cuddAPI.c.

 {
     return(dd->treeZ);
 
 } /* end of Cudd_ReadZddTree */

DdNode* Cudd_ReadZero ( DdManager * dd )

Function********************************************************************

Synopsis [Returns the zero constant of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadOne Cudd_ReadLogicZero]

Definition at line 1036 of file cuddAPI.c.

 {
     return(DD_ZERO(dd));
 
 } /* end of Cudd_ReadZero */

int Cudd_RemoveHook	(	DdManager *	dd,
		DD_HFP	f,
		Cudd_HookType	where
	)

Function********************************************************************

Synopsis [Removes a function from a hook.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_AddHook]

Definition at line 3306 of file cuddAPI.c.

 {
     DdHook **hook, *nextHook;
 
     switch (where) {
     case CUDD_PRE_GC_HOOK:
         hook = &(dd->preGCHook);
         break;
     case CUDD_POST_GC_HOOK:
         hook = &(dd->postGCHook);
         break;
     case CUDD_PRE_REORDERING_HOOK:
         hook = &(dd->preReorderingHook);
         break;
     case CUDD_POST_REORDERING_HOOK:
         hook = &(dd->postReorderingHook);
         break;
     default:
         return(0);
     }
     nextHook = *hook;
     while (nextHook != NULL) {
         if (nextHook->f == f) {
             *hook = nextHook->next;
             ABC_FREE(nextHook);
             return(1);
         }
         hook = &(nextHook->next);
         nextHook = nextHook->next;
     }
 
     return(0);
 
 } /* end of Cudd_RemoveHook */

int Cudd_ReorderingReporting ( DdManager * dd )

Function********************************************************************

Synopsis [Returns 1 if reporting of reordering stats is enabled.]

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

SideEffects [none]

SeeAlso [Cudd_EnableReorderingReporting Cudd_DisableReorderingReporting]

Definition at line 3591 of file cuddAPI.c.

 {
     return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK));
 
 } /* end of Cudd_ReorderingReporting */

int Cudd_ReorderingStatus	(	DdManager *	unique,
		Cudd_ReorderingType *	method
	)

Function********************************************************************

Synopsis [Reports the status of automatic dynamic reordering of BDDs and ADDs.]

Description [Reports the status of automatic dynamic reordering of BDDs and ADDs. Parameter method is set to the reordering method currently selected. Returns 1 if automatic reordering is enabled; 0 otherwise.]

SideEffects [Parameter method is set to the reordering method currently selected.]

SeeAlso [Cudd_AutodynEnable Cudd_AutodynDisable Cudd_ReorderingStatusZdd]

Definition at line 735 of file cuddAPI.c.

 {
     *method = unique->autoMethod;
     return(unique->autoDyn);
 
 } /* end of Cudd_ReorderingStatus */

int Cudd_ReorderingStatusZdd	(	DdManager *	unique,
		Cudd_ReorderingType *	method
	)

Function********************************************************************

Synopsis [Reports the status of automatic dynamic reordering of ZDDs.]

Description [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.]

SideEffects [Parameter method is set to the ZDD reordering method currently selected.]

SeeAlso [Cudd_AutodynEnableZdd Cudd_AutodynDisableZdd Cudd_ReorderingStatus]

Definition at line 812 of file cuddAPI.c.

 {
     *method = unique->autoMethodZ;
     return(unique->autoDynZ);
 
 } /* end of Cudd_ReorderingStatusZdd */

void Cudd_SetArcviolation	(	DdManager *	dd,
		int	arcviolation
	)

Function********************************************************************

Synopsis [Sets the value of the arcviolation parameter used in group sifting.]

Description [Sets the value of the arcviolation parameter. This parameter is used in group sifting 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.]

SideEffects [None]

SeeAlso [Cudd_ReadArcviolation]

Definition at line 2790 of file cuddAPI.c.

 {
     dd->arcviolation = arcviolation;
 
 } /* end of Cudd_SetArcviolation */

void Cudd_SetBackground	(	DdManager *	dd,
		DdNode *	bck
	)

Function********************************************************************

Synopsis [Sets the background constant of the manager.]

Description [Sets the background constant of the manager. It assumes that the DdNode pointer bck is already referenced.]

SideEffects [None]

Definition at line 1131 of file cuddAPI.c.

 {
     dd->background = bck;
 
 } /* end of Cudd_SetBackground */

void Cudd_SetEpsilon	(	DdManager *	dd,
		CUDD_VALUE_TYPE	ep
	)

Function********************************************************************

Synopsis [Sets the epsilon parameter of the manager to ep.]

Description [Sets the epsilon parameter of the manager to ep. The epsilon parameter control the comparison between floating point numbers.]

SideEffects [None]

SeeAlso [Cudd_ReadEpsilon]

Definition at line 2451 of file cuddAPI.c.

 {
     dd->epsilon = ep;
 
 } /* end of Cudd_SetEpsilon */

void Cudd_SetGroupcheck	(	DdManager *	dd,
		Cudd_AggregationType	gc
	)

Function********************************************************************

Synopsis [Sets the parameter groupcheck of the manager to gc.]

Description [Sets the parameter groupcheck of the manager to gc. The groupcheck parameter determines the aggregation criterion in group sifting.]

SideEffects [None]

SeeAlso [Cudd_ReadGroupCheck]

Definition at line 2496 of file cuddAPI.c.

 {
     dd->groupcheck = gc;
 
 } /* end of Cudd_SetGroupcheck */

void Cudd_SetLooseUpTo	(	DdManager *	dd,
		unsigned int	lut
	)

Function********************************************************************

Synopsis [Sets the looseUpTo parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadLooseUpTo Cudd_SetMinHit]

Definition at line 1345 of file cuddAPI.c.

 {
     if (lut == 0) {
         unsigned long datalimit = getSoftDataLimit();
         lut = (unsigned int) (datalimit / (sizeof(DdNode) *
                                            DD_MAX_LOOSE_FRACTION));
     }
     dd->looseUpTo = lut;
 
 } /* end of Cudd_SetLooseUpTo */

void Cudd_SetMaxCacheHard	(	DdManager *	dd,
		unsigned int	mc
	)

Function********************************************************************

Synopsis [Sets the maxCacheHard parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadMaxCacheHard Cudd_SetMaxCache]

Definition at line 1415 of file cuddAPI.c.

 {
     if (mc == 0) {
         unsigned long datalimit = getSoftDataLimit();
         mc = (unsigned int) (datalimit / (sizeof(DdCache) *
                                           DD_MAX_CACHE_FRACTION));
     }
     dd->maxCacheHard = mc;
 
 } /* end of Cudd_SetMaxCacheHard */

void Cudd_SetMaxGrowth	(	DdManager *	dd,
		double	mg
	)

Function********************************************************************

Synopsis [Sets the maxGrowth parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate]

Definition at line 2013 of file cuddAPI.c.

 {
     dd->maxGrowth = mg;
 
 } /* end of Cudd_SetMaxGrowth */

void Cudd_SetMaxGrowthAlternate	(	DdManager *	dd,
		double	mg
	)

Function********************************************************************

Synopsis [Sets the maxGrowthAlt parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowth Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]

Definition at line 2064 of file cuddAPI.c.

 {
     dd->maxGrowthAlt = mg;
 
 } /* end of Cudd_SetMaxGrowthAlternate */

void Cudd_SetMaxLive	(	DdManager *	dd,
		unsigned int	maxLive
	)

Function********************************************************************

Synopsis [Sets the maximum allowed number of live nodes.]

Description [Sets the maximum allowed number of live nodes. When this number is exceeded, the package returns NULL.]

SideEffects [none]

SeeAlso [Cudd_ReadMaxLive]

Definition at line 3833 of file cuddAPI.c.

 {
     dd->maxLive = maxLive;
 
 } /* end of Cudd_SetMaxLive */

void Cudd_SetMaxMemory	(	DdManager *	dd,
		unsigned long	maxMemory
	)

Function********************************************************************

Synopsis [Sets the maximum allowed memory.]

Description [Sets the maximum allowed memory. When this number is exceeded, the package returns NULL.]

SideEffects [none]

SeeAlso [Cudd_ReadMaxMemory]

Definition at line 3876 of file cuddAPI.c.

 {
     dd->maxmemhard = maxMemory;
 
 } /* end of Cudd_SetMaxMemory */

void Cudd_SetMinHit	(	DdManager *	dd,
		unsigned int	hr
	)

Function********************************************************************

Synopsis [Sets the hit rate that causes resizinig of the computed table.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadMinHit]

Definition at line 1298 of file cuddAPI.c.

 {
     /* Internally, the package manipulates the ratio of hits to
     ** misses instead of the ratio of hits to accesses. */
     dd->minHit = (double) hr / (100.0 - (double) hr);
 
 } /* end of Cudd_SetMinHit */

void Cudd_SetNextReordering	(	DdManager *	dd,
		unsigned int	next
	)

Function********************************************************************

Synopsis [Sets the threshold for the next dynamic reordering.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadNextReordering]

Definition at line 3766 of file cuddAPI.c.

 {
     dd->nextDyn = next;
 
 } /* end of Cudd_SetNextReordering */

void Cudd_SetNumberXovers	(	DdManager *	dd,
		int	numberXovers
	)

Function********************************************************************

Synopsis [Sets the number of crossovers used by the genetic algorithm for reordering.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReadNumberXovers]

Definition at line 2896 of file cuddAPI.c.

 {
     dd->numberXovers = numberXovers;
 
 } /* end of Cudd_SetNumberXovers */

void Cudd_SetPopulationSize	(	DdManager *	dd,
		int	populationSize
	)

Function********************************************************************

Synopsis [Sets the size of the population used by the genetic algorithm for reordering.]

Description [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.]

SideEffects [Changes the manager.]

SeeAlso [Cudd_ReadPopulationSize]

Definition at line 2843 of file cuddAPI.c.

 {
     dd->populationSize = populationSize;
 
 } /* end of Cudd_SetPopulationSize */

void Cudd_SetRecomb	(	DdManager *	dd,
		int	recomb
	)

Function********************************************************************

Synopsis [Sets the value of the recombination parameter used in group sifting.]

Description [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.]

SideEffects [Changes the manager.]

SeeAlso [Cudd_ReadRecomb]

Definition at line 2682 of file cuddAPI.c.

 {
     dd->recomb = recomb;
 
 } /* end of Cudd_SetRecomb */

void Cudd_SetReorderingCycle	(	DdManager *	dd,
		int	cycle
	)

Function********************************************************************

Synopsis [Sets the reordCycle parameter of the manager.]

Description [Sets the reordCycle parameter of the manager. This parameter determines how often the alternate threshold on maximum growth is used in reordering.]

SideEffects [None]

SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate Cudd_ReadReorderingCycle]

Definition at line 2111 of file cuddAPI.c.

 {
     dd->reordCycle = cycle;
 
 } /* end of Cudd_SetReorderingCycle */

void Cudd_SetSiftMaxSwap	(	DdManager *	dd,
		int	sms
	)

Function********************************************************************

Synopsis [Sets the siftMaxSwap parameter of the manager.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_SetSiftMaxVar Cudd_ReadSiftMaxSwap]

Definition at line 1962 of file cuddAPI.c.

 {
     dd->siftMaxSwap = sms;
 
 } /* end of Cudd_SetSiftMaxSwap */

void Cudd_SetSiftMaxVar	(	DdManager *	dd,
		int	smv
	)

Function********************************************************************

Synopsis [Sets the siftMaxVar parameter of the manager.]

Description [Sets the siftMaxVar parameter of the manager. This parameter gives the maximum number of variables that will be sifted for each invocation of sifting.]

SideEffects [None]

SeeAlso [Cudd_SetSiftMaxSwap Cudd_ReadSiftMaxVar]

Definition at line 1913 of file cuddAPI.c.

 {
     dd->siftMaxVar = smv;
 
 } /* end of Cudd_SetSiftMaxVar */

void Cudd_SetStderr	(	DdManager *	dd,
		FILE *	fp
	)

Function********************************************************************

Synopsis [Sets the stderr of a manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_ReadStderr Cudd_SetStdout]

Definition at line 3717 of file cuddAPI.c.

 {
     dd->err = fp;
 
 } /* end of Cudd_SetStderr */

void Cudd_SetStdout	(	DdManager *	dd,
		FILE *	fp
	)

Function********************************************************************

Synopsis [Sets the stdout of a manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_ReadStdout Cudd_SetStderr]

Definition at line 3674 of file cuddAPI.c.

 {
     dd->out = fp;
 
 } /* end of Cudd_SetStdout */

void Cudd_SetSymmviolation	(	DdManager *	dd,
		int	symmviolation
	)

Function********************************************************************

Synopsis [Sets the value of the symmviolation parameter used in group sifting.]

Description [Sets the value of the symmviolation parameter. 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.]

SideEffects [Changes the manager.]

SeeAlso [Cudd_ReadSymmviolation]

Definition at line 2737 of file cuddAPI.c.

 {
     dd->symmviolation = symmviolation;
 
 } /* end of Cudd_SetSymmviolation */

void Cudd_SetTree	(	DdManager *	dd,
		MtrNode *	tree
	)

Function********************************************************************

Synopsis [Sets the variable group tree of the manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_FreeTree Cudd_ReadTree Cudd_SetZddTree]

Definition at line 2152 of file cuddAPI.c.

 {
     if (dd->tree != NULL) {
         Mtr_FreeTree(dd->tree);
     }
     dd->tree = tree;
     if (tree == NULL) return;
 
     fixVarTree(tree, dd->perm, dd->size);
     return;
 
 } /* end of Cudd_SetTree */

void Cudd_SetZddTree	(	DdManager *	dd,
		MtrNode *	tree
	)

Function********************************************************************

Synopsis [Sets the ZDD variable group tree of the manager.]

Description []

SideEffects [None]

SeeAlso [Cudd_FreeZddTree Cudd_ReadZddTree Cudd_SetTree]

Definition at line 2224 of file cuddAPI.c.

 {
     if (dd->treeZ != NULL) {
         Mtr_FreeTree(dd->treeZ);
     }
     dd->treeZ = tree;
     if (tree == NULL) return;
 
     fixVarTree(tree, dd->permZ, dd->sizeZ);
     return;
 
 } /* end of Cudd_SetZddTree */

int Cudd_StdPostReordHook	(	DdManager *	dd,
		const char *	str,
		void *	data
	)

Function********************************************************************

Synopsis [Sample hook function to call after reordering.]

Description [Sample hook function to call after reordering. Prints on the manager's stdout final size and reordering time. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_StdPreReordHook]

Definition at line 3501 of file cuddAPI.c.

 {
     long initialTime = (long) data;
     int retval;
     long finalTime = util_cpu_time();
     double totalTimeSec = (double)(finalTime - initialTime) / 1000.0;
 
     retval = fprintf(dd->out,"%ld nodes in %g sec\n", strcmp(str, "BDD") == 0 ?
                      Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd),
                      totalTimeSec);
     if (retval == EOF) return(0);
     retval = fflush(dd->out);
     if (retval == EOF) return(0);
     return(1);
 
 } /* end of Cudd_StdPostReordHook */

int Cudd_StdPreReordHook	(	DdManager *	dd,
		const char *	str,
		void *	data
	)

Function********************************************************************

Synopsis [Sample hook function to call before reordering.]

Description [Sample hook function to call before reordering. Prints on the manager's stdout reordering method and initial size. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_StdPostReordHook]

Definition at line 3408 of file cuddAPI.c.

 {
     Cudd_ReorderingType method = (Cudd_ReorderingType) (ptruint) data;
     int retval;
 
     retval = fprintf(dd->out,"%s reordering with ", str);
     if (retval == EOF) return(0);
     switch (method) {
     case CUDD_REORDER_SIFT_CONVERGE:
     case CUDD_REORDER_SYMM_SIFT_CONV:
     case CUDD_REORDER_GROUP_SIFT_CONV:
     case CUDD_REORDER_WINDOW2_CONV:
     case CUDD_REORDER_WINDOW3_CONV:
     case CUDD_REORDER_WINDOW4_CONV:
     case CUDD_REORDER_LINEAR_CONVERGE:
         retval = fprintf(dd->out,"converging ");
         if (retval == EOF) return(0);
         break;
     default:
         break;
     }
     switch (method) {
     case CUDD_REORDER_RANDOM:
     case CUDD_REORDER_RANDOM_PIVOT:
         retval = fprintf(dd->out,"random");
         break;
     case CUDD_REORDER_SIFT:
     case CUDD_REORDER_SIFT_CONVERGE:
         retval = fprintf(dd->out,"sifting");
         break;
     case CUDD_REORDER_SYMM_SIFT:
     case CUDD_REORDER_SYMM_SIFT_CONV:
         retval = fprintf(dd->out,"symmetric sifting");
         break;
     case CUDD_REORDER_LAZY_SIFT:
         retval = fprintf(dd->out,"lazy sifting");
         break;
     case CUDD_REORDER_GROUP_SIFT:
     case CUDD_REORDER_GROUP_SIFT_CONV:
         retval = fprintf(dd->out,"group sifting");
         break;
     case CUDD_REORDER_WINDOW2:
     case CUDD_REORDER_WINDOW3:
     case CUDD_REORDER_WINDOW4:
     case CUDD_REORDER_WINDOW2_CONV:
     case CUDD_REORDER_WINDOW3_CONV:
     case CUDD_REORDER_WINDOW4_CONV:
         retval = fprintf(dd->out,"window");
         break;
     case CUDD_REORDER_ANNEALING:
         retval = fprintf(dd->out,"annealing");
         break;
     case CUDD_REORDER_GENETIC:
         retval = fprintf(dd->out,"genetic");
         break;
     case CUDD_REORDER_LINEAR:
     case CUDD_REORDER_LINEAR_CONVERGE:
         retval = fprintf(dd->out,"linear sifting");
         break;
     case CUDD_REORDER_EXACT:
         retval = fprintf(dd->out,"exact");
         break;
     default:
         return(0);
     }
     if (retval == EOF) return(0);
 
     retval = fprintf(dd->out,": from %ld to ... ", strcmp(str, "BDD") == 0 ?
                      Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd));
     if (retval == EOF) return(0);
     fflush(dd->out);
     return(1);
 
 } /* end of Cudd_StdPreReordHook */

void Cudd_TurnOffCountDead ( DdManager * dd )

Function********************************************************************

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

Description [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.]

SideEffects [Changes the manager.]

SeeAlso [Cudd_TurnOnCountDead Cudd_DeadAreCounted]

Definition at line 2633 of file cuddAPI.c.

 {
     dd->countDead = ~0;
 
 } /* end of Cudd_TurnOffCountDead */

void Cudd_TurnOnCountDead ( DdManager * dd )

Function********************************************************************

Synopsis [Causes the dead nodes to be counted towards triggering reordering.]

Description [Causes the dead nodes to be counted towards triggering reordering. This causes more frequent reorderings. By default dead nodes are not counted.]

SideEffects [Changes the manager.]

SeeAlso [Cudd_TurnOffCountDead Cudd_DeadAreCounted]

Definition at line 2608 of file cuddAPI.c.

 {
     dd->countDead = 0;
 
 } /* end of Cudd_TurnOnCountDead */

DdNode* Cudd_zddIthVar	(	DdManager *	dd,
		int	i
	)

Function********************************************************************

Synopsis [Returns the ZDD variable with index i.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_bddIthVar Cudd_addIthVar]

Definition at line 448 of file cuddAPI.c.

 {
     DdNode *res;
     DdNode *zvar;
     DdNode *lower;
     int j;
 
     if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
 
     /* The i-th variable function has the following structure:
     ** at the level corresponding to index i there is a node whose "then"
     ** child points to the universe, and whose "else" child points to zero.
     ** Above that level there are nodes with identical children.
     */
 
     /* First we build the node at the level of index i. */
     lower = (i < dd->sizeZ - 1) ? dd->univ[dd->permZ[i]+1] : DD_ONE(dd);
     do {
         dd->reordered = 0;
         zvar = cuddUniqueInterZdd(dd, i, lower, DD_ZERO(dd));
     } while (dd->reordered == 1);
 
     if (zvar == NULL)
         return(NULL);
     cuddRef(zvar);
 
     /* Now we add the "filler" nodes above the level of index i. */
     for (j = dd->permZ[i] - 1; j >= 0; j--) {
         do {
             dd->reordered = 0;
             res = cuddUniqueInterZdd(dd, dd->invpermZ[j], zvar, zvar);
         } while (dd->reordered == 1);
         if (res == NULL) {
             Cudd_RecursiveDerefZdd(dd,zvar);
             return(NULL);
         }
         cuddRef(res);
         Cudd_RecursiveDerefZdd(dd,zvar);
         zvar = res;
     }
     cuddDeref(zvar);
     return(zvar);
 
 } /* end of Cudd_zddIthVar */

long Cudd_zddReadNodeCount ( DdManager * dd )

Function********************************************************************

Synopsis [Reports the number of nodes in ZDDs.]

Description [Reports the number of nodes in ZDDs. This number always includes the two constants 1 and 0.]

SideEffects [None]

SeeAlso [Cudd_ReadPeakNodeCount Cudd_ReadNodeCount]

Definition at line 3221 of file cuddAPI.c.

 {
     return((long)(dd->keysZ - dd->deadZ + 2));
 
 } /* end of Cudd_zddReadNodeCount */

void Cudd_zddRealignDisable ( DdManager * unique )

Function********************************************************************

Synopsis [Disables realignment of ZDD order to BDD order.]

Description []

SideEffects [None]

SeeAlso [Cudd_zddRealignEnable Cudd_zddRealignmentEnabled Cudd_bddRealignEnable Cudd_bddRealignmentEnabled]

Definition at line 889 of file cuddAPI.c.

 {
     unique->realign = 0;
     return;
 
 } /* end of Cudd_zddRealignDisable */

void Cudd_zddRealignEnable ( DdManager * unique )

Function********************************************************************

Synopsis [Enables realignment of ZDD order to BDD order.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_ReduceHeap Cudd_zddRealignDisable Cudd_zddRealignmentEnabled Cudd_bddRealignDisable Cudd_bddRealignmentEnabled]

Definition at line 867 of file cuddAPI.c.

 {
     unique->realign = 1;
     return;
 
 } /* end of Cudd_zddRealignEnable */

int Cudd_zddRealignmentEnabled ( DdManager * unique )

Function********************************************************************

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

Description [Returns 1 if the realignment of ZDD order to BDD order is enabled; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddRealignEnable Cudd_zddRealignDisable Cudd_bddRealignEnable Cudd_bddRealignDisable]

Definition at line 837 of file cuddAPI.c.

 {
     return(unique->realign);
 
 } /* end of Cudd_zddRealignmentEnabled */

int Cudd_zddVarsFromBddVars	(	DdManager *	dd,
		int	multiplicity
	)

Function********************************************************************

Synopsis [Creates one or more ZDD variables for each BDD variable.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_bddNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]

Definition at line 519 of file cuddAPI.c.

 {
     int res;
     int i, j;
     int allnew;
     int *permutation;
 
     if (multiplicity < 1) return(0);
     allnew = dd->sizeZ == 0;
     if (dd->size * multiplicity > dd->sizeZ) {
         res = cuddResizeTableZdd(dd,dd->size * multiplicity - 1);
         if (res == 0) return(0);
     }
     /* Impose the order of the BDD variables to the ZDD variables. */
     if (allnew) {
         for (i = 0; i < dd->size; i++) {
             for (j = 0; j < multiplicity; j++) {
                 dd->permZ[i * multiplicity + j] =
                     dd->perm[i] * multiplicity + j;
                 dd->invpermZ[dd->permZ[i * multiplicity + j]] =
                     i * multiplicity + j;
             }
         }
         for (i = 0; i < dd->sizeZ; i++) {
             dd->univ[i]->index = dd->invpermZ[i];
         }
     } else {
         permutation = ABC_ALLOC(int,dd->sizeZ);
         if (permutation == NULL) {
             dd->errorCode = CUDD_MEMORY_OUT;
             return(0);
         }
         for (i = 0; i < dd->size; i++) {
             for (j = 0; j < multiplicity; j++) {
                 permutation[i * multiplicity + j] =
                     dd->invperm[i] * multiplicity + j;
             }
         }
         for (i = dd->size * multiplicity; i < dd->sizeZ; i++) {
             permutation[i] = i;
         }
         res = Cudd_zddShuffleHeap(dd, permutation);
         ABC_FREE(permutation);
         if (res == 0) return(0);
     }
     /* Copy and expand the variable group tree if it exists. */
     if (dd->treeZ != NULL) {
         Cudd_FreeZddTree(dd);
     }
     if (dd->tree != NULL) {
         dd->treeZ = Mtr_CopyTree(dd->tree, multiplicity);
         if (dd->treeZ == NULL) return(0);
     } else if (multiplicity > 1) {
         dd->treeZ = Mtr_InitGroupTree(0, dd->sizeZ);
         if (dd->treeZ == NULL) return(0);
         dd->treeZ->index = dd->invpermZ[0];
     }
     /* Create groups for the ZDD variables derived from the same BDD variable.
     */
     if (multiplicity > 1) {
         char *vmask, *lmask;
 
         vmask = ABC_ALLOC(char, dd->size);
         if (vmask == NULL) {
             dd->errorCode = CUDD_MEMORY_OUT;
             return(0);
         }
         lmask =  ABC_ALLOC(char, dd->size);
         if (lmask == NULL) {
             dd->errorCode = CUDD_MEMORY_OUT;
             return(0);
         }
         for (i = 0; i < dd->size; i++) {
             vmask[i] = lmask[i] = 0;
         }
         res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask);
         ABC_FREE(vmask);
         ABC_FREE(lmask);
         if (res == 0) return(0);
     }
     return(1);
 
 } /* end of Cudd_zddVarsFromBddVars */

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

static

AutomaticStart

Function********************************************************************

Synopsis [Fixes a variable group tree.]

Description []

SideEffects [Changes the variable group tree.]

SeeAlso []

Definition at line 4359 of file cuddAPI.c.

 {
     treenode->index = treenode->low;
     treenode->low = ((int) treenode->index < size) ?
         perm[treenode->index] : treenode->index;
     if (treenode->child != NULL)
         fixVarTree(treenode->child, perm, size);
     if (treenode->younger != NULL)
         fixVarTree(treenode->younger, perm, size);
     return;
 
 } /* end of fixVarTree */

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddAPI.c,v 1.59 2009/02/19 16:14:14 fabio Exp $"

static

CFile***********************************************************************

FileName [cuddAPI.c]

PackageName [cudd]

Synopsis [Application interface functions.]

Description [External procedures included in this module:

Static procedures included in this module:

fixVarTree()

]

SeeAlso []

Author [Fabio Somenzi]

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

Definition at line 218 of file cuddAPI.c.

Functions

Variables

Function Documentation

Variable Documentation