src/aig/aig/aigDfs.c File Reference

#include "aig.h"
Include dependency graph for aigDfs.c:

Go to the source code of this file.

Functions

void Aig_ManDfs_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t * Aig_ManDfs (Aig_Man_t *p)
Vec_Ptr_t * Aig_ManDfsNodes (Aig_Man_t *p, Aig_Obj_t **ppNodes, int nNodes)
void Aig_ManDfsChoices_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t * Aig_ManDfsChoices (Aig_Man_t *p)
void Aig_ManDfsReverse_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t * Aig_ManDfsReverse (Aig_Man_t *p)
int Aig_ManLevelNum (Aig_Man_t *p)
int Aig_ManCountLevels (Aig_Man_t *p)
void Aig_ConeMark_rec (Aig_Obj_t *pObj)
void Aig_ConeCleanAndMark_rec (Aig_Obj_t *pObj)
int Aig_ConeCountAndMark_rec (Aig_Obj_t *pObj)
void Aig_ConeUnmark_rec (Aig_Obj_t *pObj)
int Aig_DagSize (Aig_Obj_t *pObj)
void Aig_SupportSize_rec (Aig_Man_t *p, Aig_Obj_t *pObj, int *pCounter)
int Aig_SupportSize (Aig_Man_t *p, Aig_Obj_t *pObj)
void Aig_Transfer_rec (Aig_Man_t *pDest, Aig_Obj_t *pObj)
Aig_Obj_t * Aig_Transfer (Aig_Man_t *pSour, Aig_Man_t *pDest, Aig_Obj_t *pRoot, int nVars)
void Aig_Compose_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pFunc, Aig_Obj_t *pVar)
Aig_Obj_t * Aig_Compose (Aig_Man_t *p, Aig_Obj_t *pRoot, Aig_Obj_t *pFunc, int iVar)
void Aig_ObjCollectCut_rec (Aig_Obj_t *pNode, Vec_Ptr_t *vNodes)
void Aig_ObjCollectCut (Aig_Obj_t *pRoot, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes)
int Aig_ObjCollectSuper_rec (Aig_Obj_t *pRoot, Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
int Aig_ObjCollectSuper (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)

Function Documentation

Aig_Obj_t* Aig_Compose ( Aig_Man_t *  p,
Aig_Obj_t *  pRoot,
Aig_Obj_t *  pFunc,
int  iVar 
)

Function*************************************************************

Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]

Description []

SideEffects []

SeeAlso []

Definition at line 546 of file aigDfs.c.

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 }

void Aig_Compose_rec ( Aig_Man_t *  p,
Aig_Obj_t *  pObj,
Aig_Obj_t *  pFunc,
Aig_Obj_t *  pVar 
)

Function*************************************************************

Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]

Description []

SideEffects []

SeeAlso []

Definition at line 518 of file aigDfs.c.

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 }

void Aig_ConeCleanAndMark_rec ( Aig_Obj_t *  pObj  ) 

Function*************************************************************

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 325 of file aigDfs.c.

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 }

int Aig_ConeCountAndMark_rec ( Aig_Obj_t *  pObj  ) 

Function*************************************************************

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 348 of file aigDfs.c.

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 }

void Aig_ConeMark_rec ( Aig_Obj_t *  pObj  ) 

Function*************************************************************

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 303 of file aigDfs.c.

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 }

void Aig_ConeUnmark_rec ( Aig_Obj_t *  pObj  ) 

Function*************************************************************

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 372 of file aigDfs.c.

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 }

int Aig_DagSize ( Aig_Obj_t *  pObj  ) 

Function*************************************************************

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 394 of file aigDfs.c.

00395 {
00396     int Counter;
00397     Counter = Aig_ConeCountAndMark_rec( Aig_Regular(pObj) );
00398     Aig_ConeUnmark_rec( Aig_Regular(pObj) );
00399     return Counter;
00400 }

int Aig_ManCountLevels ( Aig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Computes the max number of levels in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 267 of file aigDfs.c.

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 }

Vec_Ptr_t* Aig_ManDfs ( Aig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file aigDfs.c.

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 }

void Aig_ManDfs_rec ( Aig_Man_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vNodes 
)

CFile****************************************************************

FileName [aigDfs.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [DFS traversal procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
aigDfs.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file aigDfs.c.

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 }

Vec_Ptr_t* Aig_ManDfsChoices ( Aig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file aigDfs.c.

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 }

void Aig_ManDfsChoices_rec ( Aig_Man_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vNodes 
)

Function*************************************************************

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file aigDfs.c.

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 }

Vec_Ptr_t* Aig_ManDfsNodes ( Aig_Man_t *  p,
Aig_Obj_t **  ppNodes,
int  nNodes 
)

Function*************************************************************

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file aigDfs.c.

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 }

Vec_Ptr_t* Aig_ManDfsReverse ( Aig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Collects internal nodes in the reverse DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file aigDfs.c.

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 }

void Aig_ManDfsReverse_rec ( Aig_Man_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vNodes 
)

Function*************************************************************

Synopsis [Collects internal nodes in the reverse DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file aigDfs.c.

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 }

int Aig_ManLevelNum ( Aig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Computes the max number of levels in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file aigDfs.c.

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 }

void Aig_ObjCollectCut ( Aig_Obj_t *  pRoot,
Vec_Ptr_t *  vLeaves,
Vec_Ptr_t *  vNodes 
)

Function*************************************************************

Synopsis [Computes the internal nodes of the cut.]

Description [Does not include the leaves of the cut.]

SideEffects []

SeeAlso []

Definition at line 597 of file aigDfs.c.

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 }

void Aig_ObjCollectCut_rec ( Aig_Obj_t *  pNode,
Vec_Ptr_t *  vNodes 
)

Function*************************************************************

Synopsis [Computes the internal nodes of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 572 of file aigDfs.c.

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 }

int Aig_ObjCollectSuper ( Aig_Obj_t *  pObj,
Vec_Ptr_t *  vSuper 
)

Function*************************************************************

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 677 of file aigDfs.c.

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 }

int Aig_ObjCollectSuper_rec ( Aig_Obj_t *  pRoot,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vSuper 
)

Function*************************************************************

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 631 of file aigDfs.c.

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 }

int Aig_SupportSize ( Aig_Man_t *  p,
Aig_Obj_t *  pObj 
)

Function*************************************************************

Synopsis [Counts the support size of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 440 of file aigDfs.c.

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 }

void Aig_SupportSize_rec ( Aig_Man_t *  p,
Aig_Obj_t *  pObj,
int *  pCounter 
)

Function*************************************************************

Synopsis [Counts the support size of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 413 of file aigDfs.c.

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 }

Aig_Obj_t* Aig_Transfer ( Aig_Man_t *  pSour,
Aig_Man_t *  pDest,
Aig_Obj_t *  pRoot,
int  nVars 
)

Function*************************************************************

Synopsis [Transfers the AIG from one manager into another.]

Description []

SideEffects []

SeeAlso []

Definition at line 484 of file aigDfs.c.

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 }

void Aig_Transfer_rec ( Aig_Man_t *  pDest,
Aig_Obj_t *  pObj 
)

Function*************************************************************

Synopsis [Transfers the AIG from one manager into another.]

Description []

SideEffects []

SeeAlso []

Definition at line 461 of file aigDfs.c.

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 }

Generated on Tue Jan 5 12:18:11 2010 for abc70930 by  doxygen 1.6.1