abc70930: src/bdd/cudd/cuddAPI.c Source File

00001 
00167 #include    "util_hack.h"
00168 #include    "cuddInt.h"
00169 
00170 /*---------------------------------------------------------------------------*/
00171 /* Constant declarations                                                     */
00172 /*---------------------------------------------------------------------------*/
00173 
00174 /*---------------------------------------------------------------------------*/
00175 /* Stucture declarations                                                     */
00176 /*---------------------------------------------------------------------------*/
00177 
00178 /*---------------------------------------------------------------------------*/
00179 /* Type declarations                                                         */
00180 /*---------------------------------------------------------------------------*/
00181 
00182 /*---------------------------------------------------------------------------*/
00183 /* Variable declarations                                                     */
00184 /*---------------------------------------------------------------------------*/
00185 
00186 #ifndef lint
00187 static char rcsid[] DD_UNUSED = "$Id: cuddAPI.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
00188 #endif
00189 
00190 /*---------------------------------------------------------------------------*/
00191 /* Macro declarations                                                        */
00192 /*---------------------------------------------------------------------------*/
00193 
00196 /*---------------------------------------------------------------------------*/
00197 /* Static function prototypes                                                */
00198 /*---------------------------------------------------------------------------*/
00199 
00200 static void fixVarTree ARGS((MtrNode *treenode, int *perm, int size));
00201 static int addMultiplicityGroups ARGS((DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask));
00202 
00206 /*---------------------------------------------------------------------------*/
00207 /* Definition of exported functions                                          */
00208 /*---------------------------------------------------------------------------*/
00209 
00210 
00227 DdNode *
00228 Cudd_addNewVar(
00229   DdManager * dd)
00230 {
00231     DdNode *res;
00232 
00233     if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
00234     do {
00235         dd->reordered = 0;
00236         res = cuddUniqueInter(dd,dd->size,DD_ONE(dd),DD_ZERO(dd));
00237     } while (dd->reordered == 1);
00238 
00239     return(res);
00240 
00241 } /* end of Cudd_addNewVar */
00242 
00243 
00258 DdNode *
00259 Cudd_addNewVarAtLevel(
00260   DdManager * dd,
00261   int  level)
00262 {
00263     DdNode *res;
00264 
00265     if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
00266     if (level >= dd->size) return(Cudd_addIthVar(dd,level));
00267     if (!cuddInsertSubtables(dd,1,level)) return(NULL);
00268     do {
00269         dd->reordered = 0;
00270         res = cuddUniqueInter(dd,dd->size - 1,DD_ONE(dd),DD_ZERO(dd));
00271     } while (dd->reordered == 1);
00272 
00273     return(res);
00274 
00275 } /* end of Cudd_addNewVarAtLevel */
00276 
00277 
00291 DdNode *
00292 Cudd_bddNewVar(
00293   DdManager * dd)
00294 {
00295     DdNode *res;
00296 
00297     if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
00298     res = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));
00299 
00300     return(res);
00301 
00302 } /* end of Cudd_bddNewVar */
00303 
00304 
00319 DdNode *
00320 Cudd_bddNewVarAtLevel(
00321   DdManager * dd,
00322   int  level)
00323 {
00324     DdNode *res;
00325 
00326     if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
00327     if (level >= dd->size) return(Cudd_bddIthVar(dd,level));
00328     if (!cuddInsertSubtables(dd,1,level)) return(NULL);
00329     res = dd->vars[dd->size - 1];
00330 
00331     return(res);
00332 
00333 } /* end of Cudd_bddNewVarAtLevel */
00334 
00335 
00352 DdNode *
00353 Cudd_addIthVar(
00354   DdManager * dd,
00355   int  i)
00356 {
00357     DdNode *res;
00358 
00359     if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
00360     do {
00361         dd->reordered = 0;
00362         res = cuddUniqueInter(dd,i,DD_ONE(dd),DD_ZERO(dd));
00363     } while (dd->reordered == 1);
00364 
00365     return(res);
00366 
00367 } /* end of Cudd_addIthVar */
00368 
00369 
00384 DdNode *
00385 Cudd_bddIthVar(
00386   DdManager * dd,
00387   int  i)
00388 {
00389     DdNode *res;
00390 
00391     if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
00392     if (i < dd->size) {
00393         res = dd->vars[i];
00394     } else {
00395         res = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
00396     }
00397 
00398     return(res);
00399 
00400 } /* end of Cudd_bddIthVar */
00401 
00402 
00416 DdNode *
00417 Cudd_zddIthVar(
00418   DdManager * dd,
00419   int  i)
00420 {
00421     DdNode *res;
00422     DdNode *zvar;
00423     DdNode *lower;
00424     int j;
00425 
00426     if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
00427 
00428     /* The i-th variable function has the following structure:
00429     ** at the level corresponding to index i there is a node whose "then"
00430     ** child points to the universe, and whose "else" child points to zero.
00431     ** Above that level there are nodes with identical children.
00432     */
00433 
00434     /* First we build the node at the level of index i. */
00435     lower = (i < dd->sizeZ - 1) ? dd->univ[dd->permZ[i]+1] : DD_ONE(dd);
00436     do {
00437         dd->reordered = 0;
00438         zvar = cuddUniqueInterZdd(dd, i, lower, DD_ZERO(dd));
00439     } while (dd->reordered == 1);
00440 
00441     if (zvar == NULL)
00442         return(NULL);
00443     cuddRef(zvar);
00444 
00445     /* Now we add the "filler" nodes above the level of index i. */
00446     for (j = dd->permZ[i] - 1; j >= 0; j--) {
00447         do {
00448             dd->reordered = 0;
00449             res = cuddUniqueInterZdd(dd, dd->invpermZ[j], zvar, zvar);
00450         } while (dd->reordered == 1);
00451         if (res == NULL) {
00452             Cudd_RecursiveDerefZdd(dd,zvar);
00453             return(NULL);
00454         }
00455         cuddRef(res);
00456         Cudd_RecursiveDerefZdd(dd,zvar);
00457         zvar = res;
00458     }
00459     cuddDeref(zvar);
00460     return(zvar);
00461 
00462 } /* end of Cudd_zddIthVar */
00463 
00464 
00487 int
00488 Cudd_zddVarsFromBddVars(
00489   DdManager * dd /* DD manager */,
00490   int multiplicity /* how many ZDD variables are created for each BDD variable */)
00491 {
00492     int res;
00493     int i, j;
00494     int allnew;
00495     int *permutation;
00496 
00497     if (multiplicity < 1) return(0);
00498     allnew = dd->sizeZ == 0;
00499     if (dd->size * multiplicity > dd->sizeZ) {
00500         res = cuddResizeTableZdd(dd,dd->size * multiplicity - 1);
00501         if (res == 0) return(0);
00502     }
00503     /* Impose the order of the BDD variables to the ZDD variables. */
00504     if (allnew) {
00505         for (i = 0; i < dd->size; i++) {
00506             for (j = 0; j < multiplicity; j++) {
00507                 dd->permZ[i * multiplicity + j] =
00508                     dd->perm[i] * multiplicity + j;
00509                 dd->invpermZ[dd->permZ[i * multiplicity + j]] =
00510                     i * multiplicity + j;
00511             }
00512         }
00513         for (i = 0; i < dd->sizeZ; i++) {
00514             dd->univ[i]->index = dd->invpermZ[i];
00515         }
00516     } else {
00517         permutation = ALLOC(int,dd->sizeZ);
00518         if (permutation == NULL) {
00519             dd->errorCode = CUDD_MEMORY_OUT;
00520             return(0);
00521         }
00522         for (i = 0; i < dd->size; i++) {
00523             for (j = 0; j < multiplicity; j++) {
00524                 permutation[i * multiplicity + j] =
00525                     dd->invperm[i] * multiplicity + j;
00526             }
00527         }
00528         for (i = dd->size * multiplicity; i < dd->sizeZ; i++) {
00529             permutation[i] = i;
00530         }
00531         res = Cudd_zddShuffleHeap(dd, permutation);
00532         FREE(permutation);
00533         if (res == 0) return(0);
00534     }
00535     /* Copy and expand the variable group tree if it exists. */
00536     if (dd->treeZ != NULL) {
00537         Cudd_FreeZddTree(dd);
00538     }
00539     if (dd->tree != NULL) {
00540         dd->treeZ = Mtr_CopyTree(dd->tree, multiplicity);
00541         if (dd->treeZ == NULL) return(0);
00542     } else if (multiplicity > 1) {
00543         dd->treeZ = Mtr_InitGroupTree(0, dd->sizeZ);
00544         if (dd->treeZ == NULL) return(0);
00545         dd->treeZ->index = dd->invpermZ[0];
00546     }
00547     /* Create groups for the ZDD variables derived from the same BDD variable.
00548     */
00549     if (multiplicity > 1) {
00550         char *vmask, *lmask;
00551 
00552         vmask = ALLOC(char, dd->size);
00553         if (vmask == NULL) {
00554             dd->errorCode = CUDD_MEMORY_OUT;
00555             return(0);
00556         }
00557         lmask =  ALLOC(char, dd->size);
00558         if (lmask == NULL) {
00559             dd->errorCode = CUDD_MEMORY_OUT;
00560             return(0);
00561         }
00562         for (i = 0; i < dd->size; i++) {
00563             vmask[i] = lmask[i] = 0;
00564         }
00565         res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask);
00566         FREE(vmask);
00567         FREE(lmask);
00568         if (res == 0) return(0);
00569     }
00570     return(1);
00571 
00572 } /* end of Cudd_zddVarsFromBddVars */
00573 
00574 
00588 DdNode *
00589 Cudd_addConst(
00590   DdManager * dd,
00591   CUDD_VALUE_TYPE  c)
00592 {
00593     return(cuddUniqueConst(dd,c));
00594 
00595 } /* end of Cudd_addConst */
00596 
00597 
00613 int
00614 Cudd_IsNonConstant(
00615   DdNode *f)
00616 {
00617     return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f));
00618 
00619 } /* end of Cudd_IsNonConstant */
00620 
00621 
00637 void
00638 Cudd_AutodynEnable(
00639   DdManager * unique,
00640   Cudd_ReorderingType  method)
00641 {
00642     unique->autoDyn = 1;
00643     if (method != CUDD_REORDER_SAME) {
00644         unique->autoMethod = method;
00645     }
00646 #ifndef DD_NO_DEATH_ROW
00647     /* If reordering is enabled, using the death row causes too many
00648     ** invocations. Hence, we shrink the death row to just one entry.
00649     */
00650     cuddClearDeathRow(unique);
00651     unique->deathRowDepth = 1;
00652     unique->deadMask = unique->deathRowDepth - 1;
00653     if ((unsigned) unique->nextDead > unique->deadMask) {
00654         unique->nextDead = 0;
00655     }
00656     unique->deathRow = REALLOC(DdNodePtr, unique->deathRow,
00657         unique->deathRowDepth);
00658 #endif
00659     return;
00660 
00661 } /* end of Cudd_AutodynEnable */
00662 
00663 
00676 void
00677 Cudd_AutodynDisable(
00678   DdManager * unique)
00679 {
00680     unique->autoDyn = 0;
00681     return;
00682 
00683 } /* end of Cudd_AutodynDisable */
00684 
00685 
00703 int
00704 Cudd_ReorderingStatus(
00705   DdManager * unique,
00706   Cudd_ReorderingType * method)
00707 {
00708     *method = unique->autoMethod;
00709     return(unique->autoDyn);
00710 
00711 } /* end of Cudd_ReorderingStatus */
00712 
00713 
00728 void
00729 Cudd_AutodynEnableZdd(
00730   DdManager * unique,
00731   Cudd_ReorderingType method)
00732 {
00733     unique->autoDynZ = 1;
00734     if (method != CUDD_REORDER_SAME) {
00735         unique->autoMethodZ = method;
00736     }
00737     return;
00738 
00739 } /* end of Cudd_AutodynEnableZdd */
00740 
00741 
00754 void
00755 Cudd_AutodynDisableZdd(
00756   DdManager * unique)
00757 {
00758     unique->autoDynZ = 0;
00759     return;
00760 
00761 } /* end of Cudd_AutodynDisableZdd */
00762 
00763 
00780 int
00781 Cudd_ReorderingStatusZdd(
00782   DdManager * unique,
00783   Cudd_ReorderingType * method)
00784 {
00785     *method = unique->autoMethodZ;
00786     return(unique->autoDynZ);
00787 
00788 } /* end of Cudd_ReorderingStatusZdd */
00789 
00790 
00805 int
00806 Cudd_zddRealignmentEnabled(
00807   DdManager * unique)
00808 {
00809     return(unique->realign);
00810 
00811 } /* end of Cudd_zddRealignmentEnabled */
00812 
00813 
00835 void
00836 Cudd_zddRealignEnable(
00837   DdManager * unique)
00838 {
00839     unique->realign = 1;
00840     return;
00841 
00842 } /* end of Cudd_zddRealignEnable */
00843 
00844 
00857 void
00858 Cudd_zddRealignDisable(
00859   DdManager * unique)
00860 {
00861     unique->realign = 0;
00862     return;
00863 
00864 } /* end of Cudd_zddRealignDisable */
00865 
00866 
00881 int
00882 Cudd_bddRealignmentEnabled(
00883   DdManager * unique)
00884 {
00885     return(unique->realignZ);
00886 
00887 } /* end of Cudd_bddRealignmentEnabled */
00888 
00889 
00911 void
00912 Cudd_bddRealignEnable(
00913   DdManager * unique)
00914 {
00915     unique->realignZ = 1;
00916     return;
00917 
00918 } /* end of Cudd_bddRealignEnable */
00919 
00920 
00933 void
00934 Cudd_bddRealignDisable(
00935   DdManager * unique)
00936 {
00937     unique->realignZ = 0;
00938     return;
00939 
00940 } /* end of Cudd_bddRealignDisable */
00941 
00942 
00955 DdNode *
00956 Cudd_ReadOne(
00957   DdManager * dd)
00958 {
00959     return(dd->one);
00960 
00961 } /* end of Cudd_ReadOne */
00962 
00963 
00978 DdNode *
00979 Cudd_ReadZddOne(
00980   DdManager * dd,
00981   int  i)
00982 {
00983     if (i < 0)
00984         return(NULL);
00985     return(i < dd->sizeZ ? dd->univ[i] : DD_ONE(dd));
00986 
00987 } /* end of Cudd_ReadZddOne */
00988 
00989 
00990 
01004 DdNode *
01005 Cudd_ReadZero(
01006   DdManager * dd)
01007 {
01008     return(DD_ZERO(dd));
01009 
01010 } /* end of Cudd_ReadZero */
01011 
01012 
01026 DdNode *
01027 Cudd_ReadLogicZero(
01028   DdManager * dd)
01029 {
01030     return(Cudd_Not(DD_ONE(dd)));
01031 
01032 } /* end of Cudd_ReadLogicZero */
01033 
01034 
01044 DdNode *
01045 Cudd_ReadPlusInfinity(
01046   DdManager * dd)
01047 {
01048     return(dd->plusinfinity);
01049 
01050 } /* end of Cudd_ReadPlusInfinity */
01051 
01052 
01062 DdNode *
01063 Cudd_ReadMinusInfinity(
01064   DdManager * dd)
01065 {
01066     return(dd->minusinfinity);
01067 
01068 } /* end of Cudd_ReadMinusInfinity */
01069 
01070 
01080 DdNode *
01081 Cudd_ReadBackground(
01082   DdManager * dd)
01083 {
01084     return(dd->background);
01085 
01086 } /* end of Cudd_ReadBackground */
01087 
01088 
01099 void
01100 Cudd_SetBackground(
01101   DdManager * dd,
01102   DdNode * bck)
01103 {
01104     dd->background = bck;
01105 
01106 } /* end of Cudd_SetBackground */
01107 
01108 
01120 unsigned int
01121 Cudd_ReadCacheSlots(
01122   DdManager * dd)
01123 {
01124     return(dd->cacheSlots);
01125 
01126 } /* end of Cudd_ReadCacheSlots */
01127 
01128 
01143 double
01144 Cudd_ReadCacheUsedSlots(
01145   DdManager * dd)
01146 {
01147     unsigned long used = 0;
01148     int slots = dd->cacheSlots;
01149     DdCache *cache = dd->cache;
01150     int i;
01151 
01152     for (i = 0; i < slots; i++) {
01153         used += cache[i].h != 0;
01154     }
01155 
01156     return((double)used / (double) dd->cacheSlots);
01157 
01158 } /* end of Cudd_ReadCacheUsedSlots */
01159 
01160 
01172 double
01173 Cudd_ReadCacheLookUps(
01174   DdManager * dd)
01175 {
01176     return(dd->cacheHits + dd->cacheMisses +
01177            dd->totCachehits + dd->totCacheMisses);
01178 
01179 } /* end of Cudd_ReadCacheLookUps */
01180 
01181 
01193 double
01194 Cudd_ReadCacheHits(
01195   DdManager * dd)
01196 {
01197     return(dd->cacheHits + dd->totCachehits);
01198 
01199 } /* end of Cudd_ReadCacheHits */
01200 
01201 
01214 double
01215 Cudd_ReadRecursiveCalls(
01216   DdManager * dd)
01217 {
01218 #ifdef DD_COUNT
01219     return(dd->recursiveCalls);
01220 #else
01221     return(-1.0);
01222 #endif
01223 
01224 } /* end of Cudd_ReadRecursiveCalls */
01225 
01226 
01227 
01240 unsigned int
01241 Cudd_ReadMinHit(
01242   DdManager * dd)
01243 {
01244     /* Internally, the package manipulates the ratio of hits to
01245     ** misses instead of the ratio of hits to accesses. */
01246     return((unsigned int) (0.5 + 100 * dd->minHit / (1 + dd->minHit)));
01247 
01248 } /* end of Cudd_ReadMinHit */
01249 
01250 
01266 void
01267 Cudd_SetMinHit(
01268   DdManager * dd,
01269   unsigned int hr)
01270 {
01271     /* Internally, the package manipulates the ratio of hits to
01272     ** misses instead of the ratio of hits to accesses. */
01273     dd->minHit = (double) hr / (100.0 - (double) hr);
01274 
01275 } /* end of Cudd_SetMinHit */
01276 
01277 
01289 unsigned int
01290 Cudd_ReadLooseUpTo(
01291   DdManager * dd)
01292 {
01293     return(dd->looseUpTo);
01294 
01295 } /* end of Cudd_ReadLooseUpTo */
01296 
01297 
01313 void
01314 Cudd_SetLooseUpTo(
01315   DdManager * dd,
01316   unsigned int lut)
01317 {
01318     if (lut == 0) {
01319         long datalimit = getSoftDataLimit();
01320         lut = (unsigned int) (datalimit / (sizeof(DdNode) *
01321                                            DD_MAX_LOOSE_FRACTION));
01322     }
01323     dd->looseUpTo = lut;
01324 
01325 } /* end of Cudd_SetLooseUpTo */
01326 
01327 
01339 unsigned int
01340 Cudd_ReadMaxCache(
01341   DdManager * dd)
01342 {
01343     return(2 * dd->cacheSlots + dd->cacheSlack);
01344 
01345 } /* end of Cudd_ReadMaxCache */
01346 
01347 
01359 unsigned int
01360 Cudd_ReadMaxCacheHard(
01361   DdManager * dd)
01362 {
01363     return(dd->maxCacheHard);
01364 
01365 } /* end of Cudd_ReadMaxCache */
01366 
01367 
01383 void
01384 Cudd_SetMaxCacheHard(
01385   DdManager * dd,
01386   unsigned int mc)
01387 {
01388     if (mc == 0) {
01389         long datalimit = getSoftDataLimit();
01390         mc = (unsigned int) (datalimit / (sizeof(DdCache) *
01391                                           DD_MAX_CACHE_FRACTION));
01392     }
01393     dd->maxCacheHard = mc;
01394 
01395 } /* end of Cudd_SetMaxCacheHard */
01396 
01397 
01409 int
01410 Cudd_ReadSize(
01411   DdManager * dd)
01412 {
01413     return(dd->size);
01414 
01415 } /* end of Cudd_ReadSize */
01416 
01417 
01429 int
01430 Cudd_ReadZddSize(
01431   DdManager * dd)
01432 {
01433     return(dd->sizeZ);
01434 
01435 } /* end of Cudd_ReadZddSize */
01436 
01437 
01448 unsigned int
01449 Cudd_ReadSlots(
01450   DdManager * dd)
01451 {
01452     return(dd->slots);
01453 
01454 } /* end of Cudd_ReadSlots */
01455 
01456 
01471 double
01472 Cudd_ReadUsedSlots(
01473   DdManager * dd)
01474 {
01475     unsigned long used = 0;
01476     int i, j;
01477     int size = dd->size;
01478     DdNodePtr *nodelist;
01479     DdSubtable *subtable;
01480     DdNode *node;
01481     DdNode *sentinel = &(dd->sentinel);
01482 
01483     /* Scan each BDD/ADD subtable. */
01484     for (i = 0; i < size; i++) {
01485         subtable = &(dd->subtables[i]);
01486         nodelist = subtable->nodelist;
01487         for (j = 0; (unsigned) j < subtable->slots; j++) {
01488             node = nodelist[j];
01489             if (node != sentinel) {
01490                 used++;
01491             }
01492         }
01493     }
01494 
01495     /* Scan the ZDD subtables. */
01496     size = dd->sizeZ;
01497 
01498     for (i = 0; i < size; i++) {
01499         subtable = &(dd->subtableZ[i]);
01500         nodelist = subtable->nodelist;
01501         for (j = 0; (unsigned) j < subtable->slots; j++) {
01502             node = nodelist[j];
01503             if (node != NULL) {
01504                 used++;
01505             }
01506         }
01507     }
01508 
01509     /* Constant table. */
01510     subtable = &(dd->constants);
01511     nodelist = subtable->nodelist;
01512     for (j = 0; (unsigned) j < subtable->slots; j++) {
01513         node = nodelist[j];
01514         if (node != NULL) {
01515             used++;
01516         }
01517     }
01518 
01519     return((double)used / (double) dd->slots);
01520 
01521 } /* end of Cudd_ReadUsedSlots */
01522 
01523 
01540 double
01541 Cudd_ExpectedUsedSlots(
01542   DdManager * dd)
01543 {
01544     int i;
01545     int size = dd->size;
01546     DdSubtable *subtable;
01547     double empty = 0.0;
01548 
01549     /* To each subtable we apply the corollary to Theorem 8.5 (occupancy
01550     ** distribution) from Sedgewick and Flajolet's Analysis of Algorithms.
01551     ** The corollary says that for a a table with M buckets and a load ratio
01552     ** of r, the expected number of empty buckets is asymptotically given
01553     ** by M * exp(-r).
01554     */
01555 
01556     /* Scan each BDD/ADD subtable. */
01557     for (i = 0; i < size; i++) {
01558         subtable = &(dd->subtables[i]);
01559         empty += (double) subtable->slots *
01560             exp(-(double) subtable->keys / (double) subtable->slots);
01561     }
01562 
01563     /* Scan the ZDD subtables. */
01564     size = dd->sizeZ;
01565 
01566     for (i = 0; i < size; i++) {
01567         subtable = &(dd->subtableZ[i]);
01568         empty += (double) subtable->slots *
01569             exp(-(double) subtable->keys / (double) subtable->slots);
01570     }
01571 
01572     /* Constant table. */
01573     subtable = &(dd->constants);
01574     empty += (double) subtable->slots *
01575         exp(-(double) subtable->keys / (double) subtable->slots);
01576 
01577     return(1.0 - empty / (double) dd->slots);
01578 
01579 } /* end of Cudd_ExpectedUsedSlots */
01580 
01581 
01594 unsigned int
01595 Cudd_ReadKeys(
01596   DdManager * dd)
01597 {
01598     return(dd->keys);
01599 
01600 } /* end of Cudd_ReadKeys */
01601 
01602 
01614 unsigned int
01615 Cudd_ReadDead(
01616   DdManager * dd)
01617 {
01618     return(dd->dead);
01619 
01620 } /* end of Cudd_ReadDead */
01621 
01622 
01638 unsigned int
01639 Cudd_ReadMinDead(
01640   DdManager * dd)
01641 {
01642     return(dd->minDead);
01643 
01644 } /* end of Cudd_ReadMinDead */
01645 
01646 
01664 int
01665 Cudd_ReadReorderings(
01666   DdManager * dd)
01667 {
01668     return(dd->reorderings);
01669 
01670 } /* end of Cudd_ReadReorderings */
01671 
01672 
01686 long
01687 Cudd_ReadReorderingTime(
01688   DdManager * dd)
01689 {
01690     return(dd->reordTime);
01691 
01692 } /* end of Cudd_ReadReorderingTime */
01693 
01694 
01709 int
01710 Cudd_ReadGarbageCollections(
01711   DdManager * dd)
01712 {
01713     return(dd->garbageCollections);
01714 
01715 } /* end of Cudd_ReadGarbageCollections */
01716 
01717 
01730 long
01731 Cudd_ReadGarbageCollectionTime(
01732   DdManager * dd)
01733 {
01734     return(dd->GCTime);
01735 
01736 } /* end of Cudd_ReadGarbageCollectionTime */
01737 
01738 
01752 double
01753 Cudd_ReadNodesFreed(
01754   DdManager * dd)
01755 {
01756 #ifdef DD_STATS
01757     return(dd->nodesFreed);
01758 #else
01759     return(-1.0);
01760 #endif
01761 
01762 } /* end of Cudd_ReadNodesFreed */
01763 
01764 
01778 double
01779 Cudd_ReadNodesDropped(
01780   DdManager * dd)
01781 {
01782 #ifdef DD_STATS
01783     return(dd->nodesDropped);
01784 #else
01785     return(-1.0);
01786 #endif
01787 
01788 } /* end of Cudd_ReadNodesDropped */
01789 
01790 
01804 double
01805 Cudd_ReadUniqueLookUps(
01806   DdManager * dd)
01807 {
01808 #ifdef DD_UNIQUE_PROFILE
01809     return(dd->uniqueLookUps);
01810 #else
01811     return(-1.0);
01812 #endif
01813 
01814 } /* end of Cudd_ReadUniqueLookUps */
01815 
01816 
01833 double
01834 Cudd_ReadUniqueLinks(
01835   DdManager * dd)
01836 {
01837 #ifdef DD_UNIQUE_PROFILE
01838     return(dd->uniqueLinks);
01839 #else
01840     return(-1.0);
01841 #endif
01842 
01843 } /* end of Cudd_ReadUniqueLinks */
01844 
01845 
01859 int
01860 Cudd_ReadSiftMaxVar(
01861   DdManager * dd)
01862 {
01863     return(dd->siftMaxVar);
01864 
01865 } /* end of Cudd_ReadSiftMaxVar */
01866 
01867 
01881 void
01882 Cudd_SetSiftMaxVar(
01883   DdManager * dd,
01884   int  smv)
01885 {
01886     dd->siftMaxVar = smv;
01887 
01888 } /* end of Cudd_SetSiftMaxVar */
01889 
01890 
01906 int
01907 Cudd_ReadSiftMaxSwap(
01908   DdManager * dd)
01909 {
01910     return(dd->siftMaxSwap);
01911 
01912 } /* end of Cudd_ReadSiftMaxSwap */
01913 
01914 
01930 void
01931 Cudd_SetSiftMaxSwap(
01932   DdManager * dd,
01933   int  sms)
01934 {
01935     dd->siftMaxSwap = sms;
01936 
01937 } /* end of Cudd_SetSiftMaxSwap */
01938 
01939 
01956 double
01957 Cudd_ReadMaxGrowth(
01958   DdManager * dd)
01959 {
01960     return(dd->maxGrowth);
01961 
01962 } /* end of Cudd_ReadMaxGrowth */
01963 
01964 
01981 void
01982 Cudd_SetMaxGrowth(
01983   DdManager * dd,
01984   double mg)
01985 {
01986     dd->maxGrowth = mg;
01987 
01988 } /* end of Cudd_SetMaxGrowth */
01989 
01990 
02007 double
02008 Cudd_ReadMaxGrowthAlternate(
02009   DdManager * dd)
02010 {
02011     return(dd->maxGrowthAlt);
02012 
02013 } /* end of Cudd_ReadMaxGrowthAlternate */
02014 
02015 
02032 void
02033 Cudd_SetMaxGrowthAlternate(
02034   DdManager * dd,
02035   double mg)
02036 {
02037     dd->maxGrowthAlt = mg;
02038 
02039 } /* end of Cudd_SetMaxGrowthAlternate */
02040 
02041 
02056 int
02057 Cudd_ReadReorderingCycle(
02058   DdManager * dd)
02059 {
02060     return(dd->reordCycle);
02061 
02062 } /* end of Cudd_ReadReorderingCycle */
02063 
02064 
02079 void
02080 Cudd_SetReorderingCycle(
02081   DdManager * dd,
02082   int cycle)
02083 {
02084     dd->reordCycle = cycle;
02085 
02086 } /* end of Cudd_SetReorderingCycle */
02087 
02088 
02100 MtrNode *
02101 Cudd_ReadTree(
02102   DdManager * dd)
02103 {
02104     return(dd->tree);
02105 
02106 } /* end of Cudd_ReadTree */
02107 
02108 
02120 void
02121 Cudd_SetTree(
02122   DdManager * dd,
02123   MtrNode * tree)
02124 {
02125     if (dd->tree != NULL) {
02126         Mtr_FreeTree(dd->tree);
02127     }
02128     dd->tree = tree;
02129     if (tree == NULL) return;
02130 
02131     fixVarTree(tree, dd->perm, dd->size);
02132     return;
02133 
02134 } /* end of Cudd_SetTree */
02135 
02136 
02148 void
02149 Cudd_FreeTree(
02150   DdManager * dd)
02151 {
02152     if (dd->tree != NULL) {
02153         Mtr_FreeTree(dd->tree);
02154         dd->tree = NULL;
02155     }
02156     return;
02157 
02158 } /* end of Cudd_FreeTree */
02159 
02160 
02172 MtrNode *
02173 Cudd_ReadZddTree(
02174   DdManager * dd)
02175 {
02176     return(dd->treeZ);
02177 
02178 } /* end of Cudd_ReadZddTree */
02179 
02180 
02192 void
02193 Cudd_SetZddTree(
02194   DdManager * dd,
02195   MtrNode * tree)
02196 {
02197     if (dd->treeZ != NULL) {
02198         Mtr_FreeTree(dd->treeZ);
02199     }
02200     dd->treeZ = tree;
02201     if (tree == NULL) return;
02202 
02203     fixVarTree(tree, dd->permZ, dd->sizeZ);
02204     return;
02205 
02206 } /* end of Cudd_SetZddTree */
02207 
02208 
02220 void
02221 Cudd_FreeZddTree(
02222   DdManager * dd)
02223 {
02224     if (dd->treeZ != NULL) {
02225         Mtr_FreeTree(dd->treeZ);
02226         dd->treeZ = NULL;
02227     }
02228     return;
02229 
02230 } /* end of Cudd_FreeZddTree */
02231 
02232 
02245 unsigned int
02246 Cudd_NodeReadIndex(
02247   DdNode * node)
02248 {
02249     return((unsigned int) Cudd_Regular(node)->index);
02250 
02251 } /* end of Cudd_NodeReadIndex */
02252 
02253 
02269 int
02270 Cudd_ReadPerm(
02271   DdManager * dd,
02272   int  i)
02273 {
02274     if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
02275     if (i < 0 || i >= dd->size) return(-1);
02276     return(dd->perm[i]);
02277 
02278 } /* end of Cudd_ReadPerm */
02279 
02280 
02296 int
02297 Cudd_ReadPermZdd(
02298   DdManager * dd,
02299   int  i)
02300 {
02301     if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
02302     if (i < 0 || i >= dd->sizeZ) return(-1);
02303     return(dd->permZ[i]);
02304 
02305 } /* end of Cudd_ReadPermZdd */
02306 
02307 
02322 int
02323 Cudd_ReadInvPerm(
02324   DdManager * dd,
02325   int  i)
02326 {
02327     if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
02328     if (i < 0 || i >= dd->size) return(-1);
02329     return(dd->invperm[i]);
02330 
02331 } /* end of Cudd_ReadInvPerm */
02332 
02333 
02348 int
02349 Cudd_ReadInvPermZdd(
02350   DdManager * dd,
02351   int  i)
02352 {
02353     if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
02354     if (i < 0 || i >= dd->sizeZ) return(-1);
02355     return(dd->invpermZ[i]);
02356 
02357 } /* end of Cudd_ReadInvPermZdd */
02358 
02359 
02375 DdNode *
02376 Cudd_ReadVars(
02377   DdManager * dd,
02378   int  i)
02379 {
02380     if (i < 0 || i > dd->size) return(NULL);
02381     return(dd->vars[i]);
02382 
02383 } /* end of Cudd_ReadVars */
02384 
02385 
02398 CUDD_VALUE_TYPE
02399 Cudd_ReadEpsilon(
02400   DdManager * dd)
02401 {
02402     return(dd->epsilon);
02403 
02404 } /* end of Cudd_ReadEpsilon */
02405 
02406 
02419 void
02420 Cudd_SetEpsilon(
02421   DdManager * dd,
02422   CUDD_VALUE_TYPE  ep)
02423 {
02424     dd->epsilon = ep;
02425 
02426 } /* end of Cudd_SetEpsilon */
02427 
02428 
02442 Cudd_AggregationType
02443 Cudd_ReadGroupcheck(
02444   DdManager * dd)
02445 {
02446     return(dd->groupcheck);
02447 
02448 } /* end of Cudd_ReadGroupCheck */
02449 
02450 
02464 void
02465 Cudd_SetGroupcheck(
02466   DdManager * dd,
02467   Cudd_AggregationType gc)
02468 {
02469     dd->groupcheck = gc;
02470 
02471 } /* end of Cudd_SetGroupcheck */
02472 
02473 
02485 int
02486 Cudd_GarbageCollectionEnabled(
02487   DdManager * dd)
02488 {
02489     return(dd->gcEnabled);
02490 
02491 } /* end of Cudd_GarbageCollectionEnabled */
02492 
02493 
02507 void
02508 Cudd_EnableGarbageCollection(
02509   DdManager * dd)
02510 {
02511     dd->gcEnabled = 1;
02512 
02513 } /* end of Cudd_EnableGarbageCollection */
02514 
02515 
02531 void
02532 Cudd_DisableGarbageCollection(
02533   DdManager * dd)
02534 {
02535     dd->gcEnabled = 0;
02536 
02537 } /* end of Cudd_DisableGarbageCollection */
02538 
02539 
02553 int
02554 Cudd_DeadAreCounted(
02555   DdManager * dd)
02556 {
02557     return(dd->countDead == 0 ? 1 : 0);
02558 
02559 } /* end of Cudd_DeadAreCounted */
02560 
02561 
02576 void
02577 Cudd_TurnOnCountDead(
02578   DdManager * dd)
02579 {
02580     dd->countDead = 0;
02581 
02582 } /* end of Cudd_TurnOnCountDead */
02583 
02584 
02601 void
02602 Cudd_TurnOffCountDead(
02603   DdManager * dd)
02604 {
02605     dd->countDead = ~0;
02606 
02607 } /* end of Cudd_TurnOffCountDead */
02608 
02609 
02625 int
02626 Cudd_ReadRecomb(
02627   DdManager * dd)
02628 {
02629     return(dd->recomb);
02630 
02631 } /* end of Cudd_ReadRecomb */
02632 
02633 
02650 void
02651 Cudd_SetRecomb(
02652   DdManager * dd,
02653   int  recomb)
02654 {
02655     dd->recomb = recomb;
02656 
02657 } /* end of Cudd_SetRecomb */
02658 
02659 
02678 int
02679 Cudd_ReadSymmviolation(
02680   DdManager * dd)
02681 {
02682     return(dd->symmviolation);
02683 
02684 } /* end of Cudd_ReadSymmviolation */
02685 
02686 
02705 void
02706 Cudd_SetSymmviolation(
02707   DdManager * dd,
02708   int  symmviolation)
02709 {
02710     dd->symmviolation = symmviolation;
02711 
02712 } /* end of Cudd_SetSymmviolation */
02713 
02714 
02732 int
02733 Cudd_ReadArcviolation(
02734   DdManager * dd)
02735 {
02736     return(dd->arcviolation);
02737 
02738 } /* end of Cudd_ReadArcviolation */
02739 
02740 
02758 void
02759 Cudd_SetArcviolation(
02760   DdManager * dd,
02761   int  arcviolation)
02762 {
02763     dd->arcviolation = arcviolation;
02764 
02765 } /* end of Cudd_SetArcviolation */
02766 
02767 
02785 int
02786 Cudd_ReadPopulationSize(
02787   DdManager * dd)
02788 {
02789     return(dd->populationSize);
02790 
02791 } /* end of Cudd_ReadPopulationSize */
02792 
02793 
02811 void
02812 Cudd_SetPopulationSize(
02813   DdManager * dd,
02814   int  populationSize)
02815 {
02816     dd->populationSize = populationSize;
02817 
02818 } /* end of Cudd_SetPopulationSize */
02819 
02820 
02838 int
02839 Cudd_ReadNumberXovers(
02840   DdManager * dd)
02841 {
02842     return(dd->numberXovers);
02843 
02844 } /* end of Cudd_ReadNumberXovers */
02845 
02846 
02864 void
02865 Cudd_SetNumberXovers(
02866   DdManager * dd,
02867   int  numberXovers)
02868 {
02869     dd->numberXovers = numberXovers;
02870 
02871 } /* end of Cudd_SetNumberXovers */
02872 
02884 long
02885 Cudd_ReadMemoryInUse(
02886   DdManager * dd)
02887 {
02888     return(dd->memused);
02889 
02890 } /* end of Cudd_ReadMemoryInUse */
02891 
02892 
02905 int
02906 Cudd_PrintInfo(
02907   DdManager * dd,
02908   FILE * fp)
02909 {
02910     int retval;
02911     Cudd_ReorderingType autoMethod, autoMethodZ;
02912 
02913     /* Modifiable parameters. */
02914     retval = fprintf(fp,"**** CUDD modifiable parameters ****\n");
02915     if (retval == EOF) return(0);
02916     retval = fprintf(fp,"Hard limit for cache size: %u\n",
02917                      Cudd_ReadMaxCacheHard(dd));
02918     if (retval == EOF) return(0);
02919     retval = fprintf(fp,"Cache hit threshold for resizing: %u%%\n",
02920                      Cudd_ReadMinHit(dd));
02921     if (retval == EOF) return(0);
02922     retval = fprintf(fp,"Garbage collection enabled: %s\n",
02923                      Cudd_GarbageCollectionEnabled(dd) ? "yes" : "no");
02924     if (retval == EOF) return(0);
02925     retval = fprintf(fp,"Limit for fast unique table growth: %u\n",
02926                      Cudd_ReadLooseUpTo(dd));
02927     if (retval == EOF) return(0);
02928     retval = fprintf(fp,
02929                      "Maximum number of variables sifted per reordering: %d\n",
02930                      Cudd_ReadSiftMaxVar(dd));
02931     if (retval == EOF) return(0);
02932     retval = fprintf(fp,
02933                      "Maximum number of variable swaps per reordering: %d\n",
02934                      Cudd_ReadSiftMaxSwap(dd));
02935     if (retval == EOF) return(0);
02936     retval = fprintf(fp,"Maximum growth while sifting a variable: %g\n",
02937                      Cudd_ReadMaxGrowth(dd));
02938     if (retval == EOF) return(0);
02939     retval = fprintf(fp,"Dynamic reordering of BDDs enabled: %s\n",
02940                      Cudd_ReorderingStatus(dd,&autoMethod) ? "yes" : "no");
02941     if (retval == EOF) return(0);
02942     retval = fprintf(fp,"Default BDD reordering method: %d\n", autoMethod);
02943     if (retval == EOF) return(0);
02944     retval = fprintf(fp,"Dynamic reordering of ZDDs enabled: %s\n",
02945                      Cudd_ReorderingStatusZdd(dd,&autoMethodZ) ? "yes" : "no");
02946     if (retval == EOF) return(0);
02947     retval = fprintf(fp,"Default ZDD reordering method: %d\n", autoMethodZ);
02948     if (retval == EOF) return(0);
02949     retval = fprintf(fp,"Realignment of ZDDs to BDDs enabled: %s\n",
02950                      Cudd_zddRealignmentEnabled(dd) ? "yes" : "no");
02951     if (retval == EOF) return(0);
02952     retval = fprintf(fp,"Realignment of BDDs to ZDDs enabled: %s\n",
02953                      Cudd_bddRealignmentEnabled(dd) ? "yes" : "no");
02954     if (retval == EOF) return(0);
02955     retval = fprintf(fp,"Dead nodes counted in triggering reordering: %s\n",
02956                      Cudd_DeadAreCounted(dd) ? "yes" : "no");
02957     if (retval == EOF) return(0);
02958     retval = fprintf(fp,"Group checking criterion: %d\n",
02959                      Cudd_ReadGroupcheck(dd));
02960     if (retval == EOF) return(0);
02961     retval = fprintf(fp,"Recombination threshold: %d\n", Cudd_ReadRecomb(dd));
02962     if (retval == EOF) return(0);
02963     retval = fprintf(fp,"Symmetry violation threshold: %d\n",
02964                      Cudd_ReadSymmviolation(dd));
02965     if (retval == EOF) return(0);
02966     retval = fprintf(fp,"Arc violation threshold: %d\n",
02967                      Cudd_ReadArcviolation(dd));
02968     if (retval == EOF) return(0);
02969     retval = fprintf(fp,"GA population size: %d\n",
02970                      Cudd_ReadPopulationSize(dd));
02971     if (retval == EOF) return(0);
02972     retval = fprintf(fp,"Number of crossovers for GA: %d\n",
02973                      Cudd_ReadNumberXovers(dd));
02974     if (retval == EOF) return(0);
02975     retval = fprintf(fp,"Next reordering threshold: %u\n",
02976                      Cudd_ReadNextReordering(dd));
02977     if (retval == EOF) return(0);
02978 
02979     /* Non-modifiable parameters. */
02980     retval = fprintf(fp,"**** CUDD non-modifiable parameters ****\n");
02981     if (retval == EOF) return(0);
02982     retval = fprintf(fp,"Memory in use: %ld\n", Cudd_ReadMemoryInUse(dd));
02983     if (retval == EOF) return(0);
02984     retval = fprintf(fp,"Peak number of nodes: %ld\n",
02985                      Cudd_ReadPeakNodeCount(dd));
02986     if (retval == EOF) return(0);
02987     retval = fprintf(fp,"Peak number of live nodes: %d\n",
02988                      Cudd_ReadPeakLiveNodeCount(dd));
02989     if (retval == EOF) return(0);
02990     retval = fprintf(fp,"Number of BDD variables: %d\n", dd->size);
02991     if (retval == EOF) return(0);
02992     retval = fprintf(fp,"Number of ZDD variables: %d\n", dd->sizeZ);
02993     if (retval == EOF) return(0);
02994     retval = fprintf(fp,"Number of cache entries: %u\n", dd->cacheSlots);
02995     if (retval == EOF) return(0);
02996     retval = fprintf(fp,"Number of cache look-ups: %.0f\n",
02997                      Cudd_ReadCacheLookUps(dd));
02998     if (retval == EOF) return(0);
02999     retval = fprintf(fp,"Number of cache hits: %.0f\n",
03000                      Cudd_ReadCacheHits(dd));
03001     if (retval == EOF) return(0);
03002     retval = fprintf(fp,"Number of cache insertions: %.0f\n",
03003                      dd->cacheinserts);
03004     if (retval == EOF) return(0);
03005     retval = fprintf(fp,"Number of cache collisions: %.0f\n",
03006                      dd->cachecollisions);
03007     if (retval == EOF) return(0);
03008     retval = fprintf(fp,"Number of cache deletions: %.0f\n",
03009                      dd->cachedeletions);
03010     if (retval == EOF) return(0);
03011     retval = cuddCacheProfile(dd,fp);
03012     if (retval == 0) return(0);
03013     retval = fprintf(fp,"Soft limit for cache size: %u\n",
03014                      Cudd_ReadMaxCache(dd));
03015     if (retval == EOF) return(0);
03016     retval = fprintf(fp,"Number of buckets in unique table: %u\n", dd->slots);
03017     if (retval == EOF) return(0);
03018     retval = fprintf(fp,"Used buckets in unique table: %.2f%% (expected %.2f%%)\n",
03019                      100.0 * Cudd_ReadUsedSlots(dd),
03020                      100.0 * Cudd_ExpectedUsedSlots(dd));
03021     if (retval == EOF) return(0);
03022 #ifdef DD_UNIQUE_PROFILE
03023     retval = fprintf(fp,"Unique lookups: %.0f\n", dd->uniqueLookUps);
03024     if (retval == EOF) return(0);
03025     retval = fprintf(fp,"Unique links: %.0f (%g per lookup)\n",
03026             dd->uniqueLinks, dd->uniqueLinks / dd->uniqueLookUps);
03027     if (retval == EOF) return(0);
03028 #endif
03029     retval = fprintf(fp,"Number of BDD and ADD nodes: %u\n", dd->keys);
03030     if (retval == EOF) return(0);
03031     retval = fprintf(fp,"Number of ZDD nodes: %u\n", dd->keysZ);
03032     if (retval == EOF) return(0);
03033     retval = fprintf(fp,"Number of dead BDD and ADD nodes: %u\n", dd->dead);
03034     if (retval == EOF) return(0);
03035     retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ);
03036     if (retval == EOF) return(0);
03037     retval = fprintf(fp,"Total number of nodes allocated: %.0f\n",
03038                      dd->allocated);
03039     if (retval == EOF) return(0);
03040     retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n",
03041                      dd->reclaimed);
03042     if (retval == EOF) return(0);
03043 #if DD_STATS
03044     retval = fprintf(fp,"Nodes freed: %.0f\n", dd->nodesFreed);
03045     if (retval == EOF) return(0);
03046     retval = fprintf(fp,"Nodes dropped: %.0f\n", dd->nodesDropped);
03047     if (retval == EOF) return(0);
03048 #endif
03049 #if DD_COUNT
03050     retval = fprintf(fp,"Number of recursive calls: %.0f\n",
03051                      Cudd_ReadRecursiveCalls(dd));
03052     if (retval == EOF) return(0);
03053 #endif
03054     retval = fprintf(fp,"Garbage collections so far: %d\n",
03055                      Cudd_ReadGarbageCollections(dd));
03056     if (retval == EOF) return(0);
03057     retval = fprintf(fp,"Time for garbage collection: %.2f sec\n",
03058                      ((double)Cudd_ReadGarbageCollectionTime(dd)/1000.0));
03059     if (retval == EOF) return(0);
03060     retval = fprintf(fp,"Reorderings so far: %d\n", dd->reorderings);
03061     if (retval == EOF) return(0);
03062     retval = fprintf(fp,"Time for reordering: %.2f sec\n",
03063                      ((double)Cudd_ReadReorderingTime(dd)/1000.0));
03064     if (retval == EOF) return(0);
03065 #if DD_COUNT
03066     retval = fprintf(fp,"Node swaps in reordering: %.0f\n",
03067         Cudd_ReadSwapSteps(dd));
03068     if (retval == EOF) return(0);
03069 #endif
03070 
03071     return(1);
03072 
03073 } /* end of Cudd_PrintInfo */
03074 
03075 
03089 long
03090 Cudd_ReadPeakNodeCount(
03091   DdManager * dd)
03092 {
03093     long count = 0;
03094     DdNodePtr *scan = dd->memoryList;
03095 
03096     while (scan != NULL) {
03097         count += DD_MEM_CHUNK;
03098         scan = (DdNodePtr *) *scan;
03099     }
03100     return(count);
03101 
03102 } /* end of Cudd_ReadPeakNodeCount */
03103 
03104 
03118 int
03119 Cudd_ReadPeakLiveNodeCount(
03120   DdManager * dd)
03121 {
03122     unsigned int live = dd->keys - dd->dead;
03123 
03124     if (live > dd->peakLiveNodes) {
03125         dd->peakLiveNodes = live;
03126     }
03127     return((int)dd->peakLiveNodes);
03128 
03129 } /* end of Cudd_ReadPeakLiveNodeCount */
03130 
03131 
03146 long
03147 Cudd_ReadNodeCount(
03148   DdManager * dd)
03149 {
03150     long count;
03151     int i;
03152 
03153 #ifndef DD_NO_DEATH_ROW
03154     cuddClearDeathRow(dd);
03155 #endif
03156 
03157     count = dd->keys - dd->dead;
03158 
03159     /* Count isolated projection functions. Their number is subtracted
03160     ** from the node count because they are not part of the BDDs.
03161     */
03162     for (i=0; i < dd->size; i++) {
03163         if (dd->vars[i]->ref == 1) count--;
03164     }
03165     /* Subtract from the count the unused constants. */
03166     if (DD_ZERO(dd)->ref == 1) count--;
03167     if (DD_PLUS_INFINITY(dd)->ref == 1) count--;
03168     if (DD_MINUS_INFINITY(dd)->ref == 1) count--;
03169 
03170     return(count);
03171 
03172 } /* end of Cudd_ReadNodeCount */
03173 
03174 
03175 
03188 long
03189 Cudd_zddReadNodeCount(
03190   DdManager * dd)
03191 {
03192     return(dd->keysZ - dd->deadZ + 2);
03193 
03194 } /* end of Cudd_zddReadNodeCount */
03195 
03196 
03211 int
03212 Cudd_AddHook(
03213   DdManager * dd,
03214   int (*f)(DdManager *, char *, void *) ,
03215   Cudd_HookType where)
03216 {
03217     DdHook **hook, *nextHook, *newHook;
03218 
03219     switch (where) {
03220     case CUDD_PRE_GC_HOOK:
03221         hook = &(dd->preGCHook);
03222         break;
03223     case CUDD_POST_GC_HOOK:
03224         hook = &(dd->postGCHook);
03225         break;
03226     case CUDD_PRE_REORDERING_HOOK:
03227         hook = &(dd->preReorderingHook);
03228         break;
03229     case CUDD_POST_REORDERING_HOOK:
03230         hook = &(dd->postReorderingHook);
03231         break;
03232     default:
03233         return(0);
03234     }
03235     /* Scan the list and find whether the function is already there.
03236     ** If so, just return. */
03237     nextHook = *hook;
03238     while (nextHook != NULL) {
03239         if (nextHook->f == f) {
03240             return(2);
03241         }
03242         hook = &(nextHook->next);
03243         nextHook = nextHook->next;
03244     }
03245     /* The function was not in the list. Create a new item and append it
03246     ** to the end of the list. */
03247     newHook = ALLOC(DdHook,1);
03248     if (newHook == NULL) {
03249         dd->errorCode = CUDD_MEMORY_OUT;
03250         return(0);
03251     }
03252     newHook->next = NULL;
03253     newHook->f = f;
03254     *hook = newHook;
03255     return(1);
03256 
03257 } /* end of Cudd_AddHook */
03258 
03259 
03273 int
03274 Cudd_RemoveHook(
03275   DdManager * dd,
03276   int (*f)(DdManager *, char *, void *) ,
03277   Cudd_HookType where)
03278 {
03279     DdHook **hook, *nextHook;
03280 
03281     switch (where) {
03282     case CUDD_PRE_GC_HOOK:
03283         hook = &(dd->preGCHook);
03284         break;
03285     case CUDD_POST_GC_HOOK:
03286         hook = &(dd->postGCHook);
03287         break;
03288     case CUDD_PRE_REORDERING_HOOK:
03289         hook = &(dd->preReorderingHook);
03290         break;
03291     case CUDD_POST_REORDERING_HOOK:
03292         hook = &(dd->postReorderingHook);
03293         break;
03294     default:
03295         return(0);
03296     }
03297     nextHook = *hook;
03298     while (nextHook != NULL) {
03299         if (nextHook->f == f) {
03300             *hook = nextHook->next;
03301             FREE(nextHook);
03302             return(1);
03303         }
03304         hook = &(nextHook->next);
03305         nextHook = nextHook->next;
03306     }
03307 
03308     return(0);
03309 
03310 } /* end of Cudd_RemoveHook */
03311 
03312 
03326 int
03327 Cudd_IsInHook(
03328   DdManager * dd,
03329   int (*f)(DdManager *, char *, void *) ,
03330   Cudd_HookType where)
03331 {
03332     DdHook *hook;
03333 
03334     switch (where) {
03335     case CUDD_PRE_GC_HOOK:
03336         hook = dd->preGCHook;
03337         break;
03338     case CUDD_POST_GC_HOOK:
03339         hook = dd->postGCHook;
03340         break;
03341     case CUDD_PRE_REORDERING_HOOK:
03342         hook = dd->preReorderingHook;
03343         break;
03344     case CUDD_POST_REORDERING_HOOK:
03345         hook = dd->postReorderingHook;
03346         break;
03347     default:
03348         return(0);
03349     }
03350     /* Scan the list and find whether the function is already there. */
03351     while (hook != NULL) {
03352         if (hook->f == f) {
03353             return(1);
03354         }
03355         hook = hook->next;
03356     }
03357     return(0);
03358 
03359 } /* end of Cudd_IsInHook */
03360 
03361 
03375 int
03376 Cudd_StdPreReordHook(
03377   DdManager *dd,
03378   char *str,
03379   void *data)
03380 {
03381     Cudd_ReorderingType method = (Cudd_ReorderingType) (ptruint) data;
03382     int retval;
03383 
03384     retval = fprintf(dd->out,"%s reordering with ", str);
03385     if (retval == EOF) return(0);
03386     switch (method) {
03387     case CUDD_REORDER_SIFT_CONVERGE:
03388     case CUDD_REORDER_SYMM_SIFT_CONV:
03389     case CUDD_REORDER_GROUP_SIFT_CONV:
03390     case CUDD_REORDER_WINDOW2_CONV:
03391     case CUDD_REORDER_WINDOW3_CONV:
03392     case CUDD_REORDER_WINDOW4_CONV:
03393     case CUDD_REORDER_LINEAR_CONVERGE:
03394         retval = fprintf(dd->out,"converging ");
03395         if (retval == EOF) return(0);
03396         break;
03397     default:
03398         break;
03399     }
03400     switch (method) {
03401     case CUDD_REORDER_RANDOM:
03402     case CUDD_REORDER_RANDOM_PIVOT:
03403         retval = fprintf(dd->out,"random");
03404         break;
03405     case CUDD_REORDER_SIFT:
03406     case CUDD_REORDER_SIFT_CONVERGE:
03407         retval = fprintf(dd->out,"sifting");
03408         break;
03409     case CUDD_REORDER_SYMM_SIFT:
03410     case CUDD_REORDER_SYMM_SIFT_CONV:
03411         retval = fprintf(dd->out,"symmetric sifting");
03412         break;
03413     case CUDD_REORDER_LAZY_SIFT:
03414         retval = fprintf(dd->out,"lazy sifting");
03415         break;
03416     case CUDD_REORDER_GROUP_SIFT:
03417     case CUDD_REORDER_GROUP_SIFT_CONV:
03418         retval = fprintf(dd->out,"group sifting");
03419         break;
03420     case CUDD_REORDER_WINDOW2:
03421     case CUDD_REORDER_WINDOW3:
03422     case CUDD_REORDER_WINDOW4:
03423     case CUDD_REORDER_WINDOW2_CONV:
03424     case CUDD_REORDER_WINDOW3_CONV:
03425     case CUDD_REORDER_WINDOW4_CONV:
03426         retval = fprintf(dd->out,"window");
03427         break;
03428     case CUDD_REORDER_ANNEALING:
03429         retval = fprintf(dd->out,"annealing");
03430         break;
03431     case CUDD_REORDER_GENETIC:
03432         retval = fprintf(dd->out,"genetic");
03433         break;
03434     case CUDD_REORDER_LINEAR:
03435     case CUDD_REORDER_LINEAR_CONVERGE:
03436         retval = fprintf(dd->out,"linear sifting");
03437         break;
03438     case CUDD_REORDER_EXACT:
03439         retval = fprintf(dd->out,"exact");
03440         break;
03441     default:
03442         return(0);
03443     }
03444     if (retval == EOF) return(0);
03445 
03446     retval = fprintf(dd->out,": from %ld to ... ", strcmp(str, "BDD") == 0 ?
03447                      Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd));
03448     if (retval == EOF) return(0);
03449     fflush(dd->out);
03450     return(1);
03451 
03452 } /* end of Cudd_StdPreReordHook */
03453 
03454 
03468 int
03469 Cudd_StdPostReordHook(
03470   DdManager *dd,
03471   char *str,
03472   void *data)
03473 {
03474     long initialTime = (long) data;
03475     int retval;
03476     long finalTime = util_cpu_time();
03477     double totalTimeSec = (double)(finalTime - initialTime) / 1000.0;
03478 
03479     retval = fprintf(dd->out,"%ld nodes in %g sec\n", strcmp(str, "BDD") == 0 ?
03480                      Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd),
03481                      totalTimeSec);
03482     if (retval == EOF) return(0);
03483     retval = fflush(dd->out);
03484     if (retval == EOF) return(0);
03485     return(1);
03486 
03487 } /* end of Cudd_StdPostReordHook */
03488 
03489 
03503 int
03504 Cudd_EnableReorderingReporting(
03505   DdManager *dd)
03506 {
03507     if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
03508         return(0);
03509     }
03510     if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
03511         return(0);
03512     }
03513     return(1);
03514 
03515 } /* end of Cudd_EnableReorderingReporting */
03516 
03517 
03531 int
03532 Cudd_DisableReorderingReporting(
03533   DdManager *dd)
03534 {
03535     if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
03536         return(0);
03537     }
03538     if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
03539         return(0);
03540     }
03541     return(1);
03542 
03543 } /* end of Cudd_DisableReorderingReporting */
03544 
03545 
03558 int
03559 Cudd_ReorderingReporting(
03560   DdManager *dd)
03561 {
03562     return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK));
03563 
03564 } /* end of Cudd_ReorderingReporting */
03565 
03566 
03579 Cudd_ErrorType
03580 Cudd_ReadErrorCode(
03581   DdManager *dd)
03582 {
03583     return(dd->errorCode);
03584 
03585 } /* end of Cudd_ReadErrorCode */
03586 
03587 
03599 void
03600 Cudd_ClearErrorCode(
03601   DdManager *dd)
03602 {
03603     dd->errorCode = CUDD_NO_ERROR;
03604 
03605 } /* end of Cudd_ClearErrorCode */
03606 
03607 
03621 FILE *
03622 Cudd_ReadStdout(
03623   DdManager *dd)
03624 {
03625     return(dd->out);
03626 
03627 } /* end of Cudd_ReadStdout */
03628 
03629 
03641 void
03642 Cudd_SetStdout(
03643   DdManager *dd,
03644   FILE *fp)
03645 {
03646     dd->out = fp;
03647 
03648 } /* end of Cudd_SetStdout */
03649 
03650 
03664 FILE *
03665 Cudd_ReadStderr(
03666   DdManager *dd)
03667 {
03668     return(dd->err);
03669 
03670 } /* end of Cudd_ReadStderr */
03671 
03672 
03684 void
03685 Cudd_SetStderr(
03686   DdManager *dd,
03687   FILE *fp)
03688 {
03689     dd->err = fp;
03690 
03691 } /* end of Cudd_SetStderr */
03692 
03693 
03709 unsigned int
03710 Cudd_ReadNextReordering(
03711   DdManager *dd)
03712 {
03713     return(dd->nextDyn);
03714 
03715 } /* end of Cudd_ReadNextReordering */
03716 
03717 
03733 void
03734 Cudd_SetNextReordering(
03735   DdManager *dd,
03736   unsigned int next)
03737 {
03738     dd->nextDyn = next;
03739 
03740 } /* end of Cudd_SetNextReordering */
03741 
03742 
03754 double
03755 Cudd_ReadSwapSteps(
03756   DdManager *dd)
03757 {
03758 #ifdef DD_COUNT
03759     return(dd->swapSteps);
03760 #else
03761     return(-1);
03762 #endif
03763 
03764 } /* end of Cudd_ReadSwapSteps */
03765 
03766 
03779 unsigned int
03780 Cudd_ReadMaxLive(
03781   DdManager *dd)
03782 {
03783     return(dd->maxLive);
03784 
03785 } /* end of Cudd_ReadMaxLive */
03786 
03787 
03800 void
03801 Cudd_SetMaxLive(
03802   DdManager *dd,
03803   unsigned int maxLive)
03804 {
03805     dd->maxLive = maxLive;
03806 
03807 } /* end of Cudd_SetMaxLive */
03808 
03809 
03822 long
03823 Cudd_ReadMaxMemory(
03824   DdManager *dd)
03825 {
03826     return(dd->maxmemhard);
03827 
03828 } /* end of Cudd_ReadMaxMemory */
03829 
03830 
03843 void
03844 Cudd_SetMaxMemory(
03845   DdManager *dd,
03846   long maxMemory)
03847 {
03848     dd->maxmemhard = maxMemory;
03849 
03850 } /* end of Cudd_SetMaxMemory */
03851 
03852 
03866 int
03867 Cudd_bddBindVar(
03868   DdManager *dd /* manager */,
03869   int index /* variable index */)
03870 {
03871     if (index >= dd->size || index < 0) return(0);
03872     dd->subtables[dd->perm[index]].bindVar = 1;
03873     return(1);
03874 
03875 } /* end of Cudd_bddBindVar */
03876 
03877 
03894 int
03895 Cudd_bddUnbindVar(
03896   DdManager *dd /* manager */,
03897   int index /* variable index */)
03898 {
03899     if (index >= dd->size || index < 0) return(0);
03900     dd->subtables[dd->perm[index]].bindVar = 0;
03901     return(1);
03902 
03903 } /* end of Cudd_bddUnbindVar */
03904 
03905 
03921 int
03922 Cudd_bddVarIsBound(
03923   DdManager *dd /* manager */,
03924   int index /* variable index */)
03925 {
03926     if (index >= dd->size || index < 0) return(0);
03927     return(dd->subtables[dd->perm[index]].bindVar);
03928 
03929 } /* end of Cudd_bddVarIsBound */
03930 
03931 
03944 int
03945 Cudd_bddSetPiVar(
03946   DdManager *dd /* manager */,
03947   int index /* variable index */)
03948 {
03949     if (index >= dd->size || index < 0) return (0);
03950     dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRIMARY_INPUT;
03951     return(1);
03952 
03953 } /* end of Cudd_bddSetPiVar */
03954 
03955 
03968 int
03969 Cudd_bddSetPsVar(
03970   DdManager *dd /* manager */,
03971   int index /* variable index */)
03972 {
03973     if (index >= dd->size || index < 0) return (0);
03974     dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRESENT_STATE;
03975     return(1);
03976 
03977 } /* end of Cudd_bddSetPsVar */
03978 
03979 
03992 int
03993 Cudd_bddSetNsVar(
03994   DdManager *dd /* manager */,
03995   int index /* variable index */)
03996 {
03997     if (index >= dd->size || index < 0) return (0);
03998     dd->subtables[dd->perm[index]].varType = CUDD_VAR_NEXT_STATE;
03999     return(1);
04000 
04001 } /* end of Cudd_bddSetNsVar */
04002 
04003 
04017 int
04018 Cudd_bddIsPiVar(
04019   DdManager *dd /* manager */,
04020   int index /* variable index */)
04021 {
04022     if (index >= dd->size || index < 0) return -1;
04023     return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRIMARY_INPUT);
04024 
04025 } /* end of Cudd_bddIsPiVar */
04026 
04027 
04041 int
04042 Cudd_bddIsPsVar(
04043   DdManager *dd,
04044   int index)
04045 {
04046     if (index >= dd->size || index < 0) return -1;
04047     return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRESENT_STATE);
04048 
04049 } /* end of Cudd_bddIsPsVar */
04050 
04051 
04065 int
04066 Cudd_bddIsNsVar(
04067   DdManager *dd,
04068   int index)
04069 {
04070     if (index >= dd->size || index < 0) return -1;
04071     return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_NEXT_STATE);
04072 
04073 } /* end of Cudd_bddIsNsVar */
04074 
04075 
04089 int
04090 Cudd_bddSetPairIndex(
04091   DdManager *dd /* manager */,
04092   int index /* variable index */,
04093   int pairIndex /* corresponding variable index */)
04094 {
04095     if (index >= dd->size || index < 0) return(0);
04096     dd->subtables[dd->perm[index]].pairIndex = pairIndex;
04097     return(1);
04098 
04099 } /* end of Cudd_bddSetPairIndex */
04100 
04101 
04115 int
04116 Cudd_bddReadPairIndex(
04117   DdManager *dd,
04118   int index)
04119 {
04120     if (index >= dd->size || index < 0) return -1;
04121     return dd->subtables[dd->perm[index]].pairIndex;
04122 
04123 } /* end of Cudd_bddReadPairIndex */
04124 
04125 
04138 int
04139 Cudd_bddSetVarToBeGrouped(
04140   DdManager *dd,
04141   int index)
04142 {
04143     if (index >= dd->size || index < 0) return(0);
04144     if (dd->subtables[dd->perm[index]].varToBeGrouped <= CUDD_LAZY_SOFT_GROUP) {
04145         dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_SOFT_GROUP;
04146     }
04147     return(1);
04148 
04149 } /* end of Cudd_bddSetVarToBeGrouped */
04150 
04151 
04165 int
04166 Cudd_bddSetVarHardGroup(
04167   DdManager *dd,
04168   int index)
04169 {
04170     if (index >= dd->size || index < 0) return(0);
04171     dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_HARD_GROUP;
04172     return(1);
04173 
04174 } /* end of Cudd_bddSetVarHardGrouped */
04175 
04176 
04189 int
04190 Cudd_bddResetVarToBeGrouped(
04191   DdManager *dd,
04192   int index)
04193 {
04194     if (index >= dd->size || index < 0) return(0);
04195     if (dd->subtables[dd->perm[index]].varToBeGrouped <=
04196         CUDD_LAZY_SOFT_GROUP) {
04197         dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_NONE;
04198     }
04199     return(1);
04200 
04201 } /* end of Cudd_bddResetVarToBeGrouped */
04202 
04203 
04216 int
04217 Cudd_bddIsVarToBeGrouped(
04218   DdManager *dd,
04219   int index)
04220 {
04221     if (index >= dd->size || index < 0) return(-1);
04222     if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP)
04223         return(0);
04224     else
04225         return(dd->subtables[dd->perm[index]].varToBeGrouped);
04226 
04227 } /* end of Cudd_bddIsVarToBeGrouped */
04228 
04229 
04242 int
04243 Cudd_bddSetVarToBeUngrouped(
04244   DdManager *dd,
04245   int index)
04246 {
04247     if (index >= dd->size || index < 0) return(0);
04248     dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_UNGROUP;
04249     return(1);
04250 
04251 } /* end of Cudd_bddSetVarToBeGrouped */
04252 
04253 
04268 int
04269 Cudd_bddIsVarToBeUngrouped(
04270   DdManager *dd,
04271   int index)
04272 {
04273     if (index >= dd->size || index < 0) return(-1);
04274     return dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP;
04275 
04276 } /* end of Cudd_bddIsVarToBeGrouped */
04277 
04278 
04293 int
04294 Cudd_bddIsVarHardGroup(
04295   DdManager *dd,
04296   int index)
04297 {
04298     if (index >= dd->size || index < 0) return(-1);
04299     if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_HARD_GROUP)
04300         return(1);
04301     return(0);
04302 
04303 } /* end of Cudd_bddIsVarToBeGrouped */
04304 
04305 
04306 /*---------------------------------------------------------------------------*/
04307 /* Definition of internal functions                                          */
04308 /*---------------------------------------------------------------------------*/
04309 
04310 /*---------------------------------------------------------------------------*/
04311 /* Definition of static functions                                            */
04312 /*---------------------------------------------------------------------------*/
04313 
04314 
04326 static void
04327 fixVarTree(
04328   MtrNode * treenode,
04329   int * perm,
04330   int  size)
04331 {
04332     treenode->index = treenode->low;
04333     treenode->low = ((int) treenode->index < size) ?
04334         perm[treenode->index] : treenode->index;
04335     if (treenode->child != NULL)
04336         fixVarTree(treenode->child, perm, size);
04337     if (treenode->younger != NULL)
04338         fixVarTree(treenode->younger, perm, size);
04339     return;
04340 
04341 } /* end of fixVarTree */
04342 
04343 
04369 static int
04370 addMultiplicityGroups(
04371   DdManager *dd /* manager */,
04372   MtrNode *treenode /* current tree node */,
04373   int multiplicity /* how many ZDD vars per BDD var */,
04374   char *vmask /* variable pairs for which a group has been already built */,
04375   char *lmask /* levels for which a group has already been built*/)
04376 {
04377     int startV, stopV, startL;
04378     int i, j;
04379     MtrNode *auxnode = treenode;
04380 
04381     while (auxnode != NULL) {
04382         if (auxnode->child != NULL) {
04383             addMultiplicityGroups(dd,auxnode->child,multiplicity,vmask,lmask);
04384         }
04385         /* Build remaining groups. */
04386         startV = dd->permZ[auxnode->index] / multiplicity;
04387         startL = auxnode->low / multiplicity;
04388         stopV = startV + auxnode->size / multiplicity;
04389         /* Walk down vmask starting at startV and build missing groups. */
04390         for (i = startV, j = startL; i < stopV; i++) {
04391             if (vmask[i] == 0) {
04392                 MtrNode *node;
04393                 while (lmask[j] == 1) j++;
04394                 node = Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity,
04395                                      MTR_FIXED);
04396                 if (node == NULL) {
04397                     return(0);
04398                 }
04399                 node->index = dd->invpermZ[i * multiplicity];
04400                 vmask[i] = 1;
04401                 lmask[j] = 1;
04402             }
04403         }
04404         auxnode = auxnode->younger;
04405     }
04406     return(1);
04407 
04408 } /* end of addMultiplicityGroups */
04409