diff options
Diffstat (limited to 'src/base/wlc/wlcReadSmt.c')
| -rw-r--r-- | src/base/wlc/wlcReadSmt.c | 681 |
1 files changed, 681 insertions, 0 deletions
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c new file mode 100644 index 00000000..35d3ed87 --- /dev/null +++ b/src/base/wlc/wlcReadSmt.c @@ -0,0 +1,681 @@ +/**CFile**************************************************************** + + FileName [wlcReadSmt.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Parses several flavors of word-level Verilog.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 22, 2014.] + + Revision [$Id: wlcReadSmt.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wlc.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// parser name types +typedef enum { + PRS_SMT_NONE = 0, + PRS_SMT_INPUT, + PRS_SMT_CONST, + PRS_SMT_LET, + PRS_SMT_ASSERT +} Prs_ManType_t; + +// parser +typedef struct Prs_Smt_t_ Prs_Smt_t; +struct Prs_Smt_t_ +{ + // input data + char * pName; // file name + char * pBuffer; // file contents + char * pLimit; // end of file + char * pCur; // current position + Abc_Nam_t * pStrs; // string manager + // network structure + Vec_Int_t vData; + // error handling + char ErrorStr[1000]; +}; + + +// create error message +static inline int Prs_SmtErrorSet( Prs_Smt_t * p, char * pError, int Value ) +{ + assert( !p->ErrorStr[0] ); + sprintf( p->ErrorStr, "%s", pError ); + return Value; +} +// clear error message +static inline void Prs_SmtErrorClear( Prs_Smt_t * p ) +{ + p->ErrorStr[0] = '\0'; +} +// print error message +static inline int Prs_SmtErrorPrint( Prs_Smt_t * p ) +{ + char * pThis; int iLine = 0; + if ( !p->ErrorStr[0] ) return 1; + for ( pThis = p->pBuffer; pThis < p->pCur; pThis++ ) + iLine += (int)(*pThis == '\n'); + printf( "Line %d: %s\n", iLine, p->ErrorStr ); + return 0; +} +static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit ) +{ + char * pBuffer; + int nFileSize, RetValue; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open input file.\n" ); + return NULL; + } + // get the file size, in bytes + fseek( pFile, 0, SEEK_END ); + nFileSize = ftell( pFile ); + // move the file current reading position to the beginning + rewind( pFile ); + // load the contents of the file into memory + pBuffer = ABC_ALLOC( char, nFileSize + 3 ); + pBuffer[0] = '\n'; + RetValue = fread( pBuffer+1, nFileSize, 1, pFile ); + // terminate the string with '\0' + pBuffer[nFileSize + 0] = '\n'; + pBuffer[nFileSize + 1] = '\0'; + *ppLimit = pBuffer + nFileSize + 2; + return pBuffer; +} +static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName ) +{ + Prs_Smt_t * p; + char * pBuffer, * pLimit; + pBuffer = Prs_SmtLoadFile( pFileName, &pLimit ); + if ( pBuffer == NULL ) + return NULL; + p = ABC_CALLOC( Prs_Smt_t, 1 ); + p->pName = pFileName; + p->pBuffer = pBuffer; + p->pLimit = pLimit; + p->pCur = pBuffer; + p->pStrs = Abc_NamStart( 1000, 24 ); + Vec_IntGrow ( &p->vData, 1000 ); + return p; +} + +static inline void Prs_SmtFree( Prs_Smt_t * p ) +{ + if ( p->pStrs ) + Abc_NamDeref( p->pStrs ); + Vec_IntErase( &p->vData ); + ABC_FREE( p->pBuffer ); + ABC_FREE( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Prs_SmtRemoveComments( Prs_Smt_t * p ) +{ + char * pTemp; + for ( pTemp = p->pBuffer; pTemp < p->pLimit; pTemp++ ) + if ( *pTemp == ';' ) + while ( *pTemp && *pTemp != '\n' ) + *pTemp++ = ' '; +} +static inline void Prs_SmtSkipSpaces( Prs_Smt_t * p ) +{ + while ( *p->pCur == ' ' || *p->pCur == '\t' || *p->pCur == '\r' || *p->pCur == '\n' ) + p->pCur++; +} +static inline int Prs_SmtIsWord( Prs_Smt_t * p, char * pWord ) +{ + Prs_SmtSkipSpaces( p ); + if ( strncmp( p->pCur, pWord, strlen(pWord) ) ) + return 0; + p->pCur += strlen(pWord); + Prs_SmtSkipSpaces( p ); + return 1; +} +static inline char * Prs_SmtFindNextPar( Prs_Smt_t * p ) +{ + char * pTemp; int Count = 1; + for ( pTemp = p->pCur; pTemp < p->pLimit; pTemp++ ) + { + if ( *pTemp == '(' ) + Count++; + else if ( *pTemp == ')' ) + Count--; + if ( Count == 0 ) + break; + } + assert( *pTemp == ')' ); + return pTemp; +} +static inline int Prs_SmtParseLet( Prs_Smt_t * p, char * pLimit, int Type ) +{ + char * pToken; + assert( *pLimit == ')' ); + *pLimit = 0; + Vec_IntPush( &p->vData, 0 ); + Vec_IntPush( &p->vData, Type ); + pToken = strtok( p->pCur, " ()" ); + while ( pToken ) + { + if ( pToken[0] != '_' && pToken[0] != '=' ) + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + } + assert( *pLimit == 0 ); + *pLimit = ')'; + p->pCur = pLimit; + return 1; +} +static inline int Prs_SmtParseFun( Prs_Smt_t * p, char * pLimit, int Type ) +{ + char * pToken; + assert( *pLimit == ')' ); + *pLimit = 0; + Vec_IntPush( &p->vData, 0 ); + Vec_IntPush( &p->vData, Type ); + pToken = strtok( p->pCur, " ()" ); + assert( pToken != NULL ); + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + if ( pToken[0] == '_' ) + pToken = strtok( NULL, " ()" ); + if ( !strcmp(pToken, "Bool") ) + { + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "1", NULL) ); + pToken = strtok( NULL, " ()" ); + if ( !strcmp(pToken, "false") ) + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "#b0", NULL) ); + else if ( !strcmp(pToken, "true") ) + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "#b1", NULL) ); + else assert( 0 ); + } + else if ( !strcmp(pToken, "BitVec") ) + { + pToken = strtok( NULL, " ()" ); + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + if ( pToken ) + { + Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + if ( pToken != NULL ) + return Prs_SmtErrorSet(p, "Trailing symbols are not recognized.", 0); + } + } + else + return Prs_SmtErrorSet(p, "Expecting either \"Bool\" or \"BitVec\".", 0); + assert( *pLimit == 0 ); + *pLimit = ')'; + p->pCur = pLimit; + return 1; +} +int Prs_SmtReadLines( Prs_Smt_t * p ) +{ + Prs_SmtSkipSpaces( p ); + while ( *p->pCur == '(' ) + { + p->pCur++; + if ( Prs_SmtIsWord(p, "let") ) + { + assert( *p->pCur == '(' ); + p->pCur++; + if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_LET ) ) + return 0; + assert( *p->pCur == ')' ); + p->pCur++; + } + else if ( Prs_SmtIsWord(p, "declare-fun") ) + { + if ( !Prs_SmtParseFun( p, Prs_SmtFindNextPar(p), PRS_SMT_INPUT ) ) + return 0; + assert( *p->pCur == ')' ); + p->pCur++; + } + else if ( Prs_SmtIsWord(p, "define-fun") ) + { + if ( !Prs_SmtParseFun( p, Prs_SmtFindNextPar(p), PRS_SMT_CONST ) ) + return 0; + assert( *p->pCur == ')' ); + p->pCur++; + } + else if ( Prs_SmtIsWord(p, "check-sat") ) + { + Vec_IntPush( &p->vData, 0 ); + return 1; + } + else if ( Prs_SmtIsWord(p, "assert") ) + {} + else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") ) + p->pCur = Prs_SmtFindNextPar(p) + 1; + else + break; + //return Prs_SmtErrorSet(p, "Unsupported directive.", 0); + Prs_SmtSkipSpaces( p ); + } + // finish parsing assert + if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) ) + return 0; + assert( *p->pCur == ')' ); + Vec_IntPush( &p->vData, 0 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Prs_SmtPrintParser( Prs_Smt_t * p ) +{ + int Entry, i; + Vec_IntForEachEntry( &p->vData, Entry, i ) + { + if ( Entry == 0 ) + { + printf( "\n" ); + if ( i == Vec_IntSize(&p->vData) - 1 ) + break; + Entry = Vec_IntEntry(&p->vData, ++i); + if ( Entry == PRS_SMT_INPUT ) + printf( "declare-fun" ); + else if ( Entry == PRS_SMT_CONST ) + printf( "define-fun" ); + else if ( Entry == PRS_SMT_LET ) + printf( "let" ); + else if ( Entry == PRS_SMT_ASSERT ) + printf( "assert" ); + else assert(0); + continue; + } + printf( " %s", Abc_NamStr(p->pStrs, Entry) ); + } +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Prs_SmtReadConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec_Int_t * vFanins, char * pName ) +{ + char Buffer[100]; + int i, nDigits, iObj, NameId, fFound; + Vec_IntClear( vFanins ); + if ( pStr[0] != '#' ) + { + // handle decimal number + int Number = atoi( pStr ); + nBits = Abc_Base2Log( Number+1 ); + assert( nBits < 32 ); + Vec_IntPush( vFanins, Number ); + } + else if ( pStr[1] == 'b' ) + { + if ( nBits == -1 ) + nBits = strlen(pStr+2); + Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); + for ( i = 0; i < nBits; i++ ) + if ( pStr[2+i] == '1' ) + Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), nBits-1-i ); + else if ( pStr[2+i] != '0' ) + return 0; + } + else if ( pStr[1] == 'x' ) + { + if ( nBits == -1 ) + nBits = strlen(pStr+2)*4; + Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); + nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 ); + if ( nDigits != (nBits + 3)/4 ) + assert( 0 ); + } + else return 0; + // create constant node + iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_CONST, 0, nBits-1, 0 ); + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + // add node's name + if ( pName == NULL ) + { + sprintf( Buffer, "_c%d_", iObj ); + pName = Buffer; + } + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + return NameId; +} +static inline int Prs_SmtReadName( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec_Int_t * vFanins ) +{ + if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' ) + { + Vec_Int_t * vTemp = Vec_IntAlloc(0); + int NameId = Prs_SmtReadConstant( pNtk, pStr, nBits, vTemp, NULL ); + Vec_IntFree( vTemp ); + if ( !NameId ) + return 0; + Vec_IntPush( vFanins, NameId ); + return 1; + } + else + { + // read name + int fFound, NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); + assert( fFound ); + Vec_IntPush( vFanins, NameId ); + return 1; + } +} +static inline int Prs_SmtStrToType( char * pName ) +{ + int Type = 0; + if ( !strcmp(pName, "ite") ) + Type = WLC_OBJ_MUX; // 08: multiplexer + else if ( !strcmp(pName, "bvlshr") ) + Type = WLC_OBJ_SHIFT_R; // 09: shift right + else if ( !strcmp(pName, "bvashr") ) + Type = WLC_OBJ_SHIFT_RA; // 10: shift right (arithmetic) + else if ( !strcmp(pName, "bvshl") ) + Type = WLC_OBJ_SHIFT_L; // 11: shift left +// else if ( !strcmp(pName, "") ) +// Type = WLC_OBJ_SHIFT_LA; // 12: shift left (arithmetic) + else if ( !strcmp(pName, "rotate_right") ) + Type = WLC_OBJ_ROTATE_R; // 13: rotate right + else if ( !strcmp(pName, "rotate_left") ) + Type = WLC_OBJ_ROTATE_L; // 14: rotate left + else if ( !strcmp(pName, "bvnot") ) + Type = WLC_OBJ_BIT_NOT; // 15: bitwise NOT + else if ( !strcmp(pName, "bvand") ) + Type = WLC_OBJ_BIT_AND; // 16: bitwise AND + else if ( !strcmp(pName, "bvor") ) + Type = WLC_OBJ_BIT_OR; // 17: bitwise OR + else if ( !strcmp(pName, "bvxor") ) + Type = WLC_OBJ_BIT_XOR; // 18: bitwise XOR + else if ( !strcmp(pName, "extract") ) + Type = WLC_OBJ_BIT_SELECT; // 19: bit selection + else if ( !strcmp(pName, "concat") ) + Type = WLC_OBJ_BIT_CONCAT; // 20: bit concatenation + else if ( !strcmp(pName, "zero_extend") ) + Type = WLC_OBJ_BIT_ZEROPAD; // 21: zero padding + else if ( !strcmp(pName, "sign_extend") ) + Type = WLC_OBJ_BIT_SIGNEXT; // 22: sign extension + else if ( !strcmp(pName, "not") ) + Type = WLC_OBJ_LOGIC_NOT; // 23: logic NOT + else if ( !strcmp(pName, "and") ) + Type = WLC_OBJ_LOGIC_AND; // 24: logic AND + else if ( !strcmp(pName, "or") ) + Type = WLC_OBJ_LOGIC_OR; // 25: logic OR + else if ( !strcmp(pName, "bvcomp") ) + Type = WLC_OBJ_COMP_EQU; // 26: compare equal +// else if ( !strcmp(pName, "") ) +// Type = WLC_OBJ_COMP_NOTEQU; // 27: compare not equal + else if ( !strcmp(pName, "bvult") ) + Type = WLC_OBJ_COMP_LESS; // 28: compare less + else if ( !strcmp(pName, "bvugt") ) + Type = WLC_OBJ_COMP_MORE; // 29: compare more + else if ( !strcmp(pName, "bvule") ) + Type = WLC_OBJ_COMP_LESSEQU; // 30: compare less or equal + else if ( !strcmp(pName, "bvuge") ) + Type = WLC_OBJ_COMP_MOREEQU; // 31: compare more or equal + else if ( !strcmp(pName, "bvredand") ) + Type = WLC_OBJ_REDUCT_AND; // 32: reduction AND + else if ( !strcmp(pName, "bvredor") ) + Type = WLC_OBJ_REDUCT_OR; // 33: reduction OR + else if ( !strcmp(pName, "bvredxor") ) + Type = WLC_OBJ_REDUCT_XOR; // 34: reduction XOR + else if ( !strcmp(pName, "bvadd") ) + Type = WLC_OBJ_ARI_ADD; // 35: arithmetic addition + else if ( !strcmp(pName, "bvsub") ) + Type = WLC_OBJ_ARI_SUB; // 36: arithmetic subtraction + else if ( !strcmp(pName, "bvmul") ) + Type = WLC_OBJ_ARI_MULTI; // 37: arithmetic multiplier + else if ( !strcmp(pName, "bvdiv") ) + Type = WLC_OBJ_ARI_DIVIDE; // 38: arithmetic division + else if ( !strcmp(pName, "bvurem") ) + Type = WLC_OBJ_ARI_MODULUS; // 39: arithmetic modulus +// else if ( !strcmp(pName, "") ) +// Type = WLC_OBJ_ARI_POWER; // 40: arithmetic power + else if ( !strcmp(pName, "bvneg") ) + Type = WLC_OBJ_ARI_MINUS; // 41: arithmetic minus +// else if ( !strcmp(pName, "") ) +// Type = WLC_OBJ_TABLE; // 42: bit table + else assert( 0 ); + return Type; +} +static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * vData, int i, Vec_Int_t * vFanins, int * pRange ) +{ + int Type, NameId; + char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) ); + // read type + Type = Prs_SmtStrToType( pName ); + if ( Type == 0 ) + return 0; + *pRange = 0; + Vec_IntClear( vFanins ); + if ( Type == WLC_OBJ_COMP_EQU ) + { + *pRange = 1; + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); + return WLC_OBJ_COMP_EQU; + } + else if ( Type == WLC_OBJ_LOGIC_NOT ) + { + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + if ( !strcmp(pName, "bvcomp") ) + { + *pRange = 1; + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); + return WLC_OBJ_COMP_NOTEQU; // 26: compare equal + } + i--; + } + else if ( Type == WLC_OBJ_BIT_SELECT ) + { + int End, Beg; + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + End = atoi( pName ); + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + Beg = atoi( pName ); + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + Prs_SmtReadName( pNtk, pName, -1, vFanins ); + Vec_IntPush( vFanins, (End << 16) | Beg ); + *pRange = End - Beg + 1; + return WLC_OBJ_BIT_SELECT; + } + while ( Vec_IntEntry(vData, ++i) ) + Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, i)), -1, vFanins ); + if ( Type == WLC_OBJ_ROTATE_R || Type == WLC_OBJ_ROTATE_L ) + { + int * pArray = Vec_IntArray(vFanins); + assert( Vec_IntSize(vFanins) == 2 ); + ABC_SWAP( int, pArray[0], pArray[1] ); + } + if ( Type >= WLC_OBJ_LOGIC_NOT && Type <= WLC_OBJ_REDUCT_XOR ) + *pRange = 1; + else if ( Type == WLC_OBJ_BIT_CONCAT ) + { + int k; + Vec_IntForEachEntry( vFanins, NameId, k ) + *pRange += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + } + else if ( Type == WLC_OBJ_MUX ) + { + int * pArray = Vec_IntArray(vFanins); + assert( Vec_IntSize(vFanins) == 3 ); + ABC_SWAP( int, pArray[1], pArray[2] ); + NameId = Vec_IntEntry(vFanins, 1); + *pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + } + else // to determine range, look at the first argument + { + NameId = Vec_IntEntry(vFanins, 0); + *pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + } + return Type; +} +Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) +{ + Wlc_Ntk_t * pNtk; + char * pName, * pBits, * pConst; + Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); + int i, iObj, Type, Entry, NameId, fFound, Range; + // start network and create primary inputs + pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 ); + pNtk->pManName = Abc_NamStart( 1000, 24 ); + for ( i = 0; i < Vec_IntSize(&p->vData) - 1; ) + { + assert( Vec_IntEntry(&p->vData, i) == 0 ); + if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT ) + { + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, atoi(pBits)-1, 0 ); + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + } + while ( Vec_IntEntry(&p->vData, ++i) ); + } + // create logic nodes + for ( i = 0; i < Vec_IntSize(&p->vData) - 1; ) + { + assert( Vec_IntEntry(&p->vData, i) == 0 ); + Entry = Vec_IntEntry(&p->vData, ++i); + if ( Entry == PRS_SMT_INPUT ) + {} + else if ( Entry == PRS_SMT_CONST ) + { + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + pConst = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + // create new node + if ( !Prs_SmtReadConstant( pNtk, pConst, atoi(pBits), vFanins, pName ) ) + return NULL; + } + else if ( Entry == PRS_SMT_LET ) + { + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range ); + if ( Type == WLC_OBJ_NONE ) + return NULL; + assert( Range > 0 ); + // create new node + iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 ); + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + // add node's name + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + } + else if ( Entry == PRS_SMT_ASSERT ) + { + Type = WLC_OBJ_BUF; + Vec_IntClear( vFanins ); + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + if ( !strcmp(pName, "not") ) + { + Type = WLC_OBJ_LOGIC_NOT; + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); + Range = 1; + } + // add fanin + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( fFound ); + Vec_IntPush( vFanins, NameId ); + // find range + if ( Type == WLC_OBJ_BUF ) + { + // find range + iObj = Vec_IntEntry(vFanins, 0); + Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ); + assert( Range == 1 ); + } + // create new node + iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 ); + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 ); + // add node's name + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, "miter_output", &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + break; + } + else assert( 0 ); + while ( Vec_IntEntry(&p->vData, ++i) ); + } + Vec_IntFree( vFanins ); + // create nameIDs + vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) ); + Vec_IntAppend( &pNtk->vNameIds, vFanins ); + Vec_IntFree( vFanins ); + return pNtk; +} +Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) +{ + Wlc_Ntk_t * pNtk = NULL; + Prs_Smt_t * p = Prs_SmtAlloc( pFileName ); + if ( p == NULL ) + return NULL; + Prs_SmtRemoveComments( p ); + Prs_SmtReadLines( p ); + //Prs_SmtPrintParser( p ); + if ( Prs_SmtErrorPrint(p) ) + { + pNtk = Prs_SmtBuild( p ); + } + Prs_SmtFree( p ); + return pNtk; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |