glu-2.2: src/calBdd/calBddManager.c Source File

00001 
00041 #include "calInt.h"
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Constant declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 
00047 /*---------------------------------------------------------------------------*/
00048 /* Type declarations                                                         */
00049 /*---------------------------------------------------------------------------*/
00050 
00051 /*---------------------------------------------------------------------------*/
00052 /* Stucture declarations                                                     */
00053 /*---------------------------------------------------------------------------*/
00054 
00055 
00056 /*---------------------------------------------------------------------------*/
00057 /* Variable declarations                                                     */
00058 /*---------------------------------------------------------------------------*/
00059 unsigned long calPrimes[] = 
00060 {
00061   1,
00062   2,
00063   3,
00064   7,
00065   13,
00066   23,
00067   59,
00068   113,
00069   241,
00070   503,
00071   1019,
00072   2039,
00073   4091,
00074   8179,
00075   11587,
00076   16369,
00077   23143,
00078   32749,
00079   46349,
00080   65521,
00081   92683,
00082   131063,
00083   185363,
00084   262139,
00085   330287,
00086   416147,
00087   524269,
00088   660557,
00089   832253,
00090   1048571,
00091   1321109,
00092   1664501,
00093   2097143,
00094   2642201,
00095   3328979,
00096   4194287,
00097   5284393,
00098   6657919,
00099   8388593,
00100   10568797,
00101   13315831,
00102   16777199,
00103   33554393,
00104   67108859,
00105   134217689,
00106   268435399,
00107   536870879,
00108   1073741789,
00109   2147483629
00110 };
00111 
00112 /*---------------------------------------------------------------------------*/
00113 /* Macro declarations                                                        */
00114 /*---------------------------------------------------------------------------*/
00115 #define CalBddManagerGetNodeManager(bddManager, id) \
00116     bddManager->nodeManagerArray[id]
00117 
00118 
00121 /*---------------------------------------------------------------------------*/
00122 /* Static function prototypes                                                */
00123 /*---------------------------------------------------------------------------*/
00124 
00125 static void BddDefaultTransformFn(Cal_BddManager_t * bddManager, CalAddress_t value1, CalAddress_t value2, CalAddress_t * result1, CalAddress_t * result2, Cal_Pointer_t pointer);
00126 #ifdef CALBDDMANAGER
00127 static int CalBddManagerPrint(Cal_BddManager_t *bddManager);
00128 #endif /* CALBDDMANAGER */
00129 
00133 /*---------------------------------------------------------------------------*/
00134 /* Definition of exported functions                                          */
00135 /*---------------------------------------------------------------------------*/
00151 Cal_BddManager
00152 Cal_BddManagerInit(void)
00153 {
00154   Cal_BddManager_t *bddManager;
00155   int i;
00156   CalBddNode_t *bddNode;
00157   Cal_Bdd_t resultBdd;
00158   
00159     
00160   bddManager = Cal_MemAlloc(Cal_BddManager_t, 1);
00161 
00162   bddManager->numVars = 0;
00163 
00164   bddManager->maxNumVars = 30;
00165   
00166   bddManager->varBdds = Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1);
00167   
00168   bddManager->pageManager1 = CalPageManagerInit(4);
00169   bddManager->pageManager2 = CalPageManagerInit(NUM_PAGES_PER_SEGMENT);
00170 
00171   bddManager->nodeManagerArray = Cal_MemAlloc(CalNodeManager_t*, bddManager->maxNumVars+1);
00172 
00173   bddManager->nodeManagerArray[0] = CalNodeManagerInit(bddManager->pageManager1);
00174   bddManager->uniqueTable = Cal_MemAlloc(CalHashTable_t *,
00175                                          bddManager->maxNumVars+1);
00176   bddManager->uniqueTable[0] = CalHashTableInit(bddManager, 0);
00177   
00178   /* Constant One */
00179   CalBddPutBddId(bddManager->bddOne, CAL_BDD_CONST_ID);
00180   CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], bddNode);
00181   CalBddPutBddNode(bddManager->bddOne, bddNode);
00182   /* ~0x0 put so that the node is not mistaken for forwarded node */
00183   CalBddPutThenBddNode(bddManager->bddOne, (CalBddNode_t *)~0x0);
00184   CalBddPutElseBddNode(bddManager->bddOne, (CalBddNode_t *)~0x0);
00185   CalBddPutRefCount(bddManager->bddOne, CAL_MAX_REF_COUNT);
00186   CalBddNot(bddManager->bddOne, bddManager->bddZero);
00187 
00188   /* Create a user BDD */
00189   CalHashTableAddDirectAux(bddManager->uniqueTable[0], bddManager->bddOne,
00190                            bddManager->bddOne, &resultBdd);
00191   CalBddPutRefCount(resultBdd, CAL_MAX_REF_COUNT);
00192   bddManager->userOneBdd =  CalBddGetBddNode(resultBdd);
00193   bddManager->userZeroBdd = CalBddNodeNot(bddManager->userOneBdd);
00194   
00195   /* Null BDD */
00196   CalBddPutBddId(bddManager->bddNull, CAL_BDD_NULL_ID);
00197   CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], bddNode);
00198   CalBddPutBddNode(bddManager->bddNull, bddNode);
00199   /* ~0x10 put so that the node is not mistaken for forwarded node or
00200      the constant nodes. */
00201   CalBddPutThenBddNode(bddManager->bddNull, (CalBddNode_t *)~0x10);
00202   CalBddPutElseBddNode(bddManager->bddNull, (CalBddNode_t *)~0x10);
00203   CalBddPutRefCount(bddManager->bddNull, CAL_MAX_REF_COUNT);
00204   /* Put in the unique table, so that it gets locked */
00205   /*CalHashTableAddDirect(bddManager->uniqueTable[0], bddNode);*/
00206 
00207   bddManager->indexToId = Cal_MemAlloc(Cal_BddId_t, bddManager->maxNumVars);
00208   bddManager->idToIndex = Cal_MemAlloc(Cal_BddIndex_t, bddManager->maxNumVars+1);
00209   bddManager->idToIndex[CAL_BDD_CONST_ID] = CAL_BDD_CONST_INDEX;
00210 
00211   bddManager->depth = DEFAULT_DEPTH;
00212   bddManager->maxDepth = DEFAULT_MAX_DEPTH;
00213   bddManager->pipelineState = READY;
00214   bddManager->pipelineDepth = PIPELINE_EXECUTION_DEPTH;
00215   bddManager->currentPipelineDepth = 0;
00216   bddManager->pipelineFn = CalOpAnd;
00217 
00218 
00219   bddManager->reqQue = Cal_MemAlloc(CalHashTable_t **, bddManager->maxDepth);
00220   bddManager->cacheTable = CalCacheTableTwoInit(bddManager);
00221   
00222   for (i=0; i < bddManager->maxDepth; i++){
00223     bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *,
00224                                          bddManager->maxNumVars+1);
00225     bddManager->reqQue[i][0] = CalHashTableInit(bddManager, 0);
00226   }
00227 
00228   bddManager->requestNodeListArray = Cal_MemAlloc(CalRequestNode_t*,
00229                                                   MAX_INSERT_DEPTH);
00230   for(i = 0; i < MAX_INSERT_DEPTH; i++){
00231     bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
00232   }
00233   bddManager->userProvisionalNodeList = Cal_Nil(CalRequestNode_t);
00234 
00235   /* Garbage collection related information */
00236   bddManager->numNodes = bddManager->numPeakNodes = 1;
00237   bddManager->numNodesFreed = 0;
00238   bddManager->gcCheck = CAL_GC_CHECK;
00239   bddManager->uniqueTableGCLimit =  CAL_MIN_GC_LIMIT;
00240   bddManager->numGC = 0;
00241   bddManager->gcMode = 1;
00242   bddManager->nodeLimit = 0;
00243   bddManager->overflow = 0;
00244   bddManager->repackAfterGCThreshold = CAL_REPACK_AFTER_GC_THRESHOLD;
00245   
00246 
00247   /* Special functions */
00248   bddManager->TransformFn = BddDefaultTransformFn;
00249   bddManager->transformEnv = 0;
00250 
00251 
00252   /* Association related information */
00253   bddManager->associationList = Cal_Nil(CalAssociation_t);
00254   /*bddManager->tempAssociation = CAL_BDD_NEW_REC(bddManager, CalAssociation_t);*/
00255   bddManager->tempAssociation = Cal_MemAlloc(CalAssociation_t, 1);
00256   bddManager->tempAssociation->id = -1;
00257   bddManager->tempAssociation->lastBddIndex = -1;
00258   bddManager->tempAssociation->varAssociation =
00259       Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1);
00260   for(i = 0; i < bddManager->maxNumVars+1; i++){
00261      bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
00262   }
00263   bddManager->tempOpCode = -1;
00264   bddManager->currentAssociation = bddManager->tempAssociation;
00265 
00266   /* BDD reordering related information */
00267   bddManager->dynamicReorderingEnableFlag = 1;
00268   bddManager->reorderMethod = CAL_REORDER_METHOD_DF;
00269   bddManager->reorderTechnique = CAL_REORDER_NONE;
00270   bddManager->numForwardedNodes = 0;
00271   bddManager->numReorderings = 0;
00272   bddManager->maxNumVarsSiftedPerReordering = 1000;
00273   bddManager->maxNumSwapsPerReordering = 2000000;
00274   bddManager->numSwaps = 0;
00275   bddManager->numTrivialSwaps = 0;
00276   bddManager->maxSiftingGrowth = 2.0;
00277   bddManager->reorderingThreshold = CAL_BDD_REORDER_THRESHOLD;
00278   bddManager->maxForwardedNodes = CAL_NUM_FORWARDED_NODES_LIMIT;
00279   bddManager->tableRepackThreshold = CAL_TABLE_REPACK_THRESHOLD;
00280   
00281 
00282   /*bddManager->superBlock = CAL_BDD_NEW_REC(bddManager, Cal_Block_t);*/
00283   bddManager->superBlock = Cal_MemAlloc(Cal_Block_t, 1);
00284   bddManager->superBlock->numChildren=0;
00285   bddManager->superBlock->children=0;
00286   bddManager->superBlock->reorderable=1;
00287   bddManager->superBlock->firstIndex= -1;
00288   bddManager->superBlock->lastIndex=0;
00289   
00290   bddManager->hooks = Cal_Nil(void);
00291   
00292   return bddManager;
00293 }
00294 
00306 int
00307 Cal_BddManagerQuit(Cal_BddManager bddManager)
00308 {
00309   int i, j;
00310 
00311   if(bddManager == Cal_Nil(Cal_BddManager_t)) return 1;
00312 
00313   for (i=0; i < bddManager->maxDepth; i++){
00314     for (j=0; j <= bddManager->numVars; j++){
00315       CalHashTableQuit(bddManager, bddManager->reqQue[i][j]);
00316     }
00317     Cal_MemFree(bddManager->reqQue[i]);
00318   }
00319   
00320   for (i=0; i <= bddManager->numVars; i++){
00321     CalHashTableQuit(bddManager, bddManager->uniqueTable[i]);
00322     CalNodeManagerQuit(bddManager->nodeManagerArray[i]);
00323   }
00324 
00325   CalCacheTableTwoQuit(bddManager->cacheTable);
00326   Cal_MemFree(bddManager->tempAssociation->varAssociation);
00327   /*CAL_BDD_FREE_REC(bddManager, bddManager->tempAssociation, CalAssociation_t);*/
00328   Cal_MemFree(bddManager->tempAssociation);
00329   /*CAL_BDD_FREE_REC(bddManager, bddManager->superBlock, Cal_Block_t);*/
00330   CalFreeBlockRecursively(bddManager->superBlock);
00331   CalAssociationListFree(bddManager);
00332   Cal_MemFree(bddManager->varBdds);
00333   Cal_MemFree(bddManager->indexToId);
00334   Cal_MemFree(bddManager->idToIndex);
00335   Cal_MemFree(bddManager->uniqueTable);
00336   Cal_MemFree(bddManager->reqQue);
00337   Cal_MemFree(bddManager->requestNodeListArray);
00338   Cal_MemFree(bddManager->nodeManagerArray);
00339   CalPageManagerQuit(bddManager->pageManager1);
00340   CalPageManagerQuit(bddManager->pageManager2);
00341   Cal_MemFree(bddManager);
00342 
00343   return 0;
00344 }
00345 
00368 void
00369 Cal_BddManagerSetParameters(Cal_BddManager bddManager,
00370                             long reorderingThreshold,
00371                             long maxForwardedNodes,
00372                             double repackAfterGCThreshold,
00373                             double tableRepackThreshold)
00374 {
00375   if (reorderingThreshold >= 0){
00376     bddManager->reorderingThreshold = reorderingThreshold;
00377   }
00378   if (maxForwardedNodes >= 0){
00379     bddManager->maxForwardedNodes = maxForwardedNodes;
00380   }
00381   if (repackAfterGCThreshold >= 0.0){
00382     bddManager->repackAfterGCThreshold = (float) repackAfterGCThreshold;
00383   }
00384   if (tableRepackThreshold >= 0.0){
00385     bddManager->tableRepackThreshold = (float) tableRepackThreshold;
00386   }
00387 }
00388 
00389 
00401 unsigned long
00402 Cal_BddManagerGetNumNodes(Cal_BddManager bddManager)
00403 {
00404   return  bddManager->numNodes;
00405 }
00406 
00407 
00408 
00420 Cal_Bdd
00421 Cal_BddManagerCreateNewVarFirst(Cal_BddManager bddManager)
00422 {
00423   return CalBddGetExternalBdd(bddManager, CalBddManagerCreateNewVar(bddManager,
00424                                                         (Cal_BddIndex_t)0));
00425 }
00426 
00438 Cal_Bdd
00439 Cal_BddManagerCreateNewVarLast(Cal_BddManager bddManager)
00440 {
00441   return CalBddGetExternalBdd(bddManager,
00442                               CalBddManagerCreateNewVar(bddManager,
00443                                                         (Cal_BddIndex_t)
00444                                                         bddManager->numVars));
00445 }
00446 
00447 
00448 
00460 Cal_Bdd
00461 Cal_BddManagerCreateNewVarBefore(Cal_BddManager bddManager,
00462                                  Cal_Bdd userBdd)
00463 {
00464   Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, userBdd);
00465   if (CalBddIsBddConst(calBdd)){
00466     return Cal_BddManagerCreateNewVarLast(bddManager);
00467   }
00468   else{
00469     return CalBddGetExternalBdd(bddManager,
00470                                 CalBddManagerCreateNewVar(bddManager,
00471                                                           CalBddGetBddIndex(bddManager, 
00472                                                   calBdd)));
00473   }
00474 }
00475 
00487 Cal_Bdd
00488 Cal_BddManagerCreateNewVarAfter(Cal_BddManager bddManager,
00489                                 Cal_Bdd userBdd)
00490 {
00491   Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, userBdd);
00492   if (CalBddIsBddConst(calBdd)){
00493     return Cal_BddManagerCreateNewVarLast(bddManager);
00494   }
00495   else{
00496     return CalBddGetExternalBdd(bddManager,
00497                                 CalBddManagerCreateNewVar(bddManager,
00498                                                           CalBddGetBddIndex(bddManager, calBdd)+1));
00499   }
00500 }
00501 
00502 
00514 Cal_Bdd
00515 Cal_BddManagerGetVarWithIndex(Cal_BddManager bddManager, Cal_BddIndex_t  index)
00516 {
00517   if (index >= bddManager->numVars){
00518     CalBddWarningMessage("Index out of range");
00519     return (Cal_Bdd) 0;
00520   }
00521   return CalBddGetExternalBdd(bddManager,
00522                               bddManager->varBdds[bddManager->indexToId[index]]); 
00523 }
00524 
00538 Cal_Bdd
00539 Cal_BddManagerGetVarWithId(Cal_BddManager bddManager,  Cal_BddId_t  id)
00540 {
00541   if (id <= 0 || id > bddManager->numVars){
00542     CalBddWarningMessage("Id out of range");
00543     return (Cal_Bdd) 0;
00544   }
00545   return CalBddGetExternalBdd(bddManager, bddManager->varBdds[id]);
00546 }
00547 
00548 /*---------------------------------------------------------------------------*/
00549 /* Definition of internal functions                                          */
00550 /*---------------------------------------------------------------------------*/
00566 Cal_Bdd_t
00567 CalBddManagerCreateNewVar(Cal_BddManager_t * bddManager, Cal_BddIndex_t  index)
00568 {
00569   Cal_Bdd_t calBdd;
00570   Cal_BddId_t varId;
00571   int totalNumVars, maxNumVars, i;
00572   CalAssociation_t *association;
00573   
00574   if (bddManager->numVars == CAL_MAX_VAR_ID){
00575     CalBddFatalMessage("Cannot create any new variable, no more Id left."); 
00576   }
00577 
00578   /*
00579    * Get the total number of variables. If the index is more than the total
00580    * number of variables, then report error.
00581    */
00582   totalNumVars = bddManager->numVars;
00583   
00584   if (index > totalNumVars){
00585     CalBddFatalMessage("The variable index out of range");
00586   }
00587   
00588 
00589   /*
00590    * Create a new variable in the manager which contains this index.
00591    * This might lead to change in the id->index, and index->id
00592    * for other managers.
00593    */
00594 
00595   /*
00596    * If the number of variables is equal to the maximum number of variables
00597    * then reallocate memory.
00598    */
00599   if (bddManager->numVars == bddManager->maxNumVars){
00600     int oldMaxNumVars;
00601     CalAssociation_t *p;
00602     
00603     oldMaxNumVars = bddManager->maxNumVars;
00604     if ((maxNumVars = 2*oldMaxNumVars) > CAL_MAX_VAR_ID){
00605       maxNumVars = CAL_MAX_VAR_ID;
00606     }
00607     bddManager->maxNumVars = maxNumVars;
00608     bddManager->varBdds = Cal_MemRealloc(Cal_Bdd_t,
00609                                          bddManager->varBdds, maxNumVars+1); 
00610     
00611     bddManager->nodeManagerArray = Cal_MemRealloc(CalNodeManager_t *,
00612                                                   bddManager->nodeManagerArray, 
00613                                                   maxNumVars+1);
00614 
00615     bddManager->idToIndex = Cal_MemRealloc(Cal_BddIndex_t, bddManager->idToIndex,
00616                                         maxNumVars+1);
00617 
00618     bddManager->indexToId = Cal_MemRealloc(Cal_BddIndex_t, bddManager->indexToId,
00619                                         maxNumVars);
00620 
00621     bddManager->uniqueTable = Cal_MemRealloc(CalHashTable_t *,
00622                                           bddManager->uniqueTable, maxNumVars+1);
00623     
00624     for (i=0; i<bddManager->maxDepth; i++){
00625       bddManager->reqQue[i] = Cal_MemRealloc(CalHashTable_t *, bddManager->reqQue[i],
00626                                           maxNumVars+1);
00627     }
00628     bddManager->tempAssociation->varAssociation = 
00629         Cal_MemRealloc(Cal_Bdd_t, bddManager->tempAssociation->varAssociation,
00630         maxNumVars+1);
00631     /* CHECK LOOP INDICES */
00632     for(i = oldMaxNumVars+1; i < maxNumVars+1; i++){
00633       bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
00634     }
00635     for(p = bddManager->associationList; p; p = p->next){
00636       p->varAssociation = 
00637           Cal_MemRealloc(Cal_Bdd_t, p->varAssociation, maxNumVars+1);
00638       /* CHECK LOOP INDICES */
00639       for(i = oldMaxNumVars+1; i < maxNumVars+1; i++){
00640         p->varAssociation[i] = bddManager->bddNull;
00641       }
00642     }
00643   }
00644 
00645   /* If the variable has been created in the middle, shift the indices. */
00646   if (index != bddManager->numVars){
00647     for (i=0; i<bddManager->numVars; i++){
00648       if (bddManager->idToIndex[i+1] >= index){
00649         bddManager->idToIndex[i+1]++;
00650       }
00651     }
00652   }
00653 
00654   /* Fix indexToId table */
00655   for (i=bddManager->numVars; i>index; i--){
00656     bddManager->indexToId[i] = bddManager->indexToId[i-1];
00657   }
00658 
00659   for(association = bddManager->associationList; association;
00660                                               association =
00661                                                   association->next){
00662     if (association->lastBddIndex >= index){
00663       association->lastBddIndex++;
00664     }
00665   }
00666   if (bddManager->tempAssociation->lastBddIndex >= index){
00667     bddManager->tempAssociation->lastBddIndex++;
00668   }
00669   
00670   bddManager->numVars++;
00671   varId = bddManager->numVars;
00672 
00673   bddManager->idToIndex[varId] = index;
00674   bddManager->indexToId[index] = varId;
00675   
00676   bddManager->nodeManagerArray[varId] =
00677       CalNodeManagerInit(bddManager->pageManager2); 
00678   bddManager->uniqueTable[varId] =
00679       CalHashTableInit(bddManager, varId);
00680     
00681   /* insert node in the uniqueTableForId */
00682   CalHashTableAddDirectAux(bddManager->uniqueTable[varId],
00683                            bddManager->bddOne, bddManager->bddZero, &calBdd);
00684   CalBddPutRefCount(calBdd, CAL_MAX_REF_COUNT);
00685   bddManager->varBdds[varId] = calBdd;
00686 
00687   bddManager->numNodes++;
00688   
00689 #ifdef __OLD__
00690   /* initialize req_que_for_id */
00691   bddManager->reqQue[varId] = Cal_MemAlloc(CalHashTable_t*, bddManager->maxDepth);
00692   for (i=0; i<manager->maxDepth; i++){
00693     bddManager->reqQue[varId][i] = CalHashTableInit(bddManager, varId);
00694   }
00695 #endif
00696   
00697   /* initialize req_que_for_id */
00698   for (i=0; i<bddManager->maxDepth; i++){
00699     bddManager->reqQue[i][varId] =
00700         CalHashTableInit(bddManager, varId);
00701   }
00702   CalBddShiftBlock(bddManager, bddManager->superBlock, (long)index);
00703   return calBdd;
00704 }
00705 
00706   
00707 /*---------------------------------------------------------------------------*/
00708 /* Definition of static functions                                            */
00709 /*---------------------------------------------------------------------------*/
00721 static void
00722 BddDefaultTransformFn(
00723   Cal_BddManager_t * bddManager,
00724   CalAddress_t  value1,
00725   CalAddress_t  value2,
00726   CalAddress_t * result1,
00727   CalAddress_t * result2,
00728   Cal_Pointer_t  pointer)
00729 {
00730   if (!value2)
00731     /* Will be a carry when taking 2's complement of value2.  Thus, */
00732     /* take 2's complement of high part. */
00733     value1= -(long)value1;
00734   else
00735     {
00736       value2= -(long)value2;
00737       value1= ~value1;
00738     }
00739   *result1=value1;
00740   *result2=value2;
00741 }
00742 
00743 #ifdef CALBDDMANAGER
00744 
00756 static int
00757 CalBddManagerPrint(Cal_BddManager_t *bddManager)
00758 {
00759   int i;
00760   CalHashTable_t *uniqueTableForId;
00761   printf("#####################   BDD MANAGER   #####################\n");
00762   for(i = 1; i < bddManager->numVars; i++){
00763     uniqueTableForId = bddManager->uniqueTable[i];
00764     CalHashTablePrint(uniqueTableForId);
00765   }
00766   fflush(stdout);
00767   return 0;
00768 }
00769 
00770 
00771 main(argc, argv)
00772 int argc;
00773 char **argv;
00774 {
00775         Cal_Bdd_t n;
00776         Cal_BddManager_t *manager;
00777 
00778         manager = CalBddManagerInit(argc, argv);
00779         n = CalBddManagerCreateVariable(bddManager);
00780         CalBddFunctionPrint(n);
00781         n = CalBddManagerGetVariable(bddManager, 0);
00782         CalBddFunctionPrint(n);
00783 }
00784 #endif /* CALBDDMANAGER */
00785 
00786 #ifdef __GC__
00787 main(argc, argv)
00788 int argc;
00789 char **argv;
00790 {
00791   Cal_BddManager_t *manager;
00792   Cal_Bdd_t vars[256];
00793   Cal_Bdd_t function, tempFunction;
00794   int i;
00795   int numVars;
00796   
00797   if (argc >= 2)
00798         numVars = atoi(argv[1]);
00799   else
00800     numVars = 3;
00801   
00802   manager = Cal_BddManagerInit();
00803   
00804   for (i = 0; i < numVars; i++){
00805     vars[i] = Cal_BddManagerCreateNewVarLast(bddManager);
00806   }
00807   
00808   function = vars[0];
00809   for (i = 1; i < numVars - 1; i++){
00810     tempFunction = Cal_BddITE(bddManager, vars[i], vars[i+1], function);
00811     Cal_BddFree(function);
00812     function = tempFunction;
00813             /*fprintf(stdout, "i = %d\n", i);
00814               unique_table_write(stdout, CalBddManager->unique_table);
00815               */
00816   }
00817   fprintf(stdout, "\n******************Before Free****************\n");
00818   for (i = 1; i <= numVars; i++){
00819     CalHashTablePrint(bddManager->uniqueTable[i]);
00820   }
00821   Cal_BddFree(function);
00822   fprintf(stdout, "\n****************After Free****************\n");
00823   for (i = 1; i <= numVars; i++){
00824     CalHashTablePrint(bddManager->uniqueTable[i]);
00825   }
00826   Cal_BddManagerGC(bddManager);
00827   fprintf(stdout, "\n****************After GC****************\n");
00828   for (i = 1; i <= numVars; i++){
00829     CalHashTablePrint(bddManager->uniqueTable[i]);
00830   }
00831 }
00832 #endif