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 static void CalHashTableSwapVarsApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_BddIndex_t gIndex, Cal_BddIndex_t hIndex, CalHashTable_t ** reqQueForSwapVars, CalHashTable_t ** reqQueForSwapVarsPlus, CalHashTable_t ** reqQueForSwapVarsMinus, CalHashTable_t ** reqQueForCompose, CalHashTable_t ** reqQueForITE);
00070 static void CalHashTableSwapVarsPlusApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_BddIndex_t hIndex, CalHashTable_t ** reqQueForSwapVars, CalHashTable_t ** reqQueForSwapVarsPlus, CalHashTable_t ** reqQueForSwapVarsMinus, CalHashTable_t ** reqQueForCompose);
00071 static void CalHashTableSwapVarsMinusApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_BddIndex_t hIndex, CalHashTable_t ** reqQueForSwapVars, CalHashTable_t ** reqQueForSwapVarsPlus, CalHashTable_t ** reqQueForSwapVarsMinus, CalHashTable_t ** reqQueForCompose);
00072
00075
00076
00077
00078
00091 Cal_Bdd
00092 Cal_BddSwapVars(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
00093 Cal_Bdd gUserBdd,
00094 Cal_Bdd hUserBdd)
00095 {
00096 Cal_Bdd_t f,g,h,tmpBdd;
00097 Cal_BddIndex_t gIndex, hIndex;
00098 CalRequest_t result;
00099 int bddId, bddIndex;
00100 CalHashTable_t *hashTable;
00101 CalHashTable_t *uniqueTableForId;
00102 CalHashTable_t **reqQueForSwapVars = bddManager->reqQue[0];
00103 CalHashTable_t **reqQueForSwapVarsPlus = bddManager->reqQue[1];
00104 CalHashTable_t **reqQueForSwapVarsMinus = bddManager->reqQue[2];
00105 CalHashTable_t **reqQueForCompose = bddManager->reqQue[3];
00106 CalHashTable_t **reqQueForITE = bddManager->reqQue[4];
00107
00108 if (CalBddPreProcessing(bddManager, 3, fUserBdd, gUserBdd, hUserBdd) == 0){
00109 return (Cal_Bdd) 0;
00110 }
00111 f = CalBddGetInternalBdd(bddManager, fUserBdd);
00112 g = CalBddGetInternalBdd(bddManager, gUserBdd);
00113 h = CalBddGetInternalBdd(bddManager, hUserBdd);
00114
00115 if(CalBddIsBddConst(g) || CalBddIsBddConst(h)){
00116 CalBddWarningMessage("Unacceptable arguments for Cal_BddSwapVars");
00117 return (Cal_Bdd) 0;
00118 }
00119 if(CalBddIsEqual(g, h)){
00120
00121
00122
00123 return CalBddGetExternalBdd(bddManager, f);
00124 }
00125 if(CalBddGetBddIndex(bddManager, g) > CalBddGetBddIndex(bddManager, h)){
00126 tmpBdd = g;
00127 g = h;
00128 h = tmpBdd;
00129 }
00130
00131 gIndex = CalBddGetBddIndex(bddManager, g);
00132 hIndex = CalBddGetBddIndex(bddManager, h);
00133
00134 CalBddGetMinId2(bddManager, f, g, bddId);
00135 CalHashTableFindOrAdd(reqQueForSwapVars[bddId], f,
00136 bddManager->bddNull, &result);
00137
00138
00139 for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00140 bddId = bddManager->indexToId[bddIndex];
00141 hashTable = reqQueForSwapVars[bddId];
00142 if(hashTable->numEntries){
00143 CalHashTableSwapVarsApply(bddManager, hashTable, gIndex, hIndex,
00144 reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus,
00145 reqQueForCompose, reqQueForITE);
00146 }
00147 hashTable = reqQueForSwapVarsPlus[bddId];
00148 if(hashTable->numEntries){
00149 CalHashTableSwapVarsPlusApply(bddManager, hashTable, hIndex,
00150 reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus,
00151 reqQueForCompose);
00152 }
00153 hashTable = reqQueForSwapVarsMinus[bddId];
00154 if(hashTable->numEntries){
00155 CalHashTableSwapVarsMinusApply(bddManager, hashTable, hIndex,
00156 reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus,
00157 reqQueForCompose);
00158 }
00159 hashTable = reqQueForCompose[bddId];
00160 if(hashTable->numEntries){
00161 CalHashTableComposeApply(bddManager, hashTable, hIndex,
00162 reqQueForCompose, reqQueForITE);
00163 }
00164 hashTable = reqQueForITE[bddId];
00165 if(hashTable->numEntries){
00166 CalHashTableITEApply(bddManager, hashTable, reqQueForITE);
00167 }
00168 }
00169
00170
00171 for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00172 bddId = bddManager->indexToId[bddIndex];
00173 uniqueTableForId = bddManager->uniqueTable[bddId];
00174 hashTable = reqQueForSwapVars[bddId];
00175 if(hashTable->numEntries){
00176 CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00177 }
00178 hashTable = reqQueForSwapVarsPlus[bddId];
00179 if(hashTable->numEntries){
00180 CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00181 }
00182 hashTable = reqQueForSwapVarsMinus[bddId];
00183 if(hashTable->numEntries){
00184 CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00185 }
00186 hashTable = reqQueForCompose[bddId];
00187 if(hashTable->numEntries){
00188 CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00189 }
00190 hashTable = reqQueForITE[bddId];
00191 if(hashTable->numEntries){
00192 CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00193 }
00194 }
00195
00196 CalRequestIsForwardedTo(result);
00197
00198
00199 for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00200 CalHashTableCleanUp(reqQueForSwapVars[bddId]);
00201 CalHashTableCleanUp(reqQueForSwapVarsPlus[bddId]);
00202 CalHashTableCleanUp(reqQueForSwapVarsMinus[bddId]);
00203 CalHashTableCleanUp(reqQueForCompose[bddId]);
00204 CalHashTableCleanUp(reqQueForITE[bddId]);
00205 }
00206 return CalBddGetExternalBdd(bddManager, result);
00207 }
00208
00209
00210
00211
00212
00213
00214
00215
00216
00228 static void
00229 CalHashTableSwapVarsApply(
00230 Cal_BddManager_t * bddManager,
00231 CalHashTable_t * hashTable,
00232 Cal_BddIndex_t gIndex,
00233 Cal_BddIndex_t hIndex,
00234 CalHashTable_t ** reqQueForSwapVars,
00235 CalHashTable_t ** reqQueForSwapVarsPlus,
00236 CalHashTable_t ** reqQueForSwapVarsMinus,
00237 CalHashTable_t ** reqQueForCompose,
00238 CalHashTable_t ** reqQueForITE)
00239 {
00240 int i, numBins = hashTable->numBins;
00241 CalBddNode_t **bins = hashTable->bins;
00242 CalRequestNode_t *requestNode;
00243 Cal_BddId_t bddId;
00244 Cal_BddIndex_t fIndex, bddIndex;
00245 Cal_Bdd_t f, calBdd;
00246 Cal_Bdd_t thenBdd, elseBdd;
00247 Cal_Bdd_t nullBdd = bddManager->bddNull;
00248 Cal_Bdd_t result;
00249
00250 for(i = 0; i < numBins; i++){
00251 for(requestNode = bins[i];
00252 requestNode != Cal_Nil(CalRequestNode_t);
00253 requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00254 CalRequestNodeGetF(requestNode, f);
00255 fIndex = CalBddGetBddIndex(bddManager, f);
00256 if(fIndex < gIndex){
00257
00258 CalBddGetThenBdd(f, calBdd);
00259 bddId = CalBddGetBddId(calBdd);
00260 bddIndex = bddManager->idToIndex[bddId];
00261 if(bddIndex <= hIndex){
00262 if(bddIndex > gIndex){
00263 bddId = bddManager->indexToId[gIndex];
00264 }
00265 CalHashTableFindOrAdd(reqQueForSwapVars[bddId],
00266 calBdd, nullBdd, &calBdd);
00267 }
00268 CalBddIcrRefCount(calBdd);
00269 CalRequestNodePutThenRequest(requestNode, calBdd);
00270
00271 CalBddGetElseBdd(f, calBdd);
00272 bddId = CalBddGetBddId(calBdd);
00273 bddIndex = bddManager->idToIndex[bddId];
00274 if(bddIndex <= hIndex){
00275 if(bddIndex > gIndex){
00276 bddId = bddManager->indexToId[gIndex];
00277 }
00278 CalHashTableFindOrAdd(reqQueForSwapVars[bddId],
00279 calBdd, nullBdd, &calBdd);
00280 }
00281 CalBddIcrRefCount(calBdd);
00282 CalRequestNodePutElseRequest(requestNode, calBdd);
00283 }
00284 else if(fIndex == gIndex){
00285
00286 CalBddGetThenBdd(f, thenBdd);
00287 CalBddGetElseBdd(f, elseBdd);
00288 if(CalBddGetBddIndex(bddManager, thenBdd) == hIndex){
00289 CalBddGetThenBdd(thenBdd, thenBdd);
00290 }
00291 if(CalBddGetBddIndex(bddManager, elseBdd) == hIndex){
00292 CalBddGetThenBdd(elseBdd, elseBdd);
00293 }
00294 if(CalBddIsEqual(thenBdd, elseBdd)){
00295 if(hIndex > CalBddGetBddIndex(bddManager, thenBdd)){
00296 CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(thenBdd)],
00297 thenBdd, CalBddOne(bddManager), &result);
00298 }
00299 else{
00300 result = thenBdd;
00301 }
00302 }
00303 else if(hIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
00304 hIndex < CalBddGetBddIndex(bddManager, elseBdd)){
00305 bddId = bddManager->indexToId[hIndex];
00306 if(!CalUniqueTableForIdFindOrAdd(bddManager,
00307 bddManager->uniqueTable[bddId], thenBdd, elseBdd, &result)){
00308 CalBddIcrRefCount(thenBdd);
00309 CalBddIcrRefCount(elseBdd);
00310 }
00311 }
00312 else{
00313 CalBddGetMinId2(bddManager, thenBdd, elseBdd, bddId);
00314 CalHashTableFindOrAdd(reqQueForSwapVarsPlus[bddId],
00315 thenBdd, elseBdd, &result);
00316 }
00317 CalBddIcrRefCount(result);
00318 CalRequestNodePutThenRequest(requestNode, result);
00319
00320 CalBddGetThenBdd(f, thenBdd);
00321 CalBddGetElseBdd(f, elseBdd);
00322 if(CalBddGetBddIndex(bddManager, thenBdd) == hIndex){
00323 CalBddGetElseBdd(thenBdd, thenBdd);
00324 }
00325 if(CalBddGetBddIndex(bddManager, elseBdd) == hIndex){
00326 CalBddGetElseBdd(elseBdd, elseBdd);
00327 }
00328 if(CalBddIsEqual(thenBdd, elseBdd)){
00329 if(hIndex > CalBddGetBddIndex(bddManager, thenBdd)){
00330 CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(thenBdd)],
00331 thenBdd, CalBddZero(bddManager), &result);
00332 }
00333 else{
00334 result = thenBdd;
00335 }
00336 }
00337 else if(hIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
00338 hIndex < CalBddGetBddIndex(bddManager, elseBdd)){
00339 bddId = bddManager->indexToId[hIndex];
00340 if(!CalUniqueTableForIdFindOrAdd(bddManager,
00341 bddManager->uniqueTable[bddId], thenBdd, elseBdd, &result)){
00342 CalBddIcrRefCount(thenBdd);
00343 CalBddIcrRefCount(elseBdd);
00344 }
00345 }
00346 else{
00347 CalBddGetMinId2(bddManager, thenBdd, elseBdd, bddId);
00348 CalHashTableFindOrAdd(reqQueForSwapVarsMinus[bddId],
00349 thenBdd, elseBdd, &result);
00350 }
00351 CalBddIcrRefCount(result);
00352 CalRequestNodePutElseRequest(requestNode, result);
00353 }
00354 else{
00355 CalComposeRequestCreate(bddManager,
00356 f, CalBddOne(bddManager), hIndex,
00357 reqQueForCompose, reqQueForITE, &result);
00358 CalBddIcrRefCount(result);
00359 CalRequestNodePutThenRequest(requestNode, result);
00360 CalComposeRequestCreate(bddManager,
00361 f, CalBddZero(bddManager), hIndex,
00362 reqQueForCompose, reqQueForITE, &result);
00363 CalBddIcrRefCount(result);
00364 CalRequestNodePutElseRequest(requestNode, result);
00365 }
00366 }
00367 }
00368 }
00369
00370
00382 static void
00383 CalHashTableSwapVarsPlusApply(
00384 Cal_BddManager_t * bddManager,
00385 CalHashTable_t * hashTable,
00386 Cal_BddIndex_t hIndex,
00387 CalHashTable_t ** reqQueForSwapVars,
00388 CalHashTable_t ** reqQueForSwapVarsPlus,
00389 CalHashTable_t ** reqQueForSwapVarsMinus,
00390 CalHashTable_t ** reqQueForCompose)
00391 {
00392 int i, numBins = hashTable->numBins;
00393 CalBddNode_t **bins = hashTable->bins;
00394 CalRequestNode_t *requestNode;
00395 Cal_BddId_t bddId;
00396 Cal_Bdd_t f1, f2, g1, g2;
00397 Cal_Bdd_t result;
00398
00399 for(i = 0; i < numBins; i++){
00400 for(requestNode = bins[i];
00401 requestNode != Cal_Nil(CalRequestNode_t);
00402 requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00403 CalRequestNodeGetCofactors(bddManager, requestNode, f1, f2, g1, g2);
00404
00405 if(CalBddGetBddIndex(bddManager, f1) == hIndex){
00406 CalBddGetThenBdd(f1, f1);
00407 }
00408 if(CalBddGetBddIndex(bddManager, g1) == hIndex){
00409 CalBddGetThenBdd(g1, g1);
00410 }
00411 if(CalBddIsEqual(f1, g1)){
00412 if(hIndex > CalBddGetBddIndex(bddManager, f1)){
00413 CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(f1)],
00414 f1, CalBddOne(bddManager), &result);
00415 }
00416 else{
00417 result = f1;
00418 }
00419 }
00420 else if(hIndex < CalBddGetBddIndex(bddManager, f1) &&
00421 hIndex < CalBddGetBddIndex(bddManager, g1)){
00422 bddId = bddManager->indexToId[hIndex];
00423 if(!CalUniqueTableForIdFindOrAdd(bddManager,
00424 bddManager->uniqueTable[bddId], f1, g1, &result)){
00425 CalBddIcrRefCount(f1);
00426 CalBddIcrRefCount(g1);
00427 }
00428 }
00429 else{
00430 CalBddGetMinId2(bddManager, f1, g1, bddId);
00431 CalHashTableFindOrAdd(reqQueForSwapVarsPlus[bddId], f1, g1, &result);
00432 }
00433 CalBddIcrRefCount(result);
00434 CalRequestNodePutThenRequest(requestNode, result);
00435
00436 if(CalBddGetBddIndex(bddManager, f2) == hIndex){
00437 CalBddGetThenBdd(f2, f2);
00438 }
00439 if(CalBddGetBddIndex(bddManager, g2) == hIndex){
00440 CalBddGetThenBdd(g2, g2);
00441 }
00442 if(CalBddIsEqual(f2, g2)){
00443 if(hIndex > CalBddGetBddIndex(bddManager, f2)){
00444 CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(f2)],
00445 f2, CalBddOne(bddManager), &result);
00446 }
00447 else{
00448 result = f2;
00449 }
00450 }
00451 else if(hIndex < CalBddGetBddIndex(bddManager, f2) &&
00452 hIndex < CalBddGetBddIndex(bddManager, g2)){
00453 bddId = bddManager->indexToId[hIndex];
00454 if(!CalUniqueTableForIdFindOrAdd(bddManager,
00455 bddManager->uniqueTable[bddId], f2, g2, &result)){
00456 CalBddIcrRefCount(f2);
00457 CalBddIcrRefCount(g2);
00458 }
00459 }
00460 else{
00461 CalBddGetMinId2(bddManager, f2, g2, bddId);
00462 CalHashTableFindOrAdd(reqQueForSwapVarsPlus[bddId], f2, g2, &result);
00463 }
00464 CalBddIcrRefCount(result);
00465 CalRequestNodePutElseRequest(requestNode, result);
00466 }
00467 }
00468 }
00469
00481 static void
00482 CalHashTableSwapVarsMinusApply(
00483 Cal_BddManager_t * bddManager,
00484 CalHashTable_t * hashTable,
00485 Cal_BddIndex_t hIndex,
00486 CalHashTable_t ** reqQueForSwapVars,
00487 CalHashTable_t ** reqQueForSwapVarsPlus,
00488 CalHashTable_t ** reqQueForSwapVarsMinus,
00489 CalHashTable_t ** reqQueForCompose)
00490 {
00491 int i, numBins = hashTable->numBins;
00492 CalBddNode_t **bins = hashTable->bins;
00493 CalRequestNode_t *requestNode;
00494 Cal_BddId_t bddId;
00495 Cal_Bdd_t f1, f2, g1, g2;
00496 Cal_Bdd_t result;
00497
00498 for(i = 0; i < numBins; i++){
00499 for(requestNode = bins[i];
00500 requestNode != Cal_Nil(CalRequestNode_t);
00501 requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00502 CalRequestNodeGetCofactors(bddManager, requestNode, f1, f2, g1, g2);
00503
00504 if(CalBddGetBddIndex(bddManager, f1) == hIndex){
00505 CalBddGetElseBdd(f1, f1);
00506 }
00507 if(CalBddGetBddIndex(bddManager, g1) == hIndex){
00508 CalBddGetElseBdd(g1, g1);
00509 }
00510 if(CalBddIsEqual(f1, g1)){
00511 if(hIndex > CalBddGetBddIndex(bddManager, f1)){
00512 CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(f1)],
00513 f1, CalBddZero(bddManager), &result);
00514 }
00515 else{
00516 result = f1;
00517 }
00518 }
00519 else if(hIndex < CalBddGetBddIndex(bddManager, f1) &&
00520 hIndex < CalBddGetBddIndex(bddManager, g1)){
00521 bddId = bddManager->indexToId[hIndex];
00522 if(!CalUniqueTableForIdFindOrAdd(bddManager,
00523 bddManager->uniqueTable[bddId], f1, g1, &result)){
00524 CalBddIcrRefCount(f1);
00525 CalBddIcrRefCount(g1);
00526 }
00527 }
00528 else{
00529 CalBddGetMinId2(bddManager, f1, g1, bddId);
00530 CalHashTableFindOrAdd(reqQueForSwapVarsMinus[bddId], f1, g1, &result);
00531 }
00532 CalBddIcrRefCount(result);
00533 CalRequestNodePutThenRequest(requestNode, result);
00534
00535 if(CalBddGetBddIndex(bddManager, f2) == hIndex){
00536 CalBddGetElseBdd(f2, f2);
00537 }
00538 if(CalBddGetBddIndex(bddManager, g2) == hIndex){
00539 CalBddGetElseBdd(g2, g2);
00540 }
00541 if(CalBddIsEqual(f2, g2)){
00542 if(hIndex > CalBddGetBddIndex(bddManager, f2)){
00543 CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(f2)],
00544 f2, CalBddZero(bddManager), &result);
00545 }
00546 else{
00547 result = f2;
00548 }
00549 }
00550 else if(hIndex < CalBddGetBddIndex(bddManager, f2) &&
00551 hIndex < CalBddGetBddIndex(bddManager, g2)){
00552 bddId = bddManager->indexToId[hIndex];
00553 if(!CalUniqueTableForIdFindOrAdd(bddManager,
00554 bddManager->uniqueTable[bddId], f2, g2, &result)){
00555 CalBddIcrRefCount(f2);
00556 CalBddIcrRefCount(g2);
00557 }
00558 }
00559 else{
00560 CalBddGetMinId2(bddManager, f2, g2, bddId);
00561 CalHashTableFindOrAdd(reqQueForSwapVarsMinus[bddId], f2, g2, &result);
00562 }
00563 CalBddIcrRefCount(result);
00564 CalRequestNodePutElseRequest(requestNode, result);
00565 }
00566 }
00567 }
00568
00569
00570
00571
00572
00573
00574
00575
00576
00577
00578
00579
00580
00581
