glu-2.2: src/cuBdd/cuddAPI.c Source File

00001 
00194 #include "util.h"
00195 #include "cuddInt.h"
00196 
00197 /*---------------------------------------------------------------------------*/
00198 /* Constant declarations                                                     */
00199 /*---------------------------------------------------------------------------*/
00200 
00201 /*---------------------------------------------------------------------------*/
00202 /* Stucture declarations                                                     */
00203 /*---------------------------------------------------------------------------*/
00204 
00205 /*---------------------------------------------------------------------------*/
00206 /* Type declarations                                                         */
00207 /*---------------------------------------------------------------------------*/
00208 
00209 /*---------------------------------------------------------------------------*/
00210 /* Variable declarations                                                     */
00211 /*---------------------------------------------------------------------------*/
00212 
00213 #ifndef lint
00214 static char rcsid[] DD_UNUSED = "$Id: cuddAPI.c,v 1.59 2009/02/19 16:14:14 fabio Exp $";
00215 #endif
00216 
00217 /*---------------------------------------------------------------------------*/
00218 /* Macro declarations                                                        */
00219 /*---------------------------------------------------------------------------*/
00220 
00223 /*---------------------------------------------------------------------------*/
00224 /* Static function prototypes                                                */
00225 /*---------------------------------------------------------------------------*/
00226 
00227 static void fixVarTree (MtrNode *treenode, int *perm, int size);
00228 static int addMultiplicityGroups (DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask);
00229 
00233 /*---------------------------------------------------------------------------*/
00234 /* Definition of exported functions                                          */
00235 /*---------------------------------------------------------------------------*/
00236 
00237 
00254 DdNode *
00255 Cudd_addNewVar(
00256   DdManager * dd)
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 */
00269 
00270 
00285 DdNode *
00286 Cudd_addNewVarAtLevel(
00287   DdManager * dd,
00288   int  level)
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 */
00303 
00304 
00318 DdNode *
00319 Cudd_bddNewVar(
00320   DdManager * dd)
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 */
00330 
00331 
00346 DdNode *
00347 Cudd_bddNewVarAtLevel(
00348   DdManager * dd,
00349   int  level)
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 */
00361 
00362 
00379 DdNode *
00380 Cudd_addIthVar(
00381   DdManager * dd,
00382   int  i)
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 */
00395 
00396 
00411 DdNode *
00412 Cudd_bddIthVar(
00413   DdManager * dd,
00414   int  i)
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 */
00428 
00429 
00443 DdNode *
00444 Cudd_zddIthVar(
00445   DdManager * dd,
00446   int  i)
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 */
00490 
00491 
00514 int
00515 Cudd_zddVarsFromBddVars(
00516   DdManager * dd /* DD manager */,
00517   int multiplicity /* how many ZDD variables are created for each BDD variable */)
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 */
00600 
00601 
00615 DdNode *
00616 Cudd_addConst(
00617   DdManager * dd,
00618   CUDD_VALUE_TYPE  c)
00619 {
00620     return(cuddUniqueConst(dd,c));
00621 
00622 } /* end of Cudd_addConst */
00623 
00624 
00640 int
00641 Cudd_IsNonConstant(
00642   DdNode *f)
00643 {
00644     return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f));
00645 
00646 } /* end of Cudd_IsNonConstant */
00647 
00648 
00664 void
00665 Cudd_AutodynEnable(
00666   DdManager * unique,
00667   Cudd_ReorderingType  method)
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 */
00689 
00690 
00703 void
00704 Cudd_AutodynDisable(
00705   DdManager * unique)
00706 {
00707     unique->autoDyn = 0;
00708     return;
00709 
00710 } /* end of Cudd_AutodynDisable */
00711 
00712 
00730 int
00731 Cudd_ReorderingStatus(
00732   DdManager * unique,
00733   Cudd_ReorderingType * method)
00734 {
00735     *method = unique->autoMethod;
00736     return(unique->autoDyn);
00737 
00738 } /* end of Cudd_ReorderingStatus */
00739 
00740 
00755 void
00756 Cudd_AutodynEnableZdd(
00757   DdManager * unique,
00758   Cudd_ReorderingType method)
00759 {
00760     unique->autoDynZ = 1;
00761     if (method != CUDD_REORDER_SAME) {
00762         unique->autoMethodZ = method;
00763     }
00764     return;
00765 
00766 } /* end of Cudd_AutodynEnableZdd */
00767 
00768 
00781 void
00782 Cudd_AutodynDisableZdd(
00783   DdManager * unique)
00784 {
00785     unique->autoDynZ = 0;
00786     return;
00787 
00788 } /* end of Cudd_AutodynDisableZdd */
00789 
00790 
00807 int
00808 Cudd_ReorderingStatusZdd(
00809   DdManager * unique,
00810   Cudd_ReorderingType * method)
00811 {
00812     *method = unique->autoMethodZ;
00813     return(unique->autoDynZ);
00814 
00815 } /* end of Cudd_ReorderingStatusZdd */
00816 
00817 
00832 int
00833 Cudd_zddRealignmentEnabled(
00834   DdManager * unique)
00835 {
00836     return(unique->realign);
00837 
00838 } /* end of Cudd_zddRealignmentEnabled */
00839 
00840 
00862 void
00863 Cudd_zddRealignEnable(
00864   DdManager * unique)
00865 {
00866     unique->realign = 1;
00867     return;
00868 
00869 } /* end of Cudd_zddRealignEnable */
00870 
00871 
00884 void
00885 Cudd_zddRealignDisable(
00886   DdManager * unique)
00887 {
00888     unique->realign = 0;
00889     return;
00890 
00891 } /* end of Cudd_zddRealignDisable */
00892 
00893 
00908 int
00909 Cudd_bddRealignmentEnabled(
00910   DdManager * unique)
00911 {
00912     return(unique->realignZ);
00913 
00914 } /* end of Cudd_bddRealignmentEnabled */
00915 
00916 
00938 void
00939 Cudd_bddRealignEnable(
00940   DdManager * unique)
00941 {
00942     unique->realignZ = 1;
00943     return;
00944 
00945 } /* end of Cudd_bddRealignEnable */
00946 
00947 
00960 void
00961 Cudd_bddRealignDisable(
00962   DdManager * unique)
00963 {
00964     unique->realignZ = 0;
00965     return;
00966 
00967 } /* end of Cudd_bddRealignDisable */
00968 
00969 
00982 DdNode *
00983 Cudd_ReadOne(
00984   DdManager * dd)
00985 {
00986     return(dd->one);
00987 
00988 } /* end of Cudd_ReadOne */
00989 
00990 
01005 DdNode *
01006 Cudd_ReadZddOne(
01007   DdManager * dd,
01008   int  i)
01009 {
01010     if (i < 0)
01011         return(NULL);
01012     return(i < dd->sizeZ ? dd->univ[i] : DD_ONE(dd));
01013 
01014 } /* end of Cudd_ReadZddOne */
01015 
01016 
01017 
01031 DdNode *
01032 Cudd_ReadZero(
01033   DdManager * dd)
01034 {
01035     return(DD_ZERO(dd));
01036 
01037 } /* end of Cudd_ReadZero */
01038 
01039 
01053 DdNode *
01054 Cudd_ReadLogicZero(
01055   DdManager * dd)
01056 {
01057     return(Cudd_Not(DD_ONE(dd)));
01058 
01059 } /* end of Cudd_ReadLogicZero */
01060 
01061 
01071 DdNode *
01072 Cudd_ReadPlusInfinity(
01073   DdManager * dd)
01074 {
01075     return(dd->plusinfinity);
01076 
01077 } /* end of Cudd_ReadPlusInfinity */
01078 
01079 
01089 DdNode *
01090 Cudd_ReadMinusInfinity(
01091   DdManager * dd)
01092 {
01093     return(dd->minusinfinity);
01094 
01095 } /* end of Cudd_ReadMinusInfinity */
01096 
01097 
01107 DdNode *
01108 Cudd_ReadBackground(
01109   DdManager * dd)
01110 {
01111     return(dd->background);
01112 
01113 } /* end of Cudd_ReadBackground */
01114 
01115 
01126 void
01127 Cudd_SetBackground(
01128   DdManager * dd,
01129   DdNode * bck)
01130 {
01131     dd->background = bck;
01132 
01133 } /* end of Cudd_SetBackground */
01134 
01135 
01147 unsigned int
01148 Cudd_ReadCacheSlots(
01149   DdManager * dd)
01150 {
01151     return(dd->cacheSlots);
01152 
01153 } /* end of Cudd_ReadCacheSlots */
01154 
01155 
01170 double
01171 Cudd_ReadCacheUsedSlots(
01172   DdManager * dd)
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 */
01186 
01187 
01199 double
01200 Cudd_ReadCacheLookUps(
01201   DdManager * dd)
01202 {
01203     return(dd->cacheHits + dd->cacheMisses +
01204            dd->totCachehits + dd->totCacheMisses);
01205 
01206 } /* end of Cudd_ReadCacheLookUps */
01207 
01208 
01220 double
01221 Cudd_ReadCacheHits(
01222   DdManager * dd)
01223 {
01224     return(dd->cacheHits + dd->totCachehits);
01225 
01226 } /* end of Cudd_ReadCacheHits */
01227 
01228 
01241 double
01242 Cudd_ReadRecursiveCalls(
01243   DdManager * dd)
01244 {
01245 #ifdef DD_COUNT
01246     return(dd->recursiveCalls);
01247 #else
01248     return(-1.0);
01249 #endif
01250 
01251 } /* end of Cudd_ReadRecursiveCalls */
01252 
01253 
01254 
01267 unsigned int
01268 Cudd_ReadMinHit(
01269   DdManager * dd)
01270 {
01271     /* Internally, the package manipulates the ratio of hits to
01272     ** misses instead of the ratio of hits to accesses. */
01273     return((unsigned int) (0.5 + 100 * dd->minHit / (1 + dd->minHit)));
01274 
01275 } /* end of Cudd_ReadMinHit */
01276 
01277 
01293 void
01294 Cudd_SetMinHit(
01295   DdManager * dd,
01296   unsigned int hr)
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 */
01303 
01304 
01316 unsigned int
01317 Cudd_ReadLooseUpTo(
01318   DdManager * dd)
01319 {
01320     return(dd->looseUpTo);
01321 
01322 } /* end of Cudd_ReadLooseUpTo */
01323 
01324 
01340 void
01341 Cudd_SetLooseUpTo(
01342   DdManager * dd,
01343   unsigned int lut)
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 */
01353 
01354 
01366 unsigned int
01367 Cudd_ReadMaxCache(
01368   DdManager * dd)
01369 {
01370     return(2 * dd->cacheSlots + dd->cacheSlack);
01371 
01372 } /* end of Cudd_ReadMaxCache */
01373 
01374 
01386 unsigned int
01387 Cudd_ReadMaxCacheHard(
01388   DdManager * dd)
01389 {
01390     return(dd->maxCacheHard);
01391 
01392 } /* end of Cudd_ReadMaxCache */
01393 
01394 
01410 void
01411 Cudd_SetMaxCacheHard(
01412   DdManager * dd,
01413   unsigned int mc)
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 */
01423 
01424 
01436 int
01437 Cudd_ReadSize(
01438   DdManager * dd)
01439 {
01440     return(dd->size);
01441 
01442 } /* end of Cudd_ReadSize */
01443 
01444 
01456 int
01457 Cudd_ReadZddSize(
01458   DdManager * dd)
01459 {
01460     return(dd->sizeZ);
01461 
01462 } /* end of Cudd_ReadZddSize */
01463 
01464 
01475 unsigned int
01476 Cudd_ReadSlots(
01477   DdManager * dd)
01478 {
01479     return(dd->slots);
01480 
01481 } /* end of Cudd_ReadSlots */
01482 
01483 
01498 double
01499 Cudd_ReadUsedSlots(
01500   DdManager * dd)
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 */
01549 
01550 
01567 double
01568 Cudd_ExpectedUsedSlots(
01569   DdManager * dd)
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 */
01607 
01608 
01621 unsigned int
01622 Cudd_ReadKeys(
01623   DdManager * dd)
01624 {
01625     return(dd->keys);
01626 
01627 } /* end of Cudd_ReadKeys */
01628 
01629 
01641 unsigned int
01642 Cudd_ReadDead(
01643   DdManager * dd)
01644 {
01645     return(dd->dead);
01646 
01647 } /* end of Cudd_ReadDead */
01648 
01649 
01665 unsigned int
01666 Cudd_ReadMinDead(
01667   DdManager * dd)
01668 {
01669     return(dd->minDead);
01670 
01671 } /* end of Cudd_ReadMinDead */
01672 
01673 
01691 int
01692 Cudd_ReadReorderings(
01693   DdManager * dd)
01694 {
01695     return(dd->reorderings);
01696 
01697 } /* end of Cudd_ReadReorderings */
01698 
01699 
01713 long
01714 Cudd_ReadReorderingTime(
01715   DdManager * dd)
01716 {
01717     return(dd->reordTime);
01718 
01719 } /* end of Cudd_ReadReorderingTime */
01720 
01721 
01736 int
01737 Cudd_ReadGarbageCollections(
01738   DdManager * dd)
01739 {
01740     return(dd->garbageCollections);
01741 
01742 } /* end of Cudd_ReadGarbageCollections */
01743 
01744 
01757 long
01758 Cudd_ReadGarbageCollectionTime(
01759   DdManager * dd)
01760 {
01761     return(dd->GCTime);
01762 
01763 } /* end of Cudd_ReadGarbageCollectionTime */
01764 
01765 
01779 double
01780 Cudd_ReadNodesFreed(
01781   DdManager * dd)
01782 {
01783 #ifdef DD_STATS
01784     return(dd->nodesFreed);
01785 #else
01786     return(-1.0);
01787 #endif
01788 
01789 } /* end of Cudd_ReadNodesFreed */
01790 
01791 
01805 double
01806 Cudd_ReadNodesDropped(
01807   DdManager * dd)
01808 {
01809 #ifdef DD_STATS
01810     return(dd->nodesDropped);
01811 #else
01812     return(-1.0);
01813 #endif
01814 
01815 } /* end of Cudd_ReadNodesDropped */
01816 
01817 
01831 double
01832 Cudd_ReadUniqueLookUps(
01833   DdManager * dd)
01834 {
01835 #ifdef DD_UNIQUE_PROFILE
01836     return(dd->uniqueLookUps);
01837 #else
01838     return(-1.0);
01839 #endif
01840 
01841 } /* end of Cudd_ReadUniqueLookUps */
01842 
01843 
01860 double
01861 Cudd_ReadUniqueLinks(
01862   DdManager * dd)
01863 {
01864 #ifdef DD_UNIQUE_PROFILE
01865     return(dd->uniqueLinks);
01866 #else
01867     return(-1.0);
01868 #endif
01869 
01870 } /* end of Cudd_ReadUniqueLinks */
01871 
01872 
01886 int
01887 Cudd_ReadSiftMaxVar(
01888   DdManager * dd)
01889 {
01890     return(dd->siftMaxVar);
01891 
01892 } /* end of Cudd_ReadSiftMaxVar */
01893 
01894 
01908 void
01909 Cudd_SetSiftMaxVar(
01910   DdManager * dd,
01911   int  smv)
01912 {
01913     dd->siftMaxVar = smv;
01914 
01915 } /* end of Cudd_SetSiftMaxVar */
01916 
01917 
01933 int
01934 Cudd_ReadSiftMaxSwap(
01935   DdManager * dd)
01936 {
01937     return(dd->siftMaxSwap);
01938 
01939 } /* end of Cudd_ReadSiftMaxSwap */
01940 
01941 
01957 void
01958 Cudd_SetSiftMaxSwap(
01959   DdManager * dd,
01960   int  sms)
01961 {
01962     dd->siftMaxSwap = sms;
01963 
01964 } /* end of Cudd_SetSiftMaxSwap */
01965 
01966 
01983 double
01984 Cudd_ReadMaxGrowth(
01985   DdManager * dd)
01986 {
01987     return(dd->maxGrowth);
01988 
01989 } /* end of Cudd_ReadMaxGrowth */
01990 
01991 
02008 void
02009 Cudd_SetMaxGrowth(
02010   DdManager * dd,
02011   double mg)
02012 {
02013     dd->maxGrowth = mg;
02014 
02015 } /* end of Cudd_SetMaxGrowth */
02016 
02017 
02034 double
02035 Cudd_ReadMaxGrowthAlternate(
02036   DdManager * dd)
02037 {
02038     return(dd->maxGrowthAlt);
02039 
02040 } /* end of Cudd_ReadMaxGrowthAlternate */
02041 
02042 
02059 void
02060 Cudd_SetMaxGrowthAlternate(
02061   DdManager * dd,
02062   double mg)
02063 {
02064     dd->maxGrowthAlt = mg;
02065 
02066 } /* end of Cudd_SetMaxGrowthAlternate */
02067 
02068 
02083 int
02084 Cudd_ReadReorderingCycle(
02085   DdManager * dd)
02086 {
02087     return(dd->reordCycle);
02088 
02089 } /* end of Cudd_ReadReorderingCycle */
02090 
02091 
02106 void
02107 Cudd_SetReorderingCycle(
02108   DdManager * dd,
02109   int cycle)
02110 {
02111     dd->reordCycle = cycle;
02112 
02113 } /* end of Cudd_SetReorderingCycle */
02114 
02115 
02127 MtrNode *
02128 Cudd_ReadTree(
02129   DdManager * dd)
02130 {
02131     return(dd->tree);
02132 
02133 } /* end of Cudd_ReadTree */
02134 
02135 
02147 void
02148 Cudd_SetTree(
02149   DdManager * dd,
02150   MtrNode * tree)
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 */
02162 
02163 
02175 void
02176 Cudd_FreeTree(
02177   DdManager * dd)
02178 {
02179     if (dd->tree != NULL) {
02180         Mtr_FreeTree(dd->tree);
02181         dd->tree = NULL;
02182     }
02183     return;
02184 
02185 } /* end of Cudd_FreeTree */
02186 
02187 
02199 MtrNode *
02200 Cudd_ReadZddTree(
02201   DdManager * dd)
02202 {
02203     return(dd->treeZ);
02204 
02205 } /* end of Cudd_ReadZddTree */
02206 
02207 
02219 void
02220 Cudd_SetZddTree(
02221   DdManager * dd,
02222   MtrNode * tree)
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 */
02234 
02235 
02247 void
02248 Cudd_FreeZddTree(
02249   DdManager * dd)
02250 {
02251     if (dd->treeZ != NULL) {
02252         Mtr_FreeTree(dd->treeZ);
02253         dd->treeZ = NULL;
02254     }
02255     return;
02256 
02257 } /* end of Cudd_FreeZddTree */
02258 
02259 
02272 unsigned int
02273 Cudd_NodeReadIndex(
02274   DdNode * node)
02275 {
02276     return((unsigned int) Cudd_Regular(node)->index);
02277 
02278 } /* end of Cudd_NodeReadIndex */
02279 
02280 
02296 int
02297 Cudd_ReadPerm(
02298   DdManager * dd,
02299   int  i)
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 */
02306 
02307 
02323 int
02324 Cudd_ReadPermZdd(
02325   DdManager * dd,
02326   int  i)
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 */
02333 
02334 
02349 int
02350 Cudd_ReadInvPerm(
02351   DdManager * dd,
02352   int  i)
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 */
02359 
02360 
02375 int
02376 Cudd_ReadInvPermZdd(
02377   DdManager * dd,
02378   int  i)
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 */
02385 
02386 
02402 DdNode *
02403 Cudd_ReadVars(
02404   DdManager * dd,
02405   int  i)
02406 {
02407     if (i < 0 || i > dd->size) return(NULL);
02408     return(dd->vars[i]);
02409 
02410 } /* end of Cudd_ReadVars */
02411 
02412 
02425 CUDD_VALUE_TYPE
02426 Cudd_ReadEpsilon(
02427   DdManager * dd)
02428 {
02429     return(dd->epsilon);
02430 
02431 } /* end of Cudd_ReadEpsilon */
02432 
02433 
02446 void
02447 Cudd_SetEpsilon(
02448   DdManager * dd,
02449   CUDD_VALUE_TYPE  ep)
02450 {
02451     dd->epsilon = ep;
02452 
02453 } /* end of Cudd_SetEpsilon */
02454 
02455 
02469 Cudd_AggregationType
02470 Cudd_ReadGroupcheck(
02471   DdManager * dd)
02472 {
02473     return(dd->groupcheck);
02474 
02475 } /* end of Cudd_ReadGroupCheck */
02476 
02477 
02491 void
02492 Cudd_SetGroupcheck(
02493   DdManager * dd,
02494   Cudd_AggregationType gc)
02495 {
02496     dd->groupcheck = gc;
02497 
02498 } /* end of Cudd_SetGroupcheck */
02499 
02500 
02512 int
02513 Cudd_GarbageCollectionEnabled(
02514   DdManager * dd)
02515 {
02516     return(dd->gcEnabled);
02517 
02518 } /* end of Cudd_GarbageCollectionEnabled */
02519 
02520 
02534 void
02535 Cudd_EnableGarbageCollection(
02536   DdManager * dd)
02537 {
02538     dd->gcEnabled = 1;
02539 
02540 } /* end of Cudd_EnableGarbageCollection */
02541 
02542 
02558 void
02559 Cudd_DisableGarbageCollection(
02560   DdManager * dd)
02561 {
02562     dd->gcEnabled = 0;
02563 
02564 } /* end of Cudd_DisableGarbageCollection */
02565 
02566 
02580 int
02581 Cudd_DeadAreCounted(
02582   DdManager * dd)
02583 {
02584     return(dd->countDead == 0 ? 1 : 0);
02585 
02586 } /* end of Cudd_DeadAreCounted */
02587 
02588 
02603 void
02604 Cudd_TurnOnCountDead(
02605   DdManager * dd)
02606 {
02607     dd->countDead = 0;
02608 
02609 } /* end of Cudd_TurnOnCountDead */
02610 
02611 
02628 void
02629 Cudd_TurnOffCountDead(
02630   DdManager * dd)
02631 {
02632     dd->countDead = ~0;
02633 
02634 } /* end of Cudd_TurnOffCountDead */
02635 
02636 
02652 int
02653 Cudd_ReadRecomb(
02654   DdManager * dd)
02655 {
02656     return(dd->recomb);
02657 
02658 } /* end of Cudd_ReadRecomb */
02659 
02660 
02677 void
02678 Cudd_SetRecomb(
02679   DdManager * dd,
02680   int  recomb)
02681 {
02682     dd->recomb = recomb;
02683 
02684 } /* end of Cudd_SetRecomb */
02685 
02686 
02705 int
02706 Cudd_ReadSymmviolation(
02707   DdManager * dd)
02708 {
02709     return(dd->symmviolation);
02710 
02711 } /* end of Cudd_ReadSymmviolation */
02712 
02713 
02732 void
02733 Cudd_SetSymmviolation(
02734   DdManager * dd,
02735   int  symmviolation)
02736 {
02737     dd->symmviolation = symmviolation;
02738 
02739 } /* end of Cudd_SetSymmviolation */
02740 
02741 
02759 int
02760 Cudd_ReadArcviolation(
02761   DdManager * dd)
02762 {
02763     return(dd->arcviolation);
02764 
02765 } /* end of Cudd_ReadArcviolation */
02766 
02767 
02785 void
02786 Cudd_SetArcviolation(
02787   DdManager * dd,
02788   int  arcviolation)
02789 {
02790     dd->arcviolation = arcviolation;
02791 
02792 } /* end of Cudd_SetArcviolation */
02793 
02794 
02812 int
02813 Cudd_ReadPopulationSize(
02814   DdManager * dd)
02815 {
02816     return(dd->populationSize);
02817 
02818 } /* end of Cudd_ReadPopulationSize */
02819 
02820 
02838 void
02839 Cudd_SetPopulationSize(
02840   DdManager * dd,
02841   int  populationSize)
02842 {
02843     dd->populationSize = populationSize;
02844 
02845 } /* end of Cudd_SetPopulationSize */
02846 
02847 
02865 int
02866 Cudd_ReadNumberXovers(
02867   DdManager * dd)
02868 {
02869     return(dd->numberXovers);
02870 
02871 } /* end of Cudd_ReadNumberXovers */
02872 
02873 
02891 void
02892 Cudd_SetNumberXovers(
02893   DdManager * dd,
02894   int  numberXovers)
02895 {
02896     dd->numberXovers = numberXovers;
02897 
02898 } /* end of Cudd_SetNumberXovers */
02899 
02911 unsigned long
02912 Cudd_ReadMemoryInUse(
02913   DdManager * dd)
02914 {
02915     return(dd->memused);
02916 
02917 } /* end of Cudd_ReadMemoryInUse */
02918 
02919 
02932 int
02933 Cudd_PrintInfo(
02934   DdManager * dd,
02935   FILE * fp)
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 */
03103 
03104 
03118 long
03119 Cudd_ReadPeakNodeCount(
03120   DdManager * dd)
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 */
03132 
03133 
03147 int
03148 Cudd_ReadPeakLiveNodeCount(
03149   DdManager * dd)
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 */
03159 
03160 
03175 long
03176 Cudd_ReadNodeCount(
03177   DdManager * dd)
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 */
03202 
03203 
03204 
03217 long
03218 Cudd_zddReadNodeCount(
03219   DdManager * dd)
03220 {
03221     return((long)(dd->keysZ - dd->deadZ + 2));
03222 
03223 } /* end of Cudd_zddReadNodeCount */
03224 
03225 
03240 int
03241 Cudd_AddHook(
03242   DdManager * dd,
03243   DD_HFP f,
03244   Cudd_HookType where)
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 */
03287 
03288 
03302 int
03303 Cudd_RemoveHook(
03304   DdManager * dd,
03305   DD_HFP f,
03306   Cudd_HookType where)
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 */
03340 
03341 
03355 int
03356 Cudd_IsInHook(
03357   DdManager * dd,
03358   DD_HFP f,
03359   Cudd_HookType where)
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 */
03389 
03390 
03404 int
03405 Cudd_StdPreReordHook(
03406   DdManager *dd,
03407   const char *str,
03408   void *data)
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 */
03482 
03483 
03497 int
03498 Cudd_StdPostReordHook(
03499   DdManager *dd,
03500   const char *str,
03501   void *data)
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 */
03517 
03518 
03532 int
03533 Cudd_EnableReorderingReporting(
03534   DdManager *dd)
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 */
03545 
03546 
03560 int
03561 Cudd_DisableReorderingReporting(
03562   DdManager *dd)
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 */
03573 
03574 
03587 int
03588 Cudd_ReorderingReporting(
03589   DdManager *dd)
03590 {
03591     return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK));
03592 
03593 } /* end of Cudd_ReorderingReporting */
03594 
03595 
03608 Cudd_ErrorType
03609 Cudd_ReadErrorCode(
03610   DdManager *dd)
03611 {
03612     return(dd->errorCode);
03613 
03614 } /* end of Cudd_ReadErrorCode */
03615 
03616 
03628 void
03629 Cudd_ClearErrorCode(
03630   DdManager *dd)
03631 {
03632     dd->errorCode = CUDD_NO_ERROR;
03633 
03634 } /* end of Cudd_ClearErrorCode */
03635 
03636 
03650 FILE *
03651 Cudd_ReadStdout(
03652   DdManager *dd)
03653 {
03654     return(dd->out);
03655 
03656 } /* end of Cudd_ReadStdout */
03657 
03658 
03670 void
03671 Cudd_SetStdout(
03672   DdManager *dd,
03673   FILE *fp)
03674 {
03675     dd->out = fp;
03676 
03677 } /* end of Cudd_SetStdout */
03678 
03679 
03693 FILE *
03694 Cudd_ReadStderr(
03695   DdManager *dd)
03696 {
03697     return(dd->err);
03698 
03699 } /* end of Cudd_ReadStderr */
03700 
03701 
03713 void
03714 Cudd_SetStderr(
03715   DdManager *dd,
03716   FILE *fp)
03717 {
03718     dd->err = fp;
03719 
03720 } /* end of Cudd_SetStderr */
03721 
03722 
03738 unsigned int
03739 Cudd_ReadNextReordering(
03740   DdManager *dd)
03741 {
03742     return(dd->nextDyn);
03743 
03744 } /* end of Cudd_ReadNextReordering */
03745 
03746 
03762 void
03763 Cudd_SetNextReordering(
03764   DdManager *dd,
03765   unsigned int next)
03766 {
03767     dd->nextDyn = next;
03768 
03769 } /* end of Cudd_SetNextReordering */
03770 
03771 
03783 double
03784 Cudd_ReadSwapSteps(
03785   DdManager *dd)
03786 {
03787 #ifdef DD_COUNT
03788     return(dd->swapSteps);
03789 #else
03790     return(-1);
03791 #endif
03792 
03793 } /* end of Cudd_ReadSwapSteps */
03794 
03795 
03808 unsigned int
03809 Cudd_ReadMaxLive(
03810   DdManager *dd)
03811 {
03812     return(dd->maxLive);
03813 
03814 } /* end of Cudd_ReadMaxLive */
03815 
03816 
03829 void
03830 Cudd_SetMaxLive(
03831   DdManager *dd,
03832   unsigned int maxLive)
03833 {
03834     dd->maxLive = maxLive;
03835 
03836 } /* end of Cudd_SetMaxLive */
03837 
03838 
03851 unsigned long
03852 Cudd_ReadMaxMemory(
03853   DdManager *dd)
03854 {
03855     return(dd->maxmemhard);
03856 
03857 } /* end of Cudd_ReadMaxMemory */
03858 
03859 
03872 void
03873 Cudd_SetMaxMemory(
03874   DdManager *dd,
03875   unsigned long maxMemory)
03876 {
03877     dd->maxmemhard = maxMemory;
03878 
03879 } /* end of Cudd_SetMaxMemory */
03880 
03881 
03895 int
03896 Cudd_bddBindVar(
03897   DdManager *dd /* manager */,
03898   int index /* variable index */)
03899 {
03900     if (index >= dd->size || index < 0) return(0);
03901     dd->subtables[dd->perm[index]].bindVar = 1;
03902     return(1);
03903 
03904 } /* end of Cudd_bddBindVar */
03905 
03906 
03923 int
03924 Cudd_bddUnbindVar(
03925   DdManager *dd /* manager */,
03926   int index /* variable index */)
03927 {
03928     if (index >= dd->size || index < 0) return(0);
03929     dd->subtables[dd->perm[index]].bindVar = 0;
03930     return(1);
03931 
03932 } /* end of Cudd_bddUnbindVar */
03933 
03934 
03950 int
03951 Cudd_bddVarIsBound(
03952   DdManager *dd /* manager */,
03953   int index /* variable index */)
03954 {
03955     if (index >= dd->size || index < 0) return(0);
03956     return(dd->subtables[dd->perm[index]].bindVar);
03957 
03958 } /* end of Cudd_bddVarIsBound */
03959 
03960 
03973 int
03974 Cudd_bddSetPiVar(
03975   DdManager *dd /* manager */,
03976   int index /* variable index */)
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 */
03983 
03984 
03997 int
03998 Cudd_bddSetPsVar(
03999   DdManager *dd /* manager */,
04000   int index /* variable index */)
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 */
04007 
04008 
04021 int
04022 Cudd_bddSetNsVar(
04023   DdManager *dd /* manager */,
04024   int index /* variable index */)
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 */
04031 
04032 
04046 int
04047 Cudd_bddIsPiVar(
04048   DdManager *dd /* manager */,
04049   int index /* variable index */)
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 */
04055 
04056 
04070 int
04071 Cudd_bddIsPsVar(
04072   DdManager *dd,
04073   int index)
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 */
04079 
04080 
04094 int
04095 Cudd_bddIsNsVar(
04096   DdManager *dd,
04097   int index)
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 */
04103 
04104 
04118 int
04119 Cudd_bddSetPairIndex(
04120   DdManager *dd /* manager */,
04121   int index /* variable index */,
04122   int pairIndex /* corresponding variable index */)
04123 {
04124     if (index >= dd->size || index < 0) return(0);
04125     dd->subtables[dd->perm[index]].pairIndex = pairIndex;
04126     return(1);
04127 
04128 } /* end of Cudd_bddSetPairIndex */
04129 
04130 
04144 int
04145 Cudd_bddReadPairIndex(
04146   DdManager *dd,
04147   int index)
04148 {
04149     if (index >= dd->size || index < 0) return -1;
04150     return dd->subtables[dd->perm[index]].pairIndex;
04151 
04152 } /* end of Cudd_bddReadPairIndex */
04153 
04154 
04167 int
04168 Cudd_bddSetVarToBeGrouped(
04169   DdManager *dd,
04170   int index)
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 */
04179 
04180 
04194 int
04195 Cudd_bddSetVarHardGroup(
04196   DdManager *dd,
04197   int index)
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 */
04204 
04205 
04218 int
04219 Cudd_bddResetVarToBeGrouped(
04220   DdManager *dd,
04221   int index)
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 */
04231 
04232 
04245 int
04246 Cudd_bddIsVarToBeGrouped(
04247   DdManager *dd,
04248   int index)
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 */
04257 
04258 
04271 int
04272 Cudd_bddSetVarToBeUngrouped(
04273   DdManager *dd,
04274   int index)
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 */
04281 
04282 
04297 int
04298 Cudd_bddIsVarToBeUngrouped(
04299   DdManager *dd,
04300   int index)
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 */
04306 
04307 
04322 int
04323 Cudd_bddIsVarHardGroup(
04324   DdManager *dd,
04325   int index)
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 */
04333 
04334 
04335 /*---------------------------------------------------------------------------*/
04336 /* Definition of internal functions                                          */
04337 /*---------------------------------------------------------------------------*/
04338 
04339 /*---------------------------------------------------------------------------*/
04340 /* Definition of static functions                                            */
04341 /*---------------------------------------------------------------------------*/
04342 
04343 
04355 static void
04356 fixVarTree(
04357   MtrNode * treenode,
04358   int * perm,
04359   int  size)
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 */
04371 
04372 
04398 static int
04399 addMultiplicityGroups(
04400   DdManager *dd /* manager */,
04401   MtrNode *treenode /* current tree node */,
04402   int multiplicity /* how many ZDD vars per BDD var */,
04403   char *vmask /* variable pairs for which a group has been already built */,
04404   char *lmask /* levels for which a group has already been built*/)
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 */