src/calBdd/calReorderDF.c File Reference

#include "calInt.h"
Include dependency graph for calReorderDF.c:

Go to the source code of this file.

Defines

#define BddNodeIcrRefCount(f)
#define BddNodeDcrRefCount(f)
#define BddGetCofactors(bddManager, f, id, fThen, fElse)
#define BddNodeGetThenBddNode(bddNode)
#define BddNodeGetElseBddNode(bddNode)

Functions

static int UniqueTableForIdFindOrAdd (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalBddNode_t *thenBdd, CalBddNode_t *elseBdd, CalBddNode_t **bddPtr)
static void HashTableAddDirect (CalHashTable_t *hashTable, CalBddNode_t *bddNode)
static int HashTableFindOrAdd (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalBddNode_t *thenBdd, CalBddNode_t *elseBdd, CalBddNode_t **bddPtr)
static void BddConvertDataStruct (Cal_BddManager_t *bddManager)
static void BddConvertDataStructBack (Cal_BddManager_t *bddManager)
static void BddReallocateNodes (Cal_BddManager_t *bddManager)
static void BddExchangeAux (Cal_BddManager_t *bddManager, CalBddNode_t *f, int id, int nextId)
static int CheckValidityOfNodes (Cal_BddManager_t *bddManager, long id)
static void SweepVarTable (Cal_BddManager_t *bddManager, long id)
static void BddExchange (Cal_BddManager_t *bddManager, long id)
static void BddExchangeVarBlocks (Cal_BddManager_t *bddManager, Cal_Block parent, long blockIndex)
static int BddReorderWindow2 (Cal_BddManager_t *bddManager, Cal_Block block, long i)
static int BddReorderWindow3 (Cal_BddManager_t *bddManager, Cal_Block block, long i)
static void BddReorderStableWindow3Aux (Cal_BddManager_t *bddManager, Cal_Block block, char *levels)
static void BddReorderStableWindow3 (Cal_BddManager_t *bddManager)
static void BddSiftBlock (Cal_BddManager_t *bddManager, Cal_Block block, long startPosition, double maxSizeFactor)
static void BddReorderSiftAux (Cal_BddManager_t *bddManager, Cal_Block block, Cal_Block *toSift, double maxSizeFactor)
static void BddReorderSift (Cal_BddManager_t *bddManager, double maxSizeFactor)
static int CeilLog2 (int number)
void CalBddReorderAuxDF (Cal_BddManager_t *bddManager)
static void NodeManagerAllocNode (Cal_BddManager_t *bddManager, CalBddNode_t **nodePtr)

Variables

static CalNodeManager_t * nodeManager
static int freeListId

Define Documentation

#define BddGetCofactors ( bddManager,
f,
id,
fThen,
fElse   ) 
Value:
{                                                                       \
  CalBddNode_t *_bddNode = CAL_BDD_POINTER(f);                          \
  Cal_Assert(bddManager->idToIndex[_bddNode->thenBddId] <=              \
             bddManager->idToIndex[id]);                                \
  if (bddManager->idToIndex[_bddNode->thenBddId] ==                     \
      bddManager->idToIndex[id]){                                       \
    fThen = _bddNode->thenBddNode;                                      \
    fElse = _bddNode->elseBddNode;                                      \
  }                                                                     \
  else{                                                                 \
    fThen = fElse = f;                                                  \
  }                                                                     \
}

Definition at line 92 of file calReorderDF.c.

#define BddNodeDcrRefCount ( f   ) 
Value:
{ \
  CalBddNode_t *_bddNode = CAL_BDD_POINTER(f); \
  if ((_bddNode->elseBddId < CAL_MAX_REF_COUNT) && (_bddNode->elseBddId)){ \
    _bddNode->elseBddId--; \
  } \
  else if (_bddNode->elseBddId == 0){ \
    CalBddWarningMessage("Trying to decrement reference count below zero"); \
  } \
}

Definition at line 81 of file calReorderDF.c.

#define BddNodeGetElseBddNode ( bddNode   ) 
Value:
((CalBddNode_t*) ((CalAddress_t)                          \
                  (CAL_BDD_POINTER(bddNode)->elseBddNode) \
                  ^ (CAL_TAG0(bddNode))))

Definition at line 112 of file calReorderDF.c.

#define BddNodeGetThenBddNode ( bddNode   ) 
Value:
((CalBddNode_t*) ((CalAddress_t)                          \
                  (CAL_BDD_POINTER(bddNode)->thenBddNode) \
                  ^ (CAL_TAG0(bddNode))))

Definition at line 107 of file calReorderDF.c.

#define BddNodeIcrRefCount ( f   ) 
Value:
{                                               \
  CalBddNode_t *_bddNode = CAL_BDD_POINTER(f);  \
  if (_bddNode->elseBddId < CAL_MAX_REF_COUNT){ \
    _bddNode->elseBddId++;                      \
  }                                             \
}

Definition at line 73 of file calReorderDF.c.

Function Documentation

static void BddConvertDataStruct ( Cal_BddManager_t *  bddManager  )  [static]

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

Synopsis [Changes the data structure of the bdd nodes.]

Description [New data structure: thenBddId -> id elseBddId -> ref count]

SideEffects [required]

SeeAlso [optional]

Definition at line 376 of file calReorderDF.c.

00377 {
00378   CalBddNode_t *bddNode, *thenBddNode, *elseBddNode,
00379       *next = Cal_Nil(CalBddNode_t); 
00380   CalBddNode_t *last;
00381   long numBins;
00382   int i, refCount, id, index;
00383   long oldNumEntries;
00384   CalHashTable_t *uniqueTableForId;
00385 
00386   if (bddManager->numPeakNodes < bddManager->numNodes){
00387     bddManager->numPeakNodes = bddManager->numNodes;
00388   }
00389 
00390   for(index = 0; index < bddManager->numVars; index++){
00391     id = bddManager->indexToId[index];
00392     uniqueTableForId = bddManager->uniqueTable[id];
00393     oldNumEntries = uniqueTableForId->numEntries;
00394     numBins = uniqueTableForId->numBins;
00395     for(i = 0; i < numBins; i++){
00396       last = NULL;
00397       bddNode = uniqueTableForId->bins[i];
00398       while(bddNode != Cal_Nil(CalBddNode_t)){
00399         next = CalBddNodeGetNextBddNode(bddNode);
00400         CalBddNodeGetRefCount(bddNode, refCount);
00401         thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00402         elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00403         if(refCount == 0){
00404           if (last == NULL){
00405             uniqueTableForId->bins[i] = next;
00406           }
00407           else{
00408             last->nextBddNode = next;
00409           }
00410           CalBddNodeDcrRefCount(CAL_BDD_POINTER(thenBddNode));
00411           CalBddNodeDcrRefCount(CAL_BDD_POINTER(elseBddNode));
00412           CalNodeManagerFreeNode(nodeManager, bddNode);
00413           uniqueTableForId->numEntries--;
00414         }
00415         else {
00416           bddNode->thenBddId = id;
00417           bddNode->elseBddId = refCount;
00418           bddNode->nextBddNode = next;
00419           bddNode->thenBddNode = thenBddNode;
00420           bddNode->elseBddNode = elseBddNode;
00421           last = bddNode; 
00422         }
00423         bddNode = next;
00424       }
00425     }
00426     if ((uniqueTableForId->numBins > uniqueTableForId->numEntries) &&
00427         (uniqueTableForId->sizeIndex > HASH_TABLE_DEFAULT_SIZE_INDEX)){
00428       CalHashTableRehash(uniqueTableForId, 0);
00429     }
00430     bddManager->numNodes -= oldNumEntries - uniqueTableForId->numEntries;
00431     bddManager->numNodesFreed += oldNumEntries - uniqueTableForId->numEntries;
00432   }
00433   id = 0;
00434   uniqueTableForId = bddManager->uniqueTable[id];
00435   numBins = uniqueTableForId->numBins;
00436   for(i = 0; i < numBins; i++){
00437     bddNode = uniqueTableForId->bins[i];
00438     while(bddNode != Cal_Nil(CalBddNode_t)){
00439       next = CalBddNodeGetNextBddNode(bddNode);
00440       CalBddNodeGetRefCount(bddNode, refCount);
00441       Cal_Assert(refCount);
00442       thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00443       elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00444       bddNode->thenBddId = id;
00445       bddNode->elseBddId = refCount;
00446       bddNode->nextBddNode = next;
00447       bddNode->thenBddNode = thenBddNode;
00448       bddNode->elseBddNode = elseBddNode;
00449       bddNode = next;
00450     }
00451   }
00452   bddNode = bddManager->bddOne.bddNode;
00453   CalBddNodeGetRefCount(bddNode, refCount);
00454   Cal_Assert(refCount);
00455   thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00456   elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00457   bddNode->thenBddId = id;
00458   bddNode->elseBddId = refCount;
00459   bddNode->nextBddNode = next;
00460   bddNode->thenBddNode = thenBddNode;
00461   bddNode->elseBddNode = elseBddNode;
00462 }

static void BddConvertDataStructBack ( Cal_BddManager_t *  bddManager  )  [static]

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

Synopsis [Changes the data structure of the bdd nodes to the original one.]

Description [Data structure conversion: thenBddId -> id elseBddId -> ref count] SideEffects [required]

SeeAlso [optional]

Definition at line 478 of file calReorderDF.c.

00479 {
00480   Cal_Bdd_t thenBdd, elseBdd;
00481   
00482   CalBddNode_t *bddNode, *nextBddNode, **bins;
00483   long numBins;
00484   int i, id, index;
00485   CalHashTable_t *uniqueTableForId;
00486   uniqueTableForId = bddManager->uniqueTable[0];
00487   numBins = uniqueTableForId->numBins;
00488   bins = uniqueTableForId->bins;
00489   for(i = 0; i < numBins; i++) {
00490     for(bddNode = bins[i];
00491         bddNode != Cal_Nil(CalBddNode_t);
00492         bddNode = nextBddNode) {
00493       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00494       CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
00495       bddNode->thenBddId = CAL_BDD_POINTER(bddNode->thenBddNode)->thenBddId;
00496       bddNode->elseBddId = CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId;
00497     }
00498   }
00499   for(index = 0; index < bddManager->numVars; index++){
00500     id = bddManager->indexToId[index];
00501     uniqueTableForId = bddManager->uniqueTable[id];
00502     numBins = uniqueTableForId->numBins;
00503     bins = uniqueTableForId->bins;
00504     for(i = 0; i < numBins; i++) {
00505       for(bddNode = bins[i];
00506           bddNode != Cal_Nil(CalBddNode_t);
00507           bddNode = nextBddNode) {
00508         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00509         CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
00510         bddNode->thenBddId = CAL_BDD_POINTER(bddNode->thenBddNode)->thenBddId;
00511         bddNode->elseBddId = CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId;
00512       Cal_Assert(!CalBddNodeIsForwarded(bddNode));
00513       Cal_Assert(!CalBddNodeIsRefCountZero(bddNode));
00514       CalBddNodeGetThenBdd(bddNode, thenBdd);
00515       CalBddNodeGetElseBdd(bddNode, elseBdd);
00516       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00517       Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00518       }
00519     }
00520   }
00521   bddNode = bddManager->bddOne.bddNode;
00522   CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
00523   bddNode->thenBddId = 0;
00524   bddNode->elseBddId = 0;
00525 }

static void BddExchange ( Cal_BddManager_t *  bddManager,
long  id 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1065 of file calReorderDF.c.

01066 {
01067   Cal_BddId_t  nextId;
01068   CalBddNode_t **ptr, *bddNode, *nodeList;
01069   CalHashTable_t *table, *nextTable;
01070   Cal_BddIndex_t index, nextIndex;
01071   int i;
01072   CalBddNode_t  *f1, *f2;
01073   CalAssociation_t *p;
01074   CalNodeManager_t *nodeManager;
01075   
01076   index = bddManager->idToIndex[id];
01077   nextIndex = index+1;
01078   nextId = bddManager->indexToId[nextIndex];
01079 
01080   if (CalTestInteract(bddManager, id, nextId)){
01081     bddManager->numSwaps++;
01082     nodeManager = bddManager->nodeManagerArray[id];
01083     table = bddManager->uniqueTable[id];
01084     nextTable = bddManager->uniqueTable[nextId];
01085     nodeList = (CalBddNode_t*)0;
01086     for(i = 0; i < table->numBins; i++){
01087       for (ptr = &table->bins[i], bddNode = *ptr; bddNode;
01088            bddNode = *ptr){
01089         Cal_Assert(bddNode->elseBddId != 0);
01090         f1 = bddNode->elseBddNode;
01091         f2 = bddNode->thenBddNode;
01092         if ((CAL_BDD_POINTER(f1)->thenBddId != nextId) &&
01093             (CAL_BDD_POINTER(f2)->thenBddId != nextId)){ 
01094           ptr = &bddNode->nextBddNode;
01095         }
01096         else{
01097           *ptr = bddNode->nextBddNode;
01098           bddNode->nextBddNode = nodeList;
01099           nodeList = bddNode;
01100         }
01101       }
01102     }
01103     for (bddNode = nodeList; bddNode ; bddNode = nodeList){
01104       BddExchangeAux(bddManager, bddNode, id, nextId);
01105       nodeList = bddNode->nextBddNode;
01106       HashTableAddDirect(nextTable, bddNode);
01107       table->numEntries--;
01108     }
01109     SweepVarTable(bddManager, nextId);
01110   }
01111   else {
01112     bddManager->numTrivialSwaps++;
01113   }
01114   
01115   CalFixupAssoc(bddManager, id, nextId, bddManager->tempAssociation);
01116   for(p = bddManager->associationList; p; p = p->next){
01117     CalFixupAssoc(bddManager, id, nextId, p);
01118   }
01119 
01120   bddManager->idToIndex[id] = nextIndex;
01121   bddManager->idToIndex[nextId] = index;
01122   bddManager->indexToId[index] = nextId;
01123   bddManager->indexToId[nextIndex] = id;
01124 
01125   Cal_Assert(CheckValidityOfNodes(bddManager, id));
01126   Cal_Assert(CheckValidityOfNodes(bddManager, nextId));
01127   Cal_Assert(CalCheckAssoc(bddManager));
01128 #ifdef _CAL_VERBOSE
01129   /*fprintf(stdout,"Variable order after swap:\n");*/
01130   for (i=0; i<bddManager->numVars; i++){
01131     fprintf(stdout, "%3d ", bddManager->indexToId[i]);
01132   }
01133   fprintf(stdout, "%8d\n", bddManager->numNodes);
01134 #endif
01135 }

static void BddExchangeAux ( Cal_BddManager_t *  bddManager,
CalBddNode_t *  f,
int  id,
int  nextId 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 901 of file calReorderDF.c.

00903 {
00904   CalBddNode_t *f0, *f1;
00905   CalBddNode_t *f00, *f01, *f10, *f11;
00906   CalBddNode_t *newF0, *newF1;
00907   int f0Found, f1Found;
00908   int fIndex;
00909   
00910   f0 = f->elseBddNode;
00911   f1 = f->thenBddNode;
00912 
00913   if (CAL_BDD_POINTER(f0)->thenBddId == nextId){
00914     f00 = BddNodeGetElseBddNode(f0);
00915     f01 = BddNodeGetThenBddNode(f0);
00916   }
00917   else {
00918     f00 = f01 = f0;
00919   }
00920   if (CAL_BDD_POINTER(f1)->thenBddId == nextId){
00921     f10 = BddNodeGetElseBddNode(f1);
00922     f11 = BddNodeGetThenBddNode(f1);
00923   }
00924   else {
00925     f10 = f11 = f1;
00926   }
00927   
00928   if (f00 == f10){
00929     newF0 = f00;
00930     f0Found = 1;
00931   }
00932   else{
00933     f0Found = UniqueTableForIdFindOrAdd(bddManager,
00934                                         bddManager->uniqueTable[id], f10,
00935                                         f00, &newF0);
00936   }
00937   BddNodeIcrRefCount(newF0);
00938   if (f01 == f11){
00939     newF1 = f11;
00940     f1Found = 1;
00941   }
00942   else{
00943     f1Found = UniqueTableForIdFindOrAdd(bddManager,
00944                                         bddManager->uniqueTable[id], f11,
00945                                         f01, &newF1);
00946   }
00947   BddNodeIcrRefCount(newF1);
00948 
00949   f->thenBddId = nextId;
00950   f->elseBddNode = newF0;
00951   f->thenBddNode = newF1;
00952 
00953   fIndex = bddManager->idToIndex[id];
00954   Cal_Assert(fIndex <
00955              bddManager->idToIndex[CAL_BDD_POINTER(f00)->thenBddId]);
00956   Cal_Assert(fIndex <
00957              bddManager->idToIndex[CAL_BDD_POINTER(f10)->thenBddId]);
00958   Cal_Assert(fIndex <
00959              bddManager->idToIndex[CAL_BDD_POINTER(f01)->thenBddId]);
00960   Cal_Assert(fIndex <
00961              bddManager->idToIndex[CAL_BDD_POINTER(f11)->thenBddId]);
00962   Cal_Assert(CAL_BDD_POINTER(f00)->thenBddId != nextId);
00963   Cal_Assert(CAL_BDD_POINTER(f01)->thenBddId != nextId);
00964   Cal_Assert(CAL_BDD_POINTER(f10)->thenBddId != nextId);
00965   Cal_Assert(CAL_BDD_POINTER(f11)->thenBddId != nextId);
00966   
00967   if (!f0Found){
00968     BddNodeIcrRefCount(f00);
00969     BddNodeIcrRefCount(f10);
00970   }
00971 
00972   if (!f1Found){
00973     BddNodeIcrRefCount(f01);
00974     BddNodeIcrRefCount(f11);
00975   }
00976 
00977   BddNodeDcrRefCount(f0);
00978   BddNodeDcrRefCount(f1);
00979 }

static void BddExchangeVarBlocks ( Cal_BddManager_t *  bddManager,
Cal_Block  parent,
long  blockIndex 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1150 of file calReorderDF.c.

01152 {
01153   Cal_Block b1, b2, temp;
01154   long i, j, k, l, firstBlockWidth, secondBlockWidth;
01155 
01156   b1 = parent->children[blockIndex];
01157   b2 = parent->children[blockIndex+1];
01158   /* This slides the blocks past each other in a kind of interleaving */
01159   /* fashion. */
01160   firstBlockWidth = b1->lastIndex - b1->firstIndex;
01161   secondBlockWidth = b2->lastIndex - b2->firstIndex;
01162   
01163   for (i=0; i <= firstBlockWidth + secondBlockWidth; i++){
01164     j = i - firstBlockWidth;
01165     if (j < 0) j=0;
01166     k = ((i > secondBlockWidth) ? secondBlockWidth : i);
01167     while (j <= k) {
01168           l = b2->firstIndex + j - i + j;
01169           BddExchange(bddManager, bddManager->indexToId[l-1]);
01170           ++j;
01171         }
01172   }
01173   CalBddBlockDelta(b1, secondBlockWidth+1);
01174   CalBddBlockDelta(b2, -(firstBlockWidth+1));
01175   temp = parent->children[blockIndex];
01176   parent->children[blockIndex] = parent->children[blockIndex+1];
01177   parent->children[blockIndex+1] = temp;
01178 }

static void BddReallocateNodes ( Cal_BddManager_t *  bddManager  )  [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 774 of file calReorderDF.c.

00775 {
00776   int i;
00777   int index;
00778   CalNodeManager_t *nodeManager;
00779   CalPageManager_t *pageManager;
00780   int numSegments;
00781   CalAddress_t **pageSegmentArray;
00782   
00783   pageManager = bddManager->pageManager2;
00784   numSegments = pageManager->numSegments;
00785   pageSegmentArray = pageManager->pageSegmentArray;
00786   
00787   /* Reinitialize the page manager */
00788   pageManager->totalNumPages = 0;
00789   pageManager->numSegments = 0;
00790   pageManager->maxNumSegments = MAX_NUM_SEGMENTS;
00791   pageManager->pageSegmentArray 
00792       = Cal_MemAlloc(CalAddress_t *, pageManager->maxNumSegments);
00793   pageManager->freePageList = Cal_Nil(CalAddress_t);
00794   
00795   /* Do a bottom up traversal */
00796 
00797   for (index = bddManager->numVars-1; index >= 0; index--){
00798     int id;
00799     CalHashTable_t *uniqueTableForId;
00800     int numPagesRequired, newSizeIndex;
00801     CalBddNode_t *bddNode, *dupNode, *thenNode, *elseNode, **oldBins;
00802     long hashValue, oldNumBins;
00803     
00804     id = bddManager->indexToId[index];
00805     uniqueTableForId = bddManager->uniqueTable[id];
00806     nodeManager = bddManager->nodeManagerArray[id];
00807     oldBins = uniqueTableForId->bins;
00808     oldNumBins = uniqueTableForId->numBins;
00809     nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
00810     nodeManager->numPages = 0;
00811     numPagesRequired =
00812         uniqueTableForId->numEntries/NUM_NODES_PER_PAGE;
00813     nodeManager->maxNumPages =
00814         2*(numPagesRequired ? numPagesRequired : 1);
00815     Cal_MemFree(nodeManager->pageList);
00816     nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
00817                                          nodeManager->maxNumPages); 
00818     /* Create the new set of bins */
00819     newSizeIndex =
00820         CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY);
00821     if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
00822       newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00823     }
00824     uniqueTableForId->sizeIndex = newSizeIndex;
00825     uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
00826     uniqueTableForId->maxCapacity =
00827         uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
00828     
00829     uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
00830                                           uniqueTableForId->numBins); 
00831     memset((char *)uniqueTableForId->bins, 0, 
00832            uniqueTableForId->numBins*sizeof(CalBddNode_t *)); 
00833     for (i=0; i<oldNumBins; i++){
00834       for (bddNode = oldBins[i]; bddNode; bddNode = bddNode->nextBddNode){ 
00835         CalNodeManagerAllocNode(nodeManager, dupNode);
00836         thenNode = bddNode->thenBddNode;
00837         CalBddNodeIsForwardedTo(thenNode);
00838         Cal_Assert(thenNode);
00839         Cal_Assert(!CalBddNodeIsForwarded(thenNode));
00840         elseNode = bddNode->elseBddNode;
00841         CalBddNodeIsForwardedTo(elseNode);
00842         Cal_Assert(elseNode);
00843         Cal_Assert(!CalBddNodeIsForwarded(CAL_BDD_POINTER(elseNode)));
00844         Cal_Assert(bddManager->idToIndex[bddNode->thenBddId] <
00845                    bddManager->idToIndex[thenNode->thenBddId]); 
00846         Cal_Assert(bddManager->idToIndex[bddNode->thenBddId] <
00847                    bddManager->idToIndex[CAL_BDD_POINTER(elseNode)->thenBddId]);
00848         dupNode->thenBddNode = thenNode;
00849         dupNode->elseBddNode = elseNode;
00850         dupNode->thenBddId = bddNode->thenBddId;
00851         dupNode->elseBddId = bddNode->elseBddId;
00852         hashValue = CalDoHash2(thenNode, elseNode, uniqueTableForId);
00853         dupNode->nextBddNode = uniqueTableForId->bins[hashValue];
00854         uniqueTableForId->bins[hashValue] = dupNode;
00855         bddNode->thenBddNode = dupNode;
00856         bddNode->elseBddNode = (CalBddNode_t *)0;
00857         bddNode->thenBddId = id;
00858         Cal_Assert(bddManager->idToIndex[dupNode->thenBddId] <
00859                    bddManager->idToIndex[thenNode->thenBddId]); 
00860         Cal_Assert(bddManager->idToIndex[dupNode->thenBddId] <
00861                    bddManager->idToIndex[CAL_BDD_POINTER(elseNode)->thenBddId]);
00862       }
00863     }
00864     Cal_MemFree(oldBins);
00865     CalBddIsForwardedTo(bddManager->varBdds[id]);
00866   }
00867 
00868   if (bddManager->pipelineState == CREATE){
00869     /* There are some results computed in pipeline */
00870     CalBddReorderFixProvisionalNodes(bddManager);
00871   }
00872   
00873   /* Fix the user BDDs */
00874   CalBddReorderFixUserBddPtrs(bddManager);
00875 
00876   /* Fix the association */
00877   CalReorderAssociationFix(bddManager);
00878 
00879   Cal_Assert(CalCheckAssoc(bddManager));
00880   
00881   /* Free the page manager related stuff*/
00882   for(i = 0; i < numSegments; i++){
00883     free(pageSegmentArray[i]);
00884   }
00885   Cal_MemFree(pageSegmentArray);
00886 }

static void BddReorderSift ( Cal_BddManager_t *  bddManager,
double  maxSizeFactor 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1553 of file calReorderDF.c.

01554 {
01555   Cal_Block *toSift;
01556 
01557   toSift = Cal_MemAlloc(Cal_Block, bddManager->numVars);
01558   BddReorderSiftAux(bddManager, bddManager->superBlock, toSift,
01559                        maxSizeFactor); 
01560   Cal_MemFree(toSift);
01561 }

static void BddReorderSiftAux ( Cal_BddManager_t *  bddManager,
Cal_Block  block,
Cal_Block *  toSift,
double  maxSizeFactor 
) [static]

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

Synopsis [Reorder variables using "sift" algorithm.]

Description [Reorder variables using "sift" algorithm.]

SideEffects [None]

Definition at line 1483 of file calReorderDF.c.

01485 {
01486   long i, j, k;
01487   long width;
01488   long maxWidth;
01489   long widest;
01490   long numVarsShifted = 0;
01491   bddManager->numSwaps = 0;
01492   if (block->reorderable) {
01493     for (i=0; i < block->numChildren; ++i){
01494       toSift[i] = block->children[i];
01495     }
01496     while (i &&
01497            (numVarsShifted <=
01498             bddManager->maxNumVarsSiftedPerReordering) &&
01499            (bddManager->numSwaps <=
01500             bddManager->maxNumSwapsPerReordering)){ 
01501           i--;
01502       numVarsShifted++;
01503           maxWidth = 0;
01504           widest = 0;
01505           for (j=0; j <= i; ++j) {
01506         for (width=0, k=toSift[j]->firstIndex; k <= toSift[j]->lastIndex; ++k){
01507           width +=
01508               bddManager->uniqueTable[bddManager->indexToId[k]]->numEntries; 
01509         }
01510         width /= toSift[j]->lastIndex - toSift[j]->firstIndex+1;
01511         if (width > maxWidth) {
01512                   maxWidth = width;
01513                   widest = j;
01514                 }
01515       }
01516           if (maxWidth > 1) {
01517         for (j=0; block->children[j] != toSift[widest]; ++j);
01518 #ifdef _CAL_VERBOSE
01519         fprintf(stdout,"Moving block %3d -- %3d\n",
01520                 bddManager->indexToId[block->children[j]-> firstIndex],
01521                 bddManager->indexToId[block->children[j]->lastIndex]);
01522         fflush(stdout);
01523         for (l=0; l<bddManager->numVars; l++){
01524           fprintf(stdout, "%3d ", bddManager->indexToId[l]);
01525         }
01526         fprintf(stdout, "%8d\n", bddManager->numNodes);
01527 #endif
01528         BddSiftBlock(bddManager, block, j, maxSizeFactor);
01529         toSift[widest] = toSift[i];
01530       }
01531           else {
01532         break;
01533       }
01534         }
01535   }
01536   for (i=0; i < block->numChildren; ++i)
01537     BddReorderSiftAux(bddManager, block->children[i], toSift,
01538                       maxSizeFactor);  
01539 }

static void BddReorderStableWindow3 ( Cal_BddManager_t *  bddManager  )  [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1370 of file calReorderDF.c.

01371 {
01372   char *levels;
01373   levels =  Cal_MemAlloc(char, bddManager->numVars);
01374   bddManager->numSwaps = 0;
01375   BddReorderStableWindow3Aux(bddManager, bddManager->superBlock, levels);
01376   Cal_MemFree(levels);
01377 }

static void BddReorderStableWindow3Aux ( Cal_BddManager_t *  bddManager,
Cal_Block  block,
char *  levels 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1302 of file calReorderDF.c.

01304 {
01305   long i;
01306   int moved;
01307   int anySwapped;
01308 
01309   if (block->reorderable) {
01310     for (i=0; i < block->numChildren-1; ++i) levels[i]=1;
01311     do {
01312           anySwapped=0;
01313           for (i=0; i < block->numChildren-1; i++){
01314             if (levels[i]){
01315 #ifdef _CAL_VERBOSE
01316           fprintf(stdout,"Moving block %3d -- %3d\n",
01317                   bddManager->indexToId[block->children[i]-> firstIndex],
01318                   bddManager->indexToId[block->children[i]->lastIndex]);
01319           fflush(stdout);
01320           for (j=0; j<bddManager->numVars; j++){
01321             fprintf(stdout, "%3d ", bddManager->indexToId[j]);
01322           }
01323           fprintf(stdout, "%8d\n", bddManager->numNodes);
01324 #endif
01325           if (i < block->numChildren-2){
01326             moved = BddReorderWindow3(bddManager, block, i);
01327           }
01328           else{
01329             moved = BddReorderWindow2(bddManager, block, i);
01330           }
01331           if (moved){
01332                     if (i > 0) {
01333               levels[i-1]=1;
01334               if (i > 1)
01335                 levels[i-2]=1;
01336             }
01337                     levels[i]=1;
01338                     levels[i+1]=1;
01339                     if (i < block->numChildren-2){
01340               levels[i+2]=1;
01341               if (i < block->numChildren-3) {
01342                             levels[i+3]=1;
01343                             if (i < block->numChildren-4) levels[i+4]=1;
01344                           }
01345             }
01346                     anySwapped=1;
01347           }
01348           else levels[i]=0;
01349         }
01350       }
01351     } while (anySwapped);
01352   }
01353   for (i=0; i < block->numChildren; ++i){
01354     BddReorderStableWindow3Aux(bddManager, block->children[i], levels);
01355   }
01356 }

static int BddReorderWindow2 ( Cal_BddManager_t *  bddManager,
Cal_Block  block,
long  i 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1192 of file calReorderDF.c.

01193 {
01194   long size, bestSize;
01195 
01196   /* 1 2 */
01197   bestSize = bddManager->numNodes;
01198   BddExchangeVarBlocks(bddManager, block, i);
01199   /* 2 1 */
01200   size = bddManager->numNodes;
01201   if (size < bestSize) return (1);
01202   BddExchangeVarBlocks(bddManager, block, i);
01203   return (0);
01204 }

static int BddReorderWindow3 ( Cal_BddManager_t *  bddManager,
Cal_Block  block,
long  i 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1219 of file calReorderDF.c.

01220 {
01221   int best;
01222   long size, bestSize;
01223   long origSize;
01224   
01225   origSize = bddManager->numNodes;
01226   best = 0;
01227   /* 1 2 3 */
01228   bestSize = bddManager->numNodes;
01229   BddExchangeVarBlocks(bddManager, block, i);
01230   /* 2 1 3 */
01231   size=bddManager->numNodes;
01232   if (size < bestSize) {
01233     best=1;
01234     bestSize=size;
01235   }
01236   BddExchangeVarBlocks(bddManager, block, i+1);
01237   /* 2 3 1 */
01238   size=bddManager->numNodes;
01239   if (size < bestSize) {
01240     best=2;
01241     bestSize=size;
01242   }
01243   BddExchangeVarBlocks(bddManager, block, i);
01244   /* 3 2 1 */
01245   size=bddManager->numNodes;
01246   if (size <= bestSize) {
01247     best=3;
01248     bestSize=size;
01249   }
01250   BddExchangeVarBlocks(bddManager, block, i+1);
01251   /* 3 1 2 */
01252   size=bddManager->numNodes;
01253   if (size <= bestSize) {
01254     best=4;
01255     bestSize=size;
01256   }
01257   BddExchangeVarBlocks(bddManager, block, i);
01258   /* 1 3 2 */
01259   size=bddManager->numNodes;
01260   if (size <= bestSize) {
01261     best=5;
01262     bestSize=size;
01263   }
01264   switch (best){
01265       case 0:
01266         BddExchangeVarBlocks(bddManager, block, i+1);
01267         break;
01268       case 1:
01269         BddExchangeVarBlocks(bddManager, block, i+1);
01270         BddExchangeVarBlocks(bddManager, block, i);
01271         break;
01272       case 2:
01273         BddExchangeVarBlocks(bddManager, block, i+1);
01274         BddExchangeVarBlocks(bddManager, block, i);
01275         BddExchangeVarBlocks(bddManager, block, i+1);
01276         break;
01277       case 3:
01278         BddExchangeVarBlocks(bddManager, block, i);
01279         BddExchangeVarBlocks(bddManager, block, i+1);
01280         break;
01281       case 4:
01282         BddExchangeVarBlocks(bddManager, block, i);
01283         break;
01284       case 5:
01285         break;
01286   }
01287   return ((best > 0) && (origSize > bestSize));
01288 }

static void BddSiftBlock ( Cal_BddManager_t *  bddManager,
Cal_Block  block,
long  startPosition,
double  maxSizeFactor 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1391 of file calReorderDF.c.

01393 {
01394   long startSize;
01395   long bestSize;
01396   long bestPosition;
01397   long currentSize;
01398   long currentPosition;
01399   long maxSize;
01400   
01401   startSize = bddManager->numNodes;
01402   bestSize = startSize;
01403   bestPosition = startPosition;
01404   currentSize = startSize;
01405   currentPosition = startPosition;
01406   maxSize = maxSizeFactor*startSize;
01407   if (bddManager->nodeLimit && maxSize > bddManager->nodeLimit)
01408     maxSize = bddManager->nodeLimit;
01409 
01410   /* Need to do optimization here */
01411   if (startPosition > (block->numChildren >> 1)){
01412     while (currentPosition < block->numChildren-1 && currentSize <= maxSize){
01413       BddExchangeVarBlocks(bddManager, block, currentPosition);
01414       ++currentPosition;
01415       currentSize = bddManager->numNodes;
01416       if (currentSize < bestSize){
01417         bestSize = currentSize;
01418         bestPosition=currentPosition;
01419       }
01420     }
01421     while (currentPosition != startPosition){
01422       --currentPosition;
01423       BddExchangeVarBlocks(bddManager, block, currentPosition);
01424     }
01425     currentSize = startSize;
01426     while (currentPosition && currentSize <= maxSize){
01427       --currentPosition;
01428       BddExchangeVarBlocks(bddManager, block, currentPosition);
01429       currentSize = bddManager->numNodes;
01430       if (currentSize <= bestSize){
01431         bestSize = currentSize;
01432         bestPosition = currentPosition;
01433       }
01434     }
01435     while (currentPosition != bestPosition){
01436       BddExchangeVarBlocks(bddManager, block, currentPosition);
01437       ++currentPosition;
01438     }
01439   }
01440   else{
01441     while (currentPosition && currentSize <= maxSize){
01442       --currentPosition;
01443       BddExchangeVarBlocks(bddManager, block, currentPosition);
01444       currentSize = bddManager->numNodes;
01445       if (currentSize < bestSize){
01446         bestSize = currentSize;
01447         bestPosition = currentPosition;
01448       }
01449     }
01450     while (currentPosition != startPosition){
01451       BddExchangeVarBlocks(bddManager, block, currentPosition);
01452       ++currentPosition;
01453     }
01454     currentSize = startSize;
01455     while (currentPosition < block->numChildren-1 && currentSize <= maxSize){
01456       BddExchangeVarBlocks(bddManager, block, currentPosition);
01457       currentSize = bddManager->numNodes;
01458       ++currentPosition;
01459       if (currentSize <= bestSize){
01460         bestSize = currentSize;
01461         bestPosition = currentPosition;
01462       }
01463     }
01464     while (currentPosition != bestPosition){
01465       --currentPosition;
01466       BddExchangeVarBlocks(bddManager, block, currentPosition);
01467     }
01468   }
01469 }

void CalBddReorderAuxDF ( Cal_BddManager_t *  bddManager  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 163 of file calReorderDF.c.

00164 {
00165   CalHashTableGC(bddManager, bddManager->uniqueTable[0]);
00166   /*Cal_BddManagerGC(bddManager);Cal_Assert(CalCheckAllValidity(bddManager));*/
00167   /* If we want to check the validity, we need to garbage collect */
00168   CalInitInteract(bddManager); /* Initialize the interaction matrix
00169                                   before changing the data structure */
00170   nodeManager = CalNodeManagerInit(bddManager->pageManager2);
00171   freeListId = 1;
00172 #ifdef _CAL_QUANTIFY_
00173   quantify_start_recording_data();
00174 #endif
00175   BddConvertDataStruct(bddManager);
00176   if (bddManager->reorderTechnique == CAL_REORDER_WINDOW){
00177     BddReorderStableWindow3(bddManager);
00178   }
00179   else {
00180     BddReorderSift(bddManager, bddManager->maxSiftingGrowth);
00181   }
00182   BddReallocateNodes(bddManager);
00183   BddConvertDataStructBack(bddManager);
00184 #ifdef _CAL_QUANTIFY_
00185   quantify_stop_recording_data();
00186 #endif
00187   nodeManager->numPages = 0; /* Since these pages have already been
00188                                 freed */
00189   CalNodeManagerQuit(nodeManager);
00190   Cal_Assert(CalCheckAllValidity(bddManager));
00191   Cal_MemFree(bddManager->interact);
00192   bddManager->numReorderings++;
00193 }

static int CeilLog2 ( int  number  )  [static]

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

Synopsis [Returns the smallest integer greater than or equal to log2 of a number]

Description [Returns the smallest integer greater than or equal to log2 of a number (The assumption is that the number is >= 1)]

SideEffects [None]

Definition at line 1578 of file calReorderDF.c.

01579 {
01580   int num, count;
01581   for (num=number, count=0; num > 1; num >>= 1, count++);
01582   if ((1 << count) != number) count++;
01583   return count;
01584 }

static int CheckValidityOfNodes ( Cal_BddManager_t *  bddManager,
long  id 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 993 of file calReorderDF.c.

00994 {
00995 #ifndef NDEBUG
00996   CalHashTable_t *table = bddManager->uniqueTable[id];
00997   int i;
00998   CalBddNode_t *bddNode;
00999   int index = bddManager->idToIndex[id];
01000   for(i = 0; i < table->numBins; ++i){
01001     for (bddNode = table->bins[i]; bddNode; bddNode = bddNode->nextBddNode){
01002       int thenIndex = bddManager->idToIndex[bddNode->thenBddNode->thenBddId];
01003       int elseIndex =
01004         bddManager->idToIndex[CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId]; 
01005       assert((thenIndex > index) && (elseIndex > index));
01006     }
01007   }
01008 #endif
01009   return 1;
01010 }

static void HashTableAddDirect ( CalHashTable_t *  hashTable,
CalBddNode_t *  bddNode 
) [static]

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

Synopsis [Directly insert a BDD node in the hash table.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 298 of file calReorderDF.c.

00299 {
00300   int hashValue;
00301   CalBddNode_t *thenBddNode, *elseBddNode;
00302 
00303   hashTable->numEntries++;
00304   if(hashTable->numEntries >= hashTable->maxCapacity){
00305     CalHashTableRehash(hashTable, 1);
00306   }
00307   thenBddNode = bddNode->thenBddNode;
00308   Cal_Assert(CalBddNodeIsOutPos(thenBddNode));
00309   elseBddNode = bddNode->elseBddNode;
00310   hashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
00311   bddNode->nextBddNode = hashTable->bins[hashValue];
00312   hashTable->bins[hashValue] = bddNode;
00313 }

static int HashTableFindOrAdd ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable,
CalBddNode_t *  thenBdd,
CalBddNode_t *  elseBdd,
CalBddNode_t **  bddPtr 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 328 of file calReorderDF.c.

00331 {
00332   CalBddNode_t *ptr;
00333   int hashValue;
00334   
00335   Cal_Assert(CalBddNodeIsOutPos(thenBdd));
00336   hashValue = CalDoHash2(thenBdd, elseBdd, hashTable);
00337   for (ptr = hashTable->bins[hashValue]; ptr; ptr = ptr->nextBddNode){
00338     if ((ptr->thenBddNode == thenBdd) &&
00339         (ptr->elseBddNode == elseBdd)){
00340       *bddPtr = ptr;
00341       return 1;
00342     }
00343   }
00344   hashTable->numEntries++;
00345   if(hashTable->numEntries > hashTable->maxCapacity){
00346     CalHashTableRehash(hashTable,1);
00347     hashValue = CalDoHash2(thenBdd, elseBdd, hashTable);
00348   }
00349 
00350   NodeManagerAllocNode(bddManager, &ptr);
00351 
00352   ptr->thenBddNode = thenBdd;
00353   ptr->elseBddNode = elseBdd;
00354   ptr->nextBddNode = hashTable->bins[hashValue];
00355   ptr->thenBddId = hashTable->bddId;
00356   ptr->elseBddId = 0;
00357   hashTable->bins[hashValue] = ptr;
00358   *bddPtr = ptr;
00359   return 0;
00360 }

static void NodeManagerAllocNode ( Cal_BddManager_t *  bddManager,
CalBddNode_t **  nodePtr 
) [static]

Definition at line 203 of file calReorderDF.c.

00204 {
00205   /* First check the free list of bddManager */
00206   if (nodeManager->freeNodeList){
00207     *nodePtr = nodeManager->freeNodeList;
00208     nodeManager->freeNodeList =
00209         ((CalBddNode_t *)(*nodePtr))->nextBddNode;
00210   }
00211   else{
00212     if (freeListId < bddManager->numVars){
00213       /* Find the next id with free list */
00214       for (; freeListId <= bddManager->numVars; freeListId++){
00215         CalNodeManager_t *nodeManagerForId =
00216             bddManager->nodeManagerArray[freeListId]; 
00217         if (nodeManagerForId->freeNodeList){
00218           *nodePtr = nodeManagerForId->freeNodeList;
00219           nodeManagerForId->freeNodeList = (CalBddNode_t *)0;
00220           nodeManager->freeNodeList =
00221               ((CalBddNode_t *)(*nodePtr))->nextBddNode;
00222           break;
00223         }
00224       }
00225     }
00226   }
00227   if (!(*nodePtr)){
00228     /* Create a new page */
00229     CalBddNode_t *_freeNodeList, *_nextNode, *_node;                        
00230     _freeNodeList =                                                         
00231         (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager);  
00232     for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0;       
00233         _node != _freeNodeList; _nextNode = _node--){                       
00234       _node->nextBddNode = _nextNode;                                       
00235     }                                                                       
00236     nodeManager->freeNodeList = _freeNodeList + 1;                          
00237     *nodePtr = _node;
00238     if (nodeManager->numPages == nodeManager->maxNumPages){             
00239       nodeManager->maxNumPages *= 2;                                      
00240       nodeManager->pageList =                                            
00241           Cal_MemRealloc(CalAddress_t *, nodeManager->pageList, 
00242                          nodeManager->maxNumPages);                       
00243     }                                                                       
00244     nodeManager->pageList[nodeManager->numPages++] =
00245         (CalAddress_t *)_freeNodeList;     
00246   }
00247 }

static void SweepVarTable ( Cal_BddManager_t *  bddManager,
long  id 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1024 of file calReorderDF.c.

01025 {
01026   CalHashTable_t *table = bddManager->uniqueTable[id];
01027   long numNodesFreed, oldNumEntries;
01028   CalBddNode_t **ptr, *bddNode;
01029   int i;
01030   
01031   oldNumEntries = table->numEntries;
01032   for(i = 0; i < table->numBins; ++i){
01033     for (ptr = &table->bins[i], bddNode = *ptr; bddNode;
01034          bddNode = *ptr){
01035       if (bddNode->elseBddId == 0){
01036         *ptr = bddNode->nextBddNode;
01037         CalNodeManagerFreeNode(nodeManager, bddNode);
01038         BddNodeDcrRefCount(bddNode->thenBddNode);
01039         BddNodeDcrRefCount(bddNode->elseBddNode);
01040         table->numEntries--;
01041       }
01042       else{
01043         ptr = &bddNode->nextBddNode;
01044       }
01045     }
01046   }
01047   numNodesFreed = oldNumEntries - table->numEntries;
01048   bddManager->numNodes -= numNodesFreed;
01049   bddManager->numNodesFreed += numNodesFreed;
01050 }

static int UniqueTableForIdFindOrAdd ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable,
CalBddNode_t *  thenBdd,
CalBddNode_t *  elseBdd,
CalBddNode_t **  bddPtr 
) [static]

AutomaticStart

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

Synopsis [find or add in the unique table for id.]

Description [optional]

SideEffects [If a new BDD node is created (found == false), then the numNodes field of the manager needs to be incremented.]

SeeAlso [optional]

Definition at line 262 of file calReorderDF.c.

00267 {
00268   int found = 0; 
00269   if (thenBdd == elseBdd){
00270     *bddPtr = thenBdd;
00271     found = 1;
00272   }
00273   else if(CalBddNodeIsOutPos(thenBdd)){
00274     found = HashTableFindOrAdd(bddManager, hashTable, thenBdd, elseBdd, bddPtr);
00275   }
00276   else{
00277     found = HashTableFindOrAdd(bddManager, hashTable,
00278                                CalBddNodeNot(thenBdd),
00279                                CalBddNodeNot(elseBdd), bddPtr); 
00280     *bddPtr = CalBddNodeNot(*bddPtr);
00281   }
00282   if (!found) bddManager->numNodes++;
00283   return found;
00284 }

Variable Documentation

int freeListId [static]

Definition at line 64 of file calReorderDF.c.

CalNodeManager_t* nodeManager [static]

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

FileName [calReorderDF.c]

PackageName [cal]

Synopsis [Routines for dynamic reordering of variables.]

Description [This method is based on traditional dynamic reordering technique found in depth-first based packages. The data structure is first converted to conform to traditional one and then reordering is performed. At the end the nodes are arranged back on the pages. The computational overheads are in terms of converting the data structure back and forth and the memory overhead due to the extra space needed to arrange the nodes. This overhead can be eliminated by proper implementation. For details, please refer to the work by Rajeev K. Ranjan et al - "Dynamic variable reordering in a breadth-first manipulation based package: Challenges and Solutions"- Proceedings of ICCD'97.]

SeeAlso [calReorderBF.c calReorderUtil.c]

Author [Rajeev K. Ranjan (rajeev@ic. eecs.berkeley.edu)]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

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.]

Definition at line 63 of file calReorderDF.c.

Generated on Tue Jan 12 13:57:13 2010 for glu-2.2 by  doxygen 1.6.1