00001 
00021 #include "aig.h"
00022 
00026 
00030 
00043 Aig_Man_t * Aig_ManStart( int nNodesMax )
00044 {
00045     Aig_Man_t * p;
00046     if ( nNodesMax <= 0 )
00047         nNodesMax = 10007;
00048     
00049     p = ALLOC( Aig_Man_t, 1 );
00050     memset( p, 0, sizeof(Aig_Man_t) );
00051     
00052     p->nTravIds = 1;
00053     p->fCatchExor = 0;
00054     
00055     p->vPis  = Vec_PtrAlloc( 100 );
00056     p->vPos  = Vec_PtrAlloc( 100 );
00057     p->vObjs = Vec_PtrAlloc( 1000 );
00058     p->vBufs = Vec_PtrAlloc( 100 );
00059     
00060     p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax );
00061     
00062     p->pConst1 = Aig_ManFetchMemory( p );
00063     p->pConst1->Type = AIG_OBJ_CONST1;
00064     p->pConst1->fPhase = 1;
00065     p->nObjs[AIG_OBJ_CONST1]++;
00066     
00067     p->nTableSize = Aig_PrimeCudd( nNodesMax );
00068     p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
00069     memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
00070     return p;
00071 }
00072 
00084 Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
00085 {
00086     Aig_Man_t * pNew;
00087     Aig_Obj_t * pObj;
00088     int i;
00089     
00090     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
00091     pNew->pName = Aig_UtilStrsav( p->pName );
00092     
00093     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
00094     Aig_ManForEachPi( p, pObj, i )
00095         pObj->pData = Aig_ObjCreatePi(pNew);
00096     return pNew;
00097 }
00098 
00110 Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
00111 {
00112     if ( pObj->pData )
00113         return pObj->pData;
00114     Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
00115     if ( Aig_ObjIsBuf(pObj) )
00116         return pObj->pData = Aig_ObjChild0Copy(pObj);
00117     Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
00118     return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
00119 }
00120 
00132 Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
00133 {
00134     Aig_Man_t * pNew;
00135     Aig_Obj_t * pObj;
00136     int i;
00137     
00138     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
00139     pNew->pName = Aig_UtilStrsav( p->pName );
00140     pNew->nRegs = p->nRegs;
00141     pNew->nAsserts = p->nAsserts;
00142     if ( p->vFlopNums )
00143         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
00144     
00145     Aig_ManCleanData( p );
00146     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
00147     Aig_ManForEachPi( p, pObj, i )
00148         pObj->pData = Aig_ObjCreatePi(pNew);
00149     
00150     if ( fOrdered )
00151     {
00152         Aig_ManForEachObj( p, pObj, i )
00153             if ( Aig_ObjIsBuf(pObj) )
00154                 pObj->pData = Aig_ObjChild0Copy(pObj);
00155             else if ( Aig_ObjIsNode(pObj) )
00156                 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
00157     }
00158     else
00159     {
00160         Aig_ManForEachObj( p, pObj, i )
00161             if ( !Aig_ObjIsPo(pObj) )
00162             {
00163                 Aig_ManDup_rec( pNew, p, pObj );        
00164                 assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
00165             }
00166     }
00167     
00168     Aig_ManForEachPo( p, pObj, i )
00169         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
00170     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
00171     
00172     if ( !Aig_ManCheck(pNew) )
00173         printf( "Aig_ManDup(): The check has failed.\n" );
00174     return pNew;
00175 }
00176 
00188 Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
00189 {
00190     Aig_Man_t * pNew;
00191     Aig_Obj_t * pObj;
00192     int i;
00193     
00194     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
00195     pNew->pName = Aig_UtilStrsav( p->pName );
00196     
00197     Aig_ManCleanData( p );
00198     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
00199     Aig_ManForEachPi( p, pObj, i )
00200         pObj->pData = Aig_ObjCreatePi(pNew);
00201     
00202     Aig_ManDup_rec( pNew, p, pNode1 );   
00203     Aig_ManDup_rec( pNew, p, pNode2 );   
00204     
00205     pObj = Aig_Exor( pNew, pNode1->pData, pNode2->pData ); 
00206     pObj = Aig_NotCond( pObj, Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) );
00207     
00208     Aig_ObjCreatePo( pNew, pObj );
00209     
00210     if ( !Aig_ManCheck(pNew) )
00211         printf( "Aig_ManDup(): The check has failed.\n" );
00212     return pNew;
00213 }
00214 
00215 
00227 void Aig_ManStop( Aig_Man_t * p )
00228 {
00229     Aig_Obj_t * pObj;
00230     int i;
00231     if ( p->vMapped )
00232         Vec_PtrFree( p->vMapped );
00233     
00234     if ( p->time1 ) { PRT( "time1", p->time1 ); }
00235     if ( p->time2 ) { PRT( "time2", p->time2 ); }
00236     
00237     if ( p->pManTime )
00238         Aig_TManStop( p->pManTime );
00239     
00240     if ( p->pFanData ) 
00241         Aig_ManFanoutStop( p );
00242     
00243     Aig_ManForEachObj( p, pObj, i )
00244         assert( !pObj->fMarkA && !pObj->fMarkB );
00245 
00246     Aig_MmFixedStop( p->pMemObjs, 0 );
00247     if ( p->vPis )     Vec_PtrFree( p->vPis );
00248     if ( p->vPos )     Vec_PtrFree( p->vPos );
00249     if ( p->vObjs )    Vec_PtrFree( p->vObjs );
00250     if ( p->vBufs )    Vec_PtrFree( p->vBufs );
00251     if ( p->vLevelR )  Vec_IntFree( p->vLevelR );
00252     if ( p->vLevels )  Vec_VecFree( p->vLevels );
00253     if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
00254     FREE( p->pName );
00255     FREE( p->pObjCopies );
00256     FREE( p->pReprs );
00257     FREE( p->pEquivs );
00258     free( p->pTable );
00259     free( p );
00260 }
00261 
00273 int Aig_ManCleanup( Aig_Man_t * p )
00274 {
00275     Vec_Ptr_t * vObjs;
00276     Aig_Obj_t * pNode;
00277     int i, nNodesOld;
00278     nNodesOld = Aig_ManNodeNum(p);
00279     
00280     vObjs = Vec_PtrAlloc( 100 );
00281     Aig_ManForEachObj( p, pNode, i )
00282         if ( Aig_ObjIsNode(pNode) && Aig_ObjRefs(pNode) == 0 )
00283             Vec_PtrPush( vObjs, pNode );
00284     
00285     Vec_PtrForEachEntry( vObjs, pNode, i )
00286         Aig_ObjDelete_rec( p, pNode, 1 );
00287     Vec_PtrFree( vObjs );
00288     return nNodesOld - Aig_ManNodeNum(p);
00289 }
00290 
00302 void Aig_ManPrintStats( Aig_Man_t * p )
00303 {
00304     printf( "PI/PO/Lat = %5d/%5d/%5d   ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
00305     printf( "A = %7d. ",    Aig_ManAndNum(p) );
00306     if ( Aig_ManExorNum(p) )
00307         printf( "X = %5d. ",    Aig_ManExorNum(p) );
00308 
00309         printf( "B = %5d. ",    Aig_ManBufNum(p) );
00310 
00311 
00312 
00313     printf( "Max = %7d. ",  Aig_ManObjNumMax(p) );
00314     printf( "Lev = %3d. ",  Aig_ManLevels(p) );
00315     if ( Aig_ManRegNum(p) )
00316         printf( "Lat = %5d. ", Aig_ManRegNum(p) );
00317     printf( "\n" );
00318     fflush( stdout );
00319 }
00320 
00324 
00325