00001
00021 #include "abc.h"
00022
00026
00027 struct Abc_ManCut_t_
00028 {
00029
00030 int nNodeSizeMax;
00031 int nConeSizeMax;
00032 int nNodeFanStop;
00033 int nConeFanStop;
00034
00035 Vec_Ptr_t * vNodeLeaves;
00036 Vec_Ptr_t * vConeLeaves;
00037 Vec_Ptr_t * vVisited;
00038 Vec_Vec_t * vLevels;
00039 Vec_Ptr_t * vNodesTfo;
00040 };
00041
00042 static int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit );
00043 static int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit );
00044 static void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
00045
00049
00061 static inline void Abc_NodesMark( Vec_Ptr_t * vVisited )
00062 {
00063 Abc_Obj_t * pNode;
00064 int i;
00065 Vec_PtrForEachEntry( vVisited, pNode, i )
00066 pNode->fMarkA = 1;
00067 }
00068
00080 static inline void Abc_NodesUnmark( Vec_Ptr_t * vVisited )
00081 {
00082 Abc_Obj_t * pNode;
00083 int i;
00084 Vec_PtrForEachEntry( vVisited, pNode, i )
00085 pNode->fMarkA = 0;
00086 }
00087
00099 static inline void Abc_NodesUnmarkB( Vec_Ptr_t * vVisited )
00100 {
00101 Abc_Obj_t * pNode;
00102 int i;
00103 Vec_PtrForEachEntry( vVisited, pNode, i )
00104 pNode->fMarkB = 0;
00105 }
00106
00119 static inline int Abc_NodeGetLeafCostOne( Abc_Obj_t * pNode, int nFaninLimit )
00120 {
00121 int Cost;
00122
00123 assert( pNode->fMarkB == 1 );
00124
00125 if ( Abc_ObjIsCi(pNode) )
00126 return 999;
00127
00128 Cost = (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
00129
00130 if ( Cost < 2 )
00131 return Cost;
00132
00133 if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
00134 return 999;
00135
00136 return Cost;
00137 }
00138
00151 static inline int Abc_NodeGetLeafCostTwo( Abc_Obj_t * pNode, int nFaninLimit,
00152 Abc_Obj_t ** ppLeafToAdd, Abc_Obj_t ** pNodeToMark1, Abc_Obj_t ** pNodeToMark2 )
00153 {
00154 Abc_Obj_t * pFanin0, * pFanin1, * pTemp;
00155 Abc_Obj_t * pGrand, * pGrandToAdd;
00156
00157 assert( pNode->fMarkB == 1 );
00158
00159 if ( Abc_ObjIsCi(pNode) )
00160 return 999;
00161
00162
00163
00164
00165 pFanin0 = Abc_ObjFanin0(pNode);
00166 pFanin1 = Abc_ObjFanin1(pNode);
00167 assert( !pFanin0->fMarkB && !pFanin1->fMarkB );
00168
00169
00170 if ( Abc_ObjIsCi(pFanin0) && Abc_ObjIsCi(pFanin1) )
00171 return 999;
00172
00173 if ( !Abc_ObjIsCi(pFanin0) && Abc_ObjFanin0(pFanin0)->fMarkB && Abc_ObjFanin1(pFanin0)->fMarkB )
00174 {
00175 *ppLeafToAdd = pFanin1;
00176 *pNodeToMark1 = pFanin0;
00177 *pNodeToMark2 = NULL;
00178 return 1;
00179 }
00180 if ( !Abc_ObjIsCi(pFanin1) && Abc_ObjFanin0(pFanin1)->fMarkB && Abc_ObjFanin1(pFanin1)->fMarkB )
00181 {
00182 *ppLeafToAdd = pFanin0;
00183 *pNodeToMark1 = pFanin1;
00184 *pNodeToMark2 = NULL;
00185 return 1;
00186 }
00187
00188
00189 if ( Abc_ObjIsCi(pFanin1) )
00190 pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
00191
00192 pGrandToAdd = NULL;
00193 if ( Abc_ObjIsCi(pFanin0) )
00194 {
00195 *pNodeToMark1 = NULL;
00196 pGrandToAdd = pFanin0;
00197 }
00198 else
00199 {
00200 *pNodeToMark1 = pFanin0;
00201 pGrand = Abc_ObjFanin0(pFanin0);
00202 if ( !pGrand->fMarkB )
00203 {
00204 if ( pGrandToAdd && pGrandToAdd != pGrand )
00205 return 999;
00206 pGrandToAdd = pGrand;
00207 }
00208 pGrand = Abc_ObjFanin1(pFanin0);
00209 if ( !pGrand->fMarkB )
00210 {
00211 if ( pGrandToAdd && pGrandToAdd != pGrand )
00212 return 999;
00213 pGrandToAdd = pGrand;
00214 }
00215 }
00216
00217 *pNodeToMark2 = pFanin1;
00218 pGrand = Abc_ObjFanin0(pFanin1);
00219 if ( !pGrand->fMarkB )
00220 {
00221 if ( pGrandToAdd && pGrandToAdd != pGrand )
00222 return 999;
00223 pGrandToAdd = pGrand;
00224 }
00225 pGrand = Abc_ObjFanin1(pFanin1);
00226 if ( !pGrand->fMarkB )
00227 {
00228 if ( pGrandToAdd && pGrandToAdd != pGrand )
00229 return 999;
00230 pGrandToAdd = pGrand;
00231 }
00232 assert( pGrandToAdd != NULL );
00233 *ppLeafToAdd = pGrandToAdd;
00234 return 1;
00235 }
00236
00237
00249 Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain )
00250 {
00251 Abc_Obj_t * pNode;
00252 int i;
00253
00254 assert( !Abc_ObjIsComplement(pRoot) );
00255 assert( Abc_ObjIsNode(pRoot) );
00256
00257
00258 Vec_PtrClear( p->vVisited );
00259 Vec_PtrPush( p->vVisited, pRoot );
00260 Vec_PtrPush( p->vVisited, Abc_ObjFanin0(pRoot) );
00261 Vec_PtrPush( p->vVisited, Abc_ObjFanin1(pRoot) );
00262 pRoot->fMarkB = 1;
00263 Abc_ObjFanin0(pRoot)->fMarkB = 1;
00264 Abc_ObjFanin1(pRoot)->fMarkB = 1;
00265
00266
00267 Vec_PtrClear( p->vNodeLeaves );
00268 Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin0(pRoot) );
00269 Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin1(pRoot) );
00270
00271
00272 while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vNodeLeaves, p->nNodeSizeMax, p->nNodeFanStop ) );
00273 assert( Vec_PtrSize(p->vNodeLeaves) <= p->nNodeSizeMax );
00274
00275
00276 if ( !fContain )
00277 {
00278
00279 Abc_NodesUnmarkB( p->vVisited );
00280 return p->vNodeLeaves;
00281 }
00282
00283
00284
00285 assert( p->nNodeSizeMax < p->nConeSizeMax );
00286
00287 Vec_PtrClear( p->vConeLeaves );
00288 Vec_PtrForEachEntry( p->vNodeLeaves, pNode, i )
00289 Vec_PtrPush( p->vConeLeaves, pNode );
00290
00291 while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vConeLeaves, p->nConeSizeMax, p->nConeFanStop ) );
00292 assert( Vec_PtrSize(p->vConeLeaves) <= p->nConeSizeMax );
00293
00294 Abc_NodesUnmarkB( p->vVisited );
00295 return p->vNodeLeaves;
00296 }
00297
00312 int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit )
00313 {
00314 Abc_Obj_t * pNode, * pFaninBest, * pNext;
00315 int CostBest, CostCur, i;
00316
00317 CostBest = 100;
00318 pFaninBest = NULL;
00319
00320 Vec_PtrForEachEntry( vLeaves, pNode, i )
00321 {
00322 CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
00323
00324
00325 if ( CostBest > CostCur ||
00326 (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
00327 {
00328 CostBest = CostCur;
00329 pFaninBest = pNode;
00330 }
00331 if ( CostBest == 0 )
00332 break;
00333 }
00334 if ( pFaninBest == NULL )
00335 return 0;
00336
00337
00338 assert( CostBest < 3 );
00339 if ( vLeaves->nSize - 1 + CostBest > nSizeLimit )
00340 return 0;
00341
00342
00343 assert( Abc_ObjIsNode(pFaninBest) );
00344
00345 Vec_PtrRemove( vLeaves, pFaninBest );
00346
00347
00348
00349 pNext = Abc_ObjFanin0(pFaninBest);
00350 if ( !pNext->fMarkB )
00351 {
00352
00353 pNext->fMarkB = 1;
00354 Vec_PtrPush( vLeaves, pNext );
00355 Vec_PtrPush( vVisited, pNext );
00356 }
00357
00358 pNext = Abc_ObjFanin1(pFaninBest);
00359 if ( !pNext->fMarkB )
00360 {
00361
00362 pNext->fMarkB = 1;
00363 Vec_PtrPush( vLeaves, pNext );
00364 Vec_PtrPush( vVisited, pNext );
00365 }
00366 assert( vLeaves->nSize <= nSizeLimit );
00367
00368 return 1;
00369 }
00370
00385 int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit )
00386 {
00387 Abc_Obj_t * pNode, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2;
00388 int CostCur, i;
00389
00390 Vec_PtrForEachEntry( vLeaves, pNode, i )
00391 {
00392 CostCur = Abc_NodeGetLeafCostTwo( pNode, nFaninLimit, &pLeafToAdd, &pNodeToMark1, &pNodeToMark2 );
00393 if ( CostCur < 2 )
00394 break;
00395 }
00396 if ( CostCur > 2 )
00397 return 0;
00398
00399 Vec_PtrRemove( vLeaves, pNode );
00400
00401 if ( pLeafToAdd )
00402 {
00403 assert( !pLeafToAdd->fMarkB );
00404 pLeafToAdd->fMarkB = 1;
00405 Vec_PtrPush( vLeaves, pLeafToAdd );
00406 Vec_PtrPush( vVisited, pLeafToAdd );
00407 }
00408
00409 if ( pNodeToMark1 )
00410 {
00411 assert( !pNodeToMark1->fMarkB );
00412 pNodeToMark1->fMarkB = 1;
00413 Vec_PtrPush( vVisited, pNodeToMark1 );
00414 }
00415 if ( pNodeToMark2 )
00416 {
00417 assert( !pNodeToMark2->fMarkB );
00418 pNodeToMark2->fMarkB = 1;
00419 Vec_PtrPush( vVisited, pNodeToMark2 );
00420 }
00421
00422 return 1;
00423 }
00424
00425
00437 void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited, int fIncludeFanins )
00438 {
00439 Abc_Obj_t * pTemp;
00440 int i;
00441
00442 Abc_NodesMark( vLeaves );
00443
00444 Vec_PtrClear( vVisited );
00445
00446 if ( fIncludeFanins )
00447 Vec_PtrForEachEntry( vLeaves, pTemp, i )
00448 Vec_PtrPush( vVisited, pTemp );
00449
00450 for ( i = 0; i < nRoots; i++ )
00451 Abc_NodeConeMarkCollect_rec( ppRoots[i], vVisited );
00452
00453 Abc_NodesUnmark( vLeaves );
00454 Abc_NodesUnmark( vVisited );
00455 }
00456
00468 void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
00469 {
00470 if ( pNode->fMarkA == 1 )
00471 return;
00472
00473 if ( Abc_ObjIsNode(pNode) )
00474 {
00475 Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
00476 Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
00477 }
00478 assert( pNode->fMarkA == 0 );
00479 pNode->fMarkA = 1;
00480 Vec_PtrPush( vVisited, pNode );
00481 }
00482
00494 DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
00495 {
00496 Abc_Obj_t * pNode;
00497 DdNode * bFunc0, * bFunc1, * bFunc;
00498 int i;
00499
00500 Abc_NodeConeCollect( &pRoot, 1, vLeaves, vVisited, 0 );
00501
00502 Vec_PtrForEachEntry( vLeaves, pNode, i )
00503 pNode->pCopy = (Abc_Obj_t *)pbVars[i];
00504
00505 Vec_PtrForEachEntry( vVisited, pNode, i )
00506 {
00507 assert( !Abc_ObjIsPi(pNode) );
00508 bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
00509 bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
00510 bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
00511 pNode->pCopy = (Abc_Obj_t *)bFunc;
00512 }
00513 Cudd_Ref( bFunc );
00514
00515 Vec_PtrForEachEntry( vVisited, pNode, i )
00516 Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
00517 Cudd_Deref( bFunc );
00518 return bFunc;
00519 }
00520
00532 DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited )
00533 {
00534 DdNode * bFunc0, * bFunc1, * bFunc, * bTrans, * bTemp, * bCube, * bResult;
00535 Abc_Obj_t * pNode;
00536 int i;
00537
00538 Abc_NodeConeCollect( (Abc_Obj_t **)vRoots->pArray, vRoots->nSize, vLeaves, vVisited, 0 );
00539
00540 Vec_PtrForEachEntry( vLeaves, pNode, i )
00541 pNode->pCopy = (Abc_Obj_t *)pbVarsX[i];
00542
00543 Vec_PtrForEachEntry( vVisited, pNode, i )
00544 {
00545 bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
00546 bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
00547 bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
00548 pNode->pCopy = (Abc_Obj_t *)bFunc;
00549 }
00550
00551 bTrans = b1; Cudd_Ref( bTrans );
00552 Vec_PtrForEachEntry( vRoots, pNode, i )
00553 {
00554 bFunc = Cudd_bddXnor( dd, (DdNode *)pNode->pCopy, pbVarsY[i] ); Cudd_Ref( bFunc );
00555 bTrans = Cudd_bddAnd( dd, bTemp = bTrans, bFunc ); Cudd_Ref( bTrans );
00556 Cudd_RecursiveDeref( dd, bTemp );
00557 Cudd_RecursiveDeref( dd, bFunc );
00558 }
00559
00560 Vec_PtrForEachEntry( vVisited, pNode, i )
00561 Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
00562
00563 bCube = Extra_bddComputeRangeCube( dd, vRoots->nSize, vRoots->nSize + vLeaves->nSize ); Cudd_Ref( bCube );
00564 bResult = Cudd_bddExistAbstract( dd, bTrans, bCube ); Cudd_Ref( bResult );
00565 bResult = Cudd_Not( bResult );
00566 Cudd_RecursiveDeref( dd, bCube );
00567 Cudd_RecursiveDeref( dd, bTrans );
00568 Cudd_Deref( bResult );
00569 return bResult;
00570 }
00571
00583 Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop )
00584 {
00585 Abc_ManCut_t * p;
00586 p = ALLOC( Abc_ManCut_t, 1 );
00587 memset( p, 0, sizeof(Abc_ManCut_t) );
00588 p->vNodeLeaves = Vec_PtrAlloc( 100 );
00589 p->vConeLeaves = Vec_PtrAlloc( 100 );
00590 p->vVisited = Vec_PtrAlloc( 100 );
00591 p->vLevels = Vec_VecAlloc( 100 );
00592 p->vNodesTfo = Vec_PtrAlloc( 100 );
00593 p->nNodeSizeMax = nNodeSizeMax;
00594 p->nConeSizeMax = nConeSizeMax;
00595 p->nNodeFanStop = nNodeFanStop;
00596 p->nConeFanStop = nConeFanStop;
00597 return p;
00598 }
00599
00611 void Abc_NtkManCutStop( Abc_ManCut_t * p )
00612 {
00613 Vec_PtrFree( p->vNodeLeaves );
00614 Vec_PtrFree( p->vConeLeaves );
00615 Vec_PtrFree( p->vVisited );
00616 Vec_VecFree( p->vLevels );
00617 Vec_PtrFree( p->vNodesTfo );
00618 free( p );
00619 }
00620
00632 Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
00633 {
00634 return p->vConeLeaves;
00635 }
00636
00648 Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p )
00649 {
00650 return p->vNodeLeaves;
00651 }
00652
00664 Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p )
00665 {
00666 return p->vVisited;
00667 }
00668
00669
00670
00687 Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int LevelMax )
00688 {
00689 Abc_Ntk_t * pNtk = pRoot->pNtk;
00690 Vec_Ptr_t * vVec;
00691 Abc_Obj_t * pNode, * pFanout;
00692 int i, k, v, LevelMin;
00693 assert( Abc_NtkIsStrash(pNtk) );
00694
00695
00696 Vec_VecForEachLevel( p->vLevels, vVec, i )
00697 assert( vVec->nSize == 0 );
00698
00699
00700 Abc_NtkIncrementTravId( pNtk );
00701 LevelMin = -1;
00702 Vec_PtrForEachEntry( vLeaves, pNode, i )
00703 {
00704 if ( pNode->Level > (unsigned)LevelMax )
00705 continue;
00706 Abc_NodeSetTravIdCurrent( pNode );
00707 Vec_VecPush( p->vLevels, pNode->Level, pNode );
00708 if ( LevelMin < (int)pNode->Level )
00709 LevelMin = pNode->Level;
00710 }
00711 assert( LevelMin >= 0 );
00712
00713
00714 if ( pRoot )
00715 Abc_NodeMffcLabelAig( pRoot );
00716
00717
00718 Vec_PtrClear( p->vNodesTfo );
00719 Vec_VecForEachEntryStart( p->vLevels, pNode, i, k, LevelMin )
00720 {
00721 if ( i > LevelMax )
00722 break;
00723
00724 if ( !Abc_NodeIsTravIdCurrent(pNode) )
00725 {
00726
00727 if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) ||
00728 !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
00729 continue;
00730
00731 Vec_PtrPush( p->vNodesTfo, pNode );
00732 Abc_NodeSetTravIdCurrent( pNode );
00733 }
00734
00735 Abc_ObjForEachFanout( pNode, pFanout, v )
00736 {
00737
00738 if ( Abc_ObjIsCo(pFanout) || pFanout->Level > (unsigned)LevelMax )
00739 continue;
00740
00741 if ( Abc_NodeIsTravIdCurrent(pFanout) )
00742 continue;
00743
00744 Vec_VecPushUnique( p->vLevels, pFanout->Level, pFanout );
00745 }
00746 }
00747
00748
00749 Vec_VecForEachLevelStart( p->vLevels, vVec, i, LevelMin )
00750 {
00751 if ( i > LevelMax )
00752 break;
00753 Vec_PtrClear( vVec );
00754 }
00755 return p->vNodesTfo;
00756 }
00757
00761
00762