abc70930: src/aig/hop/hopDfs.c Source File

00001 
00021 #include "hop.h"
00022 
00026 
00030 
00042 void Hop_ManDfs_rec( Hop_Obj_t * pObj, Vec_Ptr_t * vNodes )
00043 {
00044     assert( !Hop_IsComplement(pObj) );
00045     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
00046         return;
00047     Hop_ManDfs_rec( Hop_ObjFanin0(pObj), vNodes );
00048     Hop_ManDfs_rec( Hop_ObjFanin1(pObj), vNodes );
00049     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00050     Hop_ObjSetMarkA(pObj);
00051     Vec_PtrPush( vNodes, pObj );
00052 }
00053 
00065 Vec_Ptr_t * Hop_ManDfs( Hop_Man_t * p )
00066 {
00067     Vec_Ptr_t * vNodes;
00068     Hop_Obj_t * pObj;
00069     int i;
00070     vNodes = Vec_PtrAlloc( Hop_ManNodeNum(p) );
00071     Hop_ManForEachNode( p, pObj, i )
00072         Hop_ManDfs_rec( pObj, vNodes );
00073     Hop_ManForEachNode( p, pObj, i )
00074         Hop_ObjClearMarkA(pObj);
00075     return vNodes;
00076 }
00077 
00089 Vec_Ptr_t * Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode )
00090 {
00091     Vec_Ptr_t * vNodes;
00092     Hop_Obj_t * pObj;
00093     int i;
00094     assert( !Hop_IsComplement(pNode) );
00095     vNodes = Vec_PtrAlloc( 16 );
00096     Hop_ManDfs_rec( pNode, vNodes );
00097     Vec_PtrForEachEntry( vNodes, pObj, i )
00098         Hop_ObjClearMarkA(pObj);
00099     return vNodes;
00100 }
00101 
00113 int Hop_ManCountLevels( Hop_Man_t * p )
00114 {
00115     Vec_Ptr_t * vNodes;
00116     Hop_Obj_t * pObj;
00117     int i, LevelsMax, Level0, Level1;
00118     // initialize the levels
00119     Hop_ManConst1(p)->pData = NULL;
00120     Hop_ManForEachPi( p, pObj, i )
00121         pObj->pData = NULL;
00122     // compute levels in a DFS order
00123     vNodes = Hop_ManDfs( p );
00124     Vec_PtrForEachEntry( vNodes, pObj, i )
00125     {
00126         Level0 = (int)Hop_ObjFanin0(pObj)->pData;
00127         Level1 = (int)Hop_ObjFanin1(pObj)->pData;
00128         pObj->pData = (void *)(1 + Hop_ObjIsExor(pObj) + AIG_MAX(Level0, Level1));
00129     }
00130     Vec_PtrFree( vNodes );
00131     // get levels of the POs
00132     LevelsMax = 0;
00133     Hop_ManForEachPo( p, pObj, i )
00134         LevelsMax = AIG_MAX( LevelsMax, (int)Hop_ObjFanin0(pObj)->pData );
00135     return LevelsMax;
00136 }
00137 
00149 void Hop_ManCreateRefs( Hop_Man_t * p )
00150 {
00151     Hop_Obj_t * pObj;
00152     int i;
00153     if ( p->fRefCount )
00154         return;
00155     p->fRefCount = 1;
00156     // clear refs
00157     Hop_ObjClearRef( Hop_ManConst1(p) );
00158     Hop_ManForEachPi( p, pObj, i )
00159         Hop_ObjClearRef( pObj );
00160     Hop_ManForEachNode( p, pObj, i )
00161         Hop_ObjClearRef( pObj );
00162     Hop_ManForEachPo( p, pObj, i )
00163         Hop_ObjClearRef( pObj );
00164     // set refs
00165     Hop_ManForEachNode( p, pObj, i )
00166     {
00167         Hop_ObjRef( Hop_ObjFanin0(pObj) );
00168         Hop_ObjRef( Hop_ObjFanin1(pObj) );
00169     }
00170     Hop_ManForEachPo( p, pObj, i )
00171         Hop_ObjRef( Hop_ObjFanin0(pObj) );
00172 }
00173 
00185 void Hop_ConeMark_rec( Hop_Obj_t * pObj )
00186 {
00187     assert( !Hop_IsComplement(pObj) );
00188     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
00189         return;
00190     Hop_ConeMark_rec( Hop_ObjFanin0(pObj) );
00191     Hop_ConeMark_rec( Hop_ObjFanin1(pObj) );
00192     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00193     Hop_ObjSetMarkA( pObj );
00194 }
00195 
00207 void Hop_ConeCleanAndMark_rec( Hop_Obj_t * pObj )
00208 {
00209     assert( !Hop_IsComplement(pObj) );
00210     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
00211         return;
00212     Hop_ConeCleanAndMark_rec( Hop_ObjFanin0(pObj) );
00213     Hop_ConeCleanAndMark_rec( Hop_ObjFanin1(pObj) );
00214     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00215     Hop_ObjSetMarkA( pObj );
00216     pObj->pData = NULL;
00217 }
00218 
00230 int Hop_ConeCountAndMark_rec( Hop_Obj_t * pObj )
00231 {
00232     int Counter;
00233     assert( !Hop_IsComplement(pObj) );
00234     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
00235         return 0;
00236     Counter = 1 + Hop_ConeCountAndMark_rec( Hop_ObjFanin0(pObj) ) + 
00237         Hop_ConeCountAndMark_rec( Hop_ObjFanin1(pObj) );
00238     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00239     Hop_ObjSetMarkA( pObj );
00240     return Counter;
00241 }
00242 
00254 void Hop_ConeUnmark_rec( Hop_Obj_t * pObj )
00255 {
00256     assert( !Hop_IsComplement(pObj) );
00257     if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
00258         return;
00259     Hop_ConeUnmark_rec( Hop_ObjFanin0(pObj) ); 
00260     Hop_ConeUnmark_rec( Hop_ObjFanin1(pObj) );
00261     assert( Hop_ObjIsMarkA(pObj) ); // loop detection
00262     Hop_ObjClearMarkA( pObj );
00263 }
00264 
00276 int Hop_DagSize( Hop_Obj_t * pObj )
00277 {
00278     int Counter;
00279     Counter = Hop_ConeCountAndMark_rec( Hop_Regular(pObj) );
00280     Hop_ConeUnmark_rec( Hop_Regular(pObj) );
00281     return Counter;
00282 }
00283 
00295 void Hop_Transfer_rec( Hop_Man_t * pDest, Hop_Obj_t * pObj )
00296 {
00297     assert( !Hop_IsComplement(pObj) );
00298     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
00299         return;
00300     Hop_Transfer_rec( pDest, Hop_ObjFanin0(pObj) ); 
00301     Hop_Transfer_rec( pDest, Hop_ObjFanin1(pObj) );
00302     pObj->pData = Hop_And( pDest, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
00303     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00304     Hop_ObjSetMarkA( pObj );
00305 }
00306 
00318 Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pRoot, int nVars )
00319 {
00320     Hop_Obj_t * pObj;
00321     int i;
00322     // solve simple cases
00323     if ( pSour == pDest )
00324         return pRoot;
00325     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
00326         return Hop_NotCond( Hop_ManConst1(pDest), Hop_IsComplement(pRoot) );
00327     // set the PI mapping
00328     Hop_ManForEachPi( pSour, pObj, i )
00329     {
00330         if ( i == nVars )
00331            break;
00332         pObj->pData = Hop_IthVar(pDest, i);
00333     }
00334     // transfer and set markings
00335     Hop_Transfer_rec( pDest, Hop_Regular(pRoot) );
00336     // clear the markings
00337     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
00338     return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
00339 }
00340 
00352 void Hop_Compose_rec( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFunc, Hop_Obj_t * pVar )
00353 {
00354     assert( !Hop_IsComplement(pObj) );
00355     if ( Hop_ObjIsMarkA(pObj) )
00356         return;
00357     if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
00358     {
00359         pObj->pData = pObj == pVar ? pFunc : pObj;
00360         return;
00361     }
00362     Hop_Compose_rec( p, Hop_ObjFanin0(pObj), pFunc, pVar ); 
00363     Hop_Compose_rec( p, Hop_ObjFanin1(pObj), pFunc, pVar );
00364     pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
00365     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00366     Hop_ObjSetMarkA( pObj );
00367 }
00368 
00380 Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar )
00381 {
00382     // quit if the PI variable is not defined
00383     if ( iVar >= Hop_ManPiNum(p) )
00384     {
00385         printf( "Hop_Compose(): The PI variable %d is not defined.\n", iVar );
00386         return NULL;
00387     }
00388     // recursively perform composition
00389     Hop_Compose_rec( p, Hop_Regular(pRoot), pFunc, Hop_ManPi(p, iVar) );
00390     // clear the markings
00391     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
00392     return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
00393 }
00394 
00398 
00399