abc70930: src/aig/aig/aigDfs.c Source File

00001 
00021 #include "aig.h"
00022 
00026 
00030 
00042 void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
00043 {
00044     if ( pObj == NULL )
00045         return;
00046     assert( !Aig_IsComplement(pObj) );
00047     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00048         return;
00049     assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
00050     Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
00051     Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
00052     assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
00053     Aig_ObjSetTravIdCurrent(p, pObj);
00054     Vec_PtrPush( vNodes, pObj );
00055 }
00056 
00068 Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
00069 {
00070     Vec_Ptr_t * vNodes;
00071     Aig_Obj_t * pObj;
00072     int i;
00073     Aig_ManIncrementTravId( p );
00074     // mark constant and PIs
00075     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
00076     Aig_ManForEachPi( p, pObj, i )
00077         Aig_ObjSetTravIdCurrent( p, pObj );
00078     // if there are latches, mark them
00079     if ( Aig_ManLatchNum(p) > 0 )
00080         Aig_ManForEachObj( p, pObj, i )
00081             if ( Aig_ObjIsLatch(pObj) )
00082                 Aig_ObjSetTravIdCurrent( p, pObj );
00083     // go through the nodes
00084     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
00085     Aig_ManForEachObj( p, pObj, i )
00086         if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
00087             Aig_ManDfs_rec( p, pObj, vNodes );
00088     return vNodes;
00089 }
00090 
00102 Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
00103 {
00104     Vec_Ptr_t * vNodes;
00105     Aig_Obj_t * pObj;
00106     int i;
00107     assert( Aig_ManLatchNum(p) == 0 );
00108     Aig_ManIncrementTravId( p );
00109     // mark constant and PIs
00110     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
00111     Aig_ManForEachPi( p, pObj, i )
00112         Aig_ObjSetTravIdCurrent( p, pObj );
00113     // go through the nodes
00114     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
00115     for ( i = 0; i < nNodes; i++ )
00116         Aig_ManDfs_rec( p, ppNodes[i], vNodes );
00117     return vNodes;
00118 }
00119 
00131 void Aig_ManDfsChoices_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
00132 {
00133     if ( pObj == NULL )
00134         return;
00135     assert( !Aig_IsComplement(pObj) );
00136     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00137         return;
00138     assert( Aig_ObjIsNode(pObj) );
00139     Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
00140     Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes );
00141     Aig_ManDfsChoices_rec( p, p->pEquivs[pObj->Id], vNodes );
00142     assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
00143     Aig_ObjSetTravIdCurrent(p, pObj);
00144     Vec_PtrPush( vNodes, pObj );
00145 }
00146 
00158 Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p )
00159 {
00160     Vec_Ptr_t * vNodes;
00161     Aig_Obj_t * pObj;
00162     int i;
00163     assert( p->pEquivs != NULL );
00164     Aig_ManIncrementTravId( p );
00165     // mark constant and PIs
00166     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
00167     Aig_ManForEachPi( p, pObj, i )
00168         Aig_ObjSetTravIdCurrent( p, pObj );
00169     // go through the nodes
00170     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
00171     Aig_ManForEachPo( p, pObj, i )
00172         Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
00173     return vNodes;
00174 }
00175 
00187 void Aig_ManDfsReverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
00188 {
00189     Aig_Obj_t * pFanout;
00190     int iFanout = -1, i;
00191     assert( !Aig_IsComplement(pObj) );
00192     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00193         return;
00194     assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
00195     Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
00196         Aig_ManDfsReverse_rec( p, pFanout, vNodes );
00197     assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
00198     Aig_ObjSetTravIdCurrent(p, pObj);
00199     Vec_PtrPush( vNodes, pObj );
00200 }
00201 
00213 Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
00214 {
00215     Vec_Ptr_t * vNodes;
00216     Aig_Obj_t * pObj;
00217     int i;
00218     Aig_ManIncrementTravId( p );
00219     // mark POs
00220     Aig_ManForEachPo( p, pObj, i )
00221         Aig_ObjSetTravIdCurrent( p, pObj );
00222     // if there are latches, mark them
00223     if ( Aig_ManLatchNum(p) > 0 )
00224         Aig_ManForEachObj( p, pObj, i )
00225             if ( Aig_ObjIsLatch(pObj) )
00226                 Aig_ObjSetTravIdCurrent( p, pObj );
00227     // go through the nodes
00228     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
00229     Aig_ManForEachObj( p, pObj, i )
00230         if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
00231             Aig_ManDfsReverse_rec( p, pObj, vNodes );
00232     return vNodes;
00233 }
00234 
00246 int Aig_ManLevelNum( Aig_Man_t * p )
00247 {
00248     Aig_Obj_t * pObj;
00249     int i, LevelsMax;
00250     LevelsMax = 0;
00251     Aig_ManForEachPo( p, pObj, i )
00252         LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
00253     return LevelsMax;
00254 }
00255 
00267 int Aig_ManCountLevels( Aig_Man_t * p )
00268 {
00269     Vec_Ptr_t * vNodes;
00270     Aig_Obj_t * pObj;
00271     int i, LevelsMax, Level0, Level1;
00272     // initialize the levels
00273     Aig_ManConst1(p)->iData = 0;
00274     Aig_ManForEachPi( p, pObj, i )
00275         pObj->iData = 0;
00276     // compute levels in a DFS order
00277     vNodes = Aig_ManDfs( p );
00278     Vec_PtrForEachEntry( vNodes, pObj, i )
00279     {
00280         Level0 = Aig_ObjFanin0(pObj)->iData;
00281         Level1 = Aig_ObjFanin1(pObj)->iData;
00282         pObj->iData = 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1);
00283     }
00284     Vec_PtrFree( vNodes );
00285     // get levels of the POs
00286     LevelsMax = 0;
00287     Aig_ManForEachPo( p, pObj, i )
00288         LevelsMax = AIG_MAX( LevelsMax, Aig_ObjFanin0(pObj)->iData );
00289     return LevelsMax;
00290 }
00291 
00303 void Aig_ConeMark_rec( Aig_Obj_t * pObj )
00304 {
00305     assert( !Aig_IsComplement(pObj) );
00306     if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
00307         return;
00308     Aig_ConeMark_rec( Aig_ObjFanin0(pObj) );
00309     Aig_ConeMark_rec( Aig_ObjFanin1(pObj) );
00310     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
00311     Aig_ObjSetMarkA( pObj );
00312 }
00313 
00325 void Aig_ConeCleanAndMark_rec( Aig_Obj_t * pObj )
00326 {
00327     assert( !Aig_IsComplement(pObj) );
00328     if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
00329         return;
00330     Aig_ConeCleanAndMark_rec( Aig_ObjFanin0(pObj) );
00331     Aig_ConeCleanAndMark_rec( Aig_ObjFanin1(pObj) );
00332     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
00333     Aig_ObjSetMarkA( pObj );
00334     pObj->pData = NULL;
00335 }
00336 
00348 int Aig_ConeCountAndMark_rec( Aig_Obj_t * pObj )
00349 {
00350     int Counter;
00351     assert( !Aig_IsComplement(pObj) );
00352     if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
00353         return 0;
00354     Counter = 1 + Aig_ConeCountAndMark_rec( Aig_ObjFanin0(pObj) ) + 
00355         Aig_ConeCountAndMark_rec( Aig_ObjFanin1(pObj) );
00356     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
00357     Aig_ObjSetMarkA( pObj );
00358     return Counter;
00359 }
00360 
00372 void Aig_ConeUnmark_rec( Aig_Obj_t * pObj )
00373 {
00374     assert( !Aig_IsComplement(pObj) );
00375     if ( !Aig_ObjIsNode(pObj) || !Aig_ObjIsMarkA(pObj) )
00376         return;
00377     Aig_ConeUnmark_rec( Aig_ObjFanin0(pObj) ); 
00378     Aig_ConeUnmark_rec( Aig_ObjFanin1(pObj) );
00379     assert( Aig_ObjIsMarkA(pObj) ); // loop detection
00380     Aig_ObjClearMarkA( pObj );
00381 }
00382 
00394 int Aig_DagSize( Aig_Obj_t * pObj )
00395 {
00396     int Counter;
00397     Counter = Aig_ConeCountAndMark_rec( Aig_Regular(pObj) );
00398     Aig_ConeUnmark_rec( Aig_Regular(pObj) );
00399     return Counter;
00400 }
00401 
00413 void Aig_SupportSize_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pCounter )
00414 {
00415     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00416         return;
00417     Aig_ObjSetTravIdCurrent(p, pObj);
00418     if ( Aig_ObjIsPi(pObj) )
00419     {
00420         (*pCounter)++;
00421         return;
00422     }
00423     assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
00424     Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter );
00425     if ( Aig_ObjFanin1(pObj) )
00426         Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter );
00427 }
00428 
00440 int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
00441 {
00442     int Counter = 0;
00443     assert( !Aig_IsComplement(pObj) );
00444     assert( !Aig_ObjIsPo(pObj) );
00445     Aig_ManIncrementTravId( p );
00446     Aig_SupportSize_rec( p, pObj, &Counter );
00447     return Counter;
00448 }
00449 
00461 void Aig_Transfer_rec( Aig_Man_t * pDest, Aig_Obj_t * pObj )
00462 {
00463     assert( !Aig_IsComplement(pObj) );
00464     if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
00465         return;
00466     Aig_Transfer_rec( pDest, Aig_ObjFanin0(pObj) ); 
00467     Aig_Transfer_rec( pDest, Aig_ObjFanin1(pObj) );
00468     pObj->pData = Aig_And( pDest, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
00469     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
00470     Aig_ObjSetMarkA( pObj );
00471 }
00472 
00484 Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoot, int nVars )
00485 {
00486     Aig_Obj_t * pObj;
00487     int i;
00488     // solve simple cases
00489     if ( pSour == pDest )
00490         return pRoot;
00491     if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) )
00492         return Aig_NotCond( Aig_ManConst1(pDest), Aig_IsComplement(pRoot) );
00493     // set the PI mapping
00494     Aig_ManForEachPi( pSour, pObj, i )
00495     {
00496         if ( i == nVars )
00497            break;
00498         pObj->pData = Aig_IthVar(pDest, i);
00499     }
00500     // transfer and set markings
00501     Aig_Transfer_rec( pDest, Aig_Regular(pRoot) );
00502     // clear the markings
00503     Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
00504     return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
00505 }
00506 
00518 void Aig_Compose_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFunc, Aig_Obj_t * pVar )
00519 {
00520     assert( !Aig_IsComplement(pObj) );
00521     if ( Aig_ObjIsMarkA(pObj) )
00522         return;
00523     if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPi(pObj) )
00524     {
00525         pObj->pData = pObj == pVar ? pFunc : pObj;
00526         return;
00527     }
00528     Aig_Compose_rec( p, Aig_ObjFanin0(pObj), pFunc, pVar ); 
00529     Aig_Compose_rec( p, Aig_ObjFanin1(pObj), pFunc, pVar );
00530     pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
00531     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
00532     Aig_ObjSetMarkA( pObj );
00533 }
00534 
00546 Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar )
00547 {
00548     // quit if the PI variable is not defined
00549     if ( iVar >= Aig_ManPiNum(p) )
00550     {
00551         printf( "Aig_Compose(): The PI variable %d is not defined.\n", iVar );
00552         return NULL;
00553     }
00554     // recursively perform composition
00555     Aig_Compose_rec( p, Aig_Regular(pRoot), pFunc, Aig_ManPi(p, iVar) );
00556     // clear the markings
00557     Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
00558     return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
00559 }
00560 
00572 void Aig_ObjCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
00573 {
00574 //    Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode);
00575 //    Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode);
00576     if ( pNode->fMarkA )
00577         return;
00578     pNode->fMarkA = 1;
00579     assert( Aig_ObjIsNode(pNode) );
00580     Aig_ObjCollectCut_rec( Aig_ObjFanin0(pNode), vNodes );
00581     Aig_ObjCollectCut_rec( Aig_ObjFanin1(pNode), vNodes );
00582     Vec_PtrPush( vNodes, pNode );
00583 //printf( "added %d  ", pNode->Id );
00584 }
00585 
00597 void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
00598 {
00599     Aig_Obj_t * pObj;
00600     int i;
00601     // collect and mark the leaves
00602     Vec_PtrClear( vNodes );
00603     Vec_PtrForEachEntry( vLeaves, pObj, i )
00604     {
00605         assert( pObj->fMarkA == 0 );
00606         pObj->fMarkA = 1;
00607 //        printf( "%d " , pObj->Id );
00608     }
00609 //printf( "\n" );
00610     // collect and mark the nodes
00611     Aig_ObjCollectCut_rec( pRoot, vNodes );
00612     // clean the nodes
00613     Vec_PtrForEachEntry( vNodes, pObj, i )
00614         pObj->fMarkA = 0;
00615     Vec_PtrForEachEntry( vLeaves, pObj, i )
00616         pObj->fMarkA = 0;
00617 }
00618 
00619 
00631 int Aig_ObjCollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
00632 {
00633     int RetValue1, RetValue2, i;
00634     // check if the node is visited
00635     if ( Aig_Regular(pObj)->fMarkA )
00636     {
00637         // check if the node occurs in the same polarity
00638         for ( i = 0; i < vSuper->nSize; i++ )
00639             if ( vSuper->pArray[i] == pObj )
00640                 return 1;
00641         // check if the node is present in the opposite polarity
00642         for ( i = 0; i < vSuper->nSize; i++ )
00643             if ( vSuper->pArray[i] == Aig_Not(pObj) )
00644                 return -1;
00645         assert( 0 );
00646         return 0;
00647     }
00648     // if the new node is complemented or a PI, another gate begins
00649     if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) )
00650     {
00651         Vec_PtrPush( vSuper, pObj );
00652         Aig_Regular(pObj)->fMarkA = 1;
00653         return 0;
00654     }
00655     assert( !Aig_IsComplement(pObj) );
00656     assert( Aig_ObjIsNode(pObj) );
00657     // go through the branches
00658     RetValue1 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
00659     RetValue2 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
00660     if ( RetValue1 == -1 || RetValue2 == -1 )
00661         return -1;
00662     // return 1 if at least one branch has a duplicate
00663     return RetValue1 || RetValue2;
00664 }
00665 
00677 int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
00678 {
00679     int RetValue, i;
00680     assert( !Aig_IsComplement(pObj) );
00681     assert( Aig_ObjIsNode(pObj) );
00682     // collect the nodes in the implication supergate
00683     Vec_PtrClear( vSuper );
00684     RetValue = Aig_ObjCollectSuper_rec( pObj, pObj, vSuper );
00685     assert( Vec_PtrSize(vSuper) > 1 );
00686     // unmark the visited nodes
00687     Vec_PtrForEachEntry( vSuper, pObj, i )
00688         Aig_Regular(pObj)->fMarkA = 0;
00689     // if we found the node and its complement in the same implication supergate, 
00690     // return empty set of nodes (meaning that we should use constant-0 node)
00691     if ( RetValue == -1 )
00692         vSuper->nSize = 0;
00693     return RetValue;
00694 }
00695 
00699 
00700