00001
00040 #include "calInt.h"
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058
00059
00060
00061
00062
00065
00066
00067
00068
00069
00072
00073
00074
00075
00076
00077
00078
00090 void
00091 CalHashTableApply(Cal_BddManager_t * bddManager, CalHashTable_t *
00092 hashTable, CalHashTable_t ** reqQueAtPipeDepth, CalOpProc_t
00093 calOpProc)
00094 {
00095 int i, numBins;
00096 CalBddNode_t **bins = 0;
00097 CalRequestNode_t *requestNode;
00098 Cal_Bdd_t fx, gx, fxbar, gxbar, result;
00099 Cal_BddId_t bddId;
00100
00101 numBins = hashTable->numBins;
00102 bins = hashTable->bins;
00103 for(i = 0; i < numBins; i++){
00104 for(requestNode = bins[i];
00105 requestNode != Cal_Nil(CalRequestNode_t);
00106 requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00107
00108 CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar);
00109 Cal_Assert(((CalAddress_t)(fx.bddNode)) & ~0xf);
00110 Cal_Assert(((CalAddress_t)(gx.bddNode)) & ~0xf);
00111 Cal_Assert(((CalAddress_t)(fxbar.bddNode)) & ~0xf);
00112 Cal_Assert(((CalAddress_t)(gxbar.bddNode)) & ~0xf);
00113 if((*calOpProc)(bddManager, fx, gx, &result) == 0){
00114 CalBddNormalize(fx, gx);
00115 CalBddGetMinId2(bddManager, fx, gx, bddId);
00116 CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fx, gx, &result);
00117 }
00118 CalBddIcrRefCount(result);
00119 CalRequestNodePutThenRequest(requestNode, result);
00120 if((*calOpProc)(bddManager, fxbar, gxbar, &result) == 0){
00121 CalBddNormalize(fxbar, gxbar);
00122 CalBddGetMinId2(bddManager, fxbar, gxbar, bddId);
00123 CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fxbar, gxbar, &result);
00124 }
00125 CalBddIcrRefCount(result);
00126 CalRequestNodePutElseRequest(requestNode, result);
00127 }
00128 }
00129 }
00130
00142 void
00143 CalHashTableReduce(Cal_BddManager_t * bddManager,
00144 CalHashTable_t * hashTable,
00145 CalHashTable_t * uniqueTableForId)
00146 {
00147 int i, numBins = hashTable->numBins;
00148 CalBddNode_t **bins = hashTable->bins;
00149 Cal_BddId_t currentBddId = uniqueTableForId->bddId;
00150 CalNodeManager_t *nodeManager = uniqueTableForId->nodeManager;
00151 CalRequestNode_t *requestNode, *next;
00152 CalBddNode_t *bddNode, *endNode;
00153 Cal_Bdd_t thenBdd, elseBdd, result;
00154 Cal_BddRefCount_t refCount;
00155
00156 endNode = hashTable->endNode;
00157 for(i = 0; i < numBins; i++){
00158 for(requestNode = bins[i];
00159 requestNode != Cal_Nil(CalRequestNode_t);
00160 requestNode = next){
00161 next = CalRequestNodeGetNextRequestNode(requestNode);
00162
00163 CalRequestNodeGetThenRequest(requestNode, thenBdd);
00164 CalRequestNodeGetElseRequest(requestNode, elseBdd);
00165 CalRequestIsForwardedTo(thenBdd);
00166 CalRequestIsForwardedTo(elseBdd);
00167 if(CalBddIsEqual(thenBdd, elseBdd)){
00168 CalRequestNodeGetRefCount(requestNode, refCount);
00169 CalRequestAddRefCount(thenBdd, refCount - 2);
00170 CalRequestNodePutThenRequest(requestNode, thenBdd);
00171 CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00172 endNode->nextBddNode = requestNode;
00173 endNode = requestNode;
00174 }
00175 else
00176 if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
00177 thenBdd, elseBdd, &result) == 1){
00178 CalBddDcrRefCount(thenBdd);
00179 CalBddDcrRefCount(elseBdd);
00180 CalRequestNodeGetRefCount(requestNode, refCount);
00181 CalBddAddRefCount(result, refCount);
00182 CalRequestNodePutThenRequest(requestNode, result);
00183 CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00184 endNode->nextBddNode = requestNode;
00185 endNode = requestNode;
00186 }
00187 else if(CalBddIsOutPos(thenBdd)){
00188 CalRequestNodePutThenRequest(requestNode, thenBdd);
00189 CalRequestNodePutElseRequest(requestNode, elseBdd);
00190 CalHashTableAddDirect(uniqueTableForId, requestNode);
00191 bddManager->numNodes++;
00192 bddManager->gcCheck--;
00193 }
00194 else{
00195 CalNodeManagerAllocNode(nodeManager, bddNode);
00196 CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
00197 CalBddNodePutThenBddNode(bddNode, CalBddGetBddNodeNot(thenBdd));
00198 CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
00199 CalBddNodePutElseBddNode(bddNode, CalBddGetBddNodeNot(elseBdd));
00200 CalRequestNodeGetRefCount(requestNode, refCount);
00201 CalBddNodePutRefCount(bddNode, refCount);
00202 CalHashTableAddDirect(uniqueTableForId, bddNode);
00203 bddManager->numNodes++;
00204 bddManager->gcCheck--;
00205 CalRequestNodePutThenRequestId(requestNode, currentBddId);
00206 CalRequestNodePutThenRequestNode(requestNode, CalBddNodeNot(bddNode));
00207 CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00208 endNode->nextBddNode = requestNode;
00209 endNode = requestNode;
00210 }
00211 }
00212 }
00213 memset((char *)bins, 0, hashTable->numBins * sizeof(CalBddNode_t *));
00214 hashTable->endNode = endNode;
00215 }
00216
00217
00218
00219
00220
00221
00222
00223
00224
