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

00001 
00039 #include "calInt.h"
00040 
00041 /*---------------------------------------------------------------------------*/
00042 /* Constant declarations                                                     */
00043 /*---------------------------------------------------------------------------*/
00044 
00045 /*---------------------------------------------------------------------------*/
00046 /* Type declarations                                                         */
00047 /*---------------------------------------------------------------------------*/
00048 
00049 /*---------------------------------------------------------------------------*/
00050 /* Stucture declarations                                                     */
00051 /*---------------------------------------------------------------------------*/
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Variable declarations                                                     */
00055 /*---------------------------------------------------------------------------*/
00056 
00057 /*---------------------------------------------------------------------------*/
00058 /* Macro declarations                                                        */
00059 /*---------------------------------------------------------------------------*/
00060 
00063 /*---------------------------------------------------------------------------*/
00064 /* Static function prototypes                                                */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 
00070 /*---------------------------------------------------------------------------*/
00071 /* Definition of exported functions                                          */
00072 /*---------------------------------------------------------------------------*/
00073 /*---------------------------------------------------------------------------*/
00074 /* Definition of internal functions                                          */
00075 /*---------------------------------------------------------------------------*/
00087 void
00088 CalBddReorderFixUserBddPtrs(Cal_BddManager bddManager)
00089 {
00090   CalHashTable_t *userBddUniqueTable = bddManager->uniqueTable[0];
00091   int i;
00092   int numBins;
00093   int rehashFlag;
00094   CalBddNode_t **bins;
00095   CalBddNode_t *bddNode;
00096   CalBddNode_t *nextBddNode;
00097   CalBddNode_t *thenBddNode;
00098   CalBddNode_t *elseBddNode;
00099   Cal_Bdd_t internalBdd;
00100 
00101   numBins = userBddUniqueTable->numBins;
00102   bins = userBddUniqueTable->bins;
00103 
00104   for(i = 0; i < numBins; i++) {
00105     for(bddNode = bins[i];
00106         bddNode != Cal_Nil(CalBddNode_t);
00107         bddNode = nextBddNode) {
00108       /*
00109        * Process one bddNode at a time
00110        */
00111       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00112       rehashFlag = 0;
00113 
00114       thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00115       elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00116       CalBddNodeGetThenBdd(bddNode, internalBdd);
00117       if (CalBddIsForwarded(internalBdd)) {
00118         CalBddForward(internalBdd);
00119         CalBddNodePutThenBdd(bddNode, internalBdd);
00120         rehashFlag = 1;
00121       }
00122       Cal_Assert(CalBddIsForwarded(internalBdd) == 0);
00123       /*Cal_Assert(!CalBddIsRefCountZero(internalBdd));*/
00124       /*
00125        * Rehash if necessary
00126        */
00127       if (rehashFlag) {
00128         CalUniqueTableForIdRehashNode(userBddUniqueTable, bddNode,
00129                                       thenBddNode, elseBddNode);
00130       }
00131     }
00132   }
00133 }
00134 
00146 int
00147 CalCheckAllValidity(Cal_BddManager bddManager)
00148 {
00149   int id;
00150   for(id = 0; id <= bddManager->numVars; id++){
00151     CalCheckValidityOfNodesForId(bddManager, id);
00152   }
00153   CalCheckAssociationValidity(bddManager);
00154   if (bddManager->pipelineState == CREATE){
00155     CalCheckPipelineValidity(bddManager);
00156   }
00157   CalCheckRefCountValidity(bddManager);
00158   CalCheckCacheTableValidity(bddManager);
00159   return 1;
00160 }
00161 
00162 
00174 int
00175 CalCheckValidityOfNodesForId(Cal_BddManager bddManager, int id)
00176 {
00177   int i, numBins;
00178   CalHashTable_t *uniqueTableForId;
00179   CalBddNode_t *bddNode, *nextBddNode;
00180   Cal_Bdd_t thenBdd, elseBdd;
00181   
00182   uniqueTableForId = bddManager->uniqueTable[id];
00183   Cal_Assert(uniqueTableForId->startNode.nextBddNode == NULL);
00184   numBins = uniqueTableForId->numBins;
00185   for (i = 0; i < numBins; i++){
00186     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00187          bddNode = nextBddNode){
00188       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00189       CalCheckValidityOfANode(bddManager, bddNode, id);
00190       CalBddNodeGetThenBdd(bddNode, thenBdd);
00191       CalBddNodeGetElseBdd(bddNode, elseBdd);
00192       Cal_Assert(CalDoHash2(CalBddGetBddNode(thenBdd),
00193                             CalBddGetBddNode(elseBdd), 
00194                             uniqueTableForId) == i);
00195     }
00196   }
00197   return 1;
00198 }
00199 
00200 
00212 int
00213 CalCheckValidityOfNodesForWindow(Cal_BddManager bddManager,
00214                                  Cal_BddIndex_t index, int numLevels)
00215 {
00216   int i, numBins, j;
00217   CalHashTable_t *uniqueTableForId;
00218   CalBddNode_t *bddNode, *nextBddNode;
00219   Cal_Bdd_t thenBdd, elseBdd;
00220 
00221   for (i = 0; i < numLevels; i++){
00222     uniqueTableForId =
00223         bddManager->uniqueTable[bddManager->indexToId[index+i]]; 
00224     numBins = uniqueTableForId->numBins;
00225     for (j = 0; j < numBins; j++){
00226       for (bddNode = uniqueTableForId->bins[j]; bddNode;
00227            bddNode = nextBddNode){
00228         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00229         Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00230         CalBddNodeGetThenBdd(bddNode, thenBdd);
00231         CalBddNodeGetElseBdd(bddNode, elseBdd);
00232         Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00233         Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00234         Cal_Assert(CalDoHash2(CalBddGetBddNode(thenBdd),
00235                               CalBddGetBddNode(elseBdd), 
00236                              uniqueTableForId) == j);
00237       }
00238     }
00239     for (bddNode = uniqueTableForId->startNode.nextBddNode; bddNode;
00240          bddNode = nextBddNode){ 
00241       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00242       CalBddNodeGetThenBdd(bddNode, thenBdd);
00243       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00244     }
00245   }
00246   return 1;
00247 }
00248 
00249 
00250   
00262 int
00263 CalCheckValidityOfANode(Cal_BddManager_t *bddManager, CalBddNode_t
00264                      *bddNode, int id) 
00265 {
00266   Cal_Bdd_t thenBdd, elseBdd, thenBdd_, elseBdd_, bdd;
00267   if (id != 0){
00268     /* id = 0 corresponds to the constants and the user BDDs */
00269     Cal_Assert(bddManager->idToIndex[id] <
00270                bddManager->idToIndex[bddNode->thenBddId]);   
00271     Cal_Assert(bddManager->idToIndex[id] < 
00272                bddManager->idToIndex[bddNode->elseBddId]);
00273   }
00274   Cal_Assert(!CalBddNodeIsForwarded(bddNode));
00275   Cal_Assert(!CalBddNodeIsRefCountZero(bddNode));
00276   CalBddNodeGetThenBdd(bddNode, thenBdd);
00277   CalBddNodeGetElseBdd(bddNode, elseBdd);
00278   Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00279   Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00280   Cal_Assert(!CalBddIsRefCountZero(thenBdd));
00281   Cal_Assert(!CalBddIsRefCountZero(elseBdd));
00282   /* Make sure that the then and else bdd nodes are part of the
00283      respective unique tables */
00284   if (bddNode->thenBddId != 0){
00285     CalBddGetThenBdd(thenBdd, thenBdd_);
00286     CalBddGetElseBdd(thenBdd, elseBdd_);
00287     Cal_Assert(
00288       CalUniqueTableForIdLookup(bddManager,
00289                                 bddManager->uniqueTable[bddNode->thenBddId],  
00290                                 thenBdd_, elseBdd_, &bdd));
00291   }
00292   if (bddNode->elseBddId != 0){
00293     CalBddGetThenBdd(elseBdd, thenBdd_);
00294     CalBddGetElseBdd(elseBdd, elseBdd_);
00295     Cal_Assert(
00296       CalUniqueTableForIdLookup(bddManager,
00297                                 bddManager->uniqueTable[bddNode->elseBddId],
00298                                 thenBdd_, elseBdd_, &bdd));
00299   }
00300   return 1;
00301 }
00302 
00314 void
00315 CalCheckRefCountValidity(Cal_BddManager_t *bddManager)
00316 {
00317   int i, numBins, index;
00318   CalHashTable_t *uniqueTableForId;
00319   CalBddNode_t *bddNode, *nextBddNode;
00320   Cal_Bdd_t thenBdd, elseBdd, internalBdd;
00321   CalAssociation_t *assoc, *nextAssoc;
00322   
00323   /* First traverse the user BDDs */
00324   uniqueTableForId = bddManager->uniqueTable[0];
00325   numBins = uniqueTableForId->numBins;
00326   for (i = 0; i < numBins; i++){
00327     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00328          bddNode = nextBddNode){
00329       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00330       CalBddNodeGetThenBdd(bddNode, internalBdd);
00331       CalBddDcrRefCount(internalBdd);
00332     }
00333   }
00334       /* Traverse the associations */
00335   
00336   for(assoc = bddManager->associationList;
00337       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00338     nextAssoc = assoc->next;
00339     for (i=1; i <= bddManager->numVars; i++){
00340         if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00341             CalBddDcrRefCount(assoc->varAssociation[i]);
00342         }
00343     }
00344   }
00345   /* temporary association */
00346   assoc = bddManager->tempAssociation;
00347   for (i=1; i <= bddManager->numVars; i++){
00348       if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00349           CalBddDcrRefCount(assoc->varAssociation[i]);
00350       }
00351   }
00352 
00353   
00354   /* Now traverse all the nodes in order */
00355   for (index = 0; index < bddManager->numVars; index++){
00356     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00357     numBins = uniqueTableForId->numBins;
00358     for (i = 0; i < numBins; i++){
00359       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00360            bddNode = nextBddNode){
00361         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00362         CalBddNodeGetThenBdd(bddNode, thenBdd);
00363         CalBddNodeGetElseBdd(bddNode, elseBdd);
00364         CalBddDcrRefCount(thenBdd);
00365         CalBddDcrRefCount(elseBdd);
00366       }
00367     }
00368   }
00369 
00370   /* All the reference count must be zero  or max */
00371   for (index = 0; index < bddManager->numVars; index++){
00372     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00373     numBins = uniqueTableForId->numBins;
00374     for (i = 0; i < numBins; i++){
00375       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00376            bddNode = nextBddNode){
00377         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00378         /* If the pipeline execution is going on, the following
00379            assertion will not hold */
00380         if (bddManager->pipelineState != CREATE){
00381           Cal_Assert(CalBddNodeIsRefCountZero(bddNode) ||
00382                      CalBddNodeIsRefCountMax(bddNode));
00383         }
00384       }
00385     }
00386   }
00387 
00388   /* Put back the ref count */
00389   /* traverse all the nodes in order */
00390   for (index = 0; index < bddManager->numVars; index++){
00391     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00392     numBins = uniqueTableForId->numBins;
00393     for (i = 0; i < numBins; i++){
00394       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00395            bddNode = nextBddNode){
00396         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00397         CalBddNodeGetThenBdd(bddNode, thenBdd);
00398         CalBddNodeGetElseBdd(bddNode, elseBdd);
00399         CalBddIcrRefCount(thenBdd);
00400         CalBddIcrRefCount(elseBdd);
00401       }
00402     }
00403   }
00404       /* Traverse the associations */
00405   for(assoc = bddManager->associationList;
00406       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00407     nextAssoc = assoc->next;
00408     for (i=1; i <= bddManager->numVars; i++){
00409         if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00410             CalBddIcrRefCount(assoc->varAssociation[i]);
00411         }
00412     }
00413   }
00414   /* temporary association */
00415   assoc = bddManager->tempAssociation;
00416   for (i=1; i <= bddManager->numVars; i++){
00417       if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00418           CalBddIcrRefCount(assoc->varAssociation[i]);
00419       }
00420   }
00421 
00422   /* Traverse the user BDDs */
00423   uniqueTableForId = bddManager->uniqueTable[0];
00424   numBins = uniqueTableForId->numBins;
00425   for (i = 0; i < numBins; i++){
00426     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00427          bddNode = nextBddNode){
00428       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00429       CalBddNodeGetThenBdd(bddNode, internalBdd);
00430       CalBddIcrRefCount(internalBdd);
00431     }
00432   }
00433 }
00434 
00446 int
00447 CalCheckAssoc(Cal_BddManager_t *bddManager)
00448 {
00449   CalAssociation_t *assoc, *nextAssoc;
00450   int i;
00451   int expectedLastBddIndex, bddIndex;
00452 
00453   for(assoc = bddManager->associationList;
00454       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00455     nextAssoc = assoc->next;
00456     expectedLastBddIndex = -1;
00457     for (i=1; i <= bddManager->numVars; i++){
00458       if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
00459         bddIndex = bddManager->idToIndex[i];
00460         if (expectedLastBddIndex < bddIndex){
00461           expectedLastBddIndex = bddIndex;
00462         }
00463       }
00464     }
00465     Cal_Assert(expectedLastBddIndex == assoc->lastBddIndex);
00466   }
00467   /* fix temporary association */
00468   assoc = bddManager->tempAssociation;
00469   expectedLastBddIndex = -1;
00470   for (i=1; i <= bddManager->numVars; i++){
00471     if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
00472       bddIndex = bddManager->idToIndex[i];
00473       if (expectedLastBddIndex < bddIndex){
00474         expectedLastBddIndex = bddIndex;
00475       }
00476     }
00477   }
00478   Cal_Assert(expectedLastBddIndex == assoc->lastBddIndex);
00479   return 1;
00480 }
00481 
00493 void
00494 CalFixupAssoc(Cal_BddManager_t *bddManager, long id1, long id2,
00495            CalAssociation_t *assoc)
00496 {
00497   if (assoc->lastBddIndex == -1) return;
00498   /* Variable with id1 is moving down a spot. */
00499   if ((CalBddIsBddNull(bddManager, assoc->varAssociation[id1]) == 0)
00500       && (assoc->lastBddIndex == bddManager->idToIndex[id1])){
00501     assoc->lastBddIndex++;
00502   }
00503   else if ((CalBddIsBddNull(bddManager, assoc->varAssociation[id1])) &&
00504            (CalBddIsBddNull(bddManager, assoc->varAssociation[id2]) ==
00505             0) && 
00506   (assoc->lastBddIndex == bddManager->idToIndex[id2])){
00507     assoc->lastBddIndex--;
00508   }
00509   Cal_Assert((assoc->lastBddIndex >= 0) && (assoc->lastBddIndex <=
00510                                            CAL_BDD_CONST_INDEX));
00511    
00512 }
00527 void
00528 CalBddReorderFixCofactors(Cal_BddManager bddManager, Cal_BddId_t id)
00529 {
00530   CalHashTable_t *uniqueTableForId =
00531       bddManager->uniqueTable[id];
00532   CalBddNode_t *bddNode, *nextBddNode, **bins, *thenBddNode, *elseBddNode;
00533   Cal_Bdd_t f0, f1;
00534   long numBins;
00535   int i, rehashFlag;
00536   
00537   numBins = uniqueTableForId->numBins;
00538   bins = uniqueTableForId->bins;
00539 
00540   for(i = 0; i < numBins; i++) {
00541     for(bddNode = bins[i];
00542         bddNode != Cal_Nil(CalBddNode_t);
00543         bddNode = nextBddNode) {
00544       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00545       /*
00546        * Process one bddNode at a time
00547        */
00548       /*
00549       ** Because we have kept all the forwarding nodes in the list,
00550       ** this should not be a forwarding node.
00551       */
00552       Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00553       Cal_Assert(CalBddNodeIsRefCountZero(bddNode) == 0);
00554       thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00555       elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00556       rehashFlag = 0;
00557       CalBddNodeGetThenBdd(bddNode, f1);
00558       CalBddNodeGetElseBdd(bddNode, f0);
00559       if (CalBddIsForwarded(f1)) {
00560         CalBddForward(f1);
00561         CalBddNodePutThenBdd(bddNode, f1);
00562         rehashFlag = 1;
00563       }
00564       Cal_Assert(CalBddIsForwarded(f1) == 0);
00565       if (CalBddIsForwarded(f0)) {
00566         CalBddForward(f0);
00567         CalBddNodePutElseBdd(bddNode, f0); 
00568         rehashFlag = 1;
00569       }
00570       Cal_Assert(CalBddIsForwarded(f0) == 0);
00571       /* Rehash if necessary */
00572       if (rehashFlag) {
00573         CalUniqueTableForIdRehashNode(uniqueTableForId, bddNode, thenBddNode,
00574                                       elseBddNode);
00575       }
00576     }
00577   }
00578 }
00579 
00591 void
00592 CalBddReorderReclaimForwardedNodes(Cal_BddManager bddManager, int
00593                                 startIndex, int endIndex)
00594 {
00595   Cal_BddIndex_t index;
00596   Cal_BddId_t id;
00597   CalHashTable_t *uniqueTableForId;
00598   CalNodeManager_t *nodeManager;
00599   
00600   for(index = startIndex; index <= endIndex; index++){
00601     id = bddManager->indexToId[index];
00602     uniqueTableForId = bddManager->uniqueTable[id];
00603     nodeManager = uniqueTableForId->nodeManager;
00604     uniqueTableForId->endNode->nextBddNode = nodeManager->freeNodeList;
00605     nodeManager->freeNodeList = uniqueTableForId->startNode.nextBddNode;
00606     uniqueTableForId->endNode = &(uniqueTableForId->startNode);
00607     uniqueTableForId->startNode.nextBddNode = NULL;
00608   }
00609   bddManager->numForwardedNodes = 0;
00610 }
00611 
00612 
00613 
00614 /*---------------------------------------------------------------------------*/
00615 /* Definition of static functions                                          */
00616 /*---------------------------------------------------------------------------*/
00617