src/calBdd/calBddManager.c File Reference

#include "calInt.h"

Include dependency graph for calBddManager.c:

Defines
#define	CalBddManagerGetNodeManager(bddManager, id) bddManager->nodeManagerArray[id]
Functions
static void	BddDefaultTransformFn (Cal_BddManager_t bddManager, CalAddress_t value1, CalAddress_t value2, CalAddress_t result1, CalAddress_t *result2, Cal_Pointer_t pointer)
Cal_BddManager	Cal_BddManagerInit (void)
int	Cal_BddManagerQuit (Cal_BddManager bddManager)
void	Cal_BddManagerSetParameters (Cal_BddManager bddManager, long reorderingThreshold, long maxForwardedNodes, double repackAfterGCThreshold, double tableRepackThreshold)
unsigned long	Cal_BddManagerGetNumNodes (Cal_BddManager bddManager)
Cal_Bdd	Cal_BddManagerCreateNewVarFirst (Cal_BddManager bddManager)
Cal_Bdd	Cal_BddManagerCreateNewVarLast (Cal_BddManager bddManager)
Cal_Bdd	Cal_BddManagerCreateNewVarBefore (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd	Cal_BddManagerCreateNewVarAfter (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd	Cal_BddManagerGetVarWithIndex (Cal_BddManager bddManager, Cal_BddIndex_t index)
Cal_Bdd	Cal_BddManagerGetVarWithId (Cal_BddManager bddManager, Cal_BddId_t id)
Cal_Bdd_t	CalBddManagerCreateNewVar (Cal_BddManager_t *bddManager, Cal_BddIndex_t index)
Variables
unsigned long	calPrimes []

Define Documentation

#define CalBddManagerGetNodeManager	(	bddManager,
		id		)	bddManager->nodeManagerArray[id]

Definition at line 115 of file calBddManager.c.

Function Documentation

static void BddDefaultTransformFn	(	Cal_BddManager_t *	bddManager,
		CalAddress_t	value1,
		CalAddress_t	value2,
		CalAddress_t *	result1,
		CalAddress_t *	result2,
		Cal_Pointer_t	pointer
	)			`[static]`

AutomaticStart

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 722 of file calBddManager.c.

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 }

Cal_Bdd Cal_BddManagerCreateNewVarAfter	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Function********************************************************************

Synopsis [Creates and returns a new variable after the specified one in the variable order.]

Description [Creates and returns a new variable after the specified one in the variable order.]

SideEffects [None]

Definition at line 488 of file calBddManager.c.

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 }

Cal_Bdd Cal_BddManagerCreateNewVarBefore	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Function********************************************************************

Synopsis [Creates and returns a new variable before the specified one in the variable order.]

Description [Creates and returns a new variable before the specified one in the variable order.]

SideEffects [None]

Definition at line 461 of file calBddManager.c.

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 }

Cal_Bdd Cal_BddManagerCreateNewVarFirst ( Cal_BddManager bddManager )

Function********************************************************************

Synopsis [Creates and returns a new variable at the start of the variable order.]

Description [Creates and returns a new variable at the start of the variable order.]

SideEffects [None]

Definition at line 421 of file calBddManager.c.

00422 {
00423   return CalBddGetExternalBdd(bddManager, CalBddManagerCreateNewVar(bddManager,
00424                                                         (Cal_BddIndex_t)0));
00425 }

Cal_Bdd Cal_BddManagerCreateNewVarLast ( Cal_BddManager bddManager )

Function********************************************************************

Synopsis [Creates and returns a new variable at the end of the variable order.]

Description [Creates and returns a new variable at the end of the variable order.]

SideEffects [None]

Definition at line 439 of file calBddManager.c.

00440 {
00441   return CalBddGetExternalBdd(bddManager,
00442                               CalBddManagerCreateNewVar(bddManager,
00443                                                         (Cal_BddIndex_t)
00444                                                         bddManager->numVars));
00445 }

unsigned long Cal_BddManagerGetNumNodes ( Cal_BddManager bddManager )

Function********************************************************************

Synopsis [Returns the number of BDD nodes]

Description [Returns the number of BDD nodes]

SideEffects [None]

SeeAlso [Cal_BddTotalSize]

Definition at line 402 of file calBddManager.c.

00403 {
00404   return  bddManager->numNodes;
00405 }

Cal_Bdd Cal_BddManagerGetVarWithId	(	Cal_BddManager	bddManager,
		Cal_BddId_t	id
	)

Function********************************************************************

Synopsis [Returns the variable with the specified id, null if no such variable exists]

Description [Returns the variable with the specified id, null if no such variable exists]

SideEffects [None]

SeeAlso [optional]

Definition at line 539 of file calBddManager.c.

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 }

Cal_Bdd Cal_BddManagerGetVarWithIndex	(	Cal_BddManager	bddManager,
		Cal_BddIndex_t	index
	)

Function********************************************************************

Synopsis [Returns the variable with the specified index, null if no such variable exists]

Description [Returns the variable with the specified index, null if no such variable exists]

SideEffects [None]

Definition at line 515 of file calBddManager.c.

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 }

Cal_BddManager Cal_BddManagerInit ( void )

AutomaticEnd Function********************************************************************

Synopsis [Creates and initializes a new BDD manager.]

Description [Initializes and allocates fields of the BDD manager. Some of the fields are initialized for maxNumVars+1 or numVars+1, whereas some of them are initialized for maxNumVars or numVars. The first kind of fields are associated with the id of a variable and the second ones are with the index of the variable.]

SideEffects [None]

SeeAlso [Cal_BddManagerQuit]

Definition at line 152 of file calBddManager.c.

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 }

int Cal_BddManagerQuit ( Cal_BddManager bddManager )

Function********************************************************************

Synopsis [Frees the BDD manager and all the associated allocations]

Description [Frees the BDD manager and all the associated allocations]

SideEffects [None]

SeeAlso [Cal_BddManagerInit]

Definition at line 307 of file calBddManager.c.

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 }

void Cal_BddManagerSetParameters	(	Cal_BddManager	bddManager,
		long	reorderingThreshold,
		long	maxForwardedNodes,
		double	repackAfterGCThreshold,
		double	tableRepackThreshold
	)

Function********************************************************************

Synopsis [Sets appropriate fields of BDD Manager.]

Description [This function is used to set the parameters which are used to control the reordering process. "reorderingThreshold" determines the number of nodes below which reordering will NOT be invoked, "maxForwardedNodes" determines the maximum number of forwarded nodes which are allowed (at that point the cleanup must be done), and "repackingThreshold" determines the fraction of the page utilized below which repacking has to be invoked. These parameters have different effect on the computational and memory usage aspects of reordeing. For instance, higher value of "maxForwardedNodes" will result in process consuming more memory, and a lower value on the other hand would invoke the cleanup process repeatedly resulting in increased computation.]

SideEffects [Sets appropriate fields of BDD Manager]

SeeAlso []

Definition at line 369 of file calBddManager.c.

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 }

Cal_Bdd_t CalBddManagerCreateNewVar	(	Cal_BddManager_t *	bddManager,
		Cal_BddIndex_t	index
	)

Function********************************************************************

Synopsis [This function creates and returns a new variable with given index value.]

Description [Right now this function does not handle the case when the package is working in multiprocessor mode. We need to put in the necessary code later.]

SideEffects [If the number of variables in the manager exceeds that of value of numMaxVars, then we need to reallocate various fields of the manager. Also depending upon the value of "index", idToIndex and indexToId tables would change.]

Definition at line 567 of file calBddManager.c.

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 }

Variable Documentation

unsigned long calPrimes[]

CFile***********************************************************************

FileName [calBddManager.c]

PackageName [cal]

Synopsis [Routines for maintaing the manager and creating variables etc.]

Description []

SeeAlso [optional]

Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) ]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: calBddManager.c,v 1.9 2002/09/21 20:39:24 fabio Exp

]

Definition at line 59 of file calBddManager.c.

src/calBdd/calBddManager.c File Reference

Defines

Functions

Variables

Define Documentation

Function Documentation

Variable Documentation