diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-20 00:27:47 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-20 00:27:47 -0700 |
commit | 8cd00e0407714353fac051c266edcdfbdd4d8a35 (patch) | |
tree | 913a0560d826fb134711a88ac618f885b5e6db8e /src/aig | |
parent | d5555c51f00436bcf770b7cc9721bbca80aff08e (diff) | |
download | abc-8cd00e0407714353fac051c266edcdfbdd4d8a35.tar.gz abc-8cd00e0407714353fac051c266edcdfbdd4d8a35.tar.bz2 abc-8cd00e0407714353fac051c266edcdfbdd4d8a35.zip |
Fixing c++ portability issues.
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/giaAiger_new.c | 1251 | ||||
-rw-r--r-- | src/aig/gia/giaAiger_old.c | 1255 |
2 files changed, 0 insertions, 2506 deletions
diff --git a/src/aig/gia/giaAiger_new.c b/src/aig/gia/giaAiger_new.c deleted file mode 100644 index 67981b26..00000000 --- a/src/aig/gia/giaAiger_new.c +++ /dev/null @@ -1,1251 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaAiger.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [Procedures to read/write binary AIGER format developed by - Armin Biere, Johannes Kepler University (http://fmv.jku.at/)] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaAiger.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef ABC_UINT64_T word; - -static inline int Gia_ObjObjPhaseDiff( Gia_Man_t * p, int i, int j ) { return Gia_ManObj(p, i)->fPhase ^ Gia_ManObj(p, j)->fPhase; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Extracts one unsigned AIG edge from the input buffer.] - - Description [This procedure is a slightly modified version of Armin Biere's - procedure "unsigned decode (FILE * file)". ] - - SideEffects [Updates the current reading position.] - - SeeAlso [] - -***********************************************************************/ -unsigned Gia_ReadAigerDecode( char ** ppPos ) -{ - unsigned x = 0, i = 0; - unsigned char ch; - while ((ch = *(*ppPos)++) & 0x80) - x |= (ch & 0x7f) << (7 * i++); - return x | (ch << (7 * i)); -} - -/**Function************************************************************* - - Synopsis [Extracts one signed AIG edge from the input buffer.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ReadAigerDecodeInt( char ** ppPos ) -{ - unsigned Res; - Res = Gia_ReadAigerDecode( ppPos ); - if ( Res & 1 ) - return -((int)(Res >> 1)); - return Res >> 1; -} - -/**Function************************************************************* - - Synopsis [Decodes the encoded array of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_WriteDecodeLiterals( char ** ppPos, int nEntries ) -{ - Vec_Int_t * vLits; - int Lit, LitPrev, Diff, i; - vLits = Vec_IntAlloc( nEntries ); - LitPrev = Gia_ReadAigerDecode( ppPos ); - Vec_IntPush( vLits, LitPrev ); - for ( i = 1; i < nEntries; i++ ) - { -// Diff = Lit - LitPrev; -// Diff = (Lit < LitPrev)? -Diff : Diff; -// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev); - Diff = Gia_ReadAigerDecode( ppPos ); - Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1; - Lit = Diff + LitPrev; - Vec_IntPush( vLits, Lit ); - LitPrev = Lit; - } - return vLits; -} - - -/**Function************************************************************* - - Synopsis [Returns the file size.] - - Description [The file should be closed.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_FixFileName( char * pFileName ) -{ - char * pName; - for ( pName = pFileName; *pName; pName++ ) - if ( *pName == '>' ) - *pName = '\\'; -} - -/**Function************************************************************* - - Synopsis [Returns the file size.] - - Description [The file should be closed.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_FileSize( char * pFileName ) -{ - FILE * pFile; - int nFileSize; - pFile = fopen( pFileName, "r" ); - if ( pFile == NULL ) - { - printf( "Gia_FileSize(): The file is unavailable (absent or open).\n" ); - return 0; - } - fseek( pFile, 0, SEEK_END ); - nFileSize = ftell( pFile ); - fclose( pFile ); - return nFileSize; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Gia_FileNameGeneric( char * FileName ) -{ - char * pDot, * pRes; - pRes = Gia_UtilStrsav( FileName ); - if ( (pDot = strrchr( pRes, '.' )) ) - *pDot = 0; - return pRes; -} - -/**Function************************************************************* - - Synopsis [Write integer into the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ReadInt( unsigned char * pPos ) -{ - int i, Value = 0; - for ( i = 0; i < 4; i++ ) - Value |= ((unsigned)(*pPos++)) << (i << 3); - return Value; -} - -/**Function************************************************************* - - Synopsis [Reads decoded value.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev ) -{ - int Item = Gia_ReadAigerDecode( ppPos ); - if ( Item & 1 ) - return iPrev + (Item >> 1); - return iPrev - (Item >> 1); -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Rpr_t * Gia_ReadEquivClasses_old( unsigned char ** ppPos, int nSize ) -{ - Gia_Rpr_t * pReprs; - unsigned char * pStop; - int i, Item, fProved, iRepr, iNode; - pStop = *ppPos; - pStop += Gia_ReadInt( *ppPos ); *ppPos += 4; - pReprs = ABC_CALLOC( Gia_Rpr_t, nSize ); - for ( i = 0; i < nSize; i++ ) - pReprs[i].iRepr = GIA_VOID; - iRepr = iNode = 0; - while ( *ppPos < pStop ) - { - Item = Gia_ReadAigerDecode( ppPos ); - if ( Item & 1 ) - { - iRepr += (Item >> 1); - iNode = iRepr; -//printf( "\nRepr = %d ", iRepr ); - continue; - } - Item >>= 1; - fProved = (Item & 1); - Item >>= 1; - iNode += Item; - pReprs[iNode].fProved = fProved; - pReprs[iNode].iRepr = iRepr; - assert( iRepr < iNode ); -//printf( "Node = %d ", iNode ); - } - return pReprs; -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize, int nAlloc ) -{ - Gia_Rpr_t * pReprs; - unsigned char * pStop; - int i, k, iRepr, iNode, nMembers; - // find place to stop - pStop = *ppPos + nSize; - // prepare equivalence classes - pReprs = ABC_CALLOC( Gia_Rpr_t, nAlloc ); - for ( i = 0; i < nAlloc; i++ ) - pReprs[i].iRepr = GIA_VOID; - // skip the number of classes - Gia_ReadAigerDecode( ppPos ); - // read classes - iRepr = 0; - while ( *ppPos < pStop ) - { - nMembers = Gia_ReadAigerDecode( ppPos ); - iRepr += Gia_ReadAigerDecode( ppPos ); - iNode = iRepr; - for ( k = 1; k < nMembers; k++ ) - { - iNode += Gia_ReadAigerDecode( ppPos ); - pReprs[ Gia_Lit2Var(iNode) ].iRepr = Gia_Lit2Var(iRepr); - assert( Gia_Lit2Var(iRepr) < Gia_Lit2Var(iNode) ); -//if ( !iRepr ) -//printf( "%4d: Reading equiv %d -> %d\n", k, iNode, iRepr ); - } - } - return pReprs; -} - -/**Function************************************************************* - - Synopsis [Read flop classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ReadFlopClasses( unsigned char ** ppPos, Vec_Int_t * vClasses, int nSize ) -{ - int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; - assert( nAlloc/4 == nSize ); - assert( Vec_IntSize(vClasses) == nSize ); - memcpy( Vec_IntArray(vClasses), *ppPos, 4*nSize ); - *ppPos += 4 * nSize; -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Gia_ReadMapping( unsigned char ** ppPos, int nSize ) -{ - int * pMapping; - unsigned char * pStop; - int k, j, nFanins, nAlloc, iNode = 0, iOffset = nSize; - pStop = *ppPos; - pStop += Gia_ReadInt( *ppPos ); *ppPos += 4; - nAlloc = nSize + pStop - *ppPos; - pMapping = ABC_CALLOC( int, nAlloc ); - while ( *ppPos < pStop ) - { - k = iOffset; - pMapping[k++] = nFanins = Gia_ReadAigerDecode( ppPos ); - for ( j = 0; j <= nFanins; j++ ) - pMapping[k++] = iNode = Gia_ReadDiffValue( ppPos, iNode ); - pMapping[iNode] = iOffset; - iOffset = k; - } - assert( iOffset <= nAlloc ); - return pMapping; -} - -/**Function************************************************************* - - Synopsis [Read switching from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned char * Gia_ReadSwitching( unsigned char ** ppPos, int nSize ) -{ - unsigned char * pSwitching; - int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; - assert( nAlloc == nSize ); - pSwitching = ABC_ALLOC( unsigned char, nSize ); - memcpy( pSwitching, *ppPos, nSize ); - *ppPos += nSize; - return pSwitching; -} - -/**Function************************************************************* - - Synopsis [Read placement from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Plc_t * Gia_ReadPlacement( unsigned char ** ppPos, int nSize ) -{ - Gia_Plc_t * pPlacement; - int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; - assert( nAlloc/4 == nSize ); - pPlacement = ABC_ALLOC( Gia_Plc_t, nSize ); - memcpy( pPlacement, *ppPos, 4*nSize ); - *ppPos += 4 * nSize; - return pPlacement; -} - -/**Function************************************************************* - - Synopsis [Reads char and 64-bit int using little-endian style.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char Gia_ReadBlockHeader( char ** ppCur, word * pWord ) -{ - int i; - char Char = *(*ppCur)++; - *pWord = 0; - for ( i = 0; i < 8; i++ ) - { -// printf( "%d\n", (unsigned char)(*(*ppCur)) ); - *pWord |= ((word)(unsigned char)(*(*ppCur)++)) << (i<<3); - } - return Char; -} - -/**Function************************************************************* - - Synopsis [Reads the AIG in the binary AIGER format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ) -{ - FILE * pFile; - Gia_Man_t * pNew; - Vec_Int_t * vLits = NULL; - Vec_Int_t * vNodes, * vDrivers;//, * vTerms; - int iObj, iNode0, iNode1; - int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits; - char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType; - unsigned uLit0, uLit1, uLit; - - // read the file into the buffer - Gia_FixFileName( pFileName ); - nFileSize = Gia_FileSize( pFileName ); - pFile = fopen( pFileName, "rb" ); - pContents = ABC_ALLOC( char, nFileSize ); - fread( pContents, nFileSize, 1, pFile ); - fclose( pFile ); - - // check if the input file format is correct - if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') ) - { - fprintf( stdout, "Wrong input file format.\n" ); - free( pContents ); - return NULL; - } - - // read the file type - pCur = pContents; while ( *pCur++ != ' ' ); - // read the number of objects - nTotal = atoi( pCur ); while ( *pCur++ != ' ' ); - // read the number of inputs - nInputs = atoi( pCur ); while ( *pCur++ != ' ' ); - // read the number of latches - nLatches = atoi( pCur ); while ( *pCur++ != ' ' ); - // read the number of outputs - nOutputs = atoi( pCur ); while ( *pCur++ != ' ' ); - // read the number of nodes - nAnds = atoi( pCur ); while ( *pCur++ != '\n' ); - // check the parameters - if ( nTotal != nInputs + nLatches + nAnds ) - { - fprintf( stdout, "The paramters are wrong.\n" ); - return NULL; - } - - // allocate the empty AIG - pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 ); - pName = Gia_FileNameGeneric( pFileName ); - pNew->pName = Gia_UtilStrsav( pName ); -// pNew->pSpec = Gia_UtilStrsav( pFileName ); - ABC_FREE( pName ); - - // prepare the array of nodes - vNodes = Vec_IntAlloc( 1 + nTotal ); - Vec_IntPush( vNodes, 0 ); - - // create the PIs - for ( i = 0; i < nInputs + nLatches; i++ ) - { - iObj = Gia_ManAppendCi(pNew); - Vec_IntPush( vNodes, iObj ); - } - - // remember the beginning of latch/PO literals - pDrivers = pCur; - if ( pContents[3] == ' ' ) // standard AIGER - { - // scroll to the beginning of the binary data - for ( i = 0; i < nLatches + nOutputs; ) - if ( *pCur++ == '\n' ) - i++; - } - else // modified AIGER - { - vLits = Gia_WriteDecodeLiterals( &pCur, nLatches + nOutputs ); - } - - // create the AND gates - for ( i = 0; i < nAnds; i++ ) - { - uLit = ((i + 1 + nInputs + nLatches) << 1); - uLit1 = uLit - Gia_ReadAigerDecode( &pCur ); - uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur ); -// assert( uLit1 > uLit0 ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); - iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); - assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches ); -// Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) ); - Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) ); - } - - // remember the place where symbols begin - pSymbols = pCur; - - // read the latch driver literals - vDrivers = Vec_IntAlloc( nLatches + nOutputs ); - if ( pContents[3] == ' ' ) // standard AIGER - { - pCur = pDrivers; - for ( i = 0; i < nLatches; i++ ) - { - uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); - Vec_IntPush( vDrivers, iNode0 ); - } - // read the PO driver literals - for ( i = 0; i < nOutputs; i++ ) - { - uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); - Vec_IntPush( vDrivers, iNode0 ); - } - - } - else - { - // read the latch driver literals - for ( i = 0; i < nLatches; i++ ) - { - uLit0 = Vec_IntEntry( vLits, i ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); - Vec_IntPush( vDrivers, iNode0 ); - } - // read the PO driver literals - for ( i = 0; i < nOutputs; i++ ) - { - uLit0 = Vec_IntEntry( vLits, i+nLatches ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); - Vec_IntPush( vDrivers, iNode0 ); - } - Vec_IntFree( vLits ); - } - - // create the POs - for ( i = 0; i < nOutputs; i++ ) - Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) ); - for ( i = 0; i < nLatches; i++ ) - Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) ); - Vec_IntFree( vDrivers ); - - // create the latches - Gia_ManSetRegNum( pNew, nLatches ); - - // check if there are other types of information to read - pCur = pSymbols; - if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' ) - { - char Char; - word Size; - pCur++; - - // read model name (old style) - if ( *pCur == 'n' ) - { - pCur++; - ABC_FREE( pNew->pName ); - pNew->pName = Gia_UtilStrsav( pCur ); - pCur += (int)(strlen(pNew->pName) + 1); - } - - Char = Gia_ReadBlockHeader( &pCur, &Size ); - if ( Char == '\n' && Size == 0xAC1D0FF1CEC0FFEE ) - { - while ( (Char = Gia_ReadBlockHeader(&pCur, &Size)) ) - { - switch (Char) - { - case 'N': - // read model name - ABC_FREE( pNew->pName ); - pNew->pName = ABC_ALLOC( char, (int)Size + 1 ); - strncpy( pNew->pName, pCur, (int)Size ); - pNew->pName[(int)Size] = '\0'; - pCur += (int)Size; - break; - case '=': - // read equivalence classes - pNew->pReprs = Gia_ReadEquivClasses( &pCur, (int)Size, Gia_ManObjNum(pNew) ); - pNew->pNexts = Gia_ManDeriveNexts( pNew ); - break; - case 'c': - // read number of constraints - pNew->nConstrs = Gia_ReadInt( pCur ); pCur += 4; - break; - default: - printf( "Unrecognized data.\n" ); - break; - } - } - } - else - { - printf( "Extended AIGER reader: Internal signature does not match.\n" ); - } - -/* - if ( *pCur == 'e' ) - { - pCur++; - // read equivalence classes - pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) ); - pNew->pNexts = Gia_ManDeriveNexts( pNew ); - } - if ( *pCur == 'f' ) - { - pCur++; - // read flop classes - pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) ); - Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) ); - } - if ( *pCur == 'm' ) - { - pCur++; - // read mapping - pNew->pMapping = Gia_ReadMapping( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 'p' ) - { - pCur++; - // read placement - pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 's' ) - { - pCur++; - // read switching activity - pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 'c' ) - { - pCur++; - // read number of constraints - pNew->nConstrs = Gia_ReadInt( pCur ); pCur += 4; - } - if ( *pCur == 'n' ) - { - pCur++; - // read model name - ABC_FREE( pNew->pName ); - pNew->pName = Gia_UtilStrsav( pCur ); - } -*/ - } - - // skipping the comments - ABC_FREE( pContents ); - Vec_IntFree( vNodes ); -/* - // check the result - if ( fCheck && !Gia_ManCheck( pNew ) ) - { - printf( "Gia_ReadAiger: The network check has failed.\n" ); - Gia_ManStop( pNew ); - return NULL; - } -*/ - return pNew; -} - - -/**Function************************************************************* - - Synopsis [Adds one unsigned AIG edge to the output buffer.] - - Description [This procedure is a slightly modified version of Armin Biere's - procedure "void encode (FILE * file, unsigned x)" ] - - SideEffects [Returns the current writing position.] - - SeeAlso [] - -***********************************************************************/ -int Gia_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x ) -{ - unsigned char ch; - while (x & ~0x7f) - { - ch = (x & 0x7f) | 0x80; - pBuffer[Pos++] = ch; - x >>= 7; - } - ch = x; - pBuffer[Pos++] = ch; - return Pos; -} - -/**Function************************************************************* - - Synopsis [Adds one signed int to the output buffer.] - - Description [] - - SideEffects [Returns the current writing position.] - - SeeAlso [] - -***********************************************************************/ -int Gia_WriteAigerEncodeInt( unsigned char * pBuffer, int Pos, int x ) -{ - if ( x >= 0 ) - return Gia_WriteAigerEncode( pBuffer, Pos, ((unsigned)(x) << 1) ); - return Gia_WriteAigerEncode( pBuffer, Pos, ((unsigned)(-x) << 1) | 1 ); -} - -/**Function************************************************************* - - Synopsis [Create the array of literals to be written.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_WriteAigerLiterals( Gia_Man_t * p ) -{ - Vec_Int_t * vLits; - Gia_Obj_t * pObj; - int i; - vLits = Vec_IntAlloc( Gia_ManPoNum(p) ); - Gia_ManForEachRi( p, pObj, i ) - Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) ); - Gia_ManForEachPo( p, pObj, i ) - Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) ); - return vLits; -} - -/**Function************************************************************* - - Synopsis [Creates the binary encoded array of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Str_t * Gia_WriteEncodeLiterals( Vec_Int_t * vLits ) -{ - Vec_Str_t * vBinary; - int Pos = 0, Lit, LitPrev, Diff, i; - vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) ); - LitPrev = Vec_IntEntry( vLits, 0 ); - Pos = Gia_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); - Vec_IntForEachEntryStart( vLits, Lit, i, 1 ) - { - Diff = Lit - LitPrev; - Diff = (Lit < LitPrev)? -Diff : Diff; - Diff = (Diff << 1) | (int)(Lit < LitPrev); - Pos = Gia_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff ); - LitPrev = Lit; - if ( Pos + 10 > vBinary->nCap ) - Vec_StrGrow( vBinary, vBinary->nCap+1 ); - } - vBinary->nSize = Pos; -/* - // verify - { - extern Vec_Int_t * Gia_WriteDecodeLiterals( char ** ppPos, int nEntries ); - char * pPos = Vec_StrArray( vBinary ); - Vec_Int_t * vTemp = Gia_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) ); - for ( i = 0; i < Vec_IntSize(vLits); i++ ) - { - int Entry1 = Vec_IntEntry(vLits,i); - int Entry2 = Vec_IntEntry(vTemp,i); - assert( Entry1 == Entry2 ); - } - Vec_IntFree( vTemp ); - } -*/ - return vBinary; -} - -/**Function************************************************************* - - Synopsis [Write integer into the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_WriteInt( char * pBuffer, int Value ) -{ - int i; - for ( i = 0; i < 4; i++ ) - pBuffer[i] = (char)(0xff & (Value >> (i<<3))); -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned char * Gia_WriteEquivClasses_old( Gia_Man_t * p, int * pEquivSize ) -{ - unsigned char * pBuffer; - int iRepr, iNode, iPrevRepr, iPrevNode, iLit, nItems, iPos; - assert( p->pReprs && p->pNexts ); - // count the number of entries to be written - nItems = 0; - for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ ) - { - nItems += Gia_ObjIsConst( p, iRepr ); - if ( !Gia_ObjIsHead(p, iRepr) ) - continue; - Gia_ClassForEachObj( p, iRepr, iNode ) - nItems++; - } - pBuffer = ABC_ALLOC( char, sizeof(int) * (nItems + 1) ); - // write constant class - iPos = Gia_WriteAigerEncode( pBuffer, 4, Gia_Var2Lit(0, 1) ); - iPrevNode = 0; - for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ ) - if ( Gia_ObjIsConst(p, iNode) ) - { - iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); - iPrevNode = iNode; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) ); - } - // write non-constant classes - iPrevRepr = 0; - Gia_ManForEachClass( p, iRepr ) - { - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iRepr - iPrevRepr, 1) ); - iPrevRepr = iPrevNode = iRepr; - Gia_ClassForEachObj1( p, iRepr, iNode ) - { - iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); - iPrevNode = iNode; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) ); - } - } - Gia_WriteInt( pBuffer, iPos ); - *pEquivSize = iPos; - return pBuffer; -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize ) -{ - unsigned char * pBuffer; - int k, iNode, iRepr, iPrevLit, iNodeLit, iPrevReprLit, iReprLit; - int nItems, iPos, nClasses, nMembers; - assert( p->pReprs && p->pNexts ); - Gia_ManSetPhase(p); - // count the number of entries to be written - nItems = 0; - nMembers = 0; - nClasses = 0; - for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ ) - { - nItems += Gia_ObjIsConst( p, iRepr ); - nMembers += Gia_ObjIsConst( p, iRepr ); - if ( !Gia_ObjIsHead(p, iRepr) ) - continue; - nClasses++; - Gia_ClassForEachObj( p, iRepr, iNode ) - nItems++; - } - nClasses += (nMembers > 0); - // allocate place for data - pBuffer = (unsigned char *)ABC_ALLOC( int, nItems+1 ); - // write the number of classes - iPos = Gia_WriteAigerEncode( pBuffer, 0, nClasses ); - // write constant class - if ( nMembers ) - { - iPos = Gia_WriteAigerEncode( pBuffer, iPos, nMembers+1 ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(0,0) ); - iPrevLit = Gia_Var2Lit(0,0); - k = 1; - for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ ) - if ( Gia_ObjIsConst(p, iNode) ) - { - iNodeLit = Gia_Var2Lit( iNode, Gia_ObjPhase(Gia_ManObj(p, iNode)) ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, iNodeLit - iPrevLit ); - iPrevLit = iNodeLit; -//printf( "%4d : Writing equiv %d -> %d\n", k++, iNode, 0 ); - } - } - // write non-constant classes - iPrevReprLit = 0; - Gia_ManForEachClass( p, iRepr ) - { - // write number of members - nMembers = 0; - Gia_ClassForEachObj( p, iRepr, iNode ) - nMembers++; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, nMembers ); - // write representative - iReprLit = Gia_Var2Lit( iRepr, Gia_ObjPhase(Gia_ManObj(p, iRepr)) ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, iReprLit - iPrevReprLit ); - iPrevReprLit = iReprLit; - // write members - iPrevLit = iReprLit; - Gia_ClassForEachObj1( p, iRepr, iNode ) - { - iNodeLit = Gia_Var2Lit( iNode, Gia_ObjPhase(Gia_ManObj(p, iNode)) ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, iNodeLit - iPrevLit ); - iPrevLit = iNodeLit; -//printf( "Writing equiv %d -> %d\n", iNode, iRepr ); - } - } - *pEquivSize = iPos; - return pBuffer; -} - -/**Function************************************************************* - - Synopsis [Reads decoded value.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_WriteDiffValue( char * pPos, int iPos, int iPrev, int iThis ) -{ - if ( iPrev < iThis ) - return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iThis - iPrev, 1) ); - return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iPrev - iThis, 0) ); -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned char * Gia_WriteMapping( Gia_Man_t * p, int * pMapSize ) -{ - unsigned char * pBuffer; - int i, k, iPrev, iFan, nItems, iPos = 4; - assert( p->pMapping ); - // count the number of entries to be written - nItems = 0; - Gia_ManForEachLut( p, i ) - nItems += 2 + Gia_ObjLutSize( p, i ); - pBuffer = ABC_ALLOC( char, sizeof(int) * (nItems + 1) ); - // write non-constant classes - iPrev = 0; - Gia_ManForEachLut( p, i ) - { -//printf( "\nSize = %d ", Gia_ObjLutSize(p, i) ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_ObjLutSize(p, i) ); - Gia_LutForEachFanin( p, i, iFan, k ) - { -//printf( "Fan = %d ", iFan ); - iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, iFan ); - iPrev = iFan; - } - iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, i ); - iPrev = i; -//printf( "Node = %d ", i ); - } -//printf( "\n" ); - Gia_WriteInt( pBuffer, iPos ); - *pMapSize = iPos; - return pBuffer; -} - -/**Function************************************************************* - - Synopsis [Writes char and 64-bit int using little-endian style.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_WriteBlockHeader( FILE * pFile, char Char, word Word ) -{ - int i; - fprintf( pFile, "%c", Char ); - for ( i = 0; i < 8; i++ ) - fprintf( pFile, "%c", (unsigned char)(0xff & (Word >> (i<<3))) ); -} - -/**Function************************************************************* - - Synopsis [Write integer into the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_WriteIntF( FILE * pFile, int Value ) -{ - int i; - for ( i = 0; i < 4; i++ ) - fprintf( pFile, "%c", (char)(0xff & (Value >> (i<<3))) ); -} - -/**Function************************************************************* - - Synopsis [Writes the AIG in the binary AIGER format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact ) -{ - FILE * pFile; - Gia_Man_t * p; - Gia_Obj_t * pObj; - int i, nBufferSize, Pos; - unsigned char * pBuffer; - unsigned uLit0, uLit1, uLit; - - if ( Gia_ManCoNum(pInit) == 0 ) - { - printf( "AIG cannot be written because it has no POs.\n" ); - return; - } - - // start the output stream - pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - fprintf( stdout, "Gia_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName ); - return; - } - - // create normalized AIG - if ( !Gia_ManIsNormalized(pInit) ) - { -// printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" ); - p = Gia_ManDupNormalized( pInit ); - } - else - p = pInit; - - // write the header "M I L O A" where M = I + L + A - fprintf( pFile, "aig%s %u %u %u %u %u\n", - fCompact? "2" : "", - Gia_ManCiNum(p) + Gia_ManAndNum(p), - Gia_ManPiNum(p), - Gia_ManRegNum(p), - Gia_ManPoNum(p), - Gia_ManAndNum(p) ); - - if ( !fCompact ) - { - // write latch drivers - Gia_ManForEachRi( p, pObj, i ) - fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) ); - // write PO drivers - Gia_ManForEachPo( p, pObj, i ) - fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) ); - } - else - { - Vec_Int_t * vLits = Gia_WriteAigerLiterals( p ); - Vec_Str_t * vBinary = Gia_WriteEncodeLiterals( vLits ); - fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile ); - Vec_StrFree( vBinary ); - Vec_IntFree( vLits ); - } - - // write the nodes into the buffer - Pos = 0; - nBufferSize = 6 * Gia_ManAndNum(p) + 100; // skeptically assuming 3 chars per one AIG edge - pBuffer = ABC_ALLOC( unsigned char, nBufferSize ); - Gia_ManForEachAnd( p, pObj, i ) - { - uLit = Gia_Var2Lit( i, 0 ); - uLit0 = Gia_ObjFaninLit0( pObj, i ); - uLit1 = Gia_ObjFaninLit1( pObj, i ); - assert( uLit0 < uLit1 ); - Pos = Gia_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 ); - Pos = Gia_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); - if ( Pos > nBufferSize - 10 ) - { - printf( "Gia_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" ); - fclose( pFile ); - if ( p != pInit ) - Gia_ManStop( p ); - return; - } - } - assert( Pos < nBufferSize ); - - // write the buffer - fwrite( pBuffer, 1, Pos, pFile ); - ABC_FREE( pBuffer ); - - // write the comment - fprintf( pFile, "c" ); - // write signature - Gia_WriteBlockHeader( pFile, '\n', 0xAC1D0FF1CEC0FFEE ); - // write name - if ( p->pName ) - { - Gia_WriteBlockHeader( pFile, 'N', (word)strlen(pInit->pName) ); - fwrite( pInit->pName, 1, strlen(pInit->pName), pFile ); - } - // write equivalences - if ( p->pReprs && p->pNexts ) - { - int nEquivSize; - unsigned char * pEquivs = Gia_WriteEquivClasses( p, &nEquivSize ); - Gia_WriteBlockHeader( pFile, '=', (word)nEquivSize ); - fwrite( pEquivs, 1, nEquivSize, pFile ); - ABC_FREE( pEquivs ); - } -/* - // write flop classes - if ( p->vFlopClasses ) - { - Gia_WriteBlockHeader( pFile, 'f', 4*Gia_ManRegNum(p) ); - fwrite( Vec_IntArray(p->vFlopClasses), 1, 4*Gia_ManRegNum(p), pFile ); - } - // write mapping - if ( p->pMapping ) - { - int nMapSize; - unsigned char * pMaps = Gia_WriteMapping( p, &nMapSize ); - Gia_WriteBlockHeader( pFile, 'm', (word)nMapSize ); - fwrite( pMaps, 1, nMapSize, pFile ); - ABC_FREE( pMaps ); - } - // write placement - if ( p->pPlacement ) - { - Gia_WriteBlockHeader( pFile, 'p', (word)4*Gia_ManObjNum(p) ); - fwrite( p->pPlacement, 1, 4*Gia_ManObjNum(p), pFile ); - } - // write switching activity - if ( p->pSwitching ) - { - Gia_WriteBlockHeader( pFile, 's', (word)Gia_ManObjNum(p) ); - fwrite( p->pSwitching, 1, Gia_ManObjNum(p), pFile ); - } - // write name - if ( p->pName ) - fprintf( pFile, "n%s%c", p->pName, '\0' ); -*/ - // write constraints - if ( p->nConstrs ) - { - Gia_WriteBlockHeader( pFile, 'c', (word)p->nConstrs ); - Gia_WriteIntF( pFile, p->nConstrs ); - } - // write the closing statement - Gia_WriteBlockHeader( pFile, '\0', (word)0 ); - // write comment - fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() ); - fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); - fclose( pFile ); - if ( p != pInit ) - Gia_ManStop( p ); -} - -/**Function************************************************************* - - Synopsis [Writes the AIG in the binary AIGER format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits ) -{ - char Buffer[100]; - sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum ); - Gia_WriteAiger( p, Buffer, 0, 0 ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/giaAiger_old.c b/src/aig/gia/giaAiger_old.c deleted file mode 100644 index 9a5ba5cd..00000000 --- a/src/aig/gia/giaAiger_old.c +++ /dev/null @@ -1,1255 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaAiger.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [Procedures to read/write binary AIGER format developed by - Armin Biere, Johannes Kepler University (http://fmv.jku.at/)] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaAiger.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef ABC_UINT64_T word; - -static inline int Gia_ObjObjPhaseDiff( Gia_Man_t * p, int i, int j ) { return Gia_ManObj(p, i)->fPhase ^ Gia_ManObj(p, j)->fPhase; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Extracts one unsigned AIG edge from the input buffer.] - - Description [This procedure is a slightly modified version of Armin Biere's - procedure "unsigned decode (FILE * file)". ] - - SideEffects [Updates the current reading position.] - - SeeAlso [] - -***********************************************************************/ -unsigned Gia_ReadAigerDecode( char ** ppPos ) -{ - unsigned x = 0, i = 0; - unsigned char ch; - while ((ch = *(*ppPos)++) & 0x80) - x |= (ch & 0x7f) << (7 * i++); - return x | (ch << (7 * i)); -} - -/**Function************************************************************* - - Synopsis [Extracts one signed AIG edge from the input buffer.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ReadAigerDecodeInt( char ** ppPos ) -{ - unsigned Res; - Res = Gia_ReadAigerDecode( ppPos ); - if ( Res & 1 ) - return -((int)(Res >> 1)); - return Res >> 1; -} - -/**Function************************************************************* - - Synopsis [Decodes the encoded array of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_WriteDecodeLiterals( char ** ppPos, int nEntries ) -{ - Vec_Int_t * vLits; - int Lit, LitPrev, Diff, i; - vLits = Vec_IntAlloc( nEntries ); - LitPrev = Gia_ReadAigerDecode( ppPos ); - Vec_IntPush( vLits, LitPrev ); - for ( i = 1; i < nEntries; i++ ) - { -// Diff = Lit - LitPrev; -// Diff = (Lit < LitPrev)? -Diff : Diff; -// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev); - Diff = Gia_ReadAigerDecode( ppPos ); - Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1; - Lit = Diff + LitPrev; - Vec_IntPush( vLits, Lit ); - LitPrev = Lit; - } - return vLits; -} - - -/**Function************************************************************* - - Synopsis [Returns the file size.] - - Description [The file should be closed.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_FixFileName( char * pFileName ) -{ - char * pName; - for ( pName = pFileName; *pName; pName++ ) - if ( *pName == '>' ) - *pName = '\\'; -} - -/**Function************************************************************* - - Synopsis [Returns the file size.] - - Description [The file should be closed.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_FileSize( char * pFileName ) -{ - FILE * pFile; - int nFileSize; - pFile = fopen( pFileName, "r" ); - if ( pFile == NULL ) - { - printf( "Gia_FileSize(): The file is unavailable (absent or open).\n" ); - return 0; - } - fseek( pFile, 0, SEEK_END ); - nFileSize = ftell( pFile ); - fclose( pFile ); - return nFileSize; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Gia_FileNameGeneric( char * FileName ) -{ - char * pDot, * pRes; - pRes = Gia_UtilStrsav( FileName ); - if ( (pDot = strrchr( pRes, '.' )) ) - *pDot = 0; - return pRes; -} - -/**Function************************************************************* - - Synopsis [Write integer into the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ReadInt( unsigned char * pPos ) -{ - int i, Value = 0; - for ( i = 0; i < 4; i++ ) - Value |= ((unsigned)(*pPos++)) << (i << 3); - return Value; -} - -/**Function************************************************************* - - Synopsis [Reads decoded value.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev ) -{ - int Item = Gia_ReadAigerDecode( ppPos ); - if ( Item & 1 ) - return iPrev + (Item >> 1); - return iPrev - (Item >> 1); -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Rpr_t * Gia_ReadEquivClasses_old( unsigned char ** ppPos, int nSize ) -{ - Gia_Rpr_t * pReprs; - unsigned char * pStop; - int i, Item, fProved, iRepr, iNode; - pStop = *ppPos; - pStop += Gia_ReadInt( *ppPos ); *ppPos += 4; - pReprs = ABC_CALLOC( Gia_Rpr_t, nSize ); - for ( i = 0; i < nSize; i++ ) - pReprs[i].iRepr = GIA_VOID; - iRepr = iNode = 0; - while ( *ppPos < pStop ) - { - Item = Gia_ReadAigerDecode( ppPos ); - if ( Item & 1 ) - { - iRepr += (Item >> 1); - iNode = iRepr; -//printf( "\nRepr = %d ", iRepr ); - continue; - } - Item >>= 1; - fProved = (Item & 1); - Item >>= 1; - iNode += Item; - pReprs[iNode].fProved = fProved; - pReprs[iNode].iRepr = iRepr; - assert( iRepr < iNode ); -//printf( "Node = %d ", iNode ); - } - return pReprs; -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize, int nAlloc ) -{ - Gia_Rpr_t * pReprs; - unsigned char * pStop; - int i, k, iRepr, iNode, nMembers; - // find place to stop - pStop = *ppPos + nSize; - // prepare equivalence classes - pReprs = ABC_CALLOC( Gia_Rpr_t, nAlloc ); - for ( i = 0; i < nAlloc; i++ ) - pReprs[i].iRepr = GIA_VOID; - // skip the number of classes - Gia_ReadAigerDecode( ppPos ); - // read classes - iRepr = iNode = 0; - while ( *ppPos < pStop ) - { - nMembers = Gia_ReadAigerDecode( ppPos ); - iRepr += Gia_ReadAigerDecode( ppPos ) >> 1; - iNode = iRepr; - for ( k = 1; k < nMembers; k++ ) - { - iNode += Gia_ReadAigerDecode( ppPos ) >> 1; - pReprs[ iNode ].iRepr = iRepr; - assert( iRepr < iNode ); -//if ( !iRepr ) -//printf( "%4d: Reading equiv %d -> %d\n", k, iNode, iRepr ); - } - } - return pReprs; -} - -/**Function************************************************************* - - Synopsis [Read flop classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ReadFlopClasses( unsigned char ** ppPos, Vec_Int_t * vClasses, int nSize ) -{ - int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; - assert( nAlloc/4 == nSize ); - assert( Vec_IntSize(vClasses) == nSize ); - memcpy( Vec_IntArray(vClasses), *ppPos, 4*nSize ); - *ppPos += 4 * nSize; -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Gia_ReadMapping( unsigned char ** ppPos, int nSize ) -{ - int * pMapping; - unsigned char * pStop; - int k, j, nFanins, nAlloc, iNode = 0, iOffset = nSize; - pStop = *ppPos; - pStop += Gia_ReadInt( *ppPos ); *ppPos += 4; - nAlloc = nSize + pStop - *ppPos; - pMapping = ABC_CALLOC( int, nAlloc ); - while ( *ppPos < pStop ) - { - k = iOffset; - pMapping[k++] = nFanins = Gia_ReadAigerDecode( ppPos ); - for ( j = 0; j <= nFanins; j++ ) - pMapping[k++] = iNode = Gia_ReadDiffValue( ppPos, iNode ); - pMapping[iNode] = iOffset; - iOffset = k; - } - assert( iOffset <= nAlloc ); - return pMapping; -} - -/**Function************************************************************* - - Synopsis [Read switching from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned char * Gia_ReadSwitching( unsigned char ** ppPos, int nSize ) -{ - unsigned char * pSwitching; - int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; - assert( nAlloc == nSize ); - pSwitching = ABC_ALLOC( unsigned char, nSize ); - memcpy( pSwitching, *ppPos, nSize ); - *ppPos += nSize; - return pSwitching; -} - -/**Function************************************************************* - - Synopsis [Read placement from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Plc_t * Gia_ReadPlacement( unsigned char ** ppPos, int nSize ) -{ - Gia_Plc_t * pPlacement; - int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; - assert( nAlloc/4 == nSize ); - pPlacement = ABC_ALLOC( Gia_Plc_t, nSize ); - memcpy( pPlacement, *ppPos, 4*nSize ); - *ppPos += 4 * nSize; - return pPlacement; -} - -/**Function************************************************************* - - Synopsis [Reads char and 64-bit int using little-endian style.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char Gia_ReadBlockHeader( char ** ppCur, word * pWord ) -{ - int i; - char Char = *(*ppCur)++; - *pWord = 0; - for ( i = 0; i < 8; i++ ) - { -// printf( "%d\n", (unsigned char)(*(*ppCur)) ); - *pWord |= ((word)(unsigned char)(*(*ppCur)++)) << (i<<3); - } - return Char; -} - -/**Function************************************************************* - - Synopsis [Reads the AIG in the binary AIGER format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ) -{ - FILE * pFile; - Gia_Man_t * pNew; - Vec_Int_t * vLits = NULL; - Vec_Int_t * vNodes, * vDrivers;//, * vTerms; - int iObj, iNode0, iNode1; - int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits; - char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType; - unsigned uLit0, uLit1, uLit; - - // read the file into the buffer - Gia_FixFileName( pFileName ); - nFileSize = Gia_FileSize( pFileName ); - pFile = fopen( pFileName, "rb" ); - pContents = ABC_ALLOC( char, nFileSize ); - fread( pContents, nFileSize, 1, pFile ); - fclose( pFile ); - - // check if the input file format is correct - if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') ) - { - fprintf( stdout, "Wrong input file format.\n" ); - free( pContents ); - return NULL; - } - - // read the file type - pCur = pContents; while ( *pCur++ != ' ' ); - // read the number of objects - nTotal = atoi( pCur ); while ( *pCur++ != ' ' ); - // read the number of inputs - nInputs = atoi( pCur ); while ( *pCur++ != ' ' ); - // read the number of latches - nLatches = atoi( pCur ); while ( *pCur++ != ' ' ); - // read the number of outputs - nOutputs = atoi( pCur ); while ( *pCur++ != ' ' ); - // read the number of nodes - nAnds = atoi( pCur ); while ( *pCur++ != '\n' ); - // check the parameters - if ( nTotal != nInputs + nLatches + nAnds ) - { - fprintf( stdout, "The paramters are wrong.\n" ); - return NULL; - } - - // allocate the empty AIG - pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 ); - pName = Gia_FileNameGeneric( pFileName ); - pNew->pName = Gia_UtilStrsav( pName ); -// pNew->pSpec = Gia_UtilStrsav( pFileName ); - ABC_FREE( pName ); - - // prepare the array of nodes - vNodes = Vec_IntAlloc( 1 + nTotal ); - Vec_IntPush( vNodes, 0 ); - - // create the PIs - for ( i = 0; i < nInputs + nLatches; i++ ) - { - iObj = Gia_ManAppendCi(pNew); - Vec_IntPush( vNodes, iObj ); - } - - // remember the beginning of latch/PO literals - pDrivers = pCur; - if ( pContents[3] == ' ' ) // standard AIGER - { - // scroll to the beginning of the binary data - for ( i = 0; i < nLatches + nOutputs; ) - if ( *pCur++ == '\n' ) - i++; - } - else // modified AIGER - { - vLits = Gia_WriteDecodeLiterals( &pCur, nLatches + nOutputs ); - } - - // create the AND gates - for ( i = 0; i < nAnds; i++ ) - { - uLit = ((i + 1 + nInputs + nLatches) << 1); - uLit1 = uLit - Gia_ReadAigerDecode( &pCur ); - uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur ); -// assert( uLit1 > uLit0 ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); - iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); - assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches ); -// Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) ); - Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) ); - } - - // remember the place where symbols begin - pSymbols = pCur; - - // read the latch driver literals - vDrivers = Vec_IntAlloc( nLatches + nOutputs ); - if ( pContents[3] == ' ' ) // standard AIGER - { - pCur = pDrivers; - for ( i = 0; i < nLatches; i++ ) - { - uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); - Vec_IntPush( vDrivers, iNode0 ); - } - // read the PO driver literals - for ( i = 0; i < nOutputs; i++ ) - { - uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); - Vec_IntPush( vDrivers, iNode0 ); - } - - } - else - { - // read the latch driver literals - for ( i = 0; i < nLatches; i++ ) - { - uLit0 = Vec_IntEntry( vLits, i ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); - Vec_IntPush( vDrivers, iNode0 ); - } - // read the PO driver literals - for ( i = 0; i < nOutputs; i++ ) - { - uLit0 = Vec_IntEntry( vLits, i+nLatches ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); - Vec_IntPush( vDrivers, iNode0 ); - } - Vec_IntFree( vLits ); - } - - // create the POs - for ( i = 0; i < nOutputs; i++ ) - Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) ); - for ( i = 0; i < nLatches; i++ ) - Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) ); - Vec_IntFree( vDrivers ); - - // create the latches - Gia_ManSetRegNum( pNew, nLatches ); - - // check if there are other types of information to read - pCur = pSymbols; - if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' ) - { - char Char; - word Size; - pCur++; - - // read model name (old style) - if ( *pCur == 'n' ) - { - pCur++; - ABC_FREE( pNew->pName ); - pNew->pName = Gia_UtilStrsav( pCur ); - pCur += (int)(strlen(pNew->pName) + 1); - } - - Char = Gia_ReadBlockHeader( &pCur, &Size ); - if ( Char == '\n' && Size == 0xAC1D0FF1CEC0FFEE ) - { - while ( (Char = Gia_ReadBlockHeader(&pCur, &Size)) ) - { - switch (Char) - { - case 'N': - // read model name - ABC_FREE( pNew->pName ); - pNew->pName = ABC_ALLOC( char, (int)Size + 1 ); - strncpy( pNew->pName, pCur, (int)Size ); - pNew->pName[(int)Size] = '\0'; - pCur += (int)Size; - break; - case 'n': - // read model name - ABC_FREE( pNew->pName ); - pNew->pName = Gia_UtilStrsav( pCur ); - pCur += (int)(strlen(pNew->pName) + 1); - break; - case '=': - // read equivalence classes - pNew->pReprs = Gia_ReadEquivClasses( &pCur, (int)Size, Gia_ManObjNum(pNew) ); - pNew->pNexts = Gia_ManDeriveNexts( pNew ); - break; - case 'c': - // read number of constraints - pNew->nConstrs = Gia_ReadInt( pCur ); pCur += 4; - break; - default: - printf( "Unrecognized data.\n" ); - break; - } - } - } - else - { - printf( "Extended AIGER reader: Internal signature does not match.\n" ); - } - -/* - if ( *pCur == 'e' ) - { - pCur++; - // read equivalence classes - pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) ); - pNew->pNexts = Gia_ManDeriveNexts( pNew ); - } - if ( *pCur == 'f' ) - { - pCur++; - // read flop classes - pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) ); - Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) ); - } - if ( *pCur == 'm' ) - { - pCur++; - // read mapping - pNew->pMapping = Gia_ReadMapping( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 'p' ) - { - pCur++; - // read placement - pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 's' ) - { - pCur++; - // read switching activity - pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 'c' ) - { - pCur++; - // read number of constraints - pNew->nConstrs = Gia_ReadInt( pCur ); pCur += 4; - } - if ( *pCur == 'n' ) - { - pCur++; - // read model name - ABC_FREE( pNew->pName ); - pNew->pName = Gia_UtilStrsav( pCur ); - } -*/ - } - - // skipping the comments - ABC_FREE( pContents ); - Vec_IntFree( vNodes ); -/* - // check the result - if ( fCheck && !Gia_ManCheck( pNew ) ) - { - printf( "Gia_ReadAiger: The network check has failed.\n" ); - Gia_ManStop( pNew ); - return NULL; - } -*/ - return pNew; -} - - -/**Function************************************************************* - - Synopsis [Adds one unsigned AIG edge to the output buffer.] - - Description [This procedure is a slightly modified version of Armin Biere's - procedure "void encode (FILE * file, unsigned x)" ] - - SideEffects [Returns the current writing position.] - - SeeAlso [] - -***********************************************************************/ -int Gia_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x ) -{ - unsigned char ch; - while (x & ~0x7f) - { - ch = (x & 0x7f) | 0x80; - pBuffer[Pos++] = ch; - x >>= 7; - } - ch = x; - pBuffer[Pos++] = ch; - return Pos; -} - -/**Function************************************************************* - - Synopsis [Adds one signed int to the output buffer.] - - Description [] - - SideEffects [Returns the current writing position.] - - SeeAlso [] - -***********************************************************************/ -int Gia_WriteAigerEncodeInt( unsigned char * pBuffer, int Pos, int x ) -{ - if ( x >= 0 ) - return Gia_WriteAigerEncode( pBuffer, Pos, ((unsigned)(x) << 1) ); - return Gia_WriteAigerEncode( pBuffer, Pos, ((unsigned)(-x) << 1) | 1 ); -} - -/**Function************************************************************* - - Synopsis [Create the array of literals to be written.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_WriteAigerLiterals( Gia_Man_t * p ) -{ - Vec_Int_t * vLits; - Gia_Obj_t * pObj; - int i; - vLits = Vec_IntAlloc( Gia_ManPoNum(p) ); - Gia_ManForEachRi( p, pObj, i ) - Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) ); - Gia_ManForEachPo( p, pObj, i ) - Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) ); - return vLits; -} - -/**Function************************************************************* - - Synopsis [Creates the binary encoded array of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Str_t * Gia_WriteEncodeLiterals( Vec_Int_t * vLits ) -{ - Vec_Str_t * vBinary; - int Pos = 0, Lit, LitPrev, Diff, i; - vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) ); - LitPrev = Vec_IntEntry( vLits, 0 ); - Pos = Gia_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); - Vec_IntForEachEntryStart( vLits, Lit, i, 1 ) - { - Diff = Lit - LitPrev; - Diff = (Lit < LitPrev)? -Diff : Diff; - Diff = (Diff << 1) | (int)(Lit < LitPrev); - Pos = Gia_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff ); - LitPrev = Lit; - if ( Pos + 10 > vBinary->nCap ) - Vec_StrGrow( vBinary, vBinary->nCap+1 ); - } - vBinary->nSize = Pos; -/* - // verify - { - extern Vec_Int_t * Gia_WriteDecodeLiterals( char ** ppPos, int nEntries ); - char * pPos = Vec_StrArray( vBinary ); - Vec_Int_t * vTemp = Gia_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) ); - for ( i = 0; i < Vec_IntSize(vLits); i++ ) - { - int Entry1 = Vec_IntEntry(vLits,i); - int Entry2 = Vec_IntEntry(vTemp,i); - assert( Entry1 == Entry2 ); - } - Vec_IntFree( vTemp ); - } -*/ - return vBinary; -} - -/**Function************************************************************* - - Synopsis [Write integer into the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_WriteInt( char * pBuffer, int Value ) -{ - int i; - for ( i = 0; i < 4; i++ ) - pBuffer[i] = (char)(0xff & (Value >> (i<<3))); -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned char * Gia_WriteEquivClasses_old( Gia_Man_t * p, int * pEquivSize ) -{ - unsigned char * pBuffer; - int iRepr, iNode, iPrevRepr, iPrevNode, iLit, nItems, iPos; - assert( p->pReprs && p->pNexts ); - // count the number of entries to be written - nItems = 0; - for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ ) - { - nItems += Gia_ObjIsConst( p, iRepr ); - if ( !Gia_ObjIsHead(p, iRepr) ) - continue; - Gia_ClassForEachObj( p, iRepr, iNode ) - nItems++; - } - pBuffer = ABC_ALLOC( char, sizeof(int) * (nItems + 1) ); - // write constant class - iPos = Gia_WriteAigerEncode( pBuffer, 4, Gia_Var2Lit(0, 1) ); - iPrevNode = 0; - for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ ) - if ( Gia_ObjIsConst(p, iNode) ) - { - iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); - iPrevNode = iNode; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) ); - } - // write non-constant classes - iPrevRepr = 0; - Gia_ManForEachClass( p, iRepr ) - { - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iRepr - iPrevRepr, 1) ); - iPrevRepr = iPrevNode = iRepr; - Gia_ClassForEachObj1( p, iRepr, iNode ) - { - iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); - iPrevNode = iNode; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) ); - } - } - Gia_WriteInt( pBuffer, iPos ); - *pEquivSize = iPos; - return pBuffer; -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize ) -{ - unsigned char * pBuffer; - int k, iRepr, iNode, iPrevRepr, iPrevNode, iLit; - int nItems, iPos, nClasses, nMembers; - assert( p->pReprs && p->pNexts ); - Gia_ManSetPhase(p); - // count the number of entries to be written - nItems = 0; - nMembers = 0; - nClasses = 0; - for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ ) - { - nItems += Gia_ObjIsConst( p, iRepr ); - nMembers += Gia_ObjIsConst( p, iRepr ); - if ( !Gia_ObjIsHead(p, iRepr) ) - continue; - nClasses++; - Gia_ClassForEachObj( p, iRepr, iNode ) - nItems++; - } - nClasses += (nMembers > 0); - // allocate place for data - pBuffer = (unsigned char *)ABC_ALLOC( int, nItems+1 ); - // write the number of classes - iPos = Gia_WriteAigerEncode( pBuffer, 0, nClasses ); - // write constant class - if ( nMembers ) - { - iPos = Gia_WriteAigerEncode( pBuffer, iPos, nMembers+1 ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(0,0) ); - iPrevNode = 0; - k = 1; - for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ ) - if ( Gia_ObjIsConst(p, iNode) ) - { - iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjObjPhaseDiff(p, iNode, 0) ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, iLit ); - iPrevNode = iNode; -//printf( "%4d : Writing equiv %d -> %d\n", k++, iNode, 0 ); - } - } - // write non-constant classes - iPrevRepr = 0; - Gia_ManForEachClass( p, iRepr ) - { - // write number of members - nMembers = 0; - Gia_ClassForEachObj( p, iRepr, iNode ) - nMembers++; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, nMembers ); - // write representatives - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iRepr - iPrevRepr, 0) ); - // write members - iPrevRepr = iPrevNode = iRepr; - Gia_ClassForEachObj1( p, iRepr, iNode ) - { - iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjObjPhaseDiff(p, iNode, iRepr) ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, iLit ); - iPrevNode = iNode; -//printf( "Writing equiv %d -> %d\n", iNode, iRepr ); - } - } - *pEquivSize = iPos; - return pBuffer; -} - -/**Function************************************************************* - - Synopsis [Reads decoded value.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_WriteDiffValue( char * pPos, int iPos, int iPrev, int iThis ) -{ - if ( iPrev < iThis ) - return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iThis - iPrev, 1) ); - return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iPrev - iThis, 0) ); -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned char * Gia_WriteMapping( Gia_Man_t * p, int * pMapSize ) -{ - unsigned char * pBuffer; - int i, k, iPrev, iFan, nItems, iPos = 4; - assert( p->pMapping ); - // count the number of entries to be written - nItems = 0; - Gia_ManForEachLut( p, i ) - nItems += 2 + Gia_ObjLutSize( p, i ); - pBuffer = ABC_ALLOC( char, sizeof(int) * (nItems + 1) ); - // write non-constant classes - iPrev = 0; - Gia_ManForEachLut( p, i ) - { -//printf( "\nSize = %d ", Gia_ObjLutSize(p, i) ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_ObjLutSize(p, i) ); - Gia_LutForEachFanin( p, i, iFan, k ) - { -//printf( "Fan = %d ", iFan ); - iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, iFan ); - iPrev = iFan; - } - iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, i ); - iPrev = i; -//printf( "Node = %d ", i ); - } -//printf( "\n" ); - Gia_WriteInt( pBuffer, iPos ); - *pMapSize = iPos; - return pBuffer; -} - -/**Function************************************************************* - - Synopsis [Writes char and 64-bit int using little-endian style.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_WriteBlockHeader( FILE * pFile, char Char, word Word ) -{ - int i; - fprintf( pFile, "%c", Char ); - for ( i = 0; i < 8; i++ ) - fprintf( pFile, "%c", (unsigned char)(0xff & (Word >> (i<<3))) ); -} - -/**Function************************************************************* - - Synopsis [Write integer into the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_WriteIntF( FILE * pFile, int Value ) -{ - int i; - for ( i = 0; i < 4; i++ ) - fprintf( pFile, "%c", (char)(0xff & (Value >> (i<<3))) ); -} - -/**Function************************************************************* - - Synopsis [Writes the AIG in the binary AIGER format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact ) -{ - FILE * pFile; - Gia_Man_t * p; - Gia_Obj_t * pObj; - int i, nBufferSize, Pos; - unsigned char * pBuffer; - unsigned uLit0, uLit1, uLit; - - if ( Gia_ManCoNum(pInit) == 0 ) - { - printf( "AIG cannot be written because it has no POs.\n" ); - return; - } - - // start the output stream - pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - fprintf( stdout, "Gia_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName ); - return; - } - - // create normalized AIG - if ( !Gia_ManIsNormalized(pInit) ) - { -// printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" ); - p = Gia_ManDupNormalized( pInit ); - } - else - p = pInit; - - // write the header "M I L O A" where M = I + L + A - fprintf( pFile, "aig%s %u %u %u %u %u\n", - fCompact? "2" : "", - Gia_ManCiNum(p) + Gia_ManAndNum(p), - Gia_ManPiNum(p), - Gia_ManRegNum(p), - Gia_ManPoNum(p), - Gia_ManAndNum(p) ); - - if ( !fCompact ) - { - // write latch drivers - Gia_ManForEachRi( p, pObj, i ) - fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) ); - // write PO drivers - Gia_ManForEachPo( p, pObj, i ) - fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) ); - } - else - { - Vec_Int_t * vLits = Gia_WriteAigerLiterals( p ); - Vec_Str_t * vBinary = Gia_WriteEncodeLiterals( vLits ); - fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile ); - Vec_StrFree( vBinary ); - Vec_IntFree( vLits ); - } - - // write the nodes into the buffer - Pos = 0; - nBufferSize = 6 * Gia_ManAndNum(p) + 100; // skeptically assuming 3 chars per one AIG edge - pBuffer = ABC_ALLOC( unsigned char, nBufferSize ); - Gia_ManForEachAnd( p, pObj, i ) - { - uLit = Gia_Var2Lit( i, 0 ); - uLit0 = Gia_ObjFaninLit0( pObj, i ); - uLit1 = Gia_ObjFaninLit1( pObj, i ); - assert( uLit0 < uLit1 ); - Pos = Gia_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 ); - Pos = Gia_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); - if ( Pos > nBufferSize - 10 ) - { - printf( "Gia_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" ); - fclose( pFile ); - if ( p != pInit ) - Gia_ManStop( p ); - return; - } - } - assert( Pos < nBufferSize ); - - // write the buffer - fwrite( pBuffer, 1, Pos, pFile ); - ABC_FREE( pBuffer ); - - // write the comment - fprintf( pFile, "c" ); - // write signature - Gia_WriteBlockHeader( pFile, '\n', 0xAC1D0FF1CEC0FFEE ); - // write name - if ( p->pName ) - { - Gia_WriteBlockHeader( pFile, 'N', (word)strlen(pInit->pName) ); - fwrite( pInit->pName, 1, strlen(pInit->pName), pFile ); - } - // write equivalences - if ( p->pReprs && p->pNexts ) - { - int nEquivSize; - unsigned char * pEquivs = Gia_WriteEquivClasses( p, &nEquivSize ); - Gia_WriteBlockHeader( pFile, '=', (word)nEquivSize ); - fwrite( pEquivs, 1, nEquivSize, pFile ); - ABC_FREE( pEquivs ); - } - // write flop classes - if ( p->vFlopClasses ) - { - Gia_WriteBlockHeader( pFile, 'f', 4*Gia_ManRegNum(p) ); - fwrite( Vec_IntArray(p->vFlopClasses), 1, 4*Gia_ManRegNum(p), pFile ); - } -/* - // write mapping - if ( p->pMapping ) - { - int nMapSize; - unsigned char * pMaps = Gia_WriteMapping( p, &nMapSize ); - Gia_WriteBlockHeader( pFile, 'm', (word)nMapSize ); - fwrite( pMaps, 1, nMapSize, pFile ); - ABC_FREE( pMaps ); - } - // write placement - if ( p->pPlacement ) - { - Gia_WriteBlockHeader( pFile, 'p', (word)4*Gia_ManObjNum(p) ); - fwrite( p->pPlacement, 1, 4*Gia_ManObjNum(p), pFile ); - } - // write switching activity - if ( p->pSwitching ) - { - Gia_WriteBlockHeader( pFile, 's', (word)Gia_ManObjNum(p) ); - fwrite( p->pSwitching, 1, Gia_ManObjNum(p), pFile ); - } - // write name - if ( p->pName ) - fprintf( pFile, "n%s%c", p->pName, '\0' ); -*/ - // write constraints - if ( p->nConstrs ) - { - Gia_WriteBlockHeader( pFile, 'c', (word)p->nConstrs ); - Gia_WriteIntF( pFile, p->nConstrs ); - } - // write the closing statement - Gia_WriteBlockHeader( pFile, '\0', (word)0 ); - // write comment - fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() ); - fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); - fclose( pFile ); - if ( p != pInit ) - Gia_ManStop( p ); -} - -/**Function************************************************************* - - Synopsis [Writes the AIG in the binary AIGER format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits ) -{ - char Buffer[100]; - sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum ); - Gia_WriteAiger( p, Buffer, 0, 0 ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |