src/cuBdd/cuddAPI.c File Reference
#include "util.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 4399 of file cuddAPI.c.
04405 { 04406 int startV, stopV, startL; 04407 int i, j; 04408 MtrNode *auxnode = treenode; 04409 04410 while (auxnode != NULL) { 04411 if (auxnode->child != NULL) { 04412 addMultiplicityGroups(dd,auxnode->child,multiplicity,vmask,lmask); 04413 } 04414 /* Build remaining groups. */ 04415 startV = dd->permZ[auxnode->index] / multiplicity; 04416 startL = auxnode->low / multiplicity; 04417 stopV = startV + auxnode->size / multiplicity; 04418 /* Walk down vmask starting at startV and build missing groups. */ 04419 for (i = startV, j = startL; i < stopV; i++) { 04420 if (vmask[i] == 0) { 04421 MtrNode *node; 04422 while (lmask[j] == 1) j++; 04423 node = Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity, 04424 MTR_FIXED); 04425 if (node == NULL) { 04426 return(0); 04427 } 04428 node->index = dd->invpermZ[i * multiplicity]; 04429 vmask[i] = 1; 04430 lmask[j] = 1; 04431 } 04432 } 04433 auxnode = auxnode->younger; 04434 } 04435 return(1); 04436 04437 } /* end of addMultiplicityGroups */
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 616 of file cuddAPI.c.
00619 { 00620 return(cuddUniqueConst(dd,c)); 00621 00622 } /* end of Cudd_addConst */
| int Cudd_AddHook | ( | DdManager * | dd, | |
| DD_HFP | f, | |||
| Cudd_HookType | where | |||
| ) |
Function********************************************************************
Synopsis [Adds a function to a hook.]
Description [Adds a function to a hook. A hook is a list of application-provided functions called on certain occasions by the package. Returns 1 if the function is successfully added; 2 if the function was already in the list; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_RemoveHook]
Definition at line 3241 of file cuddAPI.c.
03245 { 03246 DdHook **hook, *nextHook, *newHook; 03247 03248 switch (where) { 03249 case CUDD_PRE_GC_HOOK: 03250 hook = &(dd->preGCHook); 03251 break; 03252 case CUDD_POST_GC_HOOK: 03253 hook = &(dd->postGCHook); 03254 break; 03255 case CUDD_PRE_REORDERING_HOOK: 03256 hook = &(dd->preReorderingHook); 03257 break; 03258 case CUDD_POST_REORDERING_HOOK: 03259 hook = &(dd->postReorderingHook); 03260 break; 03261 default: 03262 return(0); 03263 } 03264 /* Scan the list and find whether the function is already there. 03265 ** If so, just return. */ 03266 nextHook = *hook; 03267 while (nextHook != NULL) { 03268 if (nextHook->f == f) { 03269 return(2); 03270 } 03271 hook = &(nextHook->next); 03272 nextHook = nextHook->next; 03273 } 03274 /* The function was not in the list. Create a new item and append it 03275 ** to the end of the list. */ 03276 newHook = ALLOC(DdHook,1); 03277 if (newHook == NULL) { 03278 dd->errorCode = CUDD_MEMORY_OUT; 03279 return(0); 03280 } 03281 newHook->next = NULL; 03282 newHook->f = f; 03283 *hook = newHook; 03284 return(1); 03285 03286 } /* 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 380 of file cuddAPI.c.
00383 { 00384 DdNode *res; 00385 00386 if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL); 00387 do { 00388 dd->reordered = 0; 00389 res = cuddUniqueInter(dd,i,DD_ONE(dd),DD_ZERO(dd)); 00390 } while (dd->reordered == 1); 00391 00392 return(res); 00393 00394 } /* 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 255 of file cuddAPI.c.
00257 { 00258 DdNode *res; 00259 00260 if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL); 00261 do { 00262 dd->reordered = 0; 00263 res = cuddUniqueInter(dd,dd->size,DD_ONE(dd),DD_ZERO(dd)); 00264 } while (dd->reordered == 1); 00265 00266 return(res); 00267 00268 } /* 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 286 of file cuddAPI.c.
00289 { 00290 DdNode *res; 00291 00292 if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL); 00293 if (level >= dd->size) return(Cudd_addIthVar(dd,level)); 00294 if (!cuddInsertSubtables(dd,1,level)) return(NULL); 00295 do { 00296 dd->reordered = 0; 00297 res = cuddUniqueInter(dd,dd->size - 1,DD_ONE(dd),DD_ZERO(dd)); 00298 } while (dd->reordered == 1); 00299 00300 return(res); 00301 00302 } /* 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 704 of file cuddAPI.c.
00706 { 00707 unique->autoDyn = 0; 00708 return; 00709 00710 } /* 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 782 of file cuddAPI.c.
00784 { 00785 unique->autoDynZ = 0; 00786 return; 00787 00788 } /* 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 665 of file cuddAPI.c.
00668 { 00669 unique->autoDyn = 1; 00670 if (method != CUDD_REORDER_SAME) { 00671 unique->autoMethod = method; 00672 } 00673 #ifndef DD_NO_DEATH_ROW 00674 /* If reordering is enabled, using the death row causes too many 00675 ** invocations. Hence, we shrink the death row to just one entry. 00676 */ 00677 cuddClearDeathRow(unique); 00678 unique->deathRowDepth = 1; 00679 unique->deadMask = unique->deathRowDepth - 1; 00680 if ((unsigned) unique->nextDead > unique->deadMask) { 00681 unique->nextDead = 0; 00682 } 00683 unique->deathRow = REALLOC(DdNodePtr, unique->deathRow, 00684 unique->deathRowDepth); 00685 #endif 00686 return; 00687 00688 } /* 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 756 of file cuddAPI.c.
00759 { 00760 unique->autoDynZ = 1; 00761 if (method != CUDD_REORDER_SAME) { 00762 unique->autoMethodZ = method; 00763 } 00764 return; 00765 00766 } /* 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 4095 of file cuddAPI.c.
04098 { 04099 if (index >= dd->size || index < 0) return -1; 04100 return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_NEXT_STATE); 04101 04102 } /* 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 4047 of file cuddAPI.c.
04050 { 04051 if (index >= dd->size || index < 0) return -1; 04052 return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRIMARY_INPUT); 04053 04054 } /* 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 4071 of file cuddAPI.c.
04074 { 04075 if (index >= dd->size || index < 0) return -1; 04076 return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRESENT_STATE); 04077 04078 } /* 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 4323 of file cuddAPI.c.
04326 { 04327 if (index >= dd->size || index < 0) return(-1); 04328 if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_HARD_GROUP) 04329 return(1); 04330 return(0); 04331 04332 } /* 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 4246 of file cuddAPI.c.
04249 { 04250 if (index >= dd->size || index < 0) return(-1); 04251 if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP) 04252 return(0); 04253 else 04254 return(dd->subtables[dd->perm[index]].varToBeGrouped); 04255 04256 } /* 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 4298 of file cuddAPI.c.
04301 { 04302 if (index >= dd->size || index < 0) return(-1); 04303 return dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP; 04304 04305 } /* 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 412 of file cuddAPI.c.
00415 { 00416 DdNode *res; 00417 00418 if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL); 00419 if (i < dd->size) { 00420 res = dd->vars[i]; 00421 } else { 00422 res = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one)); 00423 } 00424 00425 return(res); 00426 00427 } /* 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 319 of file cuddAPI.c.
00321 { 00322 DdNode *res; 00323 00324 if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL); 00325 res = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one)); 00326 00327 return(res); 00328 00329 } /* 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 347 of file cuddAPI.c.
00350 { 00351 DdNode *res; 00352 00353 if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL); 00354 if (level >= dd->size) return(Cudd_bddIthVar(dd,level)); 00355 if (!cuddInsertSubtables(dd,1,level)) return(NULL); 00356 res = dd->vars[dd->size - 1]; 00357 00358 return(res); 00359 00360 } /* 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 961 of file cuddAPI.c.
00963 { 00964 unique->realignZ = 0; 00965 return; 00966 00967 } /* 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 939 of file cuddAPI.c.
00941 { 00942 unique->realignZ = 1; 00943 return; 00944 00945 } /* 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 909 of file cuddAPI.c.
00911 { 00912 return(unique->realignZ); 00913 00914 } /* 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 4219 of file cuddAPI.c.
04222 { 04223 if (index >= dd->size || index < 0) return(0); 04224 if (dd->subtables[dd->perm[index]].varToBeGrouped <= 04225 CUDD_LAZY_SOFT_GROUP) { 04226 dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_NONE; 04227 } 04228 return(1); 04229 04230 } /* 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 4022 of file cuddAPI.c.
04025 { 04026 if (index >= dd->size || index < 0) return (0); 04027 dd->subtables[dd->perm[index]].varType = CUDD_VAR_NEXT_STATE; 04028 return(1); 04029 04030 } /* 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 3974 of file cuddAPI.c.
03977 { 03978 if (index >= dd->size || index < 0) return (0); 03979 dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRIMARY_INPUT; 03980 return(1); 03981 03982 } /* 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 3998 of file cuddAPI.c.
04001 { 04002 if (index >= dd->size || index < 0) return (0); 04003 dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRESENT_STATE; 04004 return(1); 04005 04006 } /* 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 4195 of file cuddAPI.c.
04198 { 04199 if (index >= dd->size || index < 0) return(0); 04200 dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_HARD_GROUP; 04201 return(1); 04202 04203 } /* 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 4168 of file cuddAPI.c.
04171 { 04172 if (index >= dd->size || index < 0) return(0); 04173 if (dd->subtables[dd->perm[index]].varToBeGrouped <= CUDD_LAZY_SOFT_GROUP) { 04174 dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_SOFT_GROUP; 04175 } 04176 return(1); 04177 04178 } /* 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 4272 of file cuddAPI.c.
04275 { 04276 if (index >= dd->size || index < 0) return(0); 04277 dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_UNGROUP; 04278 return(1); 04279 04280 } /* 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 3629 of file cuddAPI.c.
03631 { 03632 dd->errorCode = CUDD_NO_ERROR; 03633 03634 } /* 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 2581 of file cuddAPI.c.
02583 { 02584 return(dd->countDead == 0 ? 1 : 0); 02585 02586 } /* 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 2559 of file cuddAPI.c.
02561 { 02562 dd->gcEnabled = 0; 02563 02564 } /* 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 3561 of file cuddAPI.c.
03563 { 03564 if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) { 03565 return(0); 03566 } 03567 if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) { 03568 return(0); 03569 } 03570 return(1); 03571 03572 } /* 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 2535 of file cuddAPI.c.
02537 { 02538 dd->gcEnabled = 1; 02539 02540 } /* 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 3533 of file cuddAPI.c.
03535 { 03536 if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) { 03537 return(0); 03538 } 03539 if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) { 03540 return(0); 03541 } 03542 return(1); 03543 03544 } /* 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 1568 of file cuddAPI.c.
01570 { 01571 int i; 01572 int size = dd->size; 01573 DdSubtable *subtable; 01574 double empty = 0.0; 01575 01576 /* To each subtable we apply the corollary to Theorem 8.5 (occupancy 01577 ** distribution) from Sedgewick and Flajolet's Analysis of Algorithms. 01578 ** The corollary says that for a table with M buckets and a load ratio 01579 ** of r, the expected number of empty buckets is asymptotically given 01580 ** by M * exp(-r). 01581 */ 01582 01583 /* Scan each BDD/ADD subtable. */ 01584 for (i = 0; i < size; i++) { 01585 subtable = &(dd->subtables[i]); 01586 empty += (double) subtable->slots * 01587 exp(-(double) subtable->keys / (double) subtable->slots); 01588 } 01589 01590 /* Scan the ZDD subtables. */ 01591 size = dd->sizeZ; 01592 01593 for (i = 0; i < size; i++) { 01594 subtable = &(dd->subtableZ[i]); 01595 empty += (double) subtable->slots * 01596 exp(-(double) subtable->keys / (double) subtable->slots); 01597 } 01598 01599 /* Constant table. */ 01600 subtable = &(dd->constants); 01601 empty += (double) subtable->slots * 01602 exp(-(double) subtable->keys / (double) subtable->slots); 01603 01604 return(1.0 - empty / (double) dd->slots); 01605 01606 } /* end of Cudd_ExpectedUsedSlots */
| void Cudd_FreeTree | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Frees the variable group tree of the manager.]
Description []
SideEffects [None]
SeeAlso [Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree]
Definition at line 2176 of file cuddAPI.c.
02178 { 02179 if (dd->tree != NULL) { 02180 Mtr_FreeTree(dd->tree); 02181 dd->tree = NULL; 02182 } 02183 return; 02184 02185 } /* end of Cudd_FreeTree */
| void Cudd_FreeZddTree | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Frees the variable group tree of the manager.]
Description []
SideEffects [None]
SeeAlso [Cudd_SetZddTree Cudd_ReadZddTree Cudd_FreeTree]
Definition at line 2248 of file cuddAPI.c.
02250 { 02251 if (dd->treeZ != NULL) { 02252 Mtr_FreeTree(dd->treeZ); 02253 dd->treeZ = NULL; 02254 } 02255 return; 02256 02257 } /* end of Cudd_FreeZddTree */
| int Cudd_GarbageCollectionEnabled | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Tells whether garbage collection is enabled.]
Description [Returns 1 if garbage collection is enabled; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_EnableGarbageCollection Cudd_DisableGarbageCollection]
Definition at line 2513 of file cuddAPI.c.
02515 { 02516 return(dd->gcEnabled); 02517 02518 } /* end of Cudd_GarbageCollectionEnabled */
| int Cudd_IsInHook | ( | DdManager * | dd, | |
| DD_HFP | f, | |||
| Cudd_HookType | where | |||
| ) |
Function********************************************************************
Synopsis [Checks whether a function is in a hook.]
Description [Checks whether a function is in a hook. A hook is a list of application-provided functions called on certain occasions by the package. Returns 1 if the function is found; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_AddHook Cudd_RemoveHook]
Definition at line 3356 of file cuddAPI.c.
03360 { 03361 DdHook *hook; 03362 03363 switch (where) { 03364 case CUDD_PRE_GC_HOOK: 03365 hook = dd->preGCHook; 03366 break; 03367 case CUDD_POST_GC_HOOK: 03368 hook = dd->postGCHook; 03369 break; 03370 case CUDD_PRE_REORDERING_HOOK: 03371 hook = dd->preReorderingHook; 03372 break; 03373 case CUDD_POST_REORDERING_HOOK: 03374 hook = dd->postReorderingHook; 03375 break; 03376 default: 03377 return(0); 03378 } 03379 /* Scan the list and find whether the function is already there. */ 03380 while (hook != NULL) { 03381 if (hook->f == f) { 03382 return(1); 03383 } 03384 hook = hook->next; 03385 } 03386 return(0); 03387 03388 } /* 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 641 of file cuddAPI.c.
00643 { 00644 return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f)); 00645 00646 } /* 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 2273 of file cuddAPI.c.
02275 { 02276 return((unsigned int) Cudd_Regular(node)->index); 02277 02278 } /* 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 2933 of file cuddAPI.c.
02936 { 02937 int retval; 02938 Cudd_ReorderingType autoMethod, autoMethodZ; 02939 02940 /* Modifiable parameters. */ 02941 retval = fprintf(fp,"**** CUDD modifiable parameters ****\n"); 02942 if (retval == EOF) return(0); 02943 retval = fprintf(fp,"Hard limit for cache size: %u\n", 02944 Cudd_ReadMaxCacheHard(dd)); 02945 if (retval == EOF) return(0); 02946 retval = fprintf(fp,"Cache hit threshold for resizing: %u%%\n", 02947 Cudd_ReadMinHit(dd)); 02948 if (retval == EOF) return(0); 02949 retval = fprintf(fp,"Garbage collection enabled: %s\n", 02950 Cudd_GarbageCollectionEnabled(dd) ? "yes" : "no"); 02951 if (retval == EOF) return(0); 02952 retval = fprintf(fp,"Limit for fast unique table growth: %u\n", 02953 Cudd_ReadLooseUpTo(dd)); 02954 if (retval == EOF) return(0); 02955 retval = fprintf(fp, 02956 "Maximum number of variables sifted per reordering: %d\n", 02957 Cudd_ReadSiftMaxVar(dd)); 02958 if (retval == EOF) return(0); 02959 retval = fprintf(fp, 02960 "Maximum number of variable swaps per reordering: %d\n", 02961 Cudd_ReadSiftMaxSwap(dd)); 02962 if (retval == EOF) return(0); 02963 retval = fprintf(fp,"Maximum growth while sifting a variable: %g\n", 02964 Cudd_ReadMaxGrowth(dd)); 02965 if (retval == EOF) return(0); 02966 retval = fprintf(fp,"Dynamic reordering of BDDs enabled: %s\n", 02967 Cudd_ReorderingStatus(dd,&autoMethod) ? "yes" : "no"); 02968 if (retval == EOF) return(0); 02969 retval = fprintf(fp,"Default BDD reordering method: %d\n", 02970 (int) autoMethod); 02971 if (retval == EOF) return(0); 02972 retval = fprintf(fp,"Dynamic reordering of ZDDs enabled: %s\n", 02973 Cudd_ReorderingStatusZdd(dd,&autoMethodZ) ? "yes" : "no"); 02974 if (retval == EOF) return(0); 02975 retval = fprintf(fp,"Default ZDD reordering method: %d\n", 02976 (int) autoMethodZ); 02977 if (retval == EOF) return(0); 02978 retval = fprintf(fp,"Realignment of ZDDs to BDDs enabled: %s\n", 02979 Cudd_zddRealignmentEnabled(dd) ? "yes" : "no"); 02980 if (retval == EOF) return(0); 02981 retval = fprintf(fp,"Realignment of BDDs to ZDDs enabled: %s\n", 02982 Cudd_bddRealignmentEnabled(dd) ? "yes" : "no"); 02983 if (retval == EOF) return(0); 02984 retval = fprintf(fp,"Dead nodes counted in triggering reordering: %s\n", 02985 Cudd_DeadAreCounted(dd) ? "yes" : "no"); 02986 if (retval == EOF) return(0); 02987 retval = fprintf(fp,"Group checking criterion: %d\n", 02988 (int) Cudd_ReadGroupcheck(dd)); 02989 if (retval == EOF) return(0); 02990 retval = fprintf(fp,"Recombination threshold: %d\n", Cudd_ReadRecomb(dd)); 02991 if (retval == EOF) return(0); 02992 retval = fprintf(fp,"Symmetry violation threshold: %d\n", 02993 Cudd_ReadSymmviolation(dd)); 02994 if (retval == EOF) return(0); 02995 retval = fprintf(fp,"Arc violation threshold: %d\n", 02996 Cudd_ReadArcviolation(dd)); 02997 if (retval == EOF) return(0); 02998 retval = fprintf(fp,"GA population size: %d\n", 02999 Cudd_ReadPopulationSize(dd)); 03000 if (retval == EOF) return(0); 03001 retval = fprintf(fp,"Number of crossovers for GA: %d\n", 03002 Cudd_ReadNumberXovers(dd)); 03003 if (retval == EOF) return(0); 03004 retval = fprintf(fp,"Next reordering threshold: %u\n", 03005 Cudd_ReadNextReordering(dd)); 03006 if (retval == EOF) return(0); 03007 03008 /* Non-modifiable parameters. */ 03009 retval = fprintf(fp,"**** CUDD non-modifiable parameters ****\n"); 03010 if (retval == EOF) return(0); 03011 retval = fprintf(fp,"Memory in use: %lu\n", Cudd_ReadMemoryInUse(dd)); 03012 if (retval == EOF) return(0); 03013 retval = fprintf(fp,"Peak number of nodes: %ld\n", 03014 Cudd_ReadPeakNodeCount(dd)); 03015 if (retval == EOF) return(0); 03016 retval = fprintf(fp,"Peak number of live nodes: %d\n", 03017 Cudd_ReadPeakLiveNodeCount(dd)); 03018 if (retval == EOF) return(0); 03019 retval = fprintf(fp,"Number of BDD variables: %d\n", dd->size); 03020 if (retval == EOF) return(0); 03021 retval = fprintf(fp,"Number of ZDD variables: %d\n", dd->sizeZ); 03022 if (retval == EOF) return(0); 03023 retval = fprintf(fp,"Number of cache entries: %u\n", dd->cacheSlots); 03024 if (retval == EOF) return(0); 03025 retval = fprintf(fp,"Number of cache look-ups: %.0f\n", 03026 Cudd_ReadCacheLookUps(dd)); 03027 if (retval == EOF) return(0); 03028 retval = fprintf(fp,"Number of cache hits: %.0f\n", 03029 Cudd_ReadCacheHits(dd)); 03030 if (retval == EOF) return(0); 03031 retval = fprintf(fp,"Number of cache insertions: %.0f\n", 03032 dd->cacheinserts); 03033 if (retval == EOF) return(0); 03034 retval = fprintf(fp,"Number of cache collisions: %.0f\n", 03035 dd->cachecollisions); 03036 if (retval == EOF) return(0); 03037 retval = fprintf(fp,"Number of cache deletions: %.0f\n", 03038 dd->cachedeletions); 03039 if (retval == EOF) return(0); 03040 retval = cuddCacheProfile(dd,fp); 03041 if (retval == 0) return(0); 03042 retval = fprintf(fp,"Soft limit for cache size: %u\n", 03043 Cudd_ReadMaxCache(dd)); 03044 if (retval == EOF) return(0); 03045 retval = fprintf(fp,"Number of buckets in unique table: %u\n", dd->slots); 03046 if (retval == EOF) return(0); 03047 retval = fprintf(fp,"Used buckets in unique table: %.2f%% (expected %.2f%%)\n", 03048 100.0 * Cudd_ReadUsedSlots(dd), 03049 100.0 * Cudd_ExpectedUsedSlots(dd)); 03050 if (retval == EOF) return(0); 03051 #ifdef DD_UNIQUE_PROFILE 03052 retval = fprintf(fp,"Unique lookups: %.0f\n", dd->uniqueLookUps); 03053 if (retval == EOF) return(0); 03054 retval = fprintf(fp,"Unique links: %.0f (%g per lookup)\n", 03055 dd->uniqueLinks, dd->uniqueLinks / dd->uniqueLookUps); 03056 if (retval == EOF) return(0); 03057 #endif 03058 retval = fprintf(fp,"Number of BDD and ADD nodes: %u\n", dd->keys); 03059 if (retval == EOF) return(0); 03060 retval = fprintf(fp,"Number of ZDD nodes: %u\n", dd->keysZ); 03061 if (retval == EOF) return(0); 03062 retval = fprintf(fp,"Number of dead BDD and ADD nodes: %u\n", dd->dead); 03063 if (retval == EOF) return(0); 03064 retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ); 03065 if (retval == EOF) return(0); 03066 retval = fprintf(fp,"Total number of nodes allocated: %.0f\n", 03067 dd->allocated); 03068 if (retval == EOF) return(0); 03069 retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n", 03070 dd->reclaimed); 03071 if (retval == EOF) return(0); 03072 #ifdef DD_STATS 03073 retval = fprintf(fp,"Nodes freed: %.0f\n", dd->nodesFreed); 03074 if (retval == EOF) return(0); 03075 retval = fprintf(fp,"Nodes dropped: %.0f\n", dd->nodesDropped); 03076 if (retval == EOF) return(0); 03077 #endif 03078 #ifdef DD_COUNT 03079 retval = fprintf(fp,"Number of recursive calls: %.0f\n", 03080 Cudd_ReadRecursiveCalls(dd)); 03081 if (retval == EOF) return(0); 03082 #endif 03083 retval = fprintf(fp,"Garbage collections so far: %d\n", 03084 Cudd_ReadGarbageCollections(dd)); 03085 if (retval == EOF) return(0); 03086 retval = fprintf(fp,"Time for garbage collection: %.2f sec\n", 03087 ((double)Cudd_ReadGarbageCollectionTime(dd)/1000.0)); 03088 if (retval == EOF) return(0); 03089 retval = fprintf(fp,"Reorderings so far: %d\n", dd->reorderings); 03090 if (retval == EOF) return(0); 03091 retval = fprintf(fp,"Time for reordering: %.2f sec\n", 03092 ((double)Cudd_ReadReorderingTime(dd)/1000.0)); 03093 if (retval == EOF) return(0); 03094 #ifdef DD_COUNT 03095 retval = fprintf(fp,"Node swaps in reordering: %.0f\n", 03096 Cudd_ReadSwapSteps(dd)); 03097 if (retval == EOF) return(0); 03098 #endif 03099 03100 return(1); 03101 03102 } /* 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 2760 of file cuddAPI.c.
02762 { 02763 return(dd->arcviolation); 02764 02765 } /* end of Cudd_ReadArcviolation */
Function********************************************************************
Synopsis [Reads the background constant of the manager.]
Description []
SideEffects [None]
Definition at line 1108 of file cuddAPI.c.
01110 { 01111 return(dd->background); 01112 01113 } /* 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 1221 of file cuddAPI.c.
01223 { 01224 return(dd->cacheHits + dd->totCachehits); 01225 01226 } /* 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 1200 of file cuddAPI.c.
01202 { 01203 return(dd->cacheHits + dd->cacheMisses + 01204 dd->totCachehits + dd->totCacheMisses); 01205 01206 } /* 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 1148 of file cuddAPI.c.
01150 { 01151 return(dd->cacheSlots); 01152 01153 } /* 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 1171 of file cuddAPI.c.
01173 { 01174 unsigned long used = 0; 01175 int slots = dd->cacheSlots; 01176 DdCache *cache = dd->cache; 01177 int i; 01178 01179 for (i = 0; i < slots; i++) { 01180 used += cache[i].h != 0; 01181 } 01182 01183 return((double)used / (double) dd->cacheSlots); 01184 01185 } /* 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 1642 of file cuddAPI.c.
01644 { 01645 return(dd->dead); 01646 01647 } /* 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 2426 of file cuddAPI.c.
02428 { 02429 return(dd->epsilon); 02430 02431 } /* 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 3609 of file cuddAPI.c.
03611 { 03612 return(dd->errorCode); 03613 03614 } /* 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 1737 of file cuddAPI.c.
01739 { 01740 return(dd->garbageCollections); 01741 01742 } /* 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 1758 of file cuddAPI.c.
01760 { 01761 return(dd->GCTime); 01762 01763 } /* 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 2470 of file cuddAPI.c.
02472 { 02473 return(dd->groupcheck); 02474 02475 } /* 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 2350 of file cuddAPI.c.
02353 { 02354 if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX); 02355 if (i < 0 || i >= dd->size) return(-1); 02356 return(dd->invperm[i]); 02357 02358 } /* 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 2376 of file cuddAPI.c.
02379 { 02380 if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX); 02381 if (i < 0 || i >= dd->sizeZ) return(-1); 02382 return(dd->invpermZ[i]); 02383 02384 } /* 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 1622 of file cuddAPI.c.
01624 { 01625 return(dd->keys); 01626 01627 } /* 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 1317 of file cuddAPI.c.
01319 { 01320 return(dd->looseUpTo); 01321 01322 } /* 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 1367 of file cuddAPI.c.
01369 { 01370 return(2 * dd->cacheSlots + dd->cacheSlack); 01371 01372 } /* 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 1387 of file cuddAPI.c.
01389 { 01390 return(dd->maxCacheHard); 01391 01392 } /* 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 1984 of file cuddAPI.c.
01986 { 01987 return(dd->maxGrowth); 01988 01989 } /* 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 2035 of file cuddAPI.c.
02037 { 02038 return(dd->maxGrowthAlt); 02039 02040 } /* 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 3809 of file cuddAPI.c.
03811 { 03812 return(dd->maxLive); 03813 03814 } /* end of Cudd_ReadMaxLive */
| unsigned long Cudd_ReadMaxMemory | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the maximum allowed memory.]
Description [Reads the maximum allowed memory. When this number is exceeded, the package returns NULL.]
SideEffects [none]
SeeAlso [Cudd_SetMaxMemory]
Definition at line 3852 of file cuddAPI.c.
03854 { 03855 return(dd->maxmemhard); 03856 03857 } /* end of Cudd_ReadMaxMemory */
| unsigned long Cudd_ReadMemoryInUse | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the memory in use by the manager measured in bytes.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 2912 of file cuddAPI.c.
02914 { 02915 return(dd->memused); 02916 02917 } /* 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 1666 of file cuddAPI.c.
01668 { 01669 return(dd->minDead); 01670 01671 } /* 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 1090 of file cuddAPI.c.
01092 { 01093 return(dd->minusinfinity); 01094 01095 } /* 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 3739 of file cuddAPI.c.
03741 { 03742 return(dd->nextDyn); 03743 03744 } /* 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 3176 of file cuddAPI.c.
03178 { 03179 long count; 03180 int i; 03181 03182 #ifndef DD_NO_DEATH_ROW 03183 cuddClearDeathRow(dd); 03184 #endif 03185 03186 count = (long) (dd->keys - dd->dead); 03187 03188 /* Count isolated projection functions. Their number is subtracted 03189 ** from the node count because they are not part of the BDDs. 03190 */ 03191 for (i=0; i < dd->size; i++) { 03192 if (dd->vars[i]->ref == 1) count--; 03193 } 03194 /* Subtract from the count the unused constants. */ 03195 if (DD_ZERO(dd)->ref == 1) count--; 03196 if (DD_PLUS_INFINITY(dd)->ref == 1) count--; 03197 if (DD_MINUS_INFINITY(dd)->ref == 1) count--; 03198 03199 return(count); 03200 03201 } /* 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 2866 of file cuddAPI.c.
02868 { 02869 return(dd->numberXovers); 02870 02871 } /* 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 983 of file cuddAPI.c.
00985 { 00986 return(dd->one); 00987 00988 } /* 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 3148 of file cuddAPI.c.
03150 { 03151 unsigned int live = dd->keys - dd->dead; 03152 03153 if (live > dd->peakLiveNodes) { 03154 dd->peakLiveNodes = live; 03155 } 03156 return((int)dd->peakLiveNodes); 03157 03158 } /* 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 3119 of file cuddAPI.c.
03121 { 03122 long count = 0; 03123 DdNodePtr *scan = dd->memoryList; 03124 03125 while (scan != NULL) { 03126 count += DD_MEM_CHUNK; 03127 scan = (DdNodePtr *) *scan; 03128 } 03129 return(count); 03130 03131 } /* 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 2297 of file cuddAPI.c.
02300 { 02301 if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX); 02302 if (i < 0 || i >= dd->size) return(-1); 02303 return(dd->perm[i]); 02304 02305 } /* 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 2324 of file cuddAPI.c.
02327 { 02328 if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX); 02329 if (i < 0 || i >= dd->sizeZ) return(-1); 02330 return(dd->permZ[i]); 02331 02332 } /* end of Cudd_ReadPermZdd */
Function********************************************************************
Synopsis [Reads the plus-infinity constant from the manager.]
Description []
SideEffects [None]
Definition at line 1072 of file cuddAPI.c.
01074 { 01075 return(dd->plusinfinity); 01076 01077 } /* 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 2813 of file cuddAPI.c.
02815 { 02816 return(dd->populationSize); 02817 02818 } /* 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 2653 of file cuddAPI.c.
02655 { 02656 return(dd->recomb); 02657 02658 } /* 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 2084 of file cuddAPI.c.
02086 { 02087 return(dd->reordCycle); 02088 02089 } /* 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 1692 of file cuddAPI.c.
01694 { 01695 return(dd->reorderings); 01696 01697 } /* 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 1714 of file cuddAPI.c.
01716 { 01717 return(dd->reordTime); 01718 01719 } /* 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 1934 of file cuddAPI.c.
01936 { 01937 return(dd->siftMaxSwap); 01938 01939 } /* 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 1887 of file cuddAPI.c.
01889 { 01890 return(dd->siftMaxVar); 01891 01892 } /* 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 1437 of file cuddAPI.c.
01439 { 01440 return(dd->size); 01441 01442 } /* 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 1476 of file cuddAPI.c.
01478 { 01479 return(dd->slots); 01480 01481 } /* 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 3694 of file cuddAPI.c.
03696 { 03697 return(dd->err); 03698 03699 } /* 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 3651 of file cuddAPI.c.
03653 { 03654 return(dd->out); 03655 03656 } /* 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 2706 of file cuddAPI.c.
02708 { 02709 return(dd->symmviolation); 02710 02711 } /* 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 2128 of file cuddAPI.c.
02130 { 02131 return(dd->tree); 02132 02133 } /* 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 1499 of file cuddAPI.c.
01501 { 01502 unsigned long used = 0; 01503 int i, j; 01504 int size = dd->size; 01505 DdNodePtr *nodelist; 01506 DdSubtable *subtable; 01507 DdNode *node; 01508 DdNode *sentinel = &(dd->sentinel); 01509 01510 /* Scan each BDD/ADD subtable. */ 01511 for (i = 0; i < size; i++) { 01512 subtable = &(dd->subtables[i]); 01513 nodelist = subtable->nodelist; 01514 for (j = 0; (unsigned) j < subtable->slots; j++) { 01515 node = nodelist[j]; 01516 if (node != sentinel) { 01517 used++; 01518 } 01519 } 01520 } 01521 01522 /* Scan the ZDD subtables. */ 01523 size = dd->sizeZ; 01524 01525 for (i = 0; i < size; i++) { 01526 subtable = &(dd->subtableZ[i]); 01527 nodelist = subtable->nodelist; 01528 for (j = 0; (unsigned) j < subtable->slots; j++) { 01529 node = nodelist[j]; 01530 if (node != NULL) { 01531 used++; 01532 } 01533 } 01534 } 01535 01536 /* Constant table. */ 01537 subtable = &(dd->constants); 01538 nodelist = subtable->nodelist; 01539 for (j = 0; (unsigned) j < subtable->slots; j++) { 01540 node = nodelist[j]; 01541 if (node != NULL) { 01542 used++; 01543 } 01544 } 01545 01546 return((double)used / (double) dd->slots); 01547 01548 } /* 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 1457 of file cuddAPI.c.
01459 { 01460 return(dd->sizeZ); 01461 01462 } /* 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 2200 of file cuddAPI.c.
02202 { 02203 return(dd->treeZ); 02204 02205 } /* 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 1032 of file cuddAPI.c.
01034 { 01035 return(DD_ZERO(dd)); 01036 01037 } /* end of Cudd_ReadZero */
| int Cudd_RemoveHook | ( | DdManager * | dd, | |
| DD_HFP | f, | |||
| Cudd_HookType | where | |||
| ) |
Function********************************************************************
Synopsis [Removes a function from a hook.]
Description [Removes a function from a hook. A hook is a list of application-provided functions called on certain occasions by the package. Returns 1 if successful; 0 the function was not in the list.]
SideEffects [None]
SeeAlso [Cudd_AddHook]
Definition at line 3303 of file cuddAPI.c.
03307 { 03308 DdHook **hook, *nextHook; 03309 03310 switch (where) { 03311 case CUDD_PRE_GC_HOOK: 03312 hook = &(dd->preGCHook); 03313 break; 03314 case CUDD_POST_GC_HOOK: 03315 hook = &(dd->postGCHook); 03316 break; 03317 case CUDD_PRE_REORDERING_HOOK: 03318 hook = &(dd->preReorderingHook); 03319 break; 03320 case CUDD_POST_REORDERING_HOOK: 03321 hook = &(dd->postReorderingHook); 03322 break; 03323 default: 03324 return(0); 03325 } 03326 nextHook = *hook; 03327 while (nextHook != NULL) { 03328 if (nextHook->f == f) { 03329 *hook = nextHook->next; 03330 FREE(nextHook); 03331 return(1); 03332 } 03333 hook = &(nextHook->next); 03334 nextHook = nextHook->next; 03335 } 03336 03337 return(0); 03338 03339 } /* 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 3588 of file cuddAPI.c.
03590 { 03591 return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)); 03592 03593 } /* 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 731 of file cuddAPI.c.
00734 { 00735 *method = unique->autoMethod; 00736 return(unique->autoDyn); 00737 00738 } /* 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 808 of file cuddAPI.c.
00811 { 00812 *method = unique->autoMethodZ; 00813 return(unique->autoDynZ); 00814 00815 } /* 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 2786 of file cuddAPI.c.
02789 { 02790 dd->arcviolation = arcviolation; 02791 02792 } /* 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 1127 of file cuddAPI.c.
01130 { 01131 dd->background = bck; 01132 01133 } /* 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 2447 of file cuddAPI.c.
02450 { 02451 dd->epsilon = ep; 02452 02453 } /* 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 2492 of file cuddAPI.c.
02495 { 02496 dd->groupcheck = gc; 02497 02498 } /* 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 1341 of file cuddAPI.c.
01344 { 01345 if (lut == 0) { 01346 unsigned long datalimit = getSoftDataLimit(); 01347 lut = (unsigned int) (datalimit / (sizeof(DdNode) * 01348 DD_MAX_LOOSE_FRACTION)); 01349 } 01350 dd->looseUpTo = lut; 01351 01352 } /* 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 1411 of file cuddAPI.c.
01414 { 01415 if (mc == 0) { 01416 unsigned long datalimit = getSoftDataLimit(); 01417 mc = (unsigned int) (datalimit / (sizeof(DdCache) * 01418 DD_MAX_CACHE_FRACTION)); 01419 } 01420 dd->maxCacheHard = mc; 01421 01422 } /* 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 2009 of file cuddAPI.c.
02012 { 02013 dd->maxGrowth = mg; 02014 02015 } /* 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 2060 of file cuddAPI.c.
02063 { 02064 dd->maxGrowthAlt = mg; 02065 02066 } /* 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 3830 of file cuddAPI.c.
03833 { 03834 dd->maxLive = maxLive; 03835 03836 } /* end of Cudd_SetMaxLive */
| void Cudd_SetMaxMemory | ( | DdManager * | dd, | |
| unsigned long | maxMemory | |||
| ) |
Function********************************************************************
Synopsis [Sets the maximum allowed memory.]
Description [Sets the maximum allowed memory. When this number is exceeded, the package returns NULL.]
SideEffects [none]
SeeAlso [Cudd_ReadMaxMemory]
Definition at line 3873 of file cuddAPI.c.
03876 { 03877 dd->maxmemhard = maxMemory; 03878 03879 } /* 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 1294 of file cuddAPI.c.
01297 { 01298 /* Internally, the package manipulates the ratio of hits to 01299 ** misses instead of the ratio of hits to accesses. */ 01300 dd->minHit = (double) hr / (100.0 - (double) hr); 01301 01302 } /* 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 3763 of file cuddAPI.c.
03766 { 03767 dd->nextDyn = next; 03768 03769 } /* 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 2892 of file cuddAPI.c.
02895 { 02896 dd->numberXovers = numberXovers; 02897 02898 } /* 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 2839 of file cuddAPI.c.
02842 { 02843 dd->populationSize = populationSize; 02844 02845 } /* 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 2678 of file cuddAPI.c.
02681 { 02682 dd->recomb = recomb; 02683 02684 } /* 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 2107 of file cuddAPI.c.
02110 { 02111 dd->reordCycle = cycle; 02112 02113 } /* 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 1958 of file cuddAPI.c.
01961 { 01962 dd->siftMaxSwap = sms; 01963 01964 } /* 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 1909 of file cuddAPI.c.
01912 { 01913 dd->siftMaxVar = smv; 01914 01915 } /* 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 3714 of file cuddAPI.c.
03717 { 03718 dd->err = fp; 03719 03720 } /* 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 3671 of file cuddAPI.c.
03674 { 03675 dd->out = fp; 03676 03677 } /* 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 2733 of file cuddAPI.c.
02736 { 02737 dd->symmviolation = symmviolation; 02738 02739 } /* 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 2148 of file cuddAPI.c.
02151 { 02152 if (dd->tree != NULL) { 02153 Mtr_FreeTree(dd->tree); 02154 } 02155 dd->tree = tree; 02156 if (tree == NULL) return; 02157 02158 fixVarTree(tree, dd->perm, dd->size); 02159 return; 02160 02161 } /* 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 2220 of file cuddAPI.c.
02223 { 02224 if (dd->treeZ != NULL) { 02225 Mtr_FreeTree(dd->treeZ); 02226 } 02227 dd->treeZ = tree; 02228 if (tree == NULL) return; 02229 02230 fixVarTree(tree, dd->permZ, dd->sizeZ); 02231 return; 02232 02233 } /* end of Cudd_SetZddTree */
| int Cudd_StdPostReordHook | ( | DdManager * | dd, | |
| const char * | str, | |||
| void * | data | |||
| ) |
Function********************************************************************
Synopsis [Sample hook function to call after reordering.]
Description [Sample hook function to call after reordering. Prints on the manager's stdout final size and reordering time. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_StdPreReordHook]
Definition at line 3498 of file cuddAPI.c.
03502 { 03503 long initialTime = (long) data; 03504 int retval; 03505 long finalTime = util_cpu_time(); 03506 double totalTimeSec = (double)(finalTime - initialTime) / 1000.0; 03507 03508 retval = fprintf(dd->out,"%ld nodes in %g sec\n", strcmp(str, "BDD") == 0 ? 03509 Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd), 03510 totalTimeSec); 03511 if (retval == EOF) return(0); 03512 retval = fflush(dd->out); 03513 if (retval == EOF) return(0); 03514 return(1); 03515 03516 } /* end of Cudd_StdPostReordHook */
| int Cudd_StdPreReordHook | ( | DdManager * | dd, | |
| const char * | str, | |||
| void * | data | |||
| ) |
Function********************************************************************
Synopsis [Sample hook function to call before reordering.]
Description [Sample hook function to call before reordering. Prints on the manager's stdout reordering method and initial size. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_StdPostReordHook]
Definition at line 3405 of file cuddAPI.c.
03409 { 03410 Cudd_ReorderingType method = (Cudd_ReorderingType) (ptruint) data; 03411 int retval; 03412 03413 retval = fprintf(dd->out,"%s reordering with ", str); 03414 if (retval == EOF) return(0); 03415 switch (method) { 03416 case CUDD_REORDER_SIFT_CONVERGE: 03417 case CUDD_REORDER_SYMM_SIFT_CONV: 03418 case CUDD_REORDER_GROUP_SIFT_CONV: 03419 case CUDD_REORDER_WINDOW2_CONV: 03420 case CUDD_REORDER_WINDOW3_CONV: 03421 case CUDD_REORDER_WINDOW4_CONV: 03422 case CUDD_REORDER_LINEAR_CONVERGE: 03423 retval = fprintf(dd->out,"converging "); 03424 if (retval == EOF) return(0); 03425 break; 03426 default: 03427 break; 03428 } 03429 switch (method) { 03430 case CUDD_REORDER_RANDOM: 03431 case CUDD_REORDER_RANDOM_PIVOT: 03432 retval = fprintf(dd->out,"random"); 03433 break; 03434 case CUDD_REORDER_SIFT: 03435 case CUDD_REORDER_SIFT_CONVERGE: 03436 retval = fprintf(dd->out,"sifting"); 03437 break; 03438 case CUDD_REORDER_SYMM_SIFT: 03439 case CUDD_REORDER_SYMM_SIFT_CONV: 03440 retval = fprintf(dd->out,"symmetric sifting"); 03441 break; 03442 case CUDD_REORDER_LAZY_SIFT: 03443 retval = fprintf(dd->out,"lazy sifting"); 03444 break; 03445 case CUDD_REORDER_GROUP_SIFT: 03446 case CUDD_REORDER_GROUP_SIFT_CONV: 03447 retval = fprintf(dd->out,"group sifting"); 03448 break; 03449 case CUDD_REORDER_WINDOW2: 03450 case CUDD_REORDER_WINDOW3: 03451 case CUDD_REORDER_WINDOW4: 03452 case CUDD_REORDER_WINDOW2_CONV: 03453 case CUDD_REORDER_WINDOW3_CONV: 03454 case CUDD_REORDER_WINDOW4_CONV: 03455 retval = fprintf(dd->out,"window"); 03456 break; 03457 case CUDD_REORDER_ANNEALING: 03458 retval = fprintf(dd->out,"annealing"); 03459 break; 03460 case CUDD_REORDER_GENETIC: 03461 retval = fprintf(dd->out,"genetic"); 03462 break; 03463 case CUDD_REORDER_LINEAR: 03464 case CUDD_REORDER_LINEAR_CONVERGE: 03465 retval = fprintf(dd->out,"linear sifting"); 03466 break; 03467 case CUDD_REORDER_EXACT: 03468 retval = fprintf(dd->out,"exact"); 03469 break; 03470 default: 03471 return(0); 03472 } 03473 if (retval == EOF) return(0); 03474 03475 retval = fprintf(dd->out,": from %ld to ... ", strcmp(str, "BDD") == 0 ? 03476 Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd)); 03477 if (retval == EOF) return(0); 03478 fflush(dd->out); 03479 return(1); 03480 03481 } /* 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 2629 of file cuddAPI.c.
02631 { 02632 dd->countDead = ~0; 02633 02634 } /* 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 2604 of file cuddAPI.c.
02606 { 02607 dd->countDead = 0; 02608 02609 } /* 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 444 of file cuddAPI.c.
00447 { 00448 DdNode *res; 00449 DdNode *zvar; 00450 DdNode *lower; 00451 int j; 00452 00453 if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL); 00454 00455 /* The i-th variable function has the following structure: 00456 ** at the level corresponding to index i there is a node whose "then" 00457 ** child points to the universe, and whose "else" child points to zero. 00458 ** Above that level there are nodes with identical children. 00459 */ 00460 00461 /* First we build the node at the level of index i. */ 00462 lower = (i < dd->sizeZ - 1) ? dd->univ[dd->permZ[i]+1] : DD_ONE(dd); 00463 do { 00464 dd->reordered = 0; 00465 zvar = cuddUniqueInterZdd(dd, i, lower, DD_ZERO(dd)); 00466 } while (dd->reordered == 1); 00467 00468 if (zvar == NULL) 00469 return(NULL); 00470 cuddRef(zvar); 00471 00472 /* Now we add the "filler" nodes above the level of index i. */ 00473 for (j = dd->permZ[i] - 1; j >= 0; j--) { 00474 do { 00475 dd->reordered = 0; 00476 res = cuddUniqueInterZdd(dd, dd->invpermZ[j], zvar, zvar); 00477 } while (dd->reordered == 1); 00478 if (res == NULL) { 00479 Cudd_RecursiveDerefZdd(dd,zvar); 00480 return(NULL); 00481 } 00482 cuddRef(res); 00483 Cudd_RecursiveDerefZdd(dd,zvar); 00484 zvar = res; 00485 } 00486 cuddDeref(zvar); 00487 return(zvar); 00488 00489 } /* 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 885 of file cuddAPI.c.
00887 { 00888 unique->realign = 0; 00889 return; 00890 00891 } /* 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 863 of file cuddAPI.c.
00865 { 00866 unique->realign = 1; 00867 return; 00868 00869 } /* 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 833 of file cuddAPI.c.
00835 { 00836 return(unique->realign); 00837 00838 } /* 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 515 of file cuddAPI.c.
00518 { 00519 int res; 00520 int i, j; 00521 int allnew; 00522 int *permutation; 00523 00524 if (multiplicity < 1) return(0); 00525 allnew = dd->sizeZ == 0; 00526 if (dd->size * multiplicity > dd->sizeZ) { 00527 res = cuddResizeTableZdd(dd,dd->size * multiplicity - 1); 00528 if (res == 0) return(0); 00529 } 00530 /* Impose the order of the BDD variables to the ZDD variables. */ 00531 if (allnew) { 00532 for (i = 0; i < dd->size; i++) { 00533 for (j = 0; j < multiplicity; j++) { 00534 dd->permZ[i * multiplicity + j] = 00535 dd->perm[i] * multiplicity + j; 00536 dd->invpermZ[dd->permZ[i * multiplicity + j]] = 00537 i * multiplicity + j; 00538 } 00539 } 00540 for (i = 0; i < dd->sizeZ; i++) { 00541 dd->univ[i]->index = dd->invpermZ[i]; 00542 } 00543 } else { 00544 permutation = ALLOC(int,dd->sizeZ); 00545 if (permutation == NULL) { 00546 dd->errorCode = CUDD_MEMORY_OUT; 00547 return(0); 00548 } 00549 for (i = 0; i < dd->size; i++) { 00550 for (j = 0; j < multiplicity; j++) { 00551 permutation[i * multiplicity + j] = 00552 dd->invperm[i] * multiplicity + j; 00553 } 00554 } 00555 for (i = dd->size * multiplicity; i < dd->sizeZ; i++) { 00556 permutation[i] = i; 00557 } 00558 res = Cudd_zddShuffleHeap(dd, permutation); 00559 FREE(permutation); 00560 if (res == 0) return(0); 00561 } 00562 /* Copy and expand the variable group tree if it exists. */ 00563 if (dd->treeZ != NULL) { 00564 Cudd_FreeZddTree(dd); 00565 } 00566 if (dd->tree != NULL) { 00567 dd->treeZ = Mtr_CopyTree(dd->tree, multiplicity); 00568 if (dd->treeZ == NULL) return(0); 00569 } else if (multiplicity > 1) { 00570 dd->treeZ = Mtr_InitGroupTree(0, dd->sizeZ); 00571 if (dd->treeZ == NULL) return(0); 00572 dd->treeZ->index = dd->invpermZ[0]; 00573 } 00574 /* Create groups for the ZDD variables derived from the same BDD variable. 00575 */ 00576 if (multiplicity > 1) { 00577 char *vmask, *lmask; 00578 00579 vmask = ALLOC(char, dd->size); 00580 if (vmask == NULL) { 00581 dd->errorCode = CUDD_MEMORY_OUT; 00582 return(0); 00583 } 00584 lmask = ALLOC(char, dd->size); 00585 if (lmask == NULL) { 00586 dd->errorCode = CUDD_MEMORY_OUT; 00587 return(0); 00588 } 00589 for (i = 0; i < dd->size; i++) { 00590 vmask[i] = lmask[i] = 0; 00591 } 00592 res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask); 00593 FREE(vmask); 00594 FREE(lmask); 00595 if (res == 0) return(0); 00596 } 00597 return(1); 00598 00599 } /* end of Cudd_zddVarsFromBddVars */
| static void fixVarTree | ( | MtrNode * | treenode, | |
| int * | perm, | |||
| int | size | |||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Fixes a variable group tree.]
Description []
SideEffects [Changes the variable group tree.]
SeeAlso []
Definition at line 4356 of file cuddAPI.c.
04360 { 04361 treenode->index = treenode->low; 04362 treenode->low = ((int) treenode->index < size) ? 04363 perm[treenode->index] : treenode->index; 04364 if (treenode->child != NULL) 04365 fixVarTree(treenode->child, perm, size); 04366 if (treenode->younger != NULL) 04367 fixVarTree(treenode->younger, perm, size); 04368 return; 04369 04370 } /* end of fixVarTree */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddAPI.c,v 1.59 2009/02/19 16:14:14 fabio Exp $" [static] |
CFile***********************************************************************
FileName [cuddAPI.c]
PackageName [cudd]
Synopsis [Application interface functions.]
Description [External procedures included in this module:
- 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 [Copyright (c) 1995-2004, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
