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