From c511bccb6777ecce8abbbcd386c4313e6b7fa8ae Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 20 Jul 2011 10:11:49 +0700 Subject: Added support for constraints in AIGER. --- src/aig/gia/giaAiger.c | 107 ++++++++++++++++++++++++++++++++++++++++++++----- src/aig/gia/giaDup.c | 1 + 2 files changed, 97 insertions(+), 11 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 3940d324..69b3bb39 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -568,7 +568,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) ***********************************************************************/ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck ) { - Gia_Man_t * pNew; + Gia_Man_t * pNew, * pTemp; Vec_Int_t * vLits = NULL; Vec_Int_t * vNodes, * vDrivers;//, * vTerms; int iObj, iNode0, iNode1; @@ -680,16 +680,6 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck Vec_IntFree( vLits ); } - // create the POs - for ( i = 0; i < nOutputs; i++ ) - Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) ); - for ( i = 0; i < nLatches; i++ ) - Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) ); - Vec_IntFree( vDrivers ); - - // create the latches - Gia_ManSetRegNum( pNew, nLatches ); - // check if there are other types of information to read pCur = pSymbols; if ( (char *)pCur + 1 < pContents + nFileSize && *pCur == 'c' ) @@ -746,6 +736,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck if ( *pCur != 'c' ) { int fBreakUsed = 0; + char * pCurOld = pCur; pNew->vUserPiIds = Vec_IntStartFull( Gia_ManPiNum(pNew) ); pNew->vUserPoIds = Vec_IntStartFull( Gia_ManPoNum(pNew) ); pNew->vUserFfIds = Vec_IntStartFull( Gia_ManRegNum(pNew) ); @@ -792,12 +783,103 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck // in case of abnormal termination, remove the arrays if ( fBreakUsed ) { + char * pName; + int Entry, nInvars, nConstr, iTerm; + + Vec_Int_t * vPoNames = Vec_IntStartFull( nOutputs ); + Vec_IntFreeP( &pNew->vUserPiIds ); Vec_IntFreeP( &pNew->vUserPoIds ); Vec_IntFreeP( &pNew->vUserFfIds ); + + // try to figure out signal names + fBreakUsed = 0; + pCur = pCurOld; + while ( pCur < pContents + nFileSize && *pCur != 'c' ) + { + // get the terminal type + if ( *pCur == 'i' || *pCur == 'l' ) + continue; + if ( *pCur != 'o' ) + { + fprintf( stdout, "Wrong terminal type.\n" ); + fBreakUsed = 1; + break; + } + // get the terminal number + iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' ); + // get the node + if ( iTerm < 0 || iTerm >= nOutputs ) + { + fprintf( stdout, "The output number (%d) is out of range.\n", iTerm ); + fBreakUsed = 1; + break; + } + if ( Vec_IntEntry(vPoNames, iTerm) != ~0 ) + { + fprintf( stdout, "The output number (%d) is listed twice.\n", iTerm ); + fBreakUsed = 1; + break; + } + + // get the name + pName = pCur; while ( *pCur++ != '\n' ); + *(pCur-1) = 0; + // assign the name + Vec_IntWriteEntry( vPoNames, iTerm, pName - pContents ); + } + + // check that all names are assigned + if ( !fBreakUsed ) + { + nInvars = nConstr = 0; + Vec_IntForEachEntry( vPoNames, Entry, i ) + { + if ( Entry == ~0 ) + continue; + if ( strncmp( pContents+Entry, "constraint:", 11 ) == 0 ) + nConstr++; + if ( strncmp( pContents+Entry, "invariant:", 10 ) == 0 ) + nInvars++; + } + + // move constraints forward in the PO list + if ( nConstr || nInvars ) + { + int k = nLatches; + Vec_Int_t * vDriversCopy = Vec_IntDup( vDrivers ); + Vec_IntForEachEntry( vPoNames, Entry, i ) + if ( Entry == ~0 || (strncmp( pContents+Entry, "constraint:", 11 ) != 0 && strncmp( pContents+Entry, "invariant:", 10 ) != 0) ) + Vec_IntWriteEntry( vDrivers, k++, Vec_IntEntry(vDriversCopy, nLatches + i) ); + Vec_IntForEachEntry( vPoNames, Entry, i ) + if ( Entry != ~0 && strncmp( pContents+Entry, "constraint:", 11 ) == 0 ) + Vec_IntWriteEntry( vDrivers, k++, Vec_IntEntry(vDriversCopy, nLatches + i) ^ 1 ); // flip polarity!!! + // update the PO count + nOutputs -= nInvars; + assert( k == nLatches + nOutputs ); + Vec_IntFree( vDriversCopy ); + // mark constraints + pNew->nConstrs = nConstr; + } + + if ( nConstr ) + fprintf( stdout, "Recognized and added %d constraints.\n", nConstr ); + if ( nInvars ) + fprintf( stdout, "Recognized and skipped %d invariants.\n", nInvars ); + } + Vec_IntFree( vPoNames ); } } + // 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 ); // skipping the comments Vec_IntFree( vNodes ); @@ -810,6 +892,9 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck return NULL; } */ + + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); return pNew; } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 3672f7c3..62586103 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -521,6 +521,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) int i, nRos = 0, nRis = 0; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->nConstrs = p->nConstrs; pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj1( p, pObj, i ) -- cgit v1.2.3