diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-06 23:15:27 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-06 23:15:27 -0800 |
commit | d2ced9f82e20fd502dab9bcbaea5c98ee18c34a1 (patch) | |
tree | 8333079f2265460afe9ead3667d4d51361bec47a /src/aig/ioa | |
parent | c345a60ee7f0156e11cf6b5e107eecc867ca2a3a (diff) | |
download | abc-d2ced9f82e20fd502dab9bcbaea5c98ee18c34a1.tar.gz abc-d2ced9f82e20fd502dab9bcbaea5c98ee18c34a1.tar.bz2 abc-d2ced9f82e20fd502dab9bcbaea5c98ee18c34a1.zip |
Changes to read multi-output testcases described using AIGER 1.9.
Diffstat (limited to 'src/aig/ioa')
-rw-r--r-- | src/aig/ioa/ioaReadAig.c | 71 | ||||
-rw-r--r-- | src/aig/ioa/ioaWriteAig.c | 10 |
2 files changed, 71 insertions, 10 deletions
diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c index 096e82e4..17c93e58 100644 --- a/src/aig/ioa/ioaReadAig.c +++ b/src/aig/ioa/ioaReadAig.c @@ -109,6 +109,7 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck Aig_Obj_t * pObj, * pNode0, * pNode1; Aig_Man_t * pNew; int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits; + int nBad = 0, nConstr = 0, nJust = 0, nFair = 0; char * pDrivers, * pSymbols, * pCur;//, * pType; unsigned uLit0, uLit1, uLit; @@ -119,27 +120,77 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck return NULL; } - // read the file type - pCur = pContents; while ( *pCur++ != ' ' ); + // read the parameters (M I L O A + B C J F) + pCur = pContents; while ( *pCur != ' ' ) pCur++; pCur++; // read the number of objects - nTotal = atoi( pCur ); while ( *pCur++ != ' ' ); + nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++; // read the number of inputs - nInputs = atoi( pCur ); while ( *pCur++ != ' ' ); + nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++; // read the number of latches - nLatches = atoi( pCur ); while ( *pCur++ != ' ' ); + nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++; // read the number of outputs - nOutputs = atoi( pCur ); while ( *pCur++ != ' ' ); + nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++; // read the number of nodes - nAnds = atoi( pCur ); while ( *pCur++ != '\n' ); + nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; + if ( *pCur == ' ' ) + { + assert( nOutputs == 0 ); + // read the number of properties + pCur++; + nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; + nOutputs += nBad; + } + if ( *pCur == ' ' ) + { + // read the number of properties + pCur++; + nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; + nOutputs += nConstr; + } + if ( *pCur == ' ' ) + { + // read the number of properties + pCur++; + nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; + nOutputs += nJust; + } + if ( *pCur == ' ' ) + { + // read the number of properties + pCur++; + nFair = atoi( 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 paramters are wrong.\n" ); + 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 = Aig_ManStart( nAnds ); + pNew->nConstrs = nConstr; // prepare the array of nodes vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds ); @@ -352,6 +403,10 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck Aig_ManCleanup( pNew ); Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) ); + // update polarity of the additional outputs + if ( nBad || nConstr || nJust || nFair ) + Aig_ManInvertConstraints( pNew ); + // check the result if ( fCheck && !Aig_ManCheck( pNew ) ) { diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c index 7aa975f2..2f682775 100644 --- a/src/aig/ioa/ioaWriteAig.c +++ b/src/aig/ioa/ioaWriteAig.c @@ -466,18 +466,23 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int Ioa_ObjSetAigerNum( pObj, nNodes++ ); // write the header "M I L O A" where M = I + L + A - fprintf( pFile, "aig%s %u %u %u %u %u\n", + fprintf( pFile, "aig%s %u %u %u %u %u", fCompact? "2" : "", Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan), Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan), Aig_ManRegNum(pMan), - Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan), + Aig_ManConstrNum(pMan) ? 0 : Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan), Aig_ManNodeNum(pMan) ); + // write the extended header "B C J F" + if ( Aig_ManConstrNum(pMan) ) + fprintf( pFile, " %u %u", Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan), Aig_ManConstrNum(pMan) ); + fprintf( pFile, "\n" ); // if the driver node is a constant, we need to complement the literal below // because, in the AIGER format, literal 0/1 is represented as number 0/1 // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0 + Aig_ManInvertConstraints( pMan ); if ( !fCompact ) { // write latch drivers @@ -502,6 +507,7 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int Vec_StrFree( vBinary ); Vec_IntFree( vLits ); } + Aig_ManInvertConstraints( pMan ); // write the nodes into the buffer Pos = 0; |