From 2575a5d6836c5bd8160b8e965c622e358b2dc742 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 10 Dec 2012 13:56:40 -0800 Subject: Unifification of custom extensions. --- abclib.dsp | 4 + src/aig/gia/gia.h | 62 +- src/aig/gia/giaAiger.c | 1544 +++++++++++++------------------------------- src/aig/gia/giaAigerExt.c | 240 +++++++ src/aig/gia/giaEquiv.c | 14 +- src/aig/gia/giaHcd.c | 2 +- src/aig/gia/giaIso.c | 6 +- src/aig/gia/giaMan.c | 8 +- src/aig/gia/module.make | 1 + src/base/abci/abc.c | 30 +- src/base/abci/abcRec2.c | 2 +- src/base/abci/abcTim.c | 6 +- src/base/cmd/cmdPlugin.c | 4 +- src/misc/tim/tim.h | 4 +- src/misc/tim/timDump.c | 8 +- src/misc/util/utilBridge.c | 51 +- src/proof/abs/absGla.c | 4 +- src/proof/abs/absGlaOld.c | 2 +- src/proof/abs/absVta.c | 2 +- src/proof/cec/cecCec.c | 2 +- src/proof/cec/cecCore.c | 4 +- src/proof/cec/cecCorr.c | 2 +- src/proof/cec/cecSeq.c | 4 +- src/proof/cec/cecSolve.c | 2 +- src/proof/cec/cecSynth.c | 2 +- src/sat/bmc/bmcCexMin2.c | 4 +- src/sat/bmc/bmcCexTools.c | 4 +- 27 files changed, 842 insertions(+), 1176 deletions(-) create mode 100644 src/aig/gia/giaAigerExt.c diff --git a/abclib.dsp b/abclib.dsp index f29813e5..804a7759 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -3411,6 +3411,10 @@ SOURCE=.\src\aig\gia\giaAiger.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaAigerExt.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaBidec.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 52db2cce..fbc9212e 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -140,6 +140,10 @@ struct Gia_Man_t_ Vec_Int_t * vDoms; // dominators unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects + Gia_Man_t * pAigExtra; // combinational logic of holes + Vec_Flt_t * vInArrs; // PI arrival times + Vec_Flt_t * vOutReqs; // PO required times + Vec_Int_t * vPacking; // packing information int * pTravIds; // separate traversal ID representation int nTravIdsAlloc; // the number of trav IDs allocated Vec_Ptr_t * vNamesIn; // the input names @@ -593,6 +597,52 @@ static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj ) printf( "X" ); } +static inline int Gia_AigerReadInt( unsigned char * pPos ) +{ + int i, Value = 0; + for ( i = 0; i < 4; i++ ) + Value = (Value << 8) | *pPos++; + return Value; +} +static inline void Gia_AigerWriteInt( unsigned char * pPos, int Value ) +{ + int i; + for ( i = 3; i >= 0; i-- ) + *pPos++ = (Value >> (8*i)) & 255; +} +static inline unsigned Gia_AigerReadUnsigned( unsigned char ** ppPos ) +{ + unsigned x = 0, i = 0; + unsigned char ch; + while ((ch = *(*ppPos)++) & 0x80) + x |= (ch & 0x7f) << (7 * i++); + return x | (ch << (7 * i)); +} +static inline void Gia_AigerWriteUnsigned( Vec_Str_t * vStr, unsigned x ) +{ + unsigned char ch; + while (x & ~0x7f) + { + ch = (x & 0x7f) | 0x80; + Vec_StrPush( vStr, ch ); + x >>= 7; + } + ch = x; + Vec_StrPush( vStr, ch ); +} +static inline int Gia_AigerWriteUnsignedBuffer( 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; +} static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); } static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; } @@ -712,13 +762,13 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re /*=== giaAiger.c ===========================================================*/ extern int Gia_FileSize( char * pFileName ); -extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck ); -extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck ); -extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact ); +extern Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck ); +extern Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck ); +extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact ); extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits ); -extern Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p ); -extern Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs ); -extern void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName ); +extern Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p ); +extern Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs ); +extern void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName ); /*=== giaBidec.c ===========================================================*/ extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited ); extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 0a35dab0..ea36add4 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -35,88 +35,30 @@ ABC_NAMESPACE_IMPL_START /**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( unsigned 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 [Decodes the encoded array of literals.] + Synopsis [] Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_WriteDecodeLiterals( unsigned 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 ) +void Gia_FileFixName( 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 [] - -***********************************************************************/ +char * Gia_FileNameGeneric( char * FileName ) +{ + char * pDot, * pRes; + pRes = Abc_UtilStrsav( FileName ); + if ( (pDot = strrchr( pRes, '.' )) ) + *pDot = 0; + return pRes; +} int Gia_FileSize( char * pFileName ) { FILE * pFile; @@ -132,49 +74,16 @@ int Gia_FileSize( char * pFileName ) fclose( pFile ); return nFileSize; } - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Gia_FileNameGeneric( char * FileName ) -{ - char * pDot, * pRes; - pRes = Abc_UtilStrsav( FileName ); - if ( (pDot = strrchr( pRes, '.' )) ) - *pDot = 0; - return pRes; -} - -/**Function************************************************************* - - Synopsis [Read integer from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ReadInt( unsigned char * pPos ) +void Gia_FileWriteBufferSize( FILE * pFile, int nSize ) { - int i, Value = 0; - for ( i = 0; i < 4; i++ ) - Value = (Value << 8) | *pPos++; - return Value; + unsigned char Buffer[5]; + Gia_AigerWriteInt( Buffer, nSize ); + fwrite( Buffer, 1, 4, pFile ); } /**Function************************************************************* - Synopsis [Reads decoded value.] + Synopsis [Create the array of literals to be written.] Description [] @@ -183,153 +92,72 @@ int Gia_ReadInt( unsigned char * pPos ) SeeAlso [] ***********************************************************************/ -unsigned Gia_ReadDiffValue( unsigned char ** ppPos, int iPrev ) +Vec_Int_t * Gia_AigerCollectLiterals( Gia_Man_t * p ) { - int Item = Gia_ReadAigerDecode( ppPos ); - if ( Item & 1 ) - return iPrev + (Item >> 1); - return iPrev - (Item >> 1); + 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 [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize ) +Vec_Int_t * Gia_AigerReadLiterals( unsigned char ** ppPos, int nEntries ) { - 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 ) + Vec_Int_t * vLits; + int Lit, LitPrev, Diff, i; + vLits = Vec_IntAlloc( nEntries ); + LitPrev = Gia_AigerReadUnsigned( ppPos ); + Vec_IntPush( vLits, LitPrev ); + for ( i = 1; i < nEntries; i++ ) { - 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 ); +// Diff = Lit - LitPrev; +// Diff = (Lit < LitPrev)? -Diff : Diff; +// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev); + Diff = Gia_AigerReadUnsigned( ppPos ); + Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1; + Lit = Diff + LitPrev; + Vec_IntPush( vLits, Lit ); + LitPrev = Lit; } - 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; + return vLits; } - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Gia_ReadMapping( unsigned char ** ppPos, int nSize ) +Vec_Str_t * Gia_AigerWriteLiterals( Vec_Int_t * vLits ) { - 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 ) + 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_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); + Vec_IntForEachEntryStart( vLits, Lit, i, 1 ) { - 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; + Diff = Lit - LitPrev; + Diff = (Lit < LitPrev)? -Diff : Diff; + Diff = (Diff << 1) | (int)(Lit < LitPrev); + Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff ); + LitPrev = Lit; + if ( Pos + 10 > vBinary->nCap ) + Vec_StrGrow( vBinary, vBinary->nCap+1 ); } - 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; + vBinary->nSize = Pos; +/* + // verify + { + extern Vec_Int_t * Gia_AigerReadLiterals( char ** ppPos, int nEntries ); + char * pPos = Vec_StrArray( vBinary ); + Vec_Int_t * vTemp = Gia_AigerReadLiterals( &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************************************************************* @@ -343,35 +171,16 @@ Gia_Plc_t * Gia_ReadPlacement( unsigned char ** ppPos, int nSize ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) +Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck ) { - FILE * pFile; - Gia_Man_t * pNew; - Vec_Int_t * vLits = NULL; + Gia_Man_t * pNew, * pTemp; + Vec_Int_t * vLits = NULL, * vPoTypes = NULL; Vec_Int_t * vNodes, * vDrivers;//, * vTerms; int iObj, iNode0, iNode1; - int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits; + int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits; int nBad = 0, nConstr = 0, nJust = 0, nFair = 0; unsigned char * pDrivers, * pSymbols, * pCur;//, * pType; - char * pContents, * pName; unsigned uLit0, uLit1, uLit; - int RetValue; - - // read the file into the buffer - Gia_FixFileName( pFileName ); - nFileSize = Gia_FileSize( pFileName ); - pFile = fopen( pFileName, "rb" ); - pContents = ABC_ALLOC( char, nFileSize ); - RetValue = 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') ) - { - ABC_FREE( pContents ); - fprintf( stdout, "Wrong input file format.\n" ); - return NULL; - } // read the parameters (M I L O A + B C J F) pCur = (unsigned char *)pContents; while ( *pCur != ' ' ) pCur++; pCur++; @@ -417,7 +226,6 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) if ( *pCur != '\n' ) { fprintf( stdout, "The parameter line is in a wrong format.\n" ); - ABC_FREE( pContents ); return NULL; } pCur++; @@ -426,13 +234,11 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) if ( nTotal != nInputs + nLatches + nAnds ) { fprintf( stdout, "The number of objects does not match.\n" ); - ABC_FREE( pContents ); return NULL; } if ( nJust || nFair ) { fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" ); - ABC_FREE( pContents ); return NULL; } @@ -446,11 +252,6 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) // allocate the empty AIG pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 ); - pName = Gia_FileNameGeneric( pFileName ); - pNew->pName = Abc_UtilStrsav( pName ); - pNew->pSpec = Abc_UtilStrsav( pFileName ); -// pNew->pSpec = Abc_UtilStrsav( pFileName ); - ABC_FREE( pName ); pNew->nConstrs = nConstr; // prepare the array of nodes @@ -475,22 +276,33 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) } else // modified AIGER { - vLits = Gia_WriteDecodeLiterals( &pCur, nLatches + nOutputs ); + vLits = Gia_AigerReadLiterals( &pCur, nLatches + nOutputs ); } // create the AND gates + if ( !fSkipStrash ) + Gia_ManHashAlloc( pNew ); for ( i = 0; i < nAnds; i++ ) { uLit = ((i + 1 + nInputs + nLatches) << 1); - uLit1 = uLit - Gia_ReadAigerDecode( &pCur ); - uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur ); + uLit1 = uLit - Gia_AigerReadUnsigned( &pCur ); + uLit0 = uLit1 - Gia_AigerReadUnsigned( &pCur ); // assert( uLit1 > uLit0 ); iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); iNode1 = Abc_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) ); + if ( fSkipStrash ) + { + if ( iNode0 == 1 && iNode1 == 1 ) + Vec_IntPush( vNodes, Gia_ManAppendPinType(pNew, 1) ); + else + Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) ); + } + else + Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) ); } + if ( !fSkipStrash ) + Gia_ManHashStop( pNew ); // remember the place where symbols begin pSymbols = pCur; @@ -544,297 +356,16 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) // create the latches Gia_ManSetRegNum( pNew, nLatches ); - // check if there are other types of information to read + // read signal names if they are of the special type pCur = pSymbols; - if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' ) + if ( *pCur != 'c' ) { - pCur++; - 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 == 'g' ) - { - pCur++; - // read gate classes - pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) ); - Gia_ReadFlopClasses( &pCur, pNew->vGateClasses, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 'v' ) - { - pCur++; - // read object classes - pNew->vObjClasses = Vec_IntStart( Gia_ReadInt(pCur)/4 ); pCur += 4; - memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) ); - pCur += 4*Vec_IntSize(pNew->vObjClasses); - } - 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 = Abc_UtilStrsav( (char *)pCur ); - } - } - Vec_IntFree( vNodes ); - - // update polarity of the additional outputs - if ( nBad || nConstr || nJust || nFair ) - Gia_ManInvertConstraints( pNew ); - - // skipping the comments -/* - // 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 [Reads the AIG in the binary AIGER format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck ) -{ - Gia_Man_t * pNew, * pTemp; - Vec_Int_t * vLits = NULL, * vPoTypes = NULL; - Vec_Int_t * vNodes, * vDrivers;//, * vTerms; - int iObj, iNode0, iNode1; - int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits; - int nBad = 0, nConstr = 0, nJust = 0, nFair = 0; - unsigned char * pDrivers, * pSymbols, * pCur;//, * pType; - unsigned uLit0, uLit1, uLit; - - // read the parameters (M I L O A + B C J F) - pCur = (unsigned char *)pContents; while ( *pCur != ' ' ) pCur++; pCur++; - // read the number of objects - nTotal = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++; - // read the number of inputs - nInputs = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++; - // read the number of latches - nLatches = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++; - // read the number of outputs - nOutputs = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++; - // read the number of nodes - nAnds = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; - if ( *pCur == ' ' ) - { - assert( nOutputs == 0 ); - // read the number of properties - pCur++; - nBad = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; - nOutputs += nBad; - } - if ( *pCur == ' ' ) - { - // read the number of properties - pCur++; - nConstr = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; - nOutputs += nConstr; - } - if ( *pCur == ' ' ) - { - // read the number of properties - pCur++; - nJust = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; - nOutputs += nJust; - } - if ( *pCur == ' ' ) - { - // read the number of properties - pCur++; - nFair = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; - nOutputs += nFair; - } - if ( *pCur != '\n' ) - { - fprintf( stdout, "The parameter line is in a wrong format.\n" ); - return NULL; - } - pCur++; - - // check the parameters - if ( nTotal != nInputs + nLatches + nAnds ) - { - fprintf( stdout, "The number of objects does not match.\n" ); - return NULL; - } - if ( nJust || nFair ) - { - fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" ); - return NULL; - } - - if ( nConstr ) - { - if ( nConstr == 1 ) - fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" ); - else - fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr ); - } - - // allocate the empty AIG - pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 ); - pNew->nConstrs = nConstr; - - // 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 - if ( !fSkipStrash ) - Gia_ManHashAlloc( pNew ); - 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 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); - iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); - assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches ); - if ( fSkipStrash ) - { - if ( iNode0 == 1 && iNode1 == 1 ) - Vec_IntPush( vNodes, Gia_ManAppendPinType(pNew, 1) ); - else - Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) ); - } - else - Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) ); - } - if ( !fSkipStrash ) - Gia_ManHashStop( pNew ); - - // 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( (char *)pCur ); while ( *pCur++ != '\n' ); - iNode0 = Abc_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( (char *)pCur ); while ( *pCur++ != '\n' ); - iNode0 = Abc_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 = Abc_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 = Abc_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 ); - - // read signal names if they are of the special type - pCur = pSymbols; - if ( *pCur != 'c' ) - { - int fBreakUsed = 0; - unsigned char * pCurOld = pCur; - pNew->vUserPiIds = Vec_IntStartFull( nInputs ); - pNew->vUserPoIds = Vec_IntStartFull( nOutputs ); - pNew->vUserFfIds = Vec_IntStartFull( nLatches ); - while ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' ) + int fBreakUsed = 0; + unsigned char * pCurOld = pCur; + pNew->vUserPiIds = Vec_IntStartFull( nInputs ); + pNew->vUserPoIds = Vec_IntStartFull( nOutputs ); + pNew->vUserFfIds = Vec_IntStartFull( nLatches ); + while ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' ) { int iTerm; char * pType = (char *)pCur; @@ -963,91 +494,151 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS // check if there are other types of information to read if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' ) { + Vec_Str_t * vStr; + char * pCurTemp; pCur++; - if ( *pCur == 'e' ) + while ( 1 ) { - pCur++; + // read extra AIG + if ( *pCur == 'a' ) + { + pCur++; + vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4; + memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) ); + pCur += Vec_StrSize(vStr); + pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0 ); + Vec_StrFree( vStr ); + } + // read number of constraints + else if ( *pCur == 'c' ) + { + pCur++; + assert( Gia_AigerReadInt(pCur) == 4 ); pCur += 4; + pNew->nConstrs = Gia_AigerReadInt( pCur ); pCur += 4; + } + // read delay information + else if ( *pCur == 'd' ) + { + pCur++; + assert( Gia_AigerReadInt(pCur) == 4*(Gia_ManPiNum(pNew) + Gia_ManPoNum(pNew)) ); pCur += 4; + pNew->vInArrs = Vec_FltStart( Gia_ManPiNum(pNew) ); + pNew->vOutReqs = Vec_FltStart( Gia_ManPoNum(pNew) ); + memcpy( Vec_FltArray(pNew->vInArrs), pCur, 4*Gia_ManPiNum(pNew) ); pCur += 4*Gia_ManPiNum(pNew); + memcpy( Vec_FltArray(pNew->vOutReqs), pCur, 4*Gia_ManPoNum(pNew) ); pCur += 4*Gia_ManPoNum(pNew); + } // read equivalence classes - pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) ); - pNew->pNexts = Gia_ManDeriveNexts( pNew ); - } - if ( *pCur == 'f' ) - { - pCur++; + else if ( *pCur == 'e' ) + { + extern Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize ); + pCur++; + // pCurTemp = pCur + Gia_AigerReadInt(pCur); pCur += 4; + pNew->pReprs = Gia_AigerReadEquivClasses( &pCur, Gia_ManObjNum(pNew) ); + pNew->pNexts = Gia_ManDeriveNexts( pNew ); + // assert( pCur == pCurTemp ); + } // read flop classes - pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) ); - Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) ); - } - if ( *pCur == 'g' ) - { - pCur++; + else if ( *pCur == 'f' ) + { + pCur++; + assert( Gia_AigerReadInt(pCur) == 4*Gia_ManRegNum(pNew) ); pCur += 4; + pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) ); + memcpy( Vec_IntArray(pNew->vFlopClasses), pCur, 4*Gia_ManRegNum(pNew) ); pCur += 4*Gia_ManRegNum(pNew); + } // read gate classes - pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) ); - Gia_ReadFlopClasses( &pCur, pNew->vGateClasses, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 'v' ) - { - pCur++; - // read object classes - pNew->vObjClasses = Vec_IntStart( Gia_ReadInt(pCur)/4 ); pCur += 4; - memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) ); - pCur += 4*Vec_IntSize(pNew->vObjClasses); - } - if ( *pCur == 'm' ) - { - pCur++; + else if ( *pCur == 'g' ) + { + pCur++; + assert( Gia_AigerReadInt(pCur) == 4*Gia_ManObjNum(pNew) ); pCur += 4; + pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) ); + memcpy( Vec_IntArray(pNew->vGateClasses), pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew); + } + // read hierarchy information + else if ( *pCur == 'h' ) + { + pCur++; + vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4; + memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) ); + pCur += Vec_StrSize(vStr); + pNew->pManTime = Tim_ManLoad( vStr, 1 ); + Vec_StrFree( vStr ); + } + // read packing + else if ( *pCur == 'k' ) + { + extern Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize ); + pCur++; + pCurTemp = pCur + Gia_AigerReadInt(pCur); pCur += 4; + pNew->vPacking = Gia_AigerReadPacking( &pCur, pCurTemp - pCur ); + assert( pCur == pCurTemp ); + } // read mapping - pNew->pMapping = Gia_ReadMapping( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 'p' ) - { - pCur++; + else if ( *pCur == 'm' ) + { + extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize ); + pCur++; + pCurTemp = pCur + Gia_AigerReadInt(pCur); pCur += 4; + pNew->pMapping = Gia_AigerReadMapping( &pCur, Gia_ManObjNum(pNew) ); + assert( pCur == pCurTemp ); + } + // read model name + else if ( *pCur == 'n' ) + { + pCur++; + if ( (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z') || (*pCur >= '0' && *pCur <= '9') ) + { + pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1; + } + else + { + pCurTemp = pCur + Gia_AigerReadInt(pCur); pCur += 4; + ABC_FREE( pNew->pName ); + pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1; + assert( pCur == pCurTemp ); + } + } // read placement - pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 's' ) - { - pCur++; + else if ( *pCur == 'p' ) + { + Gia_Plc_t * pPlacement; + pCur++; + pCurTemp = pCur + Gia_AigerReadInt(pCur); pCur += 4; + pPlacement = ABC_ALLOC( Gia_Plc_t, Gia_ManObjNum(pNew) ); + memcpy( pPlacement, pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew); + assert( pCur == pCurTemp ); + } // read switching activity - pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) ); - } - if ( *pCur == 't' ) - { - Vec_Str_t * vStr; - pCur++; + else if ( *pCur == 's' ) + { + unsigned char * pSwitching; + pCur++; + pCurTemp = pCur + Gia_AigerReadInt(pCur); pCur += 4; + pSwitching = ABC_ALLOC( unsigned char, Gia_ManObjNum(pNew) ); + memcpy( pSwitching, pCur, Gia_ManObjNum(pNew) ); pCur += Gia_ManObjNum(pNew); + assert( pCur == pCurTemp ); + } // read timing manager - vStr = Vec_StrStart( Gia_ReadInt(pCur) ); pCur += 4; - memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) ); - pCur += Vec_StrSize(vStr); - pNew->pManTime = Tim_ManLoad( vStr ); - Vec_StrFree( vStr ); - } - 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 = Abc_UtilStrsav( (char *)pCur ); + else if ( *pCur == 't' ) + { + pCur++; + vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4; + memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) ); pCur += Vec_StrSize(vStr); + pNew->pManTime = Tim_ManLoad( vStr, 0 ); + Vec_StrFree( vStr ); + } + // read object classes + else if ( *pCur == 'v' ) + { + pCur++; + pNew->vObjClasses = Vec_IntStart( Gia_AigerReadInt(pCur)/4 ); pCur += 4; + memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) ); + pCur += 4*Vec_IntSize(pNew->vObjClasses); + } + else break; } } // skipping the comments 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; - } -*/ // update polarity of the additional outputs if ( nBad || nConstr || nJust || nFair ) @@ -1083,6 +674,15 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS pNew = Gia_ManDupUnnomalize( pTemp = pNew ); Gia_ManStop( pTemp ); } +/* + // check the result + if ( fCheck && !Gia_ManCheck( pNew ) ) + { + printf( "Gia_AigerRead: The network check has failed.\n" ); + Gia_ManStop( pNew ); + return NULL; + } +*/ return pNew; } @@ -1097,7 +697,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck ) +Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck ) { FILE * pFile; Gia_Man_t * pNew; @@ -1106,14 +706,14 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck ) int RetValue; // read the file into the buffer - Gia_FixFileName( pFileName ); + Gia_FileFixName( pFileName ); nFileSize = Gia_FileSize( pFileName ); pFile = fopen( pFileName, "rb" ); pContents = ABC_ALLOC( char, nFileSize ); RetValue = fread( pContents, nFileSize, 1, pFile ); fclose( pFile ); - pNew = Gia_ReadAigerFromMemory( pContents, nFileSize, fSkipStrash, fCheck ); + pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fSkipStrash, fCheck ); ABC_FREE( pContents ); if ( pNew ) { @@ -1132,237 +732,161 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck ) /**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 [Create the array of literals to be written.] + Synopsis [Writes the AIG in into the memory buffer.] - Description [] + Description [The resulting buffer constains the AIG in AIGER format. + The resulting buffer should be deallocated by the user.] SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_WriteAigerLiterals( Gia_Man_t * p ) +Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p ) { - Vec_Int_t * vLits; + Vec_Str_t * vBuffer; 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.] + int nNodes = 0, i, uLit, uLit0, uLit1; + // set the node numbers to be used in the output file + Gia_ManConst0(p)->Value = nNodes++; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = nNodes++; + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = nNodes++; - Description [] - - SideEffects [] + // write the header "M I L O A" where M = I + L + A + vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) ); + Vec_StrPrintStr( vBuffer, "aig " ); + Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) ); + Vec_StrPrintStr( vBuffer, " " ); + Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) ); + Vec_StrPrintStr( vBuffer, " " ); + Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) ); + Vec_StrPrintStr( vBuffer, " " ); + Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) ); + Vec_StrPrintStr( vBuffer, " " ); + Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) ); + Vec_StrPrintStr( vBuffer, "\n" ); - SeeAlso [] + // write latch drivers + Gia_ManForEachRi( p, pObj, i ) + { + uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); + Vec_StrPrintNum( vBuffer, uLit ); + Vec_StrPrintStr( vBuffer, "\n" ); + } -***********************************************************************/ -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 ) + // write PO drivers + Gia_ManForEachPo( p, pObj, i ) { - 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 ); + uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); + Vec_StrPrintNum( vBuffer, uLit ); + Vec_StrPrintStr( vBuffer, "\n" ); } - vBinary->nSize = Pos; -/* - // verify + // write the nodes into the buffer + Gia_ManForEachAnd( p, pObj, i ) { - 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++ ) + uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 ); + uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); + uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) ); + assert( uLit0 != uLit1 ); + if ( uLit0 > uLit1 ) { - int Entry1 = Vec_IntEntry(vLits,i); - int Entry2 = Vec_IntEntry(vTemp,i); - assert( Entry1 == Entry2 ); + int Temp = uLit0; + uLit0 = uLit1; + uLit1 = Temp; } - Vec_IntFree( vTemp ); + Gia_AigerWriteUnsigned( vBuffer, uLit - uLit1 ); + Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 ); } -*/ - return vBinary; + Vec_StrPrintStr( vBuffer, "c" ); + return vBuffer; } /**Function************************************************************* - Synopsis [Write integer into the string.] + Synopsis [Writes the AIG in into the memory buffer.] - Description [] + Description [The resulting buffer constains the AIG in AIGER format. + The CI/CO/AND nodes are assumed to be ordered according to some rule. + The resulting buffer should be deallocated by the user.] - SideEffects [] + SideEffects [Note that in vCos, PIs are order first, followed by latches!] SeeAlso [] ***********************************************************************/ -void Gia_WriteInt( unsigned char * pPos, int Value ) +Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs ) { - int i; - for ( i = 3; i >= 0; i-- ) - *pPos++ = (Value >> (8*i)) & 255; -} - -/**Function************************************************************* - - Synopsis [Read equivalence classes from the string.] - - Description [] - - SideEffects [] + Vec_Str_t * vBuffer; + Gia_Obj_t * pObj; + int nNodes = 0, i, uLit, uLit0, uLit1; + // set the node numbers to be used in the output file + Gia_ManConst0(p)->Value = nNodes++; + Gia_ManForEachObjVec( vCis, p, pObj, i ) + { + assert( Gia_ObjIsCi(pObj) ); + pObj->Value = nNodes++; + } + Gia_ManForEachObjVec( vAnds, p, pObj, i ) + { + assert( Gia_ObjIsAnd(pObj) ); + pObj->Value = nNodes++; + } - SeeAlso [] + // write the header "M I L O A" where M = I + L + A + vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) ); + Vec_StrPrintStr( vBuffer, "aig " ); + Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) + Vec_IntSize(vAnds) ); + Vec_StrPrintStr( vBuffer, " " ); + Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) - nRegs ); + Vec_StrPrintStr( vBuffer, " " ); + Vec_StrPrintNum( vBuffer, nRegs ); + Vec_StrPrintStr( vBuffer, " " ); + Vec_StrPrintNum( vBuffer, Vec_IntSize(vCos) - nRegs ); + Vec_StrPrintStr( vBuffer, " " ); + Vec_StrPrintNum( vBuffer, Vec_IntSize(vAnds) ); + Vec_StrPrintStr( vBuffer, "\n" ); -***********************************************************************/ -unsigned char * Gia_WriteEquivClasses( 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++ ) + // write latch drivers + Gia_ManForEachObjVec( vCos, p, pObj, i ) { - nItems += Gia_ObjIsConst( p, iRepr ); - if ( !Gia_ObjIsHead(p, iRepr) ) + assert( Gia_ObjIsCo(pObj) ); + if ( i < Vec_IntSize(vCos) - nRegs ) continue; - Gia_ClassForEachObj( p, iRepr, iNode ) - nItems++; + uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); + Vec_StrPrintNum( vBuffer, uLit ); + Vec_StrPrintStr( vBuffer, "\n" ); } - pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 10) ); - // write constant class - iPos = Gia_WriteAigerEncode( pBuffer, 4, Abc_Var2Lit(0, 1) ); -//printf( "\nRepr = %d ", 0 ); - iPrevNode = 0; - for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ ) - if ( Gia_ObjIsConst(p, iNode) ) - { -//printf( "Node = %d ", iNode ); - iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); - iPrevNode = iNode; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) ); - } - // write non-constant classes - iPrevRepr = 0; - Gia_ManForEachClass( p, iRepr ) + // write output drivers + Gia_ManForEachObjVec( vCos, p, pObj, i ) { -//printf( "\nRepr = %d ", iRepr ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) ); - iPrevRepr = iPrevNode = iRepr; - Gia_ClassForEachObj1( p, iRepr, iNode ) - { -//printf( "Node = %d ", iNode ); - iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); - iPrevNode = iNode; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) ); - } + assert( Gia_ObjIsCo(pObj) ); + if ( i >= Vec_IntSize(vCos) - nRegs ) + continue; + uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); + Vec_StrPrintNum( vBuffer, uLit ); + Vec_StrPrintStr( vBuffer, "\n" ); } - Gia_WriteInt( pBuffer, iPos ); - *pEquivSize = iPos; - return pBuffer; -} - -/**Function************************************************************* - - Synopsis [Reads decoded value.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_WriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis ) -{ - if ( iPrev < iThis ) - return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) ); - return Gia_WriteAigerEncode( pPos, iPos, Abc_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( unsigned char, sizeof(int) * (nItems + 1) ); - // write non-constant classes - iPrev = 0; - Gia_ManForEachLut( p, i ) + // write the nodes into the buffer + Gia_ManForEachObjVec( vAnds, p, pObj, i ) { -//printf( "\nSize = %d ", Gia_ObjLutSize(p, i) ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_ObjLutSize(p, i) ); - Gia_LutForEachFanin( p, i, iFan, k ) + uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 ); + uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); + uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) ); + assert( uLit0 != uLit1 ); + if ( uLit0 > uLit1 ) { -//printf( "Fan = %d ", iFan ); - iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, iFan ); - iPrev = iFan; + int Temp = uLit0; + uLit0 = uLit1; + uLit1 = Temp; } - iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, i ); - iPrev = i; -//printf( "Node = %d ", i ); + Gia_AigerWriteUnsigned( vBuffer, uLit - uLit1 ); + Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 ); } -//printf( "\n" ); - Gia_WriteInt( pBuffer, iPos ); - *pMapSize = iPos; - return pBuffer; + Vec_StrPrintStr( vBuffer, "c" ); + return vBuffer; } /**Function************************************************************* @@ -1376,11 +900,12 @@ unsigned char * Gia_WriteMapping( Gia_Man_t * p, int * pMapSize ) SeeAlso [] ***********************************************************************/ -void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact ) +void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact ) { FILE * pFile; Gia_Man_t * p; Gia_Obj_t * pObj; + Vec_Str_t * vStrExt; int i, nBufferSize, Pos; unsigned char * pBuffer; unsigned uLit0, uLit1, uLit; @@ -1395,14 +920,14 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { - fprintf( stdout, "Gia_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName ); + fprintf( stdout, "Gia_AigerWrite(): Cannot open the output file \"%s\".\n", pFileName ); return; } // create normalized AIG if ( !Gia_ManIsNormalized(pInit) ) { -// printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" ); +// printf( "Gia_AigerWrite(): Normalizing AIG for writing.\n" ); p = Gia_ManDupNormalize( pInit ); p->pManTime = pInit->pManTime; pInit->pManTime = NULL; p->vNamesIn = pInit->vNamesIn; pInit->vNamesIn = NULL; @@ -1436,8 +961,8 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int } else { - Vec_Int_t * vLits = Gia_WriteAigerLiterals( p ); - Vec_Str_t * vBinary = Gia_WriteEncodeLiterals( vLits ); + Vec_Int_t * vLits = Gia_AigerCollectLiterals( p ); + Vec_Str_t * vBinary = Gia_AigerWriteLiterals( vLits ); fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile ); Vec_StrFree( vBinary ); Vec_IntFree( vLits ); @@ -1454,11 +979,11 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int uLit0 = Gia_ObjFaninLit0( pObj, i ); uLit1 = Gia_ObjFaninLit1( pObj, i ); assert( p->nPinTypes || uLit0 < uLit1 ); - Pos = Gia_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 ); - Pos = Gia_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); + Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit - uLit1 ); + Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit1 - uLit0 ); if ( Pos > nBufferSize - 10 ) { - printf( "Gia_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" ); + printf( "Gia_AigerWrite(): AIGER generation has failed because the allocated buffer is too small.\n" ); fclose( pFile ); if ( p != pInit ) Gia_ManStop( p ); @@ -1489,99 +1014,130 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int // write the comment fprintf( pFile, "c" ); + + // write additional AIG + if ( p->pAigExtra ) + { + fprintf( pFile, "a" ); + vStrExt = Gia_AigerWriteIntoMemoryStr( p->pAigExtra ); + Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); + fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); + Vec_StrFree( vStrExt ); + } +/* + // write constraints + if ( p->nConstrs ) + { + fprintf( pFile, "c" ); + Gia_FileWriteBufferSize( pFile, 4 ); + Gia_FileWriteBufferSize( pFile, p->nConstrs ); + } +*/ + // write gate classes + if ( p->vInArrs && p->vOutReqs ) + { + fprintf( pFile, "d" ); + Gia_FileWriteBufferSize( pFile, 4*(Gia_ManPiNum(p) + Gia_ManPoNum(p)) ); + assert( Vec_FltSize(p->vInArrs) == Gia_ManPiNum(p) ); + assert( Vec_FltSize(p->vOutReqs) == Gia_ManPoNum(p) ); + fwrite( Vec_FltArray(p->vInArrs), 1, 4*Gia_ManPiNum(p), pFile ); + fwrite( Vec_FltArray(p->vOutReqs), 1, 4*Gia_ManPoNum(p), pFile ); + } // write equivalences if ( p->pReprs && p->pNexts ) { - int nEquivSize; - unsigned char * pEquivs = Gia_WriteEquivClasses( p, &nEquivSize ); + extern Vec_Str_t * Gia_WriteEquivClasses( Gia_Man_t * p ); fprintf( pFile, "e" ); - fwrite( pEquivs, 1, nEquivSize, pFile ); - ABC_FREE( pEquivs ); + vStrExt = Gia_WriteEquivClasses( p ); +// Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); + fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); + Vec_StrFree( vStrExt ); } // write flop classes if ( p->vFlopClasses ) { - unsigned char Buffer[10]; - int nSize = 4*Gia_ManRegNum(p); - Gia_WriteInt( Buffer, nSize ); fprintf( pFile, "f" ); - fwrite( Buffer, 1, 4, pFile ); - fwrite( Vec_IntArray(p->vFlopClasses), 1, nSize, pFile ); + Gia_FileWriteBufferSize( pFile, 4*Gia_ManRegNum(p) ); + assert( Vec_IntSize(p->vFlopClasses) == Gia_ManRegNum(p) ); + fwrite( Vec_IntArray(p->vFlopClasses), 1, 4*Gia_ManRegNum(p), pFile ); } // write gate classes if ( p->vGateClasses ) { - unsigned char Buffer[10]; - int nSize = 4*Gia_ManObjNum(p); - Gia_WriteInt( Buffer, nSize ); fprintf( pFile, "g" ); - fwrite( Buffer, 1, 4, pFile ); - fwrite( Vec_IntArray(p->vGateClasses), 1, nSize, pFile ); + Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) ); + assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) ); + fwrite( Vec_IntArray(p->vGateClasses), 1, 4*Gia_ManObjNum(p), pFile ); } - // write object classes - if ( p->vObjClasses ) + // write hierarchy info + if ( p->pManTime ) { - unsigned char Buffer[10]; - int nSize = 4*Vec_IntSize(p->vObjClasses); - Gia_WriteInt( Buffer, nSize ); - fprintf( pFile, "v" ); - fwrite( Buffer, 1, 4, pFile ); - fwrite( Vec_IntArray(p->vObjClasses), 1, nSize, pFile ); + fprintf( pFile, "h" ); + vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 1 ); + Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); + fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); + Vec_StrFree( vStrExt ); + } + // write packing + if ( p->vPacking ) + { + extern Vec_Str_t * Gia_WritePacking( Vec_Int_t * vPacking ); + fprintf( pFile, "k" ); + vStrExt = Gia_WritePacking( p->vPacking ); + Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); + fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); + Vec_StrFree( vStrExt ); } // write mapping if ( p->pMapping ) { - int nMapSize; - unsigned char * pMaps = Gia_WriteMapping( p, &nMapSize ); + extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p ); fprintf( pFile, "m" ); - fwrite( pMaps, 1, nMapSize, pFile ); - ABC_FREE( pMaps ); + vStrExt = Gia_AigerWriteMapping( p ); + Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); + fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); + Vec_StrFree( vStrExt ); + } + // write name + if ( p->pName ) + { + fprintf( pFile, "n" ); + Gia_FileWriteBufferSize( pFile, strlen(p->pName)+1 ); + fwrite( p->pName, 1, strlen(p->pName), pFile ); + fprintf( pFile, "\0" ); } // write placement if ( p->pPlacement ) { - unsigned char Buffer[10]; - int nSize = 4*Gia_ManObjNum(p); - Gia_WriteInt( Buffer, nSize ); fprintf( pFile, "p" ); - fwrite( Buffer, 1, 4, pFile ); - fwrite( p->pPlacement, 1, nSize, pFile ); + Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) ); + fwrite( p->pPlacement, 1, 4*Gia_ManObjNum(p), pFile ); } // write switching activity if ( p->pSwitching ) { - unsigned char Buffer[10]; - int nSize = Gia_ManObjNum(p); - Gia_WriteInt( Buffer, nSize ); fprintf( pFile, "s" ); - fwrite( Buffer, 1, 4, pFile ); - fwrite( p->pSwitching, 1, nSize, pFile ); + Gia_FileWriteBufferSize( pFile, Gia_ManObjNum(p) ); + fwrite( p->pSwitching, 1, Gia_ManObjNum(p), pFile ); } // write timing information if ( p->pManTime ) { - Vec_Str_t * vStr = Tim_ManSave( (Tim_Man_t *)p->pManTime ); - unsigned char Buffer[10]; - int nSize = Vec_StrSize(vStr); - Gia_WriteInt( Buffer, nSize ); fprintf( pFile, "t" ); - fwrite( Buffer, 1, 4, pFile ); - fwrite( Vec_StrArray(vStr), 1, nSize, pFile ); - Vec_StrFree( vStr ); + vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 0 ); + Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); + fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); + Vec_StrFree( vStrExt ); } -/* - // write constraints - if ( p->nConstrs ) + // write object classes + if ( p->vObjClasses ) { - unsigned char Buffer[10]; - Gia_WriteInt( Buffer, p->nConstrs ); - fprintf( pFile, "c" ); - fwrite( Buffer, 1, 4, pFile ); + fprintf( pFile, "v" ); + Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) ); + assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) ); + fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile ); } -*/ - // write name - if ( p->pName ) - fprintf( pFile, "n%s%c", p->pName, '\0' ); + // write comments 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 ); @@ -1609,195 +1165,7 @@ void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNu { char Buffer[100]; sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum ); - Gia_WriteAiger( p, Buffer, 0, 0 ); -} - -/**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 [] - -***********************************************************************/ -void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x ) -{ - unsigned char ch; - while (x & ~0x7f) - { - ch = (x & 0x7f) | 0x80; -// putc (ch, file); -// pBuffer[Pos++] = ch; - Vec_StrPush( vStr, ch ); - x >>= 7; - } - ch = x; -// putc (ch, file); -// pBuffer[Pos++] = ch; - Vec_StrPush( vStr, ch ); -} - -/**Function************************************************************* - - Synopsis [Writes the AIG in into the memory buffer.] - - Description [The resulting buffer constains the AIG in AIGER format. - The resulting buffer should be deallocated by the user.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p ) -{ - Vec_Str_t * vBuffer; - Gia_Obj_t * pObj; - int nNodes = 0, i, uLit, uLit0, uLit1; - // set the node numbers to be used in the output file - Gia_ManConst0(p)->Value = nNodes++; - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = nNodes++; - Gia_ManForEachAnd( p, pObj, i ) - pObj->Value = nNodes++; - - // write the header "M I L O A" where M = I + L + A - vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) ); - Vec_StrPrintStr( vBuffer, "aig " ); - Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) ); - Vec_StrPrintStr( vBuffer, "\n" ); - - // write latch drivers - Gia_ManForEachRi( p, pObj, i ) - { - uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - Vec_StrPrintNum( vBuffer, uLit ); - Vec_StrPrintStr( vBuffer, "\n" ); - } - - // write PO drivers - Gia_ManForEachPo( p, pObj, i ) - { - uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - Vec_StrPrintNum( vBuffer, uLit ); - Vec_StrPrintStr( vBuffer, "\n" ); - } - // write the nodes into the buffer - Gia_ManForEachAnd( p, pObj, i ) - { - uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 ); - uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) ); - assert( uLit0 != uLit1 ); - if ( uLit0 > uLit1 ) - { - int Temp = uLit0; - uLit0 = uLit1; - uLit1 = Temp; - } - Gia_WriteAigerEncodeStr( vBuffer, uLit - uLit1 ); - Gia_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 ); - } - Vec_StrPrintStr( vBuffer, "c" ); - return vBuffer; -} - -/**Function************************************************************* - - Synopsis [Writes the AIG in into the memory buffer.] - - Description [The resulting buffer constains the AIG in AIGER format. - The CI/CO/AND nodes are assumed to be ordered according to some rule. - The resulting buffer should be deallocated by the user.] - - SideEffects [Note that in vCos, PIs are order first, followed by latches!] - - SeeAlso [] - -***********************************************************************/ -Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs ) -{ - Vec_Str_t * vBuffer; - Gia_Obj_t * pObj; - int nNodes = 0, i, uLit, uLit0, uLit1; - // set the node numbers to be used in the output file - Gia_ManConst0(p)->Value = nNodes++; - Gia_ManForEachObjVec( vCis, p, pObj, i ) - { - assert( Gia_ObjIsCi(pObj) ); - pObj->Value = nNodes++; - } - Gia_ManForEachObjVec( vAnds, p, pObj, i ) - { - assert( Gia_ObjIsAnd(pObj) ); - pObj->Value = nNodes++; - } - - // write the header "M I L O A" where M = I + L + A - vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) ); - Vec_StrPrintStr( vBuffer, "aig " ); - Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) + Vec_IntSize(vAnds) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) - nRegs ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, nRegs ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Vec_IntSize(vCos) - nRegs ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Vec_IntSize(vAnds) ); - Vec_StrPrintStr( vBuffer, "\n" ); - - // write latch drivers - Gia_ManForEachObjVec( vCos, p, pObj, i ) - { - assert( Gia_ObjIsCo(pObj) ); - if ( i < Vec_IntSize(vCos) - nRegs ) - continue; - uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - Vec_StrPrintNum( vBuffer, uLit ); - Vec_StrPrintStr( vBuffer, "\n" ); - } - // write output drivers - Gia_ManForEachObjVec( vCos, p, pObj, i ) - { - assert( Gia_ObjIsCo(pObj) ); - if ( i >= Vec_IntSize(vCos) - nRegs ) - continue; - uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - Vec_StrPrintNum( vBuffer, uLit ); - Vec_StrPrintStr( vBuffer, "\n" ); - } - - // write the nodes into the buffer - Gia_ManForEachObjVec( vAnds, p, pObj, i ) - { - uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 ); - uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) ); - assert( uLit0 != uLit1 ); - if ( uLit0 > uLit1 ) - { - int Temp = uLit0; - uLit0 = uLit1; - uLit1 = Temp; - } - Gia_WriteAigerEncodeStr( vBuffer, uLit - uLit1 ); - Gia_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 ); - } - Vec_StrPrintStr( vBuffer, "c" ); - return vBuffer; + Gia_AigerWrite( p, Buffer, 0, 0 ); } /**Function************************************************************* @@ -1811,24 +1179,24 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve SeeAlso [] ***********************************************************************/ -void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName ) +void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName ) { FILE * pFile; Vec_Str_t * vStr; if ( Gia_ManPoNum(pInit) == 0 ) { - printf( "Gia_WriteAigerSimple(): AIG cannot be written because it has no POs.\n" ); + printf( "Gia_AigerWriteSimple(): 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_WriteAigerSimple(): Cannot open the output file \"%s\".\n", pFileName ); + fprintf( stdout, "Gia_AigerWriteSimple(): Cannot open the output file \"%s\".\n", pFileName ); return; } // write the buffer - vStr = Gia_WriteAigerIntoMemoryStr( pInit ); + vStr = Gia_AigerWriteIntoMemoryStr( pInit ); fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile ); Vec_StrFree( vStr ); fclose( pFile ); diff --git a/src/aig/gia/giaAigerExt.c b/src/aig/gia/giaAigerExt.c new file mode 100644 index 00000000..fa79e589 --- /dev/null +++ b/src/aig/gia/giaAigerExt.c @@ -0,0 +1,240 @@ +/**CFile**************************************************************** + + FileName [giaAigerExt.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Custom AIGER extensions.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAigerExt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Read/write equivalence classes information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize ) +{ + Gia_Rpr_t * pReprs; + unsigned char * pStop; + int i, Item, fProved, iRepr, iNode; + pStop = *ppPos; + pStop += Gia_AigerReadInt( *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_AigerReadUnsigned( ppPos ); + if ( Item & 1 ) + { + iRepr += (Item >> 1); + iNode = iRepr; + continue; + } + Item >>= 1; + fProved = (Item & 1); + Item >>= 1; + iNode += Item; + pReprs[iNode].fProved = fProved; + pReprs[iNode].iRepr = iRepr; + assert( iRepr < iNode ); + } + return pReprs; +} +unsigned char * Gia_WriteEquivClassesInt( 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( unsigned char, sizeof(int) * (nItems + 10) ); + // write constant class + iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, 4, Abc_Var2Lit(0, 1) ); + iPrevNode = 0; + for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ ) + if ( Gia_ObjIsConst(p, iNode) ) + { + iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); + iPrevNode = iNode; + iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iLit, 0) ); + } + // write non-constant classes + iPrevRepr = 0; + Gia_ManForEachClass( p, iRepr ) + { + iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) ); + iPrevRepr = iPrevNode = iRepr; + Gia_ClassForEachObj1( p, iRepr, iNode ) + { + iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); + iPrevNode = iNode; + iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iLit, 0) ); + } + } + Gia_AigerWriteInt( pBuffer, iPos ); + *pEquivSize = iPos; + return pBuffer; +} +Vec_Str_t * Gia_WriteEquivClasses( Gia_Man_t * p ) +{ + int nEquivSize; + unsigned char * pBuffer = Gia_WriteEquivClassesInt( p, &nEquivSize ); + return Vec_StrAllocArray( pBuffer, nEquivSize ); +} + +/**Function************************************************************* + + Synopsis [Read/write mapping information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Gia_AigerReadDiffValue( unsigned char ** ppPos, int iPrev ) +{ + int Item = Gia_AigerReadUnsigned( ppPos ); + if ( Item & 1 ) + return iPrev + (Item >> 1); + return iPrev - (Item >> 1); +} +int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize ) +{ + int * pMapping; + unsigned char * pStop; + int k, j, nFanins, nAlloc, iNode = 0, iOffset = nSize; + pStop = *ppPos; + pStop += Gia_AigerReadInt( *ppPos ); *ppPos += 4; + nAlloc = nSize + pStop - *ppPos; + pMapping = ABC_CALLOC( int, nAlloc ); + while ( *ppPos < pStop ) + { + k = iOffset; + pMapping[k++] = nFanins = Gia_AigerReadUnsigned( ppPos ); + for ( j = 0; j <= nFanins; j++ ) + pMapping[k++] = iNode = Gia_AigerReadDiffValue( ppPos, iNode ); + pMapping[iNode] = iOffset; + iOffset = k; + } + assert( iOffset <= nAlloc ); + return pMapping; +} +static inline int Gia_AigerWriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis ) +{ + if ( iPrev < iThis ) + return Gia_AigerWriteUnsignedBuffer( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) ); + return Gia_AigerWriteUnsignedBuffer( pPos, iPos, Abc_Var2Lit(iPrev - iThis, 0) ); +} +unsigned char * Gia_AigerWriteMappingInt( 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( unsigned char, sizeof(int) * (nItems + 1) ); + // write non-constant classes + iPrev = 0; + Gia_ManForEachLut( p, i ) + { +//printf( "\nSize = %d ", Gia_ObjLutSize(p, i) ); + iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Gia_ObjLutSize(p, i) ); + Gia_LutForEachFanin( p, i, iFan, k ) + { +//printf( "Fan = %d ", iFan ); + iPos = Gia_AigerWriteDiffValue( pBuffer, iPos, iPrev, iFan ); + iPrev = iFan; + } + iPos = Gia_AigerWriteDiffValue( pBuffer, iPos, iPrev, i ); + iPrev = i; +//printf( "Node = %d ", i ); + } +//printf( "\n" ); + Gia_AigerWriteInt( pBuffer, iPos ); + *pMapSize = iPos; + return pBuffer; +} +Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p ) +{ + int nMapSize; + unsigned char * pBuffer = Gia_AigerWriteMappingInt( p, &nMapSize ); + return Vec_StrAllocArray( pBuffer, nMapSize ); +} + +/**Function************************************************************* + + Synopsis [Read/write packing information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize ) +{ + Vec_Int_t * vPacking = Vec_IntStart( nSize/4 ); + assert( nSize % 4 == 0 ); + memcpy( Vec_IntArray(vPacking), *ppPos, nSize ); + *ppPos += nSize; + return vPacking; +} +Vec_Str_t * Gia_WritePacking( Vec_Int_t * vPacking ) +{ + Vec_Str_t * vBuffer = Vec_StrStart( 4*Vec_IntSize(vPacking) ); + memcpy( Vec_StrArray(vBuffer), Vec_IntArray(vPacking), 4*sizeof(int) ); + return vBuffer; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index d8545cd5..5ddd9b08 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1203,7 +1203,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb return; } // read AIGER file - pMiter = Gia_ReadAiger( pFileName, 0, 0 ); + pMiter = Gia_AigerRead( pFileName, 0, 0 ); if ( pMiter == NULL ) { Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName ); @@ -1722,14 +1722,14 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f } } // write equivalence classes - Gia_WriteAiger( pGia, "gore.aig", 0, 0 ); + Gia_AigerWrite( pGia, "gore.aig", 0, 0 ); // reduce the model pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 ); if ( pReduce ) { pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); Gia_ManStop( pAux ); - Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 ); + Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 ); // Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" ); // Gia_ManPrintStatsShort( pReduce ); Gia_ManStop( pReduce ); @@ -1762,13 +1762,13 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p Abc_Print( 1, "Equivalences are not defined.\n" ); return 0; } - pGia1 = Gia_ReadAiger( pName1, 0, 0 ); + pGia1 = Gia_AigerRead( pName1, 0, 0 ); if ( pGia1 == NULL ) { Abc_Print( 1, "Cannot read first file %s.\n", pName1 ); return 0; } - pGia2 = Gia_ReadAiger( pName2, 0, 0 ); + pGia2 = Gia_AigerRead( pName2, 0, 0 ); if ( pGia2 == NULL ) { Gia_ManStop( pGia2 ); @@ -1901,13 +1901,13 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName Abc_Print( 1, "Equivalences are not defined.\n" ); return 0; } - pGia1 = Gia_ReadAiger( pName1, 0, 0 ); + pGia1 = Gia_AigerRead( pName1, 0, 0 ); if ( pGia1 == NULL ) { Abc_Print( 1, "Cannot read first file %s.\n", pName1 ); return 0; } - pGia2 = Gia_ReadAiger( pName2, 0, 0 ); + pGia2 = Gia_AigerRead( pName2, 0, 0 ); if ( pGia2 == NULL ) { Gia_ManStop( pGia2 ); diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c index 6bf86523..11f81e0a 100644 --- a/src/aig/gia/giaHcd.c +++ b/src/aig/gia/giaHcd.c @@ -626,7 +626,7 @@ Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis, Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i ) Gia_ManStop( pGia ); - Gia_WriteAiger( pMiter, "m3.aig", 0, 0 ); + Gia_AigerWrite( pMiter, "m3.aig", 0, 0 ); } else { diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c index 088649ea..eab828db 100644 --- a/src/aig/gia/giaIso.c +++ b/src/aig/gia/giaIso.c @@ -1043,7 +1043,7 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_ { assert( Gia_ManPoNum(pPart) == 1 ); assert( Gia_ManObjNum(pPart) == 2 ); - vStr = Gia_WriteAigerIntoMemoryStr( pPart ); + vStr = Gia_AigerWriteIntoMemoryStr( pPart ); Gia_ManStop( pPart ); if ( pvPiPerm ) *pvPiPerm = Vec_IntAlloc( 0 ); @@ -1060,7 +1060,7 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_ //printf( "Internal: " ); //Vec_IntPrint( vCis ); // derive the AIGER string - vStr = Gia_WriteAigerIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) ); + vStr = Gia_AigerWriteIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) ); // cleanup Vec_IntFree( vCis ); Vec_IntFree( vAnds ); @@ -1280,7 +1280,7 @@ void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ) // create AIG with two primary outputs (original and permuted) pPerm = Gia_ManDupPerm( p, vPiPerm ); pDouble = Gia_ManDupAppendNew( p, pPerm ); -//Gia_WriteAiger( pDouble, "test.aig", 0, 0 ); +//Gia_AigerWrite( pDouble, "test.aig", 0, 0 ); // analyze the two-output miter pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0 ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 8e1bc7e2..1bc6398a 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -94,6 +94,10 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_WrdFreeP( &p->vTtMemory ); Vec_PtrFreeP( &p->vTtInputs ); Vec_IntFreeP( &p->vMapping ); + Vec_IntFreeP( &p->vPacking ); + Vec_FltFreeP( &p->vInArrs ); + Vec_FltFreeP( &p->vOutReqs ); + Gia_ManStopP( &p->pAigExtra ); Vec_IntFree( p->vCis ); Vec_IntFree( p->vCos ); ABC_FREE( p->pData2 ); @@ -161,10 +165,10 @@ void Gia_ManPrintClasses_old( Gia_Man_t * p ) { Gia_Man_t * pTemp; pTemp = Gia_ManDupFlopClass( p, 1 ); - Gia_WriteAiger( pTemp, "dom1.aig", 0, 0 ); + Gia_AigerWrite( pTemp, "dom1.aig", 0, 0 ); Gia_ManStop( pTemp ); pTemp = Gia_ManDupFlopClass( p, 2 ); - Gia_WriteAiger( pTemp, "dom2.aig", 0, 0 ); + Gia_AigerWrite( pTemp, "dom2.aig", 0, 0 ); Gia_ManStop( pTemp ); } } diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 49644fa8..c5cfd930 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -1,6 +1,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAig.c \ src/aig/gia/giaAiger.c \ + src/aig/gia/giaAigerExt.c \ src/aig/gia/giaBidec.c \ src/aig/gia/giaCCof.c \ src/aig/gia/giaCex.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c65ee1bc..651b70ec 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -12840,7 +12840,7 @@ int Abc_CommandRecStart2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - pGia = Gia_ReadAiger( FileName, 1, 0 ); + pGia = Gia_AigerRead( FileName, 1, 0 ); if ( pGia == NULL ) { Abc_Print( -1, "Reading AIGER has failed.\n" ); @@ -13059,7 +13059,7 @@ int Abc_CommandRecDump2( Abc_Frame_t * pAbc, int argc, char ** argv ) { // get the input file name FileName = pArgvNew[0]; - Gia_WriteAiger( pGia, FileName, 0, 0 ); + Gia_AigerWrite( pGia, FileName, 0, 0 ); } return 0; @@ -13188,7 +13188,7 @@ int Abc_CommandRecMerge2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - pGia = Gia_ReadAiger( FileName, 0, 0 ); + pGia = Gia_AigerRead( FileName, 0, 0 ); if ( pGia == NULL ) { Abc_Print( -1, "Reading AIGER has failed.\n" ); @@ -13299,7 +13299,7 @@ int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - pGia = Gia_ReadAiger( FileName, 1, 0 ); + pGia = Gia_AigerRead( FileName, 1, 0 ); if ( pGia == NULL ) { Abc_Print( -1, "Reading AIGER has failed.\n" ); @@ -13531,7 +13531,7 @@ int Abc_CommandRecDump3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 0, "No structure in the library.\n" ); return 1; } - Gia_WriteAiger( pGia, FileName, 0, 0 ); + Gia_AigerWrite( pGia, FileName, 0, 0 ); } return 0; @@ -13605,7 +13605,7 @@ int Abc_CommandRecMerge3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - pGia = Gia_ReadAiger( FileName, 1, 0 ); + pGia = Gia_AigerRead( FileName, 1, 0 ); if ( pGia == NULL ) { Abc_Print( -1, "Reading AIGER has failed.\n" ); @@ -23444,7 +23444,7 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv ) } fclose( pFile ); - pAig = Gia_ReadAiger( FileName, fSkipStrash, 0 ); + pAig = Gia_AigerRead( FileName, fSkipStrash, 0 ); Abc_CommandUpdate9( pAbc, pAig ); return 0; @@ -23830,11 +23830,11 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fUnique ) { Gia_Man_t * pGia = Gia_ManIsoCanonicize( pAbc->pGia, fVerbose ); - Gia_WriteAigerSimple( pGia, pFileName ); + Gia_AigerWriteSimple( pGia, pFileName ); Gia_ManStop( pGia ); } else - Gia_WriteAiger( pAbc->pGia, pFileName, 0, 0 ); + Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 ); return 0; usage: @@ -25942,7 +25942,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - pSecond = Gia_ReadAiger( FileName, 0, 0 ); + pSecond = Gia_AigerRead( FileName, 0, 0 ); if ( pSecond == NULL ) { Abc_Print( -1, "Reading AIGER has failed.\n" ); @@ -26024,7 +26024,7 @@ int Abc_CommandAbc9Append( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - pSecond = Gia_ReadAiger( FileName, 0, 0 ); + pSecond = Gia_AigerRead( FileName, 0, 0 ); if ( pSecond == NULL ) { Abc_Print( -1, "Reading AIGER has failed.\n" ); @@ -26689,7 +26689,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 ); Gia_ManStop( pAux ); } - Gia_WriteAiger( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0 ); + Gia_AigerWrite( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0 ); Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName ); Gia_ManPrintStatsShort( pTemp ); Gia_ManStop( pTemp ); @@ -26702,7 +26702,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 ); Gia_ManStop( pAux ); - Gia_WriteAiger( pTemp, pFileName2, 0, 0 ); + Gia_AigerWrite( pTemp, pFileName2, 0, 0 ); Abc_Print( 1, "Reduced original network was written into file \"%s\".\n", pFileName2 ); Gia_ManPrintStatsShort( pTemp ); Gia_ManStop( pTemp ); @@ -26803,7 +26803,7 @@ int Abc_CommandAbc9Srm2( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 ); Gia_ManStop( pAux ); - Gia_WriteAiger( pTemp, pFileName, 0, 0 ); + Gia_AigerWrite( pTemp, pFileName, 0, 0 ); Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName ); Gia_ManPrintStatsShort( pTemp ); Gia_ManStop( pTemp ); @@ -27122,7 +27122,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - pSecond = Gia_ReadAiger( FileName, 0, 0 ); + pSecond = Gia_AigerRead( FileName, 0, 0 ); if ( pSecond == NULL ) { Abc_Print( -1, "Reading AIGER has failed.\n" ); diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c index b359f312..385ec520 100644 --- a/src/base/abci/abcRec2.c +++ b/src/base/abci/abcRec2.c @@ -581,7 +581,7 @@ void Abc_NtkRecFilter2(int nLimit) // remove dangling nodes and POs driven by constants newPGia = Abc_NtkDupWithoutDangling2(pGia); sprintf( fileName, "RecLib%d_Filtered%d.aig", p->nVars, nLimit); - Gia_WriteAiger( newPGia, fileName, 0, 0 ); + Gia_AigerWrite( newPGia, fileName, 0, 0 ); Abc_Print(1, "Library %s was written.", fileName); //Gia_ManHashStop(newPGia); Gia_ManStop(newPGia); diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c index 1544e1e2..41406ce4 100644 --- a/src/base/abci/abcTim.c +++ b/src/base/abci/abcTim.c @@ -223,7 +223,7 @@ void Abc_NtkTestPinGia( Abc_Ntk_t * pNtk, int fWhiteBoxOnly, int fVerbose ) Gia_Man_t * pGia; char * pFileName = "testpin.aig"; pGia = Abc_NtkTestPinDeriveGia( pNtk, fWhiteBoxOnly, fVerbose ); - Gia_WriteAiger( pGia, pFileName, 0, 0 ); + Gia_AigerWrite( pGia, pFileName, 0, 0 ); Gia_ManStop( pGia ); printf( "AIG with pins derived from mapped network \"%s\" was written into file \"%s\".\n", Abc_NtkName(pNtk), pFileName ); @@ -426,13 +426,13 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName ) Gia_ManReverseClasses( pGia, 0 ); } // write file - Gia_WriteAiger( pGia, pFileName, 0, 0 ); + Gia_AigerWrite( pGia, pFileName, 0, 0 ); // unnormalize choices if ( Gia_ManWithChoices(pGia) ) Gia_ManReverseClasses( pGia, 1 ); // read file - pGia2 = Gia_ReadAiger( pFileName, 1, 1 ); + pGia2 = Gia_AigerRead( pFileName, 1, 1 ); // normalize choices if ( Gia_ManWithChoices(pGia2) ) diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c index b89238fc..2aa95e85 100644 --- a/src/base/cmd/cmdPlugin.c +++ b/src/base/cmd/cmdPlugin.c @@ -391,7 +391,7 @@ Gia_Man_t * Abc_ManReadAig( char * pFileName, char * pToken ) fclose( pFile ); } // derive AIG - pGia = Gia_ReadAigerFromMemory( pStr, nBinaryPart, 0, 0 ); + pGia = Gia_AigerReadFromMemory( pStr, nBinaryPart, 0, 0 ); } Vec_StrFree( vStr ); return pGia; @@ -513,7 +513,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv ) } // create input file - Gia_WriteAiger( pAbc->pGia, pFileIn, 0, 0 ); + Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0 ); // create command line vCommand = Vec_StrAlloc( 100 ); diff --git a/src/misc/tim/tim.h b/src/misc/tim/tim.h index b2009ec0..5fda0e59 100644 --- a/src/misc/tim/tim.h +++ b/src/misc/tim/tim.h @@ -122,8 +122,8 @@ extern float * Tim_ManBoxDelayTable( Tim_Man_t * p, int iBox ); extern int Tim_ManBoxCopy( Tim_Man_t * p, int iBox ); extern void Tim_ManBoxSetCopy( Tim_Man_t * p, int iBox, int iCopy ); /*=== timDump.c ===========================================================*/ -extern Vec_Str_t * Tim_ManSave( Tim_Man_t * p ); -extern Tim_Man_t * Tim_ManLoad( Vec_Str_t * p ); +extern Vec_Str_t * Tim_ManSave( Tim_Man_t * p, int fHieOnly ); +extern Tim_Man_t * Tim_ManLoad( Vec_Str_t * p, int fHieOnly ); /*=== timMan.c ===========================================================*/ extern Tim_Man_t * Tim_ManStart( int nCis, int nCos ); extern Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay ); diff --git a/src/misc/tim/timDump.c b/src/misc/tim/timDump.c index c7fb8861..1cda07b9 100644 --- a/src/misc/tim/timDump.c +++ b/src/misc/tim/timDump.c @@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Vec_Str_t * Tim_ManSave( Tim_Man_t * p ) +Vec_Str_t * Tim_ManSave( Tim_Man_t * p, int fHieOnly ) { Tim_Box_t * pBox; Tim_Obj_t * pObj; @@ -71,6 +71,8 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p ) Vec_StrPutI_ne( vStr, Tim_ManBoxDelayTableId(p, pBox->iBox) ); // can be -1 if delay table is not given Vec_StrPutI_ne( vStr, Tim_ManBoxCopy(p, pBox->iBox) ); // can be -1 if the copy is node defined } + if ( fHieOnly ) + return vStr; // save the number of delay tables Vec_StrPutI_ne( vStr, Tim_ManDelayTableNum(p) ); // save the delay tables @@ -107,7 +109,7 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p ) SeeAlso [] ***********************************************************************/ -Tim_Man_t * Tim_ManLoad( Vec_Str_t * p ) +Tim_Man_t * Tim_ManLoad( Vec_Str_t * p, int fHieOnly ) { Tim_Man_t * pMan; Tim_Obj_t * pObj; @@ -149,6 +151,8 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p ) curPo += nPos; assert( curPi == nCis ); assert( curPo == nCos ); + if ( fHieOnly ) + return pMan; // create delay tables nTables = Vec_StrGetI_ne( p, &iStr ); assert( pMan->vDelayTables == NULL ); diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c index 34c22da0..493047f7 100644 --- a/src/misc/util/utilBridge.c +++ b/src/misc/util/utilBridge.c @@ -41,11 +41,6 @@ ABC_NAMESPACE_IMPL_START #define BRIDGE_VALUE_0 2 #define BRIDGE_VALUE_1 3 -extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x ); - -extern unsigned Gia_ReadAigerDecode( unsigned char ** ppPos ); -extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -79,9 +74,9 @@ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p ) // write header vStr = Vec_StrAlloc( 1000 ); - Gia_WriteAigerEncodeStr( vStr, Gia_ManPiNum(p) ); - Gia_WriteAigerEncodeStr( vStr, Gia_ManRegNum(p) ); - Gia_WriteAigerEncodeStr( vStr, Gia_ManAndNum(p) ); + Gia_AigerWriteUnsigned( vStr, Gia_ManPiNum(p) ); + Gia_AigerWriteUnsigned( vStr, Gia_ManRegNum(p) ); + Gia_AigerWriteUnsigned( vStr, Gia_ManAndNum(p) ); // write the nodes Gia_ManForEachAnd( p, pObj, i ) @@ -89,24 +84,24 @@ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p ) uLit0 = Gia_ObjFanin0Copy( pObj ); uLit1 = Gia_ObjFanin1Copy( pObj ); assert( uLit0 != uLit1 ); - Gia_WriteAigerEncodeStr( vStr, uLit0 << 1 ); - Gia_WriteAigerEncodeStr( vStr, uLit1 ); + Gia_AigerWriteUnsigned( vStr, uLit0 << 1 ); + Gia_AigerWriteUnsigned( vStr, uLit1 ); } // write latch drivers Gia_ManForEachRi( p, pObj, i ) { uLit0 = Gia_ObjFanin0Copy( pObj ); - Gia_WriteAigerEncodeStr( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 ); + Gia_AigerWriteUnsigned( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 ); } // write PO drivers - Gia_WriteAigerEncodeStr( vStr, Gia_ManPoNum(p) ); + Gia_AigerWriteUnsigned( vStr, Gia_ManPoNum(p) ); Gia_ManForEachPo( p, pObj, i ) { uLit0 = Gia_ObjFanin0Copy( pObj ); // complement property output!!! - Gia_WriteAigerEncodeStr( vStr, Abc_LitNot(uLit0) ); + Gia_AigerWriteUnsigned( vStr, Abc_LitNot(uLit0) ); } return vStr; } @@ -209,20 +204,20 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex ) Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding) Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding) Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding) - Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // depth + Gia_AigerWriteUnsigned( vStr, pCex->iFrame ); // depth - Gia_WriteAigerEncodeStr( vStr, 1 ); // concrete - Gia_WriteAigerEncodeStr( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth) + Gia_AigerWriteUnsigned( vStr, 1 ); // concrete + Gia_AigerWriteUnsigned( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth) iBit = pCex->nRegs; for ( f = 0; f <= pCex->iFrame; f++ ) { - Gia_WriteAigerEncodeStr( vStr, pCex->nPis ); // num of inputs + Gia_AigerWriteUnsigned( vStr, pCex->nPis ); // num of inputs for ( i = 0; i < pCex->nPis; i++, iBit++ ) Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit) ? BRIDGE_VALUE_1:BRIDGE_VALUE_0) ); // value } assert( iBit == pCex->nBits ); Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example) - Gia_WriteAigerEncodeStr( vStr, pCex->nRegs ); // num of flops + Gia_AigerWriteUnsigned( vStr, pCex->nRegs ); // num of flops for ( i = 0; i < pCex->nRegs; i++ ) Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!! // RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile ); @@ -264,9 +259,9 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I int i, nInputs, nFlops, nGates, nProps; unsigned iFan0, iFan1; - nInputs = Gia_ReadAigerDecode( &pBuffer ); - nFlops = Gia_ReadAigerDecode( &pBuffer ); - nGates = Gia_ReadAigerDecode( &pBuffer ); + nInputs = Gia_AigerReadUnsigned( &pBuffer ); + nFlops = Gia_AigerReadUnsigned( &pBuffer ); + nGates = Gia_AigerReadUnsigned( &pBuffer ); vLits = Vec_IntAlloc( 1000 ); Vec_IntPush( vLits, -999 ); @@ -289,8 +284,8 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I Gia_ManHashAlloc( p ); for ( i = 0; i < nGates; i++ ) { - iFan0 = Gia_ReadAigerDecode( &pBuffer ); - iFan1 = Gia_ReadAigerDecode( &pBuffer ); + iFan0 = Gia_AigerReadUnsigned( &pBuffer ); + iFan1 = Gia_AigerReadUnsigned( &pBuffer ); assert( !(iFan0 & 1) ); iFan0 >>= 1; iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 ); @@ -308,14 +303,14 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I pBufferPivot = pBuffer; // scroll through flops for ( i = 0; i < nFlops; i++ ) - Gia_ReadAigerDecode( &pBuffer ); + Gia_AigerReadUnsigned( &pBuffer ); // create POs - nProps = Gia_ReadAigerDecode( &pBuffer ); + nProps = Gia_AigerReadUnsigned( &pBuffer ); assert( nProps == 1 ); for ( i = 0; i < nProps; i++ ) { - iFan0 = Gia_ReadAigerDecode( &pBuffer ); + iFan0 = Gia_AigerReadUnsigned( &pBuffer ); iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 ); // complement property output!!! Gia_ManAppendCo( p, Abc_LitNot(iFan0) ); @@ -328,7 +323,7 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I vInits = Vec_IntAlloc( nFlops ); for ( i = 0; i < nFlops; i++ ) { - iFan0 = Gia_ReadAigerDecode( &pBuffer ); + iFan0 = Gia_AigerReadUnsigned( &pBuffer ); assert( (iFan0 & 3) == BRIDGE_VALUE_0 ); Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true iFan0 >>= 2; @@ -487,7 +482,7 @@ void Gia_ManFromBridgeTest( char * pFileName ) fclose ( pFile ); Gia_ManPrintStats( p, 0, 0, 0 ); - Gia_WriteAiger( p, "temp.aig", 0, 0 ); + Gia_AigerWrite( p, "temp.aig", 0, 0 ); Gia_ManToBridgeAbsNetlistTest( "par_.dump", p, BRIDGE_ABS_NETLIST ); Gia_ManStop( p ); diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 0ed9f450..3e933fa0 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1451,7 +1451,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose ) // dump abstraction map Vec_IntFreeP( &p->pGia->vGateClasses ); p->pGia->vGateClasses = Ga2_ManAbsTranslate( p ); - Gia_WriteAiger( p->pGia, pFileName, 0, 0 ); + Gia_AigerWrite( p->pGia, pFileName, 0, 0 ); } else if ( p->pPars->fDumpVabs ) { @@ -1464,7 +1464,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose ) vGateClasses = Ga2_ManAbsTranslate( p ); pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses ); Gia_ManCleanValue( p->pGia ); - Gia_WriteAiger( pAbs, pFileName, 0, 0 ); + Gia_AigerWrite( pAbs, pFileName, 0, 0 ); Gia_ManStop( pAbs ); Vec_IntFreeP( &vGateClasses ); } diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c index 0a0315c2..343ec935 100644 --- a/src/proof/abs/absGlaOld.c +++ b/src/proof/abs/absGlaOld.c @@ -1620,7 +1620,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose ) pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses ); Vec_IntFreeP( &vGateClasses ); // write into file - Gia_WriteAiger( pAbs, pFileName, 0, 0 ); + Gia_AigerWrite( pAbs, pFileName, 0, 0 ); Gia_ManStop( pAbs ); } diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c index b217ef13..d94a93e5 100644 --- a/src/proof/abs/absVta.c +++ b/src/proof/abs/absVta.c @@ -1440,7 +1440,7 @@ void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose ) pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses ); Vec_IntFreeP( &p->pGia->vGateClasses ); // send it out - Gia_WriteAiger( pAbs, pFileName, 0, 0 ); + Gia_AigerWrite( pAbs, pFileName, 0, 0 ); Gia_ManStop( pAbs ); } diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index 30c930a0..72c3e7db 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -263,7 +263,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) { ABC_FREE( pNew->pReprs ); ABC_FREE( pNew->pNexts ); - Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 ); + Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 ); Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" ); } if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index c45bd974..40d5fba6 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -398,7 +398,7 @@ p->timeSim += clock() - clk; } pSrm = Cec_ManFraSpecReduction( p ); -// Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 ); +// Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 ); if ( pPars->fVeryVerbose ) Gia_ManPrintStats( pSrm, 0, 0, 0 ); @@ -481,7 +481,7 @@ p->timeSat += clock() - clk; Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit ); if ( fOutputResult ) { - Gia_WriteAiger( p->pAig, "gia_cec_temp.aig", 0, 0 ); + Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 ); Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" ); } } diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index f3a84d3a..ed5f9a8e 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -1124,7 +1124,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) pNew = Gia_ManCorrReduce( pAig ); pNew = Gia_ManSeqCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); - //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 ); + //Gia_AigerWrite( pNew, "reduced.aig", 0, 0 ); } // report the results if ( pPars->fVerbose ) diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c index da60de1d..43bfa99c 100644 --- a/src/proof/cec/cecSeq.c +++ b/src/proof/cec/cecSeq.c @@ -401,14 +401,14 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) } // write equivalence classes - Gia_WriteAiger( pAig, "gore.aig", 0, 0 ); + Gia_AigerWrite( pAig, "gore.aig", 0, 0 ); // reduce the model pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 ); if ( pReduce ) { pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); Gia_ManStop( pAux ); - Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 ); + Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 ); // Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" ); // Gia_ManPrintStatsShort( pReduce ); Gia_ManStop( pReduce ); diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index 41053cf0..d560c37a 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -710,7 +710,7 @@ clk2 = clock(); if ( status == -1 ) { Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj ); - Gia_WriteAiger( pTemp, "gia_hard.aig", 0, 0 ); + Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 ); Gia_ManStop( pTemp ); Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" ); } diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c index 6fc991a8..6ab88cbe 100644 --- a/src/proof/cec/cecSynth.c +++ b/src/proof/cec/cecSynth.c @@ -309,7 +309,7 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars ) { pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL ); sprintf( Buffer, "part%03d.aig", i ); - Gia_WriteAiger( pTemp, Buffer, 0, 0 ); + Gia_AigerWrite( pTemp, Buffer, 0, 0 ); Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) ); Gia_ManStop( pTemp ); diff --git a/src/sat/bmc/bmcCexMin2.c b/src/sat/bmc/bmcCexMin2.c index 076d744c..7301c3e4 100644 --- a/src/sat/bmc/bmcCexMin2.c +++ b/src/sat/bmc/bmcCexMin2.c @@ -334,7 +334,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int printf( "%3d : ", iFrameStart ); Gia_ManPrintStats( pNew, 0, 0, 0 ); if ( fVerbose ) - Gia_WriteAiger( pNew, "temp.aig", 0, 0 ); + Gia_AigerWrite( pNew, "temp.aig", 0, 0 ); Gia_ManStop( pNew ); } else // CEX min @@ -345,7 +345,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int printf( "%3d : ", f ); Gia_ManPrintStats( pNew, 0, 0, 0 ); if ( fVerbose ) - Gia_WriteAiger( pNew, "temp.aig", 0, 0 ); + Gia_AigerWrite( pNew, "temp.aig", 0, 0 ); Gia_ManStop( pNew ); } } diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c index 87d88fd0..bbf7d1ad 100644 --- a/src/sat/bmc/bmcCexTools.c +++ b/src/sat/bmc/bmcCexTools.c @@ -173,7 +173,7 @@ void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex ) clock_t clk = clock(); pNew = Bmc_CexPerformUnrolling( p, pCex ); Gia_ManPrintStats( pNew, 0, 0, 0 ); - Gia_WriteAiger( pNew, "unroll.aig", 0, 0 ); + Gia_AigerWrite( pNew, "unroll.aig", 0, 0 ); //Bmc_CexDumpAogStats( pNew, clock() - clk ); Gia_ManStop( pNew ); printf( "CE-induced network is written into file \"unroll.aig\".\n" ); @@ -285,7 +285,7 @@ void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex ) clock_t clk = clock(); pNew = Bmc_CexBuildNetwork( p, pCex ); Gia_ManPrintStats( pNew, 0, 0, 0 ); - Gia_WriteAiger( pNew, "unate.aig", 0, 0 ); + Gia_AigerWrite( pNew, "unate.aig", 0, 0 ); //Bmc_CexDumpAogStats( pNew, clock() - clk ); Gia_ManStop( pNew ); printf( "CE-induced network is written into file \"unate.aig\".\n" ); -- cgit v1.2.3