src/bdd/cudd/cuddAPI.c File Reference
#include "util_hack.h"#include "cuddInt.h"
Go to the source code of this file.
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 4370 of file cuddAPI.c.
04376 { 04377 int startV, stopV, startL; 04378 int i, j; 04379 MtrNode *auxnode = treenode; 04380 04381 while (auxnode != NULL) { 04382 if (auxnode->child != NULL) { 04383 addMultiplicityGroups(dd,auxnode->child,multiplicity,vmask,lmask); 04384 } 04385 /* Build remaining groups. */ 04386 startV = dd->permZ[auxnode->index] / multiplicity; 04387 startL = auxnode->low / multiplicity; 04388 stopV = startV + auxnode->size / multiplicity; 04389 /* Walk down vmask starting at startV and build missing groups. */ 04390 for (i = startV, j = startL; i < stopV; i++) { 04391 if (vmask[i] == 0) { 04392 MtrNode *node; 04393 while (lmask[j] == 1) j++; 04394 node = Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity, 04395 MTR_FIXED); 04396 if (node == NULL) { 04397 return(0); 04398 } 04399 node->index = dd->invpermZ[i * multiplicity]; 04400 vmask[i] = 1; 04401 lmask[j] = 1; 04402 } 04403 } 04404 auxnode = auxnode->younger; 04405 } 04406 return(1); 04407 04408 } /* end of addMultiplicityGroups */
| static int addMultiplicityGroups ARGS | ( | (DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask) | ) | [static] |
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 589 of file cuddAPI.c.
00592 { 00593 return(cuddUniqueConst(dd,c)); 00594 00595 } /* end of Cudd_addConst */
| int Cudd_AddHook | ( | DdManager * | dd, | |
| int(*)(DdManager *, char *, void *) | 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 3212 of file cuddAPI.c.
03216 { 03217 DdHook **hook, *nextHook, *newHook; 03218 03219 switch (where) { 03220 case CUDD_PRE_GC_HOOK: 03221 hook = &(dd->preGCHook); 03222 break; 03223 case CUDD_POST_GC_HOOK: 03224 hook = &(dd->postGCHook); 03225 break; 03226 case CUDD_PRE_REORDERING_HOOK: 03227 hook = &(dd->preReorderingHook); 03228 break; 03229 case CUDD_POST_REORDERING_HOOK: 03230 hook = &(dd->postReorderingHook); 03231 break; 03232 default: 03233 return(0); 03234 } 03235 /* Scan the list and find whether the function is already there. 03236 ** If so, just return. */ 03237 nextHook = *hook; 03238 while (nextHook != NULL) { 03239 if (nextHook->f == f) { 03240 return(2); 03241 } 03242 hook = &(nextHook->next); 03243 nextHook = nextHook->next; 03244 } 03245 /* The function was not in the list. Create a new item and append it 03246 ** to the end of the list. */ 03247 newHook = ALLOC(DdHook,1); 03248 if (newHook == NULL) { 03249 dd->errorCode = CUDD_MEMORY_OUT; 03250 return(0); 03251 } 03252 newHook->next = NULL; 03253 newHook->f = f; 03254 *hook = newHook; 03255 return(1); 03256 03257 } /* end of Cudd_AddHook */
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 353 of file cuddAPI.c.
00356 { 00357 DdNode *res; 00358 00359 if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL); 00360 do { 00361 dd->reordered = 0; 00362 res = cuddUniqueInter(dd,i,DD_ONE(dd),DD_ZERO(dd)); 00363 } while (dd->reordered == 1); 00364 00365 return(res); 00366 00367 } /* end of Cudd_addIthVar */
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 228 of file cuddAPI.c.
00230 { 00231 DdNode *res; 00232 00233 if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL); 00234 do { 00235 dd->reordered = 0; 00236 res = cuddUniqueInter(dd,dd->size,DD_ONE(dd),DD_ZERO(dd)); 00237 } while (dd->reordered == 1); 00238 00239 return(res); 00240 00241 } /* end of Cudd_addNewVar */
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 259 of file cuddAPI.c.
00262 { 00263 DdNode *res; 00264 00265 if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL); 00266 if (level >= dd->size) return(Cudd_addIthVar(dd,level)); 00267 if (!cuddInsertSubtables(dd,1,level)) return(NULL); 00268 do { 00269 dd->reordered = 0; 00270 res = cuddUniqueInter(dd,dd->size - 1,DD_ONE(dd),DD_ZERO(dd)); 00271 } while (dd->reordered == 1); 00272 00273 return(res); 00274 00275 } /* 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 677 of file cuddAPI.c.
00679 { 00680 unique->autoDyn = 0; 00681 return; 00682 00683 } /* 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 755 of file cuddAPI.c.
00757 { 00758 unique->autoDynZ = 0; 00759 return; 00760 00761 } /* 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 638 of file cuddAPI.c.
00641 { 00642 unique->autoDyn = 1; 00643 if (method != CUDD_REORDER_SAME) { 00644 unique->autoMethod = method; 00645 } 00646 #ifndef DD_NO_DEATH_ROW 00647 /* If reordering is enabled, using the death row causes too many 00648 ** invocations. Hence, we shrink the death row to just one entry. 00649 */ 00650 cuddClearDeathRow(unique); 00651 unique->deathRowDepth = 1; 00652 unique->deadMask = unique->deathRowDepth - 1; 00653 if ((unsigned) unique->nextDead > unique->deadMask) { 00654 unique->nextDead = 0; 00655 } 00656 unique->deathRow = REALLOC(DdNodePtr, unique->deathRow, 00657 unique->deathRowDepth); 00658 #endif 00659 return; 00660 00661 } /* 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 729 of file cuddAPI.c.
00732 { 00733 unique->autoDynZ = 1; 00734 if (method != CUDD_REORDER_SAME) { 00735 unique->autoMethodZ = method; 00736 } 00737 return; 00738 00739 } /* 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]
| 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 4066 of file cuddAPI.c.
04069 { 04070 if (index >= dd->size || index < 0) return -1; 04071 return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_NEXT_STATE); 04072 04073 } /* 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 4018 of file cuddAPI.c.
04021 { 04022 if (index >= dd->size || index < 0) return -1; 04023 return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRIMARY_INPUT); 04024 04025 } /* 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 4042 of file cuddAPI.c.
04045 { 04046 if (index >= dd->size || index < 0) return -1; 04047 return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRESENT_STATE); 04048 04049 } /* 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 4294 of file cuddAPI.c.
04297 { 04298 if (index >= dd->size || index < 0) return(-1); 04299 if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_HARD_GROUP) 04300 return(1); 04301 return(0); 04302 04303 } /* 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 4217 of file cuddAPI.c.
04220 { 04221 if (index >= dd->size || index < 0) return(-1); 04222 if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP) 04223 return(0); 04224 else 04225 return(dd->subtables[dd->perm[index]].varToBeGrouped); 04226 04227 } /* 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 4269 of file cuddAPI.c.
04272 { 04273 if (index >= dd->size || index < 0) return(-1); 04274 return dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP; 04275 04276 } /* end of Cudd_bddIsVarToBeGrouped */
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 385 of file cuddAPI.c.
00388 { 00389 DdNode *res; 00390 00391 if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL); 00392 if (i < dd->size) { 00393 res = dd->vars[i]; 00394 } else { 00395 res = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one)); 00396 } 00397 00398 return(res); 00399 00400 } /* end of Cudd_bddIthVar */
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 292 of file cuddAPI.c.
00294 { 00295 DdNode *res; 00296 00297 if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL); 00298 res = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one)); 00299 00300 return(res); 00301 00302 } /* end of Cudd_bddNewVar */
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 320 of file cuddAPI.c.
00323 { 00324 DdNode *res; 00325 00326 if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL); 00327 if (level >= dd->size) return(Cudd_bddIthVar(dd,level)); 00328 if (!cuddInsertSubtables(dd,1,level)) return(NULL); 00329 res = dd->vars[dd->size - 1]; 00330 00331 return(res); 00332 00333 } /* 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]
| 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 934 of file cuddAPI.c.
00936 { 00937 unique->realignZ = 0; 00938 return; 00939 00940 } /* 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 912 of file cuddAPI.c.
00914 { 00915 unique->realignZ = 1; 00916 return; 00917 00918 } /* 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 882 of file cuddAPI.c.
00884 { 00885 return(unique->realignZ); 00886 00887 } /* 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 4190 of file cuddAPI.c.
04193 { 04194 if (index >= dd->size || index < 0) return(0); 04195 if (dd->subtables[dd->perm[index]].varToBeGrouped <= 04196 CUDD_LAZY_SOFT_GROUP) { 04197 dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_NONE; 04198 } 04199 return(1); 04200 04201 } /* 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 3993 of file cuddAPI.c.
03996 { 03997 if (index >= dd->size || index < 0) return (0); 03998 dd->subtables[dd->perm[index]].varType = CUDD_VAR_NEXT_STATE; 03999 return(1); 04000 04001 } /* 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]
| 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 3945 of file cuddAPI.c.
03948 { 03949 if (index >= dd->size || index < 0) return (0); 03950 dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRIMARY_INPUT; 03951 return(1); 03952 03953 } /* 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 3969 of file cuddAPI.c.
03972 { 03973 if (index >= dd->size || index < 0) return (0); 03974 dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRESENT_STATE; 03975 return(1); 03976 03977 } /* 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 4166 of file cuddAPI.c.
04169 { 04170 if (index >= dd->size || index < 0) return(0); 04171 dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_HARD_GROUP; 04172 return(1); 04173 04174 } /* 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 4139 of file cuddAPI.c.
04142 { 04143 if (index >= dd->size || index < 0) return(0); 04144 if (dd->subtables[dd->perm[index]].varToBeGrouped <= CUDD_LAZY_SOFT_GROUP) { 04145 dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_SOFT_GROUP; 04146 } 04147 return(1); 04148 04149 } /* 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 4243 of file cuddAPI.c.
04246 { 04247 if (index >= dd->size || index < 0) return(0); 04248 dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_UNGROUP; 04249 return(1); 04250 04251 } /* 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]
| 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]
| void Cudd_ClearErrorCode | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Clear the error code of a manager.]
Description []
SideEffects [None]
SeeAlso [Cudd_ReadErrorCode]
Definition at line 3600 of file cuddAPI.c.
03602 { 03603 dd->errorCode = CUDD_NO_ERROR; 03604 03605 } /* 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 2554 of file cuddAPI.c.
02556 { 02557 return(dd->countDead == 0 ? 1 : 0); 02558 02559 } /* 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 2532 of file cuddAPI.c.
02534 { 02535 dd->gcEnabled = 0; 02536 02537 } /* 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 3532 of file cuddAPI.c.
03534 { 03535 if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) { 03536 return(0); 03537 } 03538 if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) { 03539 return(0); 03540 } 03541 return(1); 03542 03543 } /* 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 2508 of file cuddAPI.c.
02510 { 02511 dd->gcEnabled = 1; 02512 02513 } /* 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 3504 of file cuddAPI.c.
03506 { 03507 if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) { 03508 return(0); 03509 } 03510 if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) { 03511 return(0); 03512 } 03513 return(1); 03514 03515 } /* 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 1541 of file cuddAPI.c.
01543 { 01544 int i; 01545 int size = dd->size; 01546 DdSubtable *subtable; 01547 double empty = 0.0; 01548 01549 /* To each subtable we apply the corollary to Theorem 8.5 (occupancy 01550 ** distribution) from Sedgewick and Flajolet's Analysis of Algorithms. 01551 ** The corollary says that for a a table with M buckets and a load ratio 01552 ** of r, the expected number of empty buckets is asymptotically given 01553 ** by M * exp(-r). 01554 */ 01555 01556 /* Scan each BDD/ADD subtable. */ 01557 for (i = 0; i < size; i++) { 01558 subtable = &(dd->subtables[i]); 01559 empty += (double) subtable->slots * 01560 exp(-(double) subtable->keys / (double) subtable->slots); 01561 } 01562 01563 /* Scan the ZDD subtables. */ 01564 size = dd->sizeZ; 01565 01566 for (i = 0; i < size; i++) { 01567 subtable = &(dd->subtableZ[i]); 01568 empty += (double) subtable->slots * 01569 exp(-(double) subtable->keys / (double) subtable->slots); 01570 } 01571 01572 /* Constant table. */ 01573 subtable = &(dd->constants); 01574 empty += (double) subtable->slots * 01575 exp(-(double) subtable->keys / (double) subtable->slots); 01576 01577 return(1.0 - empty / (double) dd->slots); 01578 01579 } /* 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]
| 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]
| 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 2486 of file cuddAPI.c.
02488 { 02489 return(dd->gcEnabled); 02490 02491 } /* end of Cudd_GarbageCollectionEnabled */
| int Cudd_IsInHook | ( | DdManager * | dd, | |
| int(*)(DdManager *, char *, void *) | 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 3327 of file cuddAPI.c.
03331 { 03332 DdHook *hook; 03333 03334 switch (where) { 03335 case CUDD_PRE_GC_HOOK: 03336 hook = dd->preGCHook; 03337 break; 03338 case CUDD_POST_GC_HOOK: 03339 hook = dd->postGCHook; 03340 break; 03341 case CUDD_PRE_REORDERING_HOOK: 03342 hook = dd->preReorderingHook; 03343 break; 03344 case CUDD_POST_REORDERING_HOOK: 03345 hook = dd->postReorderingHook; 03346 break; 03347 default: 03348 return(0); 03349 } 03350 /* Scan the list and find whether the function is already there. */ 03351 while (hook != NULL) { 03352 if (hook->f == f) { 03353 return(1); 03354 } 03355 hook = hook->next; 03356 } 03357 return(0); 03358 03359 } /* 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 614 of file cuddAPI.c.
00616 { 00617 return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f)); 00618 00619 } /* 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 2246 of file cuddAPI.c.
02248 { 02249 return((unsigned int) Cudd_Regular(node)->index); 02250 02251 } /* 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 2906 of file cuddAPI.c.
02909 { 02910 int retval; 02911 Cudd_ReorderingType autoMethod, autoMethodZ; 02912 02913 /* Modifiable parameters. */ 02914 retval = fprintf(fp,"**** CUDD modifiable parameters ****\n"); 02915 if (retval == EOF) return(0); 02916 retval = fprintf(fp,"Hard limit for cache size: %u\n", 02917 Cudd_ReadMaxCacheHard(dd)); 02918 if (retval == EOF) return(0); 02919 retval = fprintf(fp,"Cache hit threshold for resizing: %u%%\n", 02920 Cudd_ReadMinHit(dd)); 02921 if (retval == EOF) return(0); 02922 retval = fprintf(fp,"Garbage collection enabled: %s\n", 02923 Cudd_GarbageCollectionEnabled(dd) ? "yes" : "no"); 02924 if (retval == EOF) return(0); 02925 retval = fprintf(fp,"Limit for fast unique table growth: %u\n", 02926 Cudd_ReadLooseUpTo(dd)); 02927 if (retval == EOF) return(0); 02928 retval = fprintf(fp, 02929 "Maximum number of variables sifted per reordering: %d\n", 02930 Cudd_ReadSiftMaxVar(dd)); 02931 if (retval == EOF) return(0); 02932 retval = fprintf(fp, 02933 "Maximum number of variable swaps per reordering: %d\n", 02934 Cudd_ReadSiftMaxSwap(dd)); 02935 if (retval == EOF) return(0); 02936 retval = fprintf(fp,"Maximum growth while sifting a variable: %g\n", 02937 Cudd_ReadMaxGrowth(dd)); 02938 if (retval == EOF) return(0); 02939 retval = fprintf(fp,"Dynamic reordering of BDDs enabled: %s\n", 02940 Cudd_ReorderingStatus(dd,&autoMethod) ? "yes" : "no"); 02941 if (retval == EOF) return(0); 02942 retval = fprintf(fp,"Default BDD reordering method: %d\n", autoMethod); 02943 if (retval == EOF) return(0); 02944 retval = fprintf(fp,"Dynamic reordering of ZDDs enabled: %s\n", 02945 Cudd_ReorderingStatusZdd(dd,&autoMethodZ) ? "yes" : "no"); 02946 if (retval == EOF) return(0); 02947 retval = fprintf(fp,"Default ZDD reordering method: %d\n", autoMethodZ); 02948 if (retval == EOF) return(0); 02949 retval = fprintf(fp,"Realignment of ZDDs to BDDs enabled: %s\n", 02950 Cudd_zddRealignmentEnabled(dd) ? "yes" : "no"); 02951 if (retval == EOF) return(0); 02952 retval = fprintf(fp,"Realignment of BDDs to ZDDs enabled: %s\n", 02953 Cudd_bddRealignmentEnabled(dd) ? "yes" : "no"); 02954 if (retval == EOF) return(0); 02955 retval = fprintf(fp,"Dead nodes counted in triggering reordering: %s\n", 02956 Cudd_DeadAreCounted(dd) ? "yes" : "no"); 02957 if (retval == EOF) return(0); 02958 retval = fprintf(fp,"Group checking criterion: %d\n", 02959 Cudd_ReadGroupcheck(dd)); 02960 if (retval == EOF) return(0); 02961 retval = fprintf(fp,"Recombination threshold: %d\n", Cudd_ReadRecomb(dd)); 02962 if (retval == EOF) return(0); 02963 retval = fprintf(fp,"Symmetry violation threshold: %d\n", 02964 Cudd_ReadSymmviolation(dd)); 02965 if (retval == EOF) return(0); 02966 retval = fprintf(fp,"Arc violation threshold: %d\n", 02967 Cudd_ReadArcviolation(dd)); 02968 if (retval == EOF) return(0); 02969 retval = fprintf(fp,"GA population size: %d\n", 02970 Cudd_ReadPopulationSize(dd)); 02971 if (retval == EOF) return(0); 02972 retval = fprintf(fp,"Number of crossovers for GA: %d\n", 02973 Cudd_ReadNumberXovers(dd)); 02974 if (retval == EOF) return(0); 02975 retval = fprintf(fp,"Next reordering threshold: %u\n", 02976 Cudd_ReadNextReordering(dd)); 02977 if (retval == EOF) return(0); 02978 02979 /* Non-modifiable parameters. */ 02980 retval = fprintf(fp,"**** CUDD non-modifiable parameters ****\n"); 02981 if (retval == EOF) return(0); 02982 retval = fprintf(fp,"Memory in use: %ld\n", Cudd_ReadMemoryInUse(dd)); 02983 if (retval == EOF) return(0); 02984 retval = fprintf(fp,"Peak number of nodes: %ld\n", 02985 Cudd_ReadPeakNodeCount(dd)); 02986 if (retval == EOF) return(0); 02987 retval = fprintf(fp,"Peak number of live nodes: %d\n", 02988 Cudd_ReadPeakLiveNodeCount(dd)); 02989 if (retval == EOF) return(0); 02990 retval = fprintf(fp,"Number of BDD variables: %d\n", dd->size); 02991 if (retval == EOF) return(0); 02992 retval = fprintf(fp,"Number of ZDD variables: %d\n", dd->sizeZ); 02993 if (retval == EOF) return(0); 02994 retval = fprintf(fp,"Number of cache entries: %u\n", dd->cacheSlots); 02995 if (retval == EOF) return(0); 02996 retval = fprintf(fp,"Number of cache look-ups: %.0f\n", 02997 Cudd_ReadCacheLookUps(dd)); 02998 if (retval == EOF) return(0); 02999 retval = fprintf(fp,"Number of cache hits: %.0f\n", 03000 Cudd_ReadCacheHits(dd)); 03001 if (retval == EOF) return(0); 03002 retval = fprintf(fp,"Number of cache insertions: %.0f\n", 03003 dd->cacheinserts); 03004 if (retval == EOF) return(0); 03005 retval = fprintf(fp,"Number of cache collisions: %.0f\n", 03006 dd->cachecollisions); 03007 if (retval == EOF) return(0); 03008 retval = fprintf(fp,"Number of cache deletions: %.0f\n", 03009 dd->cachedeletions); 03010 if (retval == EOF) return(0); 03011 retval = cuddCacheProfile(dd,fp); 03012 if (retval == 0) return(0); 03013 retval = fprintf(fp,"Soft limit for cache size: %u\n", 03014 Cudd_ReadMaxCache(dd)); 03015 if (retval == EOF) return(0); 03016 retval = fprintf(fp,"Number of buckets in unique table: %u\n", dd->slots); 03017 if (retval == EOF) return(0); 03018 retval = fprintf(fp,"Used buckets in unique table: %.2f%% (expected %.2f%%)\n", 03019 100.0 * Cudd_ReadUsedSlots(dd), 03020 100.0 * Cudd_ExpectedUsedSlots(dd)); 03021 if (retval == EOF) return(0); 03022 #ifdef DD_UNIQUE_PROFILE 03023 retval = fprintf(fp,"Unique lookups: %.0f\n", dd->uniqueLookUps); 03024 if (retval == EOF) return(0); 03025 retval = fprintf(fp,"Unique links: %.0f (%g per lookup)\n", 03026 dd->uniqueLinks, dd->uniqueLinks / dd->uniqueLookUps); 03027 if (retval == EOF) return(0); 03028 #endif 03029 retval = fprintf(fp,"Number of BDD and ADD nodes: %u\n", dd->keys); 03030 if (retval == EOF) return(0); 03031 retval = fprintf(fp,"Number of ZDD nodes: %u\n", dd->keysZ); 03032 if (retval == EOF) return(0); 03033 retval = fprintf(fp,"Number of dead BDD and ADD nodes: %u\n", dd->dead); 03034 if (retval == EOF) return(0); 03035 retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ); 03036 if (retval == EOF) return(0); 03037 retval = fprintf(fp,"Total number of nodes allocated: %.0f\n", 03038 dd->allocated); 03039 if (retval == EOF) return(0); 03040 retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n", 03041 dd->reclaimed); 03042 if (retval == EOF) return(0); 03043 #if DD_STATS 03044 retval = fprintf(fp,"Nodes freed: %.0f\n", dd->nodesFreed); 03045 if (retval == EOF) return(0); 03046 retval = fprintf(fp,"Nodes dropped: %.0f\n", dd->nodesDropped); 03047 if (retval == EOF) return(0); 03048 #endif 03049 #if DD_COUNT 03050 retval = fprintf(fp,"Number of recursive calls: %.0f\n", 03051 Cudd_ReadRecursiveCalls(dd)); 03052 if (retval == EOF) return(0); 03053 #endif 03054 retval = fprintf(fp,"Garbage collections so far: %d\n", 03055 Cudd_ReadGarbageCollections(dd)); 03056 if (retval == EOF) return(0); 03057 retval = fprintf(fp,"Time for garbage collection: %.2f sec\n", 03058 ((double)Cudd_ReadGarbageCollectionTime(dd)/1000.0)); 03059 if (retval == EOF) return(0); 03060 retval = fprintf(fp,"Reorderings so far: %d\n", dd->reorderings); 03061 if (retval == EOF) return(0); 03062 retval = fprintf(fp,"Time for reordering: %.2f sec\n", 03063 ((double)Cudd_ReadReorderingTime(dd)/1000.0)); 03064 if (retval == EOF) return(0); 03065 #if DD_COUNT 03066 retval = fprintf(fp,"Node swaps in reordering: %.0f\n", 03067 Cudd_ReadSwapSteps(dd)); 03068 if (retval == EOF) return(0); 03069 #endif 03070 03071 return(1); 03072 03073 } /* 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 2733 of file cuddAPI.c.
02735 { 02736 return(dd->arcviolation); 02737 02738 } /* end of Cudd_ReadArcviolation */
Function********************************************************************
Synopsis [Reads the background constant of the manager.]
Description []
SideEffects [None]
Definition at line 1081 of file cuddAPI.c.
01083 { 01084 return(dd->background); 01085 01086 } /* 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 1194 of file cuddAPI.c.
01196 { 01197 return(dd->cacheHits + dd->totCachehits); 01198 01199 } /* 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 1173 of file cuddAPI.c.
01175 { 01176 return(dd->cacheHits + dd->cacheMisses + 01177 dd->totCachehits + dd->totCacheMisses); 01178 01179 } /* 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 1121 of file cuddAPI.c.
01123 { 01124 return(dd->cacheSlots); 01125 01126 } /* 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 1144 of file cuddAPI.c.
01146 { 01147 unsigned long used = 0; 01148 int slots = dd->cacheSlots; 01149 DdCache *cache = dd->cache; 01150 int i; 01151 01152 for (i = 0; i < slots; i++) { 01153 used += cache[i].h != 0; 01154 } 01155 01156 return((double)used / (double) dd->cacheSlots); 01157 01158 } /* 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 1615 of file cuddAPI.c.
01617 { 01618 return(dd->dead); 01619 01620 } /* 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 2399 of file cuddAPI.c.
02401 { 02402 return(dd->epsilon); 02403 02404 } /* 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 3580 of file cuddAPI.c.
03582 { 03583 return(dd->errorCode); 03584 03585 } /* 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 1710 of file cuddAPI.c.
01712 { 01713 return(dd->garbageCollections); 01714 01715 } /* 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 1731 of file cuddAPI.c.
01733 { 01734 return(dd->GCTime); 01735 01736 } /* 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 2443 of file cuddAPI.c.
02445 { 02446 return(dd->groupcheck); 02447 02448 } /* 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 2323 of file cuddAPI.c.
02326 { 02327 if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX); 02328 if (i < 0 || i >= dd->size) return(-1); 02329 return(dd->invperm[i]); 02330 02331 } /* 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 2349 of file cuddAPI.c.
02352 { 02353 if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX); 02354 if (i < 0 || i >= dd->sizeZ) return(-1); 02355 return(dd->invpermZ[i]); 02356 02357 } /* 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 1595 of file cuddAPI.c.
01597 { 01598 return(dd->keys); 01599 01600 } /* end of Cudd_ReadKeys */
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]
| 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 1290 of file cuddAPI.c.
01292 { 01293 return(dd->looseUpTo); 01294 01295 } /* 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 1340 of file cuddAPI.c.
01342 { 01343 return(2 * dd->cacheSlots + dd->cacheSlack); 01344 01345 } /* 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 1360 of file cuddAPI.c.
01362 { 01363 return(dd->maxCacheHard); 01364 01365 } /* 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 1957 of file cuddAPI.c.
01959 { 01960 return(dd->maxGrowth); 01961 01962 } /* 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 2008 of file cuddAPI.c.
02010 { 02011 return(dd->maxGrowthAlt); 02012 02013 } /* 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 3780 of file cuddAPI.c.
03782 { 03783 return(dd->maxLive); 03784 03785 } /* end of Cudd_ReadMaxLive */
| 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 3823 of file cuddAPI.c.
03825 { 03826 return(dd->maxmemhard); 03827 03828 } /* end of Cudd_ReadMaxMemory */
| 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 2885 of file cuddAPI.c.
02887 { 02888 return(dd->memused); 02889 02890 } /* 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 1639 of file cuddAPI.c.
01641 { 01642 return(dd->minDead); 01643 01644 } /* 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]
Function********************************************************************
Synopsis [Reads the minus-infinity constant from the manager.]
Description []
SideEffects [None]
Definition at line 1063 of file cuddAPI.c.
01065 { 01066 return(dd->minusinfinity); 01067 01068 } /* 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 3710 of file cuddAPI.c.
03712 { 03713 return(dd->nextDyn); 03714 03715 } /* 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 3147 of file cuddAPI.c.
03149 { 03150 long count; 03151 int i; 03152 03153 #ifndef DD_NO_DEATH_ROW 03154 cuddClearDeathRow(dd); 03155 #endif 03156 03157 count = dd->keys - dd->dead; 03158 03159 /* Count isolated projection functions. Their number is subtracted 03160 ** from the node count because they are not part of the BDDs. 03161 */ 03162 for (i=0; i < dd->size; i++) { 03163 if (dd->vars[i]->ref == 1) count--; 03164 } 03165 /* Subtract from the count the unused constants. */ 03166 if (DD_ZERO(dd)->ref == 1) count--; 03167 if (DD_PLUS_INFINITY(dd)->ref == 1) count--; 03168 if (DD_MINUS_INFINITY(dd)->ref == 1) count--; 03169 03170 return(count); 03171 03172 } /* 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]
| 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]
| 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 2839 of file cuddAPI.c.
02841 { 02842 return(dd->numberXovers); 02843 02844 } /* end of Cudd_ReadNumberXovers */
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 956 of file cuddAPI.c.
00958 { 00959 return(dd->one); 00960 00961 } /* 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 3119 of file cuddAPI.c.
03121 { 03122 unsigned int live = dd->keys - dd->dead; 03123 03124 if (live > dd->peakLiveNodes) { 03125 dd->peakLiveNodes = live; 03126 } 03127 return((int)dd->peakLiveNodes); 03128 03129 } /* 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 3090 of file cuddAPI.c.
03092 { 03093 long count = 0; 03094 DdNodePtr *scan = dd->memoryList; 03095 03096 while (scan != NULL) { 03097 count += DD_MEM_CHUNK; 03098 scan = (DdNodePtr *) *scan; 03099 } 03100 return(count); 03101 03102 } /* 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 2270 of file cuddAPI.c.
02273 { 02274 if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX); 02275 if (i < 0 || i >= dd->size) return(-1); 02276 return(dd->perm[i]); 02277 02278 } /* 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 2297 of file cuddAPI.c.
02300 { 02301 if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX); 02302 if (i < 0 || i >= dd->sizeZ) return(-1); 02303 return(dd->permZ[i]); 02304 02305 } /* end of Cudd_ReadPermZdd */
Function********************************************************************
Synopsis [Reads the plus-infinity constant from the manager.]
Description []
SideEffects [None]
Definition at line 1045 of file cuddAPI.c.
01047 { 01048 return(dd->plusinfinity); 01049 01050 } /* 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 2786 of file cuddAPI.c.
02788 { 02789 return(dd->populationSize); 02790 02791 } /* 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 2626 of file cuddAPI.c.
02628 { 02629 return(dd->recomb); 02630 02631 } /* 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 []
| 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 2057 of file cuddAPI.c.
02059 { 02060 return(dd->reordCycle); 02061 02062 } /* 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 1665 of file cuddAPI.c.
01667 { 01668 return(dd->reorderings); 01669 01670 } /* 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 1687 of file cuddAPI.c.
01689 { 01690 return(dd->reordTime); 01691 01692 } /* 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 1907 of file cuddAPI.c.
01909 { 01910 return(dd->siftMaxSwap); 01911 01912 } /* 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 1860 of file cuddAPI.c.
01862 { 01863 return(dd->siftMaxVar); 01864 01865 } /* 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 1410 of file cuddAPI.c.
01412 { 01413 return(dd->size); 01414 01415 } /* 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 1449 of file cuddAPI.c.
01451 { 01452 return(dd->slots); 01453 01454 } /* 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 3665 of file cuddAPI.c.
03667 { 03668 return(dd->err); 03669 03670 } /* 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 3622 of file cuddAPI.c.
03624 { 03625 return(dd->out); 03626 03627 } /* end of Cudd_ReadStdout */
| double Cudd_ReadSwapSteps | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the number of elementary reordering steps.]
Description []
SideEffects [none]
SeeAlso []
| 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 2679 of file cuddAPI.c.
02681 { 02682 return(dd->symmviolation); 02683 02684 } /* end of Cudd_ReadSymmviolation */
Function********************************************************************
Synopsis [Returns the variable group tree of the manager.]
Description []
SideEffects [None]
SeeAlso [Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree]
Definition at line 2101 of file cuddAPI.c.
02103 { 02104 return(dd->tree); 02105 02106 } /* 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]
| 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]
| 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 1472 of file cuddAPI.c.
01474 { 01475 unsigned long used = 0; 01476 int i, j; 01477 int size = dd->size; 01478 DdNodePtr *nodelist; 01479 DdSubtable *subtable; 01480 DdNode *node; 01481 DdNode *sentinel = &(dd->sentinel); 01482 01483 /* Scan each BDD/ADD subtable. */ 01484 for (i = 0; i < size; i++) { 01485 subtable = &(dd->subtables[i]); 01486 nodelist = subtable->nodelist; 01487 for (j = 0; (unsigned) j < subtable->slots; j++) { 01488 node = nodelist[j]; 01489 if (node != sentinel) { 01490 used++; 01491 } 01492 } 01493 } 01494 01495 /* Scan the ZDD subtables. */ 01496 size = dd->sizeZ; 01497 01498 for (i = 0; i < size; i++) { 01499 subtable = &(dd->subtableZ[i]); 01500 nodelist = subtable->nodelist; 01501 for (j = 0; (unsigned) j < subtable->slots; j++) { 01502 node = nodelist[j]; 01503 if (node != NULL) { 01504 used++; 01505 } 01506 } 01507 } 01508 01509 /* Constant table. */ 01510 subtable = &(dd->constants); 01511 nodelist = subtable->nodelist; 01512 for (j = 0; (unsigned) j < subtable->slots; j++) { 01513 node = nodelist[j]; 01514 if (node != NULL) { 01515 used++; 01516 } 01517 } 01518 01519 return((double)used / (double) dd->slots); 01520 01521 } /* end of Cudd_ReadUsedSlots */
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]
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]
| int Cudd_ReadZddSize | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of ZDD variables in existance.]
Description []
SideEffects [None]
SeeAlso [Cudd_ReadSize]
Definition at line 1430 of file cuddAPI.c.
01432 { 01433 return(dd->sizeZ); 01434 01435 } /* end of Cudd_ReadZddSize */
Function********************************************************************
Synopsis [Returns the variable group tree of the manager.]
Description []
SideEffects [None]
SeeAlso [Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree]
Definition at line 2173 of file cuddAPI.c.
02175 { 02176 return(dd->treeZ); 02177 02178 } /* end of Cudd_ReadZddTree */
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 1005 of file cuddAPI.c.
01007 { 01008 return(DD_ZERO(dd)); 01009 01010 } /* end of Cudd_ReadZero */
| int Cudd_RemoveHook | ( | DdManager * | dd, | |
| int(*)(DdManager *, char *, void *) | 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 3274 of file cuddAPI.c.
03278 { 03279 DdHook **hook, *nextHook; 03280 03281 switch (where) { 03282 case CUDD_PRE_GC_HOOK: 03283 hook = &(dd->preGCHook); 03284 break; 03285 case CUDD_POST_GC_HOOK: 03286 hook = &(dd->postGCHook); 03287 break; 03288 case CUDD_PRE_REORDERING_HOOK: 03289 hook = &(dd->preReorderingHook); 03290 break; 03291 case CUDD_POST_REORDERING_HOOK: 03292 hook = &(dd->postReorderingHook); 03293 break; 03294 default: 03295 return(0); 03296 } 03297 nextHook = *hook; 03298 while (nextHook != NULL) { 03299 if (nextHook->f == f) { 03300 *hook = nextHook->next; 03301 FREE(nextHook); 03302 return(1); 03303 } 03304 hook = &(nextHook->next); 03305 nextHook = nextHook->next; 03306 } 03307 03308 return(0); 03309 03310 } /* 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 3559 of file cuddAPI.c.
03561 { 03562 return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)); 03563 03564 } /* 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 704 of file cuddAPI.c.
00707 { 00708 *method = unique->autoMethod; 00709 return(unique->autoDyn); 00710 00711 } /* 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 781 of file cuddAPI.c.
00784 { 00785 *method = unique->autoMethodZ; 00786 return(unique->autoDynZ); 00787 00788 } /* 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 2759 of file cuddAPI.c.
02762 { 02763 dd->arcviolation = arcviolation; 02764 02765 } /* end of Cudd_SetArcviolation */
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 1100 of file cuddAPI.c.
01103 { 01104 dd->background = bck; 01105 01106 } /* 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 2420 of file cuddAPI.c.
02423 { 02424 dd->epsilon = ep; 02425 02426 } /* 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 2465 of file cuddAPI.c.
02468 { 02469 dd->groupcheck = gc; 02470 02471 } /* 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 1314 of file cuddAPI.c.
01317 { 01318 if (lut == 0) { 01319 long datalimit = getSoftDataLimit(); 01320 lut = (unsigned int) (datalimit / (sizeof(DdNode) * 01321 DD_MAX_LOOSE_FRACTION)); 01322 } 01323 dd->looseUpTo = lut; 01324 01325 } /* 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 1384 of file cuddAPI.c.
01387 { 01388 if (mc == 0) { 01389 long datalimit = getSoftDataLimit(); 01390 mc = (unsigned int) (datalimit / (sizeof(DdCache) * 01391 DD_MAX_CACHE_FRACTION)); 01392 } 01393 dd->maxCacheHard = mc; 01394 01395 } /* 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 1982 of file cuddAPI.c.
01985 { 01986 dd->maxGrowth = mg; 01987 01988 } /* 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 2033 of file cuddAPI.c.
02036 { 02037 dd->maxGrowthAlt = mg; 02038 02039 } /* 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 3801 of file cuddAPI.c.
03804 { 03805 dd->maxLive = maxLive; 03806 03807 } /* end of Cudd_SetMaxLive */
| void Cudd_SetMaxMemory | ( | DdManager * | dd, | |
| 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 3844 of file cuddAPI.c.
03847 { 03848 dd->maxmemhard = maxMemory; 03849 03850 } /* 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 1267 of file cuddAPI.c.
01270 { 01271 /* Internally, the package manipulates the ratio of hits to 01272 ** misses instead of the ratio of hits to accesses. */ 01273 dd->minHit = (double) hr / (100.0 - (double) hr); 01274 01275 } /* 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 3734 of file cuddAPI.c.
03737 { 03738 dd->nextDyn = next; 03739 03740 } /* 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 2865 of file cuddAPI.c.
02868 { 02869 dd->numberXovers = numberXovers; 02870 02871 } /* 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 2812 of file cuddAPI.c.
02815 { 02816 dd->populationSize = populationSize; 02817 02818 } /* 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 2651 of file cuddAPI.c.
02654 { 02655 dd->recomb = recomb; 02656 02657 } /* 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 2080 of file cuddAPI.c.
02083 { 02084 dd->reordCycle = cycle; 02085 02086 } /* 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 1931 of file cuddAPI.c.
01934 { 01935 dd->siftMaxSwap = sms; 01936 01937 } /* 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 1882 of file cuddAPI.c.
01885 { 01886 dd->siftMaxVar = smv; 01887 01888 } /* 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 3685 of file cuddAPI.c.
03688 { 03689 dd->err = fp; 03690 03691 } /* 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 3642 of file cuddAPI.c.
03645 { 03646 dd->out = fp; 03647 03648 } /* 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 2706 of file cuddAPI.c.
02709 { 02710 dd->symmviolation = symmviolation; 02711 02712 } /* end of Cudd_SetSymmviolation */
Function********************************************************************
Synopsis [Sets the variable group tree of the manager.]
Description []
SideEffects [None]
SeeAlso [Cudd_FreeTree Cudd_ReadTree Cudd_SetZddTree]
Definition at line 2121 of file cuddAPI.c.
02124 { 02125 if (dd->tree != NULL) { 02126 Mtr_FreeTree(dd->tree); 02127 } 02128 dd->tree = tree; 02129 if (tree == NULL) return; 02130 02131 fixVarTree(tree, dd->perm, dd->size); 02132 return; 02133 02134 } /* end of Cudd_SetTree */
Function********************************************************************
Synopsis [Sets the ZDD variable group tree of the manager.]
Description []
SideEffects [None]
SeeAlso [Cudd_FreeZddTree Cudd_ReadZddTree Cudd_SetTree]
Definition at line 2193 of file cuddAPI.c.
02196 { 02197 if (dd->treeZ != NULL) { 02198 Mtr_FreeTree(dd->treeZ); 02199 } 02200 dd->treeZ = tree; 02201 if (tree == NULL) return; 02202 02203 fixVarTree(tree, dd->permZ, dd->sizeZ); 02204 return; 02205 02206 } /* end of Cudd_SetZddTree */
| int Cudd_StdPostReordHook | ( | DdManager * | dd, | |
| 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 3469 of file cuddAPI.c.
03473 { 03474 long initialTime = (long) data; 03475 int retval; 03476 long finalTime = util_cpu_time(); 03477 double totalTimeSec = (double)(finalTime - initialTime) / 1000.0; 03478 03479 retval = fprintf(dd->out,"%ld nodes in %g sec\n", strcmp(str, "BDD") == 0 ? 03480 Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd), 03481 totalTimeSec); 03482 if (retval == EOF) return(0); 03483 retval = fflush(dd->out); 03484 if (retval == EOF) return(0); 03485 return(1); 03486 03487 } /* end of Cudd_StdPostReordHook */
| int Cudd_StdPreReordHook | ( | DdManager * | dd, | |
| 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 3376 of file cuddAPI.c.
03380 { 03381 Cudd_ReorderingType method = (Cudd_ReorderingType) (ptruint) data; 03382 int retval; 03383 03384 retval = fprintf(dd->out,"%s reordering with ", str); 03385 if (retval == EOF) return(0); 03386 switch (method) { 03387 case CUDD_REORDER_SIFT_CONVERGE: 03388 case CUDD_REORDER_SYMM_SIFT_CONV: 03389 case CUDD_REORDER_GROUP_SIFT_CONV: 03390 case CUDD_REORDER_WINDOW2_CONV: 03391 case CUDD_REORDER_WINDOW3_CONV: 03392 case CUDD_REORDER_WINDOW4_CONV: 03393 case CUDD_REORDER_LINEAR_CONVERGE: 03394 retval = fprintf(dd->out,"converging "); 03395 if (retval == EOF) return(0); 03396 break; 03397 default: 03398 break; 03399 } 03400 switch (method) { 03401 case CUDD_REORDER_RANDOM: 03402 case CUDD_REORDER_RANDOM_PIVOT: 03403 retval = fprintf(dd->out,"random"); 03404 break; 03405 case CUDD_REORDER_SIFT: 03406 case CUDD_REORDER_SIFT_CONVERGE: 03407 retval = fprintf(dd->out,"sifting"); 03408 break; 03409 case CUDD_REORDER_SYMM_SIFT: 03410 case CUDD_REORDER_SYMM_SIFT_CONV: 03411 retval = fprintf(dd->out,"symmetric sifting"); 03412 break; 03413 case CUDD_REORDER_LAZY_SIFT: 03414 retval = fprintf(dd->out,"lazy sifting"); 03415 break; 03416 case CUDD_REORDER_GROUP_SIFT: 03417 case CUDD_REORDER_GROUP_SIFT_CONV: 03418 retval = fprintf(dd->out,"group sifting"); 03419 break; 03420 case CUDD_REORDER_WINDOW2: 03421 case CUDD_REORDER_WINDOW3: 03422 case CUDD_REORDER_WINDOW4: 03423 case CUDD_REORDER_WINDOW2_CONV: 03424 case CUDD_REORDER_WINDOW3_CONV: 03425 case CUDD_REORDER_WINDOW4_CONV: 03426 retval = fprintf(dd->out,"window"); 03427 break; 03428 case CUDD_REORDER_ANNEALING: 03429 retval = fprintf(dd->out,"annealing"); 03430 break; 03431 case CUDD_REORDER_GENETIC: 03432 retval = fprintf(dd->out,"genetic"); 03433 break; 03434 case CUDD_REORDER_LINEAR: 03435 case CUDD_REORDER_LINEAR_CONVERGE: 03436 retval = fprintf(dd->out,"linear sifting"); 03437 break; 03438 case CUDD_REORDER_EXACT: 03439 retval = fprintf(dd->out,"exact"); 03440 break; 03441 default: 03442 return(0); 03443 } 03444 if (retval == EOF) return(0); 03445 03446 retval = fprintf(dd->out,": from %ld to ... ", strcmp(str, "BDD") == 0 ? 03447 Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd)); 03448 if (retval == EOF) return(0); 03449 fflush(dd->out); 03450 return(1); 03451 03452 } /* 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 2602 of file cuddAPI.c.
02604 { 02605 dd->countDead = ~0; 02606 02607 } /* 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 2577 of file cuddAPI.c.
02579 { 02580 dd->countDead = 0; 02581 02582 } /* end of Cudd_TurnOnCountDead */
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 417 of file cuddAPI.c.
00420 { 00421 DdNode *res; 00422 DdNode *zvar; 00423 DdNode *lower; 00424 int j; 00425 00426 if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL); 00427 00428 /* The i-th variable function has the following structure: 00429 ** at the level corresponding to index i there is a node whose "then" 00430 ** child points to the universe, and whose "else" child points to zero. 00431 ** Above that level there are nodes with identical children. 00432 */ 00433 00434 /* First we build the node at the level of index i. */ 00435 lower = (i < dd->sizeZ - 1) ? dd->univ[dd->permZ[i]+1] : DD_ONE(dd); 00436 do { 00437 dd->reordered = 0; 00438 zvar = cuddUniqueInterZdd(dd, i, lower, DD_ZERO(dd)); 00439 } while (dd->reordered == 1); 00440 00441 if (zvar == NULL) 00442 return(NULL); 00443 cuddRef(zvar); 00444 00445 /* Now we add the "filler" nodes above the level of index i. */ 00446 for (j = dd->permZ[i] - 1; j >= 0; j--) { 00447 do { 00448 dd->reordered = 0; 00449 res = cuddUniqueInterZdd(dd, dd->invpermZ[j], zvar, zvar); 00450 } while (dd->reordered == 1); 00451 if (res == NULL) { 00452 Cudd_RecursiveDerefZdd(dd,zvar); 00453 return(NULL); 00454 } 00455 cuddRef(res); 00456 Cudd_RecursiveDerefZdd(dd,zvar); 00457 zvar = res; 00458 } 00459 cuddDeref(zvar); 00460 return(zvar); 00461 00462 } /* 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]
| 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 858 of file cuddAPI.c.
00860 { 00861 unique->realign = 0; 00862 return; 00863 00864 } /* 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 836 of file cuddAPI.c.
00838 { 00839 unique->realign = 1; 00840 return; 00841 00842 } /* 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 806 of file cuddAPI.c.
00808 { 00809 return(unique->realign); 00810 00811 } /* 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 488 of file cuddAPI.c.
00491 { 00492 int res; 00493 int i, j; 00494 int allnew; 00495 int *permutation; 00496 00497 if (multiplicity < 1) return(0); 00498 allnew = dd->sizeZ == 0; 00499 if (dd->size * multiplicity > dd->sizeZ) { 00500 res = cuddResizeTableZdd(dd,dd->size * multiplicity - 1); 00501 if (res == 0) return(0); 00502 } 00503 /* Impose the order of the BDD variables to the ZDD variables. */ 00504 if (allnew) { 00505 for (i = 0; i < dd->size; i++) { 00506 for (j = 0; j < multiplicity; j++) { 00507 dd->permZ[i * multiplicity + j] = 00508 dd->perm[i] * multiplicity + j; 00509 dd->invpermZ[dd->permZ[i * multiplicity + j]] = 00510 i * multiplicity + j; 00511 } 00512 } 00513 for (i = 0; i < dd->sizeZ; i++) { 00514 dd->univ[i]->index = dd->invpermZ[i]; 00515 } 00516 } else { 00517 permutation = ALLOC(int,dd->sizeZ); 00518 if (permutation == NULL) { 00519 dd->errorCode = CUDD_MEMORY_OUT; 00520 return(0); 00521 } 00522 for (i = 0; i < dd->size; i++) { 00523 for (j = 0; j < multiplicity; j++) { 00524 permutation[i * multiplicity + j] = 00525 dd->invperm[i] * multiplicity + j; 00526 } 00527 } 00528 for (i = dd->size * multiplicity; i < dd->sizeZ; i++) { 00529 permutation[i] = i; 00530 } 00531 res = Cudd_zddShuffleHeap(dd, permutation); 00532 FREE(permutation); 00533 if (res == 0) return(0); 00534 } 00535 /* Copy and expand the variable group tree if it exists. */ 00536 if (dd->treeZ != NULL) { 00537 Cudd_FreeZddTree(dd); 00538 } 00539 if (dd->tree != NULL) { 00540 dd->treeZ = Mtr_CopyTree(dd->tree, multiplicity); 00541 if (dd->treeZ == NULL) return(0); 00542 } else if (multiplicity > 1) { 00543 dd->treeZ = Mtr_InitGroupTree(0, dd->sizeZ); 00544 if (dd->treeZ == NULL) return(0); 00545 dd->treeZ->index = dd->invpermZ[0]; 00546 } 00547 /* Create groups for the ZDD variables derived from the same BDD variable. 00548 */ 00549 if (multiplicity > 1) { 00550 char *vmask, *lmask; 00551 00552 vmask = ALLOC(char, dd->size); 00553 if (vmask == NULL) { 00554 dd->errorCode = CUDD_MEMORY_OUT; 00555 return(0); 00556 } 00557 lmask = ALLOC(char, dd->size); 00558 if (lmask == NULL) { 00559 dd->errorCode = CUDD_MEMORY_OUT; 00560 return(0); 00561 } 00562 for (i = 0; i < dd->size; i++) { 00563 vmask[i] = lmask[i] = 0; 00564 } 00565 res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask); 00566 FREE(vmask); 00567 FREE(lmask); 00568 if (res == 0) return(0); 00569 } 00570 return(1); 00571 00572 } /* end of Cudd_zddVarsFromBddVars */
| static void fixVarTree | ( | MtrNode * | treenode, | |
| int * | perm, | |||
| int | size | |||
| ) | [static] |
Function********************************************************************
Synopsis [Fixes a variable group tree.]
Description []
SideEffects [Changes the variable group tree.]
SeeAlso []
Definition at line 4327 of file cuddAPI.c.
04331 { 04332 treenode->index = treenode->low; 04333 treenode->low = ((int) treenode->index < size) ? 04334 perm[treenode->index] : treenode->index; 04335 if (treenode->child != NULL) 04336 fixVarTree(treenode->child, perm, size); 04337 if (treenode->younger != NULL) 04338 fixVarTree(treenode->younger, perm, size); 04339 return; 04340 04341 } /* end of fixVarTree */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddAPI.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $" [static] |
CFile***********************************************************************
FileName [cuddAPI.c]
PackageName [cudd]
Synopsis [Application interface functions.]
Description [External procedures included in this module:
- Cudd_addNewVar()
- Cudd_addNewVarAtLevel()
- Cudd_bddNewVar()
- Cudd_bddNewVarAtLevel()
- Cudd_addIthVar()
- Cudd_bddIthVar()
- Cudd_zddIthVar()
- Cudd_zddVarsFromBddVars()
- Cudd_addConst()
- Cudd_IsNonConstant()
- Cudd_AutodynEnable()
- Cudd_AutodynDisable()
- Cudd_ReorderingStatus()
- Cudd_AutodynEnableZdd()
- Cudd_AutodynDisableZdd()
- Cudd_ReorderingStatusZdd()
- Cudd_zddRealignmentEnabled()
- Cudd_zddRealignEnable()
- Cudd_zddRealignDisable()
- Cudd_bddRealignmentEnabled()
- Cudd_bddRealignEnable()
- Cudd_bddRealignDisable()
- Cudd_ReadOne()
- Cudd_ReadZddOne()
- Cudd_ReadZero()
- Cudd_ReadLogicZero()
- Cudd_ReadPlusInfinity()
- Cudd_ReadMinusInfinity()
- Cudd_ReadBackground()
- Cudd_SetBackground()
- Cudd_ReadCacheSlots()
- Cudd_ReadCacheUsedSlots()
- Cudd_ReadCacheLookUps()
- Cudd_ReadCacheHits()
- Cudd_ReadMinHit()
- Cudd_SetMinHit()
- Cudd_ReadLooseUpTo()
- Cudd_SetLooseUpTo()
- Cudd_ReadMaxCache()
- Cudd_ReadMaxCacheHard()
- Cudd_SetMaxCacheHard()
- Cudd_ReadSize()
- Cudd_ReadSlots()
- Cudd_ReadUsedSlots()
- Cudd_ExpectedUsedSlots()
- Cudd_ReadKeys()
- Cudd_ReadDead()
- Cudd_ReadMinDead()
- Cudd_ReadReorderings()
- Cudd_ReadReorderingTime()
- Cudd_ReadGarbageCollections()
- Cudd_ReadGarbageCollectionTime()
- Cudd_ReadNodesFreed()
- Cudd_ReadNodesDropped()
- Cudd_ReadUniqueLookUps()
- Cudd_ReadUniqueLinks()
- Cudd_ReadSiftMaxVar()
- Cudd_SetSiftMaxVar()
- Cudd_ReadMaxGrowth()
- Cudd_SetMaxGrowth()
- Cudd_ReadMaxGrowthAlternate()
- Cudd_SetMaxGrowthAlternate()
- Cudd_ReadReorderingCycle()
- Cudd_SetReorderingCycle()
- Cudd_ReadTree()
- Cudd_SetTree()
- Cudd_FreeTree()
- Cudd_ReadZddTree()
- Cudd_SetZddTree()
- Cudd_FreeZddTree()
- Cudd_NodeReadIndex()
- Cudd_ReadPerm()
- Cudd_ReadInvPerm()
- Cudd_ReadVars()
- Cudd_ReadEpsilon()
- Cudd_SetEpsilon()
- Cudd_ReadGroupCheck()
- Cudd_SetGroupcheck()
- Cudd_GarbageCollectionEnabled()
- Cudd_EnableGarbageCollection()
- Cudd_DisableGarbageCollection()
- Cudd_DeadAreCounted()
- Cudd_TurnOnCountDead()
- Cudd_TurnOffCountDead()
- Cudd_ReadRecomb()
- Cudd_SetRecomb()
- Cudd_ReadSymmviolation()
- Cudd_SetSymmviolation()
- Cudd_ReadArcviolation()
- Cudd_SetArcviolation()
- Cudd_ReadPopulationSize()
- Cudd_SetPopulationSize()
- Cudd_ReadNumberXovers()
- Cudd_SetNumberXovers()
- Cudd_ReadMemoryInUse()
- Cudd_PrintInfo()
- Cudd_ReadPeakNodeCount()
- Cudd_ReadPeakLiveNodeCount()
- Cudd_ReadNodeCount()
- Cudd_zddReadNodeCount()
- Cudd_AddHook()
- Cudd_RemoveHook()
- Cudd_IsInHook()
- Cudd_StdPreReordHook()
- Cudd_StdPostReordHook()
- Cudd_EnableReorderingReporting()
- Cudd_DisableReorderingReporting()
- Cudd_ReorderingReporting()
- Cudd_ReadErrorCode()
- Cudd_ClearErrorCode()
- Cudd_ReadStdout()
- Cudd_SetStdout()
- Cudd_ReadStderr()
- Cudd_SetStderr()
- Cudd_ReadNextReordering()
- Cudd_SetNextReordering()
- Cudd_ReadSwapSteps()
- Cudd_ReadMaxLive()
- Cudd_SetMaxLive()
- Cudd_ReadMaxMemory()
- Cudd_SetMaxMemory()
- Cudd_bddBindVar()
- Cudd_bddUnbindVar()
- Cudd_bddVarIsBound()
- Cudd_bddSetPiVar()
- Cudd_bddSetPsVar()
- Cudd_bddSetNsVar()
- Cudd_bddIsPiVar()
- Cudd_bddIsPsVar()
- Cudd_bddIsNsVar()
- Cudd_bddSetPairIndex()
- Cudd_bddReadPairIndex()
- Cudd_bddSetVarToBeGrouped()
- Cudd_bddSetVarHardGroup()
- Cudd_bddResetVarToBeGrouped()
- Cudd_bddIsVarToBeGrouped()
- Cudd_bddSetVarToBeUngrouped()
- Cudd_bddIsVarToBeUngrouped()
- Cudd_bddIsVarHardGroup()
Static procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
