VIS

src/baig/baigBddSweep.c

Go to the documentation of this file.
00001 
00018 #include "maig.h"
00019 #include "ntk.h"
00020 #include "cmd.h"
00021 #include "baig.h"
00022 #include "baigInt.h"
00023 #include "heap.h"
00024 #include "ntmaig.h"
00025 #include "ord.h"
00026 
00027 static char rcsid[] UNUSED = "$Id: baigBddSweep.c,v 1.13 2005/05/18 18:11:42 jinh Exp $";
00028 
00029 /*---------------------------------------------------------------------------*/
00030 /* Constant declarations                                                     */
00031 /*---------------------------------------------------------------------------*/
00032 
00033 
00034 /*---------------------------------------------------------------------------*/
00035 /* Stucture declarations                                                     */
00036 /*---------------------------------------------------------------------------*/
00037 
00038 
00039 /*---------------------------------------------------------------------------*/
00040 /* Type declarations                                                         */
00041 /*---------------------------------------------------------------------------*/
00042 
00043 
00044 /*---------------------------------------------------------------------------*/
00045 /* Variable declarations                                                     */
00046 /*---------------------------------------------------------------------------*/
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Macro declarations                                                        */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00055 /*---------------------------------------------------------------------------*/
00056 /* Static function prototypes                                                */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 static int SweepBddCompare(const char *x, const char *y);
00060 static int SweepBddHash(char *x, int size);
00061 
00065 /*---------------------------------------------------------------------------*/
00066 /* Definition of exported functions                                          */
00067 /*---------------------------------------------------------------------------*/
00068 void bAig_BuildAigBFSManner( Ntk_Network_t *network, mAig_Manager_t *manager, st_table *leaves, int sweep);
00069 void bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray);
00070 void bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray);
00071 
00083 static int
00084 SweepBddCompare(const char *x, const char *y)
00085 {
00086   return(bdd_ptrcmp((bdd_t *)x, (bdd_t *)y));
00087 }
00088 
00100 static int
00101 SweepBddHash(char *x, int size)
00102 {
00103 
00104   return(bdd_ptrhash((bdd_t *)x, size));
00105 }
00106 
00119 void
00120 bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray)
00121 {
00122   array_t *mVarList, *bVarList;
00123   bdd_t *bdd, *func;
00124   int bddIdIndex;
00125   int i, count, sizeLimit, mvfSize;
00126   int maxSize, curSize;
00127   array_t *tnodeArray;
00128   lsGen gen;
00129   st_generator *gen1;
00130   Ntk_Node_t *node;
00131   bAigEdge_t v;
00132   MvfAig_Function_t  *mvfAig;
00133   mAig_Manager_t *manager;
00134   mdd_manager *mgr;
00135   st_table *node2MvfAigTable;
00136   st_table * bdd2vertex;
00137   mAigMvar_t mVar;
00138   mAigBvar_t bVar;
00139   int index1, mAigId;
00140 
00141 
00142   manager = Ntk_NetworkReadMAigManager(network);
00143 
00144   mgr = Ntk_NetworkReadMddManager(network);
00145   if(mgr == 0) {
00146     Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, 
00147             Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c, 
00148             Ord_Unassigned_c, 0, 0);
00149     mgr = Ntk_NetworkReadMddManager(network);
00150   }
00151   node2MvfAigTable = 
00152       (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
00153 
00154   bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash);
00155 
00156   sizeLimit = 500;
00157   maxSize = manager->nodesArraySize;
00158 
00159   tnodeArray = 0;
00160   if(nodeArray == 0) {
00161     bVarList = mAigReadBinVarList(manager);
00162     mVarList = mAigReadMulVarList(manager);
00163     tnodeArray = array_alloc(bAigEdge_t, 0);
00164     Ntk_NetworkForEachLatch(network, gen, node) { 
00165       node = Ntk_LatchReadDataInput(node);
00166       st_lookup(node2MvfAigTable, node, &mvfAig);
00167       mvfSize = array_n(mvfAig);
00168       for(i=0; i<mvfSize; i++){
00169         v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
00170         array_insert_last(bAigEdge_t, tnodeArray, v);
00171       }
00172 
00173       mAigId = Ntk_NodeReadMAigId(node);
00174       mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
00175       for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
00176         bVar = array_fetch(mAigBvar_t, bVarList, index1++);
00177         v = bVar.node;
00178         v = bAig_GetCanonical(manager, v);
00179         array_insert_last(bAigEdge_t, tnodeArray, v);
00180       }
00181     }
00182     Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 
00183       st_lookup(node2MvfAigTable, node, &mvfAig);
00184       mvfSize = array_n(mvfAig);
00185       for(i=0; i<mvfSize; i++){
00186         v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
00187         array_insert_last(bAigEdge_t, tnodeArray, v);
00188       }
00189     }
00190   }
00191 
00192   count = bAigNodeID(manager->nodesArraySize);
00193   for(i=0; i<count; i++) {
00194     manager->bddIdArray[i] = -1;
00195     manager->bddArray[i] = 0;
00196   }
00197   manager->bddArray[0] = bdd_zero(mgr);
00198 
00199   bddIdIndex = 0;
00200   for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
00201     if(leftChild(i) != 2)       continue;
00202     bdd = bdd_get_variable(mgr, bddIdIndex);
00203     manager->bddIdArray[bAigNodeID(i)] = bddIdIndex;
00204     manager->bddArray[bAigNodeID(i)] = bdd;
00205     bddIdIndex++;
00206   }
00207 
00208   if(nodeArray) {
00209     for(i=0; i<array_n(nodeArray); i++) {
00210       v = array_fetch(bAigEdge_t, nodeArray, i);
00211       v = bAig_GetCanonical(manager, v);
00212       bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
00213     }
00214   }
00215   else {
00216     for(i=0; i<array_n(tnodeArray); i++) {
00217       v = array_fetch(bAigEdge_t, tnodeArray, i);
00218       v = bAig_GetCanonical(manager, v);
00219       bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
00220     }
00221     array_free(tnodeArray);
00222   }
00223   
00224   count = bAigNodeID(manager->nodesArraySize);
00225   for(i=0; i<count; i++) {
00226     if(manager->bddArray[i])    {
00227       bdd_free(manager->bddArray[i]);
00228       manager->bddArray[i] = 0;
00229     }
00230   }
00231 
00232   st_foreach_item(bdd2vertex, gen1, &func, &v) {
00233     bdd_free(func);
00234   }
00235   st_free_table(bdd2vertex);
00236 
00237   count = bAigNodeID(manager->nodesArraySize);
00238   curSize = 0;
00239   for(i=0; i<count; i++) {
00240     if(bAigGetPassFlag(manager, i*bAigNodeSize)) {
00241       curSize++;
00242     }
00243   }
00244   /*
00245   fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n", 
00246           maxSize/bAigNodeSize, count, (maxSize-curSize)/bAigNodeSize);
00247   fflush(vis_stdout);
00248   */
00249   return;
00250 
00251 }
00252 
00264 void
00265 bAig_BddSweepSub(
00266         bAig_Manager_t *manager, 
00267         mdd_manager *mgr, 
00268         bAigEdge_t v, 
00269         st_table *bdd2vertex,
00270         int sizeLimit,
00271         int *newBddIdIndex)
00272 {
00273   bAigEdge_t left, right, oldV, nv;
00274   bdd_t *leftBdd, *rightBdd;
00275   bdd_t *func, *nfunc, *funcBar, *newBdd;
00276   int newId, size;
00277 
00278   if(v == 0 || v == 1)  return;
00279   if(manager->bddArray[bAigNodeID(v)]) {
00280     return;
00281   }
00282 
00283   left = leftChild(v);
00284   right = rightChild(v);
00285   left = bAig_GetCanonical(manager, left);
00286   right = bAig_GetCanonical(manager, right);
00287 
00288   if(left == 2 && right == 2) {
00289     return;
00290   }
00291 
00292   bAig_BddSweepSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
00293   bAig_BddSweepSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
00294 
00295   v = bAig_GetCanonical(manager, v);
00296   if(manager->bddArray[bAigNodeID(v)]) {
00297     return;
00298   }
00299 
00300   left = leftChild(v);
00301   right = rightChild(v);
00302   left = bAig_GetCanonical(manager, left);
00303   right = bAig_GetCanonical(manager, right);
00304 
00305   leftBdd = manager->bddArray[bAigNodeID(left)];
00306   rightBdd = manager->bddArray[bAigNodeID(right)];
00307 
00308   if(leftBdd == 0) {
00309     bAig_BddSweepSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
00310     left = bAig_GetCanonical(manager, left);
00311     leftBdd = manager->bddArray[bAigNodeID(left)];
00312   }
00313 
00314   if(rightBdd == 0) {
00315     bAig_BddSweepSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
00316     right = bAig_GetCanonical(manager, right);
00317     rightBdd = manager->bddArray[bAigNodeID(right)];
00318   }
00319 
00325   if(leftBdd == 0 || rightBdd == 0) {
00326     fprintf(vis_stdout, 
00327             "ERROR : all the nodes should have bdd node at this moment\n");
00328   }
00329 
00330   func = bdd_and(leftBdd, rightBdd, 
00331              !bAig_IsInverted(left), !bAig_IsInverted(right));
00332 
00333   if(bAig_IsInverted(v))        {
00334     funcBar = bdd_not(func);
00335     nfunc = funcBar;
00336   }
00337   else {
00338     nfunc = bdd_dup(func);
00339   }
00340 
00341   if(st_lookup(bdd2vertex, nfunc, &oldV)) {
00342     bAig_Merge(manager, oldV, v);
00343   }
00344   else {
00345     funcBar = bdd_not(nfunc);
00346     if(st_lookup(bdd2vertex, funcBar, &oldV)) {
00347       bAig_Merge(manager, bAig_Not(oldV), v);
00348     }
00349     bdd_free(funcBar);
00350   }
00351   bdd_free(nfunc);
00352 
00353   v = bAig_NonInvertedEdge(v);
00354   nv = bAig_GetCanonical(manager, v);
00355   v = nv;
00356 
00357   if(manager->bddArray[bAigNodeID(v)] == 0) {
00358     size = bdd_size(func);
00359     if(size > sizeLimit) {
00360       newId = *newBddIdIndex;
00361       (*newBddIdIndex) ++;
00362       newBdd = bdd_get_variable(mgr, newId);
00363       manager->bddIdArray[bAigNodeID(v)] = newId;
00364       bdd_free(func);
00365       func = newBdd;
00366       manager->bddArray[bAigNodeID(v)] = func;
00367       st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)bAig_NonInvertedEdge(v));
00368     }
00369     else {
00370       if(bAig_IsInverted(v)) {
00371         funcBar = bdd_not(func);
00372         manager->bddArray[bAigNodeID(v)] = funcBar;
00373         st_insert(bdd2vertex, (char *)func, (char *)v);
00374       }
00375       else {
00376         manager->bddArray[bAigNodeID(v)] = func;
00377         st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)v);
00378       }
00379     }
00380   }
00381   else  bdd_free(func);
00382 
00383 }
00384 
00396 void
00397 bAig_BuildAigBFSManner(
00398         Ntk_Network_t *network, 
00399         mAig_Manager_t *manager, 
00400         st_table *leaves,
00401         int sweep)
00402 {
00403 array_t *nodeArray, *result;
00404 lsGen gen1;
00405 int iter, maxLevel, level;
00406 int i, j, k;
00407 bAigEdge_t v;
00408 Ntk_Node_t *node, *fanin, *fanout;
00409 st_table *node2mvfAigTable;
00410 array_t *curArray, *nextArray, *tmpArray;
00411 array_t *levelArray, *clevelArray;
00412 MvfAig_Function_t  *mvfAig;
00413 int mvfSize;
00414 st_generator *gen;
00415 
00416   Ntk_NetworkForEachNode(network, gen1, node) {
00417     Ntk_NodeSetUndef(node, (void *)0);
00418   }
00419 
00420   curArray = array_alloc(Ntk_Node_t *, 0);
00421   st_foreach_item(leaves, gen, &node, &fanout) {
00422     array_insert_last(Ntk_Node_t *, curArray, node);
00423     Ntk_NodeSetUndef(node, (void *)1);
00424   }
00425 
00426   levelArray = array_alloc(array_t *, 10);
00427   nextArray = array_alloc(Ntk_Node_t *, 0);
00428   iter = 0;
00429   while(1) {
00430     clevelArray = array_alloc(array_t *, 10);
00431     array_insert_last(array_t *, levelArray, clevelArray);
00432     for(i=0; i<array_n(curArray); i++) {
00433       node = array_fetch(Ntk_Node_t *, curArray, i);
00434       Ntk_NodeForEachFanout(node, j, fanout) {  
00435 
00436         level = (int)(long)Ntk_NodeReadUndef(fanout);
00437         if(level > 0)   continue;
00438 
00439         maxLevel = 0;
00440         Ntk_NodeForEachFanin(fanout, k, fanin) {
00441           level = (int)(long)Ntk_NodeReadUndef(fanin);
00442           if(level == 0) {
00443             maxLevel = 0;
00444             break;
00445           }
00446           else if(level > maxLevel) {
00447             maxLevel = level;
00448           }
00449         }
00450 
00451         if(maxLevel > 0) {
00452           Ntk_NodeSetUndef(fanout, (void *)(long)(maxLevel+1));
00453           array_insert_last(Ntk_Node_t *, nextArray, fanout);
00454           array_insert_last(Ntk_Node_t *, clevelArray, fanout);
00455         }
00456       }
00457     }
00458     
00459     curArray->num = 0;
00460     tmpArray = curArray;
00461     curArray = nextArray;
00462     nextArray = tmpArray;
00463     if(curArray->num == 0)      break;
00464 
00465     iter++;
00466   }
00467 
00468   Ntk_NetworkForEachNode(network, gen1, node) {
00469     Ntk_NodeSetUndef(node, (void *)0);
00470   }
00471 
00472   for(i=0; i<array_n(levelArray); i++) {
00473     clevelArray = array_fetch(array_t *, levelArray, i);
00474     result = ntmaig_NetworkBuildMvfAigs(network, clevelArray, leaves);
00475     MvfAig_FunctionArrayFree(result);
00476     node2mvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(
00477             network, MVFAIG_NETWORK_APPL_KEY);
00478 
00479     if(i < 50 && sweep) {
00480       nodeArray = array_alloc(bAigEdge_t, 0);
00481       for(j=0; j<array_n(clevelArray); j++) {
00482         node = array_fetch(Ntk_Node_t *, clevelArray, j);
00483         st_lookup(node2mvfAigTable, node, &mvfAig);
00484         mvfSize = array_n(mvfAig);
00485         for(k=0; k<mvfSize; k++){
00486           v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k));
00487           array_insert_last(bAigEdge_t, nodeArray, v);
00488         }
00489       }
00490 
00491       bAig_BddSweepForceMain(network, nodeArray);
00492   
00493       for(j=0; j<array_n(clevelArray); j++) {
00494         node = array_fetch(Ntk_Node_t *, clevelArray, j);
00495         st_lookup(node2mvfAigTable, node, &mvfAig);
00496         mvfSize = array_n(mvfAig);
00497         for(k=0; k<mvfSize; k++){
00498           v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k));
00499           array_insert(bAigEdge_t, nodeArray, v, k);
00500         }
00501       }
00502       array_free(nodeArray);
00503     }
00504 
00505     array_free(clevelArray);
00506   }
00507   array_free(levelArray);
00508 }
00509 
00510 
00522 void
00523 bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray)
00524 {
00525   array_t *mVarList, *bVarList;
00526   bdd_t *bdd, *func;
00527   int bddIdIndex;
00528   int i, count, sizeLimit, mvfSize;
00529   int maxSize, curSize;
00530   array_t *tnodeArray;
00531   lsGen gen;
00532   st_generator *gen1;
00533   Ntk_Node_t *node;
00534   bAigEdge_t v;
00535   MvfAig_Function_t  *mvfAig;
00536   mAig_Manager_t *manager;
00537   mdd_manager *mgr;
00538   st_table *node2MvfAigTable;
00539   st_table * bdd2vertex;
00540   mAigMvar_t mVar;
00541   mAigBvar_t bVar;
00542   int index1, mAigId;
00543   int newmask, resetNewmask;
00544   int usedAig;
00545 
00546 
00547   manager = Ntk_NetworkReadMAigManager(network);
00548 
00549   mgr = Ntk_NetworkReadMddManager(network);
00550   if(mgr == 0) {
00551     Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, 
00552             Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c, 
00553             Ord_Unassigned_c, 0, 0);
00554     mgr = Ntk_NetworkReadMddManager(network);
00555   }
00556   node2MvfAigTable = 
00557       (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
00558 
00559   bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash);
00560 
00561   sizeLimit = 500;
00562   maxSize = manager->nodesArraySize;
00563 
00564   tnodeArray = 0;
00565   if(nodeArray == 0) {
00566     bVarList = mAigReadBinVarList(manager);
00567     mVarList = mAigReadMulVarList(manager);
00568     tnodeArray = array_alloc(bAigEdge_t, 0);
00569     Ntk_NetworkForEachLatch(network, gen, node) { 
00570       node = Ntk_LatchReadDataInput(node);
00571       st_lookup(node2MvfAigTable, node, &mvfAig);
00572       mvfSize = array_n(mvfAig);
00573       for(i=0; i<mvfSize; i++){
00574         v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
00575         array_insert_last(bAigEdge_t, tnodeArray, v);
00576       }
00577 
00578       mAigId = Ntk_NodeReadMAigId(node);
00579       mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
00580       for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
00581         bVar = array_fetch(mAigBvar_t, bVarList, index1++);
00582         v = bVar.node;
00583         v = bAig_GetCanonical(manager, v);
00584         array_insert_last(bAigEdge_t, tnodeArray, v);
00585       }
00586     }
00587     Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 
00588       st_lookup(node2MvfAigTable, node, &mvfAig);
00589       mvfSize = array_n(mvfAig);
00590       for(i=0; i<mvfSize; i++){
00591         v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
00592         array_insert_last(bAigEdge_t, tnodeArray, v);
00593       }
00594     }
00595   }
00596 
00597   count = bAigNodeID(manager->nodesArraySize);
00598   for(i=0; i<count; i++) {
00599     manager->bddIdArray[i] = -1;
00600     manager->bddArray[i] = 0;
00601   }
00602   manager->bddArray[0] = bdd_zero(mgr);
00603 
00604   bddIdIndex = 0;
00605   for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
00606     if(leftChild(i) != 2)       continue;
00607     bdd = bdd_get_variable(mgr, bddIdIndex);
00608     manager->bddIdArray[bAigNodeID(i)] = bddIdIndex;
00609     manager->bddArray[bAigNodeID(i)] = bdd;
00610     bddIdIndex++;
00611   }
00612 
00613   if(nodeArray) {
00614     for(i=0; i<array_n(nodeArray); i++) {
00615       v = array_fetch(bAigEdge_t, nodeArray, i);
00616       v = bAig_GetCanonical(manager, v);
00617       bAig_BddSweepForceSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
00618     }
00619   }
00620   else {
00621     for(i=0; i<array_n(tnodeArray); i++) {
00622       v = array_fetch(bAigEdge_t, tnodeArray, i);
00623       v = bAig_GetCanonical(manager, v);
00624       bAig_BddSweepForceSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
00625     }
00626   }
00627   
00628   count = bAigNodeID(manager->nodesArraySize);
00629   for(i=0; i<count; i++) {
00630     if(manager->bddArray[i])    {
00631       bdd_free(manager->bddArray[i]);
00632       manager->bddArray[i] = 0;
00633     }
00634   }
00635 
00636   st_foreach_item(bdd2vertex, gen1, &func, &v) {
00637     bdd_free(func);
00638   }
00639   st_free_table(bdd2vertex);
00640 
00641   count = bAigNodeID(manager->nodesArraySize);
00642   curSize = 0;
00643   for(i=0; i<count; i++) {
00644     if(bAigGetPassFlag(manager, i*bAigNodeSize)) {
00645       curSize++;
00646     }
00647   }
00648 
00649 
00650   newmask = 0x00000100;
00651   resetNewmask = 0xfffffeff;
00652   if(tnodeArray) {
00653   for(i=0; i<array_n(tnodeArray); i++) {
00654     v = array_fetch(int, tnodeArray, i);
00655     bAig_SetMaskTransitiveFanin(manager, v, newmask);
00656   }
00657 
00658   usedAig = 0;
00659   for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
00660     if(flags(i) & newmask)      usedAig++;
00661   }
00662 
00663   for(i=0; i<array_n(tnodeArray); i++) {
00664     v = array_fetch(int, tnodeArray, i);
00665     bAig_ResetMaskTransitiveFanin(manager, v, newmask, resetNewmask);
00666   }
00667   array_free(tnodeArray);
00668   fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n", 
00669           maxSize/bAigNodeSize, count, usedAig);
00670   fflush(vis_stdout);
00671   }
00672 
00673 }
00674 
00686 void
00687 bAig_BddSweepForceSub(
00688         bAig_Manager_t *manager, 
00689         mdd_manager *mgr, 
00690         bAigEdge_t v, 
00691         st_table *bdd2vertex,
00692         int sizeLimit,
00693         int *newBddIdIndex)
00694 {
00695   bAigEdge_t left, right, oldV, nv;
00696   bdd_t *leftBdd, *rightBdd;
00697   bdd_t *func, *nfunc, *funcBar, *newBdd;
00698   int newId, size;
00699 
00700   if(v == 0 || v == 1)  return;
00701   if(manager->bddArray[bAigNodeID(v)]) {
00702     return;
00703   }
00704 
00705 
00706   left = leftChild(v);
00707   right = rightChild(v);
00708   left = bAig_GetCanonical(manager, left);
00709   right = bAig_GetCanonical(manager, right);
00710 
00711   if(left == 2 && right == 2) {
00712     return;
00713   }
00714 
00715   bAig_BddSweepForceSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
00716   bAig_BddSweepForceSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
00717 
00718   v = bAig_GetCanonical(manager, v);
00719   if(manager->bddArray[bAigNodeID(v)]) {
00720     return;
00721   }
00722 
00723   left = leftChild(v);
00724   right = rightChild(v);
00725   left = bAig_GetCanonical(manager, left);
00726   right = bAig_GetCanonical(manager, right);
00727 
00728   leftBdd = manager->bddArray[bAigNodeID(left)];
00729   rightBdd = manager->bddArray[bAigNodeID(right)];
00730 
00731   if(leftBdd == 0) {
00732     bAig_BddSweepForceSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
00733     left = bAig_GetCanonical(manager, left);
00734     leftBdd = manager->bddArray[bAigNodeID(left)];
00735   }
00736 
00737   if(rightBdd == 0) {
00738     bAig_BddSweepForceSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
00739     right = bAig_GetCanonical(manager, right);
00740     rightBdd = manager->bddArray[bAigNodeID(right)];
00741   }
00742 
00748   if(leftBdd == 0 || rightBdd == 0) {
00749     fprintf(vis_stdout, 
00750             "ERROR : all the nodes should have bdd node at this moment\n");
00751   }
00752 
00753   func = bdd_and(leftBdd, rightBdd, 
00754              !bAig_IsInverted(left), !bAig_IsInverted(right));
00755 
00756   if(bAig_IsInverted(v))        {
00757     funcBar = bdd_not(func);
00758     nfunc = funcBar;
00759   }
00760   else {
00761     nfunc = bdd_dup(func);
00762   }
00763 
00764   if(st_lookup(bdd2vertex, nfunc, &oldV)) {
00765     bAig_Merge(manager, oldV, v);
00766   }
00767   else {
00768     funcBar = bdd_not(nfunc);
00769     if(st_lookup(bdd2vertex, funcBar, &oldV)) {
00770       bAig_Merge(manager, bAig_Not(oldV), v);
00771     }
00772     bdd_free(funcBar);
00773   }
00774   bdd_free(nfunc);
00775 
00776   v = bAig_NonInvertedEdge(v);
00777   nv = bAig_GetCanonical(manager, v);
00778   v = nv;
00779 
00780   if(manager->bddArray[bAigNodeID(v)] == 0) {
00781     size = bdd_size(func);
00782     if(size > sizeLimit) {
00783       newId = *newBddIdIndex;
00784       (*newBddIdIndex) ++;
00785       newBdd = bdd_get_variable(mgr, newId);
00786       manager->bddIdArray[bAigNodeID(v)] = newId;
00787       bdd_free(func);
00788       func = newBdd;
00789       manager->bddArray[bAigNodeID(v)] = func;
00790       st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)bAig_NonInvertedEdge(v));
00791     }
00792     else {
00793       if(bAig_IsInverted(v)) {
00794         funcBar = bdd_not(func);
00795         manager->bddArray[bAigNodeID(v)] = funcBar;
00796         st_insert(bdd2vertex, (char *)func, (char *)v);
00797       }
00798       else {
00799         manager->bddArray[bAigNodeID(v)] = func;
00800         st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)v);
00801       }
00802     }
00803   }
00804   else  bdd_free(func);
00805 
00806   return;
00807 }