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

00001 
00021 #include "aig.h"
00022 
00026 
00030 
00042 void Aig_ManReprStart( Aig_Man_t * p, int nIdMax )
00043 {
00044     assert( Aig_ManBufNum(p) == 0 );
00045     assert( p->pReprs == NULL );
00046     p->nReprsAlloc = nIdMax;
00047     p->pReprs = ALLOC( Aig_Obj_t *, p->nReprsAlloc );
00048     memset( p->pReprs, 0, sizeof(Aig_Obj_t *) * p->nReprsAlloc );
00049 }
00050 
00062 void Aig_ManReprStop( Aig_Man_t * p )
00063 {
00064     assert( p->pReprs != NULL );
00065     FREE( p->pReprs );
00066     p->nReprsAlloc = 0;    
00067 }
00068 
00080 void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
00081 {
00082     assert( p->pReprs != NULL );
00083     assert( !Aig_IsComplement(pNode1) );
00084     assert( !Aig_IsComplement(pNode2) );
00085     assert( pNode1->Id < p->nReprsAlloc );
00086     assert( pNode2->Id < p->nReprsAlloc );
00087     assert( pNode1->Id < pNode2->Id );
00088     p->pReprs[pNode2->Id] = pNode1;
00089 }
00090 
00102 static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
00103 {
00104     assert( p->pReprs != NULL );
00105     assert( !Aig_IsComplement(pNode1) );
00106     assert( !Aig_IsComplement(pNode2) );
00107     assert( pNode1->Id < p->nReprsAlloc );
00108     assert( pNode2->Id < p->nReprsAlloc );
00109     if ( pNode1 == pNode2 )
00110         return;
00111     if ( pNode1->Id < pNode2->Id )
00112         p->pReprs[pNode2->Id] = pNode1;
00113     else
00114         p->pReprs[pNode1->Id] = pNode2;
00115 }
00116 
00128 static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
00129 {
00130     assert( p->pReprs != NULL );
00131     assert( !Aig_IsComplement(pNode) );
00132     assert( pNode->Id < p->nReprsAlloc );
00133 //    assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
00134     return p->pReprs[pNode->Id];
00135 }
00136 
00148 static inline void Aig_ObjClearRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
00149 {
00150     assert( p->pReprs != NULL );
00151     assert( !Aig_IsComplement(pNode) );
00152     assert( pNode->Id < p->nReprsAlloc );
00153     p->pReprs[pNode->Id] = NULL;
00154 }
00155 
00167 static inline Aig_Obj_t * Aig_ObjFindReprTransitive( Aig_Man_t * p, Aig_Obj_t * pNode )
00168 {
00169     Aig_Obj_t * pNext, * pRepr;
00170     if ( (pRepr = Aig_ObjFindRepr(p, pNode)) )
00171         while ( (pNext = Aig_ObjFindRepr(p, pRepr)) )
00172             pRepr = pNext;
00173     return pRepr;
00174 }
00175 
00187 static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
00188 {
00189     Aig_Obj_t * pRepr;
00190     if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
00191         return Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
00192     return pObj->pData;
00193 }
00194 static inline Aig_Obj_t * Aig_ObjChild0Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjRepr(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); }
00195 static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjRepr(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); }
00196 
00208 void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * pOld )
00209 {
00210     Aig_Obj_t * pObj, * pRepr;
00211     int k;
00212     assert( pNew->pReprs != NULL );
00213     // extend storage to fix pNew
00214     if ( pNew->nReprsAlloc < Aig_ManObjNumMax(pNew) )
00215     {
00216         int nReprsAllocNew = 2 * Aig_ManObjNumMax(pNew);
00217         pNew->pReprs = REALLOC( Aig_Obj_t *, pNew->pReprs, nReprsAllocNew );
00218         memset( pNew->pReprs + pNew->nReprsAlloc, 0, sizeof(Aig_Obj_t *) * (nReprsAllocNew-pNew->nReprsAlloc) );
00219         pNew->nReprsAlloc = nReprsAllocNew;
00220     }
00221     // go through the nodes which have representatives
00222     Aig_ManForEachObj( pOld, pObj, k )
00223         if ( (pRepr = Aig_ObjFindRepr(pOld, pObj)) )
00224             Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); 
00225 }
00226 
00238 Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
00239 {
00240     Aig_Obj_t * pRepr;
00241     if ( pObj->pData )
00242         return pObj->pData;
00243     if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
00244     {
00245         Aig_ManDupRepr_rec( pNew, p, pRepr );
00246         return pObj->pData = Aig_NotCond( pRepr->pData, pRepr->fPhase ^ pObj->fPhase );
00247     }
00248     Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
00249     Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin1(pObj) );
00250     return pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
00251 }
00252 
00264 Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
00265 {
00266     Aig_Man_t * pNew;
00267     Aig_Obj_t * pObj;
00268     int i;
00269     // start the HOP package
00270     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
00271     pNew->pName = Aig_UtilStrsav( p->pName );
00272     pNew->nRegs = p->nRegs;
00273     if ( p->vFlopNums )
00274         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
00275     // map the const and primary inputs
00276     Aig_ManCleanData( p );
00277     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
00278     Aig_ManForEachPi( p, pObj, i )
00279         pObj->pData = Aig_ObjCreatePi(pNew);
00280     // map the internal nodes
00281     if ( fOrdered )
00282     {
00283         Aig_ManForEachNode( p, pObj, i )
00284             pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
00285     }
00286     else
00287     {
00288         Aig_ManForEachPo( p, pObj, i )
00289             Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
00290     }
00291     // transfer the POs
00292     Aig_ManForEachPo( p, pObj, i )
00293         Aig_ObjCreatePo( pNew, Aig_ObjChild0Repr(p, pObj) );
00294     // check the new manager
00295     if ( !Aig_ManCheck(pNew) )
00296         printf( "Aig_ManDupRepr: Check has failed.\n" );
00297     return pNew;
00298 }
00299 
00311 int Aig_ManRemapRepr( Aig_Man_t * p )
00312 {
00313     Aig_Obj_t * pObj, * pRepr;
00314     int i, nFanouts = 0;
00315     Aig_ManForEachNode( p, pObj, i )
00316     {
00317         pRepr = Aig_ObjFindReprTransitive( p, pObj );
00318         if ( pRepr == NULL )
00319             continue;
00320         assert( pRepr->Id < pObj->Id );
00321         Aig_ObjSetRepr( p, pObj, pRepr );
00322         nFanouts += (pObj->nRefs > 0);
00323     }
00324     return nFanouts;
00325 }
00326 
00338 int Aig_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pNode, Aig_Obj_t * pOld )
00339 {
00340     // check the trivial cases
00341     if ( pNode == NULL )
00342         return 0;
00343 //    if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
00344 //        return 0;
00345     if ( pNode == pOld )
00346         return 1;
00347     // skip the visited node
00348     if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
00349         return 0;
00350     Aig_ObjSetTravIdCurrent( p, pNode );
00351     // check the children
00352     if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin0(pNode), pOld ) )
00353         return 1;
00354     if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) )
00355         return 1;
00356     // check equivalent nodes
00357     return Aig_ObjCheckTfi_rec( p, p->pEquivs[pNode->Id], pOld );
00358 }
00359 
00371 int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld )
00372 {
00373     assert( !Aig_IsComplement(pNew) );
00374     assert( !Aig_IsComplement(pOld) );
00375     Aig_ManIncrementTravId( p );
00376     return Aig_ObjCheckTfi_rec( p, pNew, pOld );
00377 }
00378 
00390 Aig_Man_t * Aig_ManRehash( Aig_Man_t * p )
00391 {
00392     Aig_Man_t * pTemp;
00393     int i, nFanouts;
00394     assert( p->pReprs != NULL );
00395     for ( i = 0; (nFanouts = Aig_ManRemapRepr( p )); i++ )
00396     {
00397 //        printf( "Iter = %3d. Fanouts = %6d. Nodes = %7d.\n", i+1, nFanouts, Aig_ManNodeNum(p) );
00398         p = Aig_ManDupRepr( pTemp = p, 1 );
00399         Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
00400         Aig_ManTransferRepr( p, pTemp );
00401         Aig_ManStop( pTemp );
00402     }
00403     return p;
00404 }
00405 
00417 void Aig_ManMarkValidChoices( Aig_Man_t * p )
00418 {
00419     Aig_Obj_t * pObj, * pRepr;
00420     int i;
00421     assert( p->pReprs != NULL );
00422     // create equivalent nodes in the manager
00423     assert( p->pEquivs == NULL );
00424     p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
00425     memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
00426     // make the choice nodes
00427     Aig_ManForEachNode( p, pObj, i )
00428     {
00429         pRepr = Aig_ObjFindRepr( p, pObj );
00430         if ( pRepr == NULL )
00431             continue;
00432         assert( pObj->nRefs == 0 );
00433         // skip constant and PI classes
00434         if ( !Aig_ObjIsNode(pRepr) )
00435         {
00436             Aig_ObjClearRepr( p, pObj );
00437             continue;
00438         }
00439         // skip choices with combinatinal loops
00440         if ( Aig_ObjCheckTfi( p, pObj, pRepr ) )
00441         {
00442             Aig_ObjClearRepr( p, pObj );
00443             continue;
00444         }
00445 //printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
00446         // add choice to the choice node
00447         p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
00448         p->pEquivs[pRepr->Id] = pObj;
00449     }
00450 }
00451 
00452 
00456 
00457