From f27979fc8fd5663d2bc9d9bad3fcbed2acfc4e17 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 28 Feb 2015 22:05:46 -0800 Subject: Improvements to the SMTLIB parser. --- src/base/wlc/wlcBlast.c | 4 + src/base/wlc/wlcReadSmt.c | 1216 +++++++++++++++++++++++++-------------------- 2 files changed, 687 insertions(+), 533 deletions(-) diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 4a935f6b..a4e5459e 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -107,6 +107,8 @@ void Wlc_BlastShiftRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int * pRes = Wlc_VecCopy( vRes, pNum, nNum ); int Fill = fSticky ? pNum[nNum-1] : 0; int i, j, fShort = 0; + if ( nShift > 32 ) + nShift = 32; assert( nShift <= 32 ); for( i = 0; i < nShift; i++ ) for( j = 0; j < nNum - fSticky; j++ ) @@ -126,6 +128,8 @@ void Wlc_BlastShiftLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, i int * pRes = Wlc_VecCopy( vRes, pNum, nNum ); int Fill = fSticky ? pNum[0] : 0; int i, j, fShort = 0; + if ( nShift > 32 ) + nShift = 32; assert( nShift <= 32 ); for( i = 0; i < nShift; i++ ) for( j = nNum-1; j >= fSticky; j-- ) diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 7093d79d..8143be6c 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [wlcReadSmt.c] + FileName [wlcParse.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,11 +14,12 @@ Date [Ver. 1.0. Started - August 22, 2014.] - Revision [$Id: wlcReadSmt.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + Revision [$Id: wlcParse.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] ***********************************************************************/ #include "wlc.h" +#include "misc/vec/vecWec.h" ABC_NAMESPACE_IMPL_START @@ -26,19 +27,9 @@ 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_SMT_VALUE -} Prs_ManType_t; - // parser -typedef struct Prs_Smt_t_ Prs_Smt_t; -struct Prs_Smt_t_ +typedef struct Smt_Prs_t_ Smt_Prs_t; +struct Smt_Prs_t_ { // input data char * pName; // file name @@ -47,81 +38,77 @@ struct Prs_Smt_t_ char * pCur; // current position Abc_Nam_t * pStrs; // string manager // network structure - Vec_Int_t vData; - Vec_Int_t vValues; + Vec_Int_t vStack; // current node on each level + //Vec_Wec_t vDepth; // objects on each level + Vec_Wec_t vObjs; // objects // error handling - char ErrorStr[1000]; + char ErrorStr[1000]; }; - -// create error message -static inline int Prs_SmtErrorSet( Prs_Smt_t * p, char * pError, int Value ) +// parser name types +typedef enum { + SMT_PRS_NONE = 0, + SMT_PRS_SET_OPTION, + SMT_PRS_SET_LOGIC, + SMT_PRS_SET_INFO, + SMT_PRS_DEFINE_FUN, + SMT_PRS_DECLARE_FUN, + SMT_PRS_ASSERT, + SMT_PRS_LET, + SMT_PRS_CHECK_SAT, + SMT_PRS_GET_VALUE, + SMT_PRS_EXIT, + SMT_PRS_END +} Smt_LineType_t; + +typedef struct Smt_Pair_t_ Smt_Pair_t; +struct Smt_Pair_t_ { - assert( !p->ErrorStr[0] ); - sprintf( p->ErrorStr, "%s", pError ); - return Value; -} -// clear error message -static inline void Prs_SmtErrorClear( Prs_Smt_t * p ) + Smt_LineType_t Type; + char * pName; +}; +static Smt_Pair_t s_Types[SMT_PRS_END] = { - p->ErrorStr[0] = '\0'; -} -// print error message -static inline int Prs_SmtErrorPrint( Prs_Smt_t * p ) + { SMT_PRS_NONE, NULL }, + { SMT_PRS_SET_OPTION, "set-option" }, + { SMT_PRS_SET_LOGIC, "set-logic" }, + { SMT_PRS_SET_INFO, "set-info" }, + { SMT_PRS_DEFINE_FUN, "define-fun" }, + { SMT_PRS_DECLARE_FUN, "declare-fun" }, + { SMT_PRS_ASSERT, "assert" }, + { SMT_PRS_LET, "let" }, + { SMT_PRS_CHECK_SAT, "check-sat" }, + { SMT_PRS_GET_VALUE, "get-value" }, + { SMT_PRS_EXIT, "exit" } +}; +static inline char * Smt_GetTypeName( Smt_LineType_t Type ) { - 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; + Smt_LineType_t i; + for ( i = 1; i < SMT_PRS_END; i++ ) + if ( s_Types[i].Type == Type ) + return s_Types[i].pName; + return NULL; } -static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit ) +static inline void Smt_AddTypes( Abc_Nam_t * p ) { - 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, char * pBuffer, char * pLimit ) -{ - Prs_Smt_t * p; - 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; + Smt_LineType_t Type; + for ( Type = 1; Type < SMT_PRS_END; Type++ ) + Abc_NamStrFindOrAdd( p, Smt_GetTypeName(Type), NULL ); + assert( Abc_NamObjNumMax(p) == SMT_PRS_END ); } -static inline void Prs_SmtFree( Prs_Smt_t * p ) -{ - if ( p->pStrs ) - Abc_NamDeref( p->pStrs ); - Vec_IntErase( &p->vData ); - Vec_IntErase( &p->vValues ); - ABC_FREE( p ); -} +static inline int Smt_EntryIsName( int Fan ) { return Abc_LitIsCompl(Fan); } +static inline int Smt_EntryIsType( int Fan, Smt_LineType_t Type ) { assert(Smt_EntryIsName(Fan)); return Abc_Lit2Var(Fan) == Type; } +static inline char * Smt_EntryName( Smt_Prs_t * p, int Fan ) { assert(Smt_EntryIsName(Fan)); return Abc_NamStr( p->pStrs, Abc_Lit2Var(Fan) ); } +static inline Vec_Int_t * Smt_EntryNode( Smt_Prs_t * p, int Fan ) { assert(!Smt_EntryIsName(Fan)); return Vec_WecEntry( &p->vObjs, Abc_Lit2Var(Fan) ); } + +static inline int Smt_VecEntryIsType( Vec_Int_t * vFans, int i, Smt_LineType_t Type ) { return i < Vec_IntSize(vFans) && Smt_EntryIsName(Vec_IntEntry(vFans, i)) && Smt_EntryIsType(Vec_IntEntry(vFans, i), Type); } +static inline char * Smt_VecEntryName( Smt_Prs_t * p, Vec_Int_t * vFans, int i ) { return Smt_EntryIsName(Vec_IntEntry(vFans, i)) ? Smt_EntryName(p, Vec_IntEntry(vFans, i)) : NULL; } +static inline Vec_Int_t * Smt_VecEntryNode( Smt_Prs_t * p, Vec_Int_t * vFans, int i ) { return Smt_EntryIsName(Vec_IntEntry(vFans, i)) ? NULL : Smt_EntryNode(p, Vec_IntEntry(vFans, i)); } + +#define Smt_ManForEachDir( p, Type, vVec, i ) \ + for ( i = 0; (i < Vec_WecSize(&p->vObjs)) && (((vVec) = Vec_WecEntry(&p->vObjs, i)), 1); i++ ) \ + if ( !Smt_VecEntryIsType(vVec, 0, Type) ) {} else //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -138,306 +125,7 @@ static inline void Prs_SmtFree( Prs_Smt_t * p ) 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; -} -static inline int Prs_SmtParseValue( Prs_Smt_t * p, char * pLimit, int Type ) -{ - char * pToken; - assert( *pLimit == ')' ); - *pLimit = 0; - pToken = strtok( p->pCur, " ()" ); - assert( pToken != NULL ); - Vec_IntPush( &p->vValues, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); - pToken = strtok( NULL, " ()" ); - assert( pToken == NULL ); - assert( *pLimit == 0 ); - *pLimit = ')'; - p->pCur = pLimit; - return 1; -} -int Prs_SmtReadLines( Prs_Smt_t * p ) -{ - int fAssert = 0; - 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, "get-value") ) - { - if ( !Prs_SmtParseValue( p, Prs_SmtFindNextPar(p), PRS_SMT_VALUE ) ) - return 0; - assert( *p->pCur == ')' ); - p->pCur++; - } - else if ( Prs_SmtIsWord(p, "assert") ) - fAssert = 1; - else if ( Prs_SmtIsWord(p, "check-sat") ) - break; - else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") ) - p->pCur = Prs_SmtFindNextPar(p) + 1; -// else - //return Prs_SmtErrorSet(p, "Unsupported directive.", 0); - Prs_SmtSkipSpaces( p ); - if ( *p->pCur != '(' && fAssert == 1 ) - { - fAssert = 0; - // finish parsing assert - if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) ) - return 0; - assert( *p->pCur == ')' ); - Vec_IntPush( &p->vData, 0 ); - // skip closing - while ( *p->pCur == ')' ) - p->pCur++; - Prs_SmtSkipSpaces( p ); - } - } - assert( fAssert == 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) ); - } - Vec_IntForEachEntry( &p->vValues, Entry, i ) - printf( "get-value %s\n", 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 * pfSigned ) +static inline int Smt_StrToType( char * pName, int * pfSigned ) { int Type = 0; *pfSigned = 0; if ( !strcmp(pName, "ite") ) @@ -534,209 +222,670 @@ static inline int Prs_SmtStrToType( char * pName, int * pfSigned ) } 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 * pfSigned ) +static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int * Value1, int * Value2 ) { - int Type, NameId; - char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) ); - // read type - Type = Prs_SmtStrToType( pName, pfSigned ); - if ( Type == 0 ) - return 0; - *pRange = 0; - Vec_IntClear( vFanins ); - if ( Type == WLC_OBJ_COMP_EQU ) + if ( Smt_EntryIsName(iSig) ) + return Smt_StrToType( Smt_EntryName(p, iSig), pfSigned ); + else { - *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; + Vec_Int_t * vFans = Smt_EntryNode( p, iSig ); + char * pStr = Smt_VecEntryName( p, vFans, 0 ); int Type; + assert( Vec_IntSize(vFans) >= 3 ); + assert( !strcmp(pStr, "_") ); // special op + *Value1 = *Value2 = -1; + assert( pStr[0] != 'b' || pStr[1] != 'v' ); + // read type + Type = Smt_StrToType( Smt_VecEntryName(p, vFans, 1), pfSigned ); + if ( Type == 0 ) + return 0; + *Value1 = atoi( Smt_VecEntryName(p, vFans, 2) ); + if ( Vec_IntSize(vFans) > 3 ) + *Value2 = atoi( Smt_VecEntryName(p, vFans, 3) ); + return Type; } - else if ( Type == WLC_OBJ_LOGIC_NOT ) +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) +{ + char Buffer[100]; + int NameId, fFound; + int iObj = Wlc_ObjAlloc( pNtk, Type, fSigned, Range-1, 0 ); + assert( Type > 0 ); + assert( Range >= 0 ); + assert( fSigned >= 0 ); + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + if ( fSigned ) { - 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--; + Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; + if ( Vec_IntSize(vFanins) > 0 ) + Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned; + if ( Vec_IntSize(vFanins) > 1 ) + Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned; } - else if ( Type == WLC_OBJ_BIT_SELECT ) + if ( pName == NULL ) { - 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; + sprintf( Buffer, "_n%d_", iObj ); + pName = Buffer; } - 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 ) + // add node's name + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); + assert( !fFound ); + assert( iObj == NameId ); + return iObj; +} +static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, char * pName ) +{ + int i, nDigits, iObj; + Vec_Int_t * vFanins = Vec_IntAlloc( 10 ); + if ( pStr[0] != '#' ) // decimal { - 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 Number = atoi( pStr ); + nBits = Abc_Base2Log( Number+1 ); + assert( nBits < 32 ); + Vec_IntPush( vFanins, Number ); + } + else if ( pStr[1] == 'b' ) // binary { - int k; - Vec_IntForEachEntry( vFanins, NameId, k ) - *pRange += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + 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 ( Type == WLC_OBJ_MUX ) + else if ( pStr[1] == 'x' ) // hexadecimal { - 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) ); + 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 ) + return 0; } - else // to determine range, look at the first argument + else return 0; + // create constant node + iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_CONST, 0, nBits, vFanins, pName ); + Vec_IntFree( vFanins ); + return iObj; +} +int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut, char * pName ) +{ + if ( Smt_EntryIsName(iNode) ) // name or constant { - NameId = Vec_IntEntry(vFanins, 0); - *pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); + if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' ) + { + // (_ BitVec 8) #x19 + return Smt_PrsBuildConstant( pNtk, pStr, RangeOut, pName ); + } + else + { + // s3087 + int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); + assert( fFound ); + return iObj; + } + } + else // node + { + Vec_Int_t * vFans = Smt_EntryNode( p, iNode ); + char * pStr0 = Smt_VecEntryName( p, vFans, 0 ); + char * pStr1 = Smt_VecEntryName( p, vFans, 1 ); + if ( pStr0 && pStr1 && pStr0[0] == '_' && pStr1[0] == 'b' && pStr1[1] == 'v' ) + { + // (_ bv1 32) + char * pStr2 = Smt_VecEntryName( p, vFans, 2 ); + assert( Vec_IntSize(vFans) == 3 ); + return Smt_PrsBuildConstant( pNtk, pStr2+2, atoi(pStr2), pName ); + } + else if ( pStr0 && pStr0[0] == '=' ) + { + assert( Vec_IntSize(vFans) == 3 ); + iNode = Vec_IntEntry(vFans, 2); + assert( Smt_EntryIsName(iNode) ); + pStr0 = Smt_EntryName(p, iNode); + // check the last one is "#b1" + if ( !strcmp("#b1", pStr0) ) + { + iNode = Vec_IntEntry(vFans, 1); + return Smt_PrsBuildNode( pNtk, p, iNode, -1, pName ); + } + else + { + Vec_Int_t * vFanins = Vec_IntAlloc( 2 ); + // get the constant + int iObj, iOper, iConst = Smt_PrsBuildConstant( pNtk, pStr0, -1, NULL ); + // check the middle one is an operator + iNode = Vec_IntEntry(vFans, 1); + iOper = Smt_PrsBuildNode( pNtk, p, iNode, -1, pName ); + // build comparator + Vec_IntPushTwo( vFanins, iOper, iConst ); + iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_COMP_EQU, 0, 1, vFanins, pName ); + Vec_IntFree( vFanins ); + return iObj; + } + } + else + { + int i, Fan, NameId, iFanin, fSigned, Range, Value1 = -1, Value2 = -1; + int Type = Smt_PrsReadType( p, Vec_IntEntry(vFans, 0), &fSigned, &Value1, &Value2 ); + // collect fanins + Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); + Vec_IntForEachEntryStart( vFans, Fan, i, 1 ) + { + iFanin = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL ); + if ( iFanin == 0 ) + { + Vec_IntFree( vFanins ); + return 0; + } + Vec_IntPush( vFanins, iFanin ); + } + // update specialized nodes + assert( Type != WLC_OBJ_BIT_SIGNEXT && Type != WLC_OBJ_BIT_ZEROPAD ); + if ( Type == WLC_OBJ_BIT_SELECT ) + { + assert( Value1 >= 0 && Value2 >= 0 && Value1 >= Value2 ); + Vec_IntPush( vFanins, (Value1 << 16) | Value2 ); + } + else if ( Type == WLC_OBJ_ROTATE_R || Type == WLC_OBJ_ROTATE_L ) + { + char Buffer[10]; + assert( Value1 >= 0 ); + sprintf( Buffer, "%d", Value1 ); + NameId = Smt_PrsBuildConstant( pNtk, Buffer, -1, NULL ); + Vec_IntPush( vFanins, NameId ); + } + // find range + Range = 0; + if ( Type >= WLC_OBJ_LOGIC_NOT && Type <= WLC_OBJ_REDUCT_XOR ) + Range = 1; + else if ( Type == WLC_OBJ_BIT_SELECT ) + Range = Value1 - Value2 + 1; + else if ( Type == WLC_OBJ_BIT_CONCAT ) + { + Vec_IntForEachEntry( vFanins, NameId, i ) + Range += 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); + Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + } + else // to determine range, look at the first argument + { + NameId = Vec_IntEntry(vFanins, 0); + Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); + } + // create node + assert( Range > 0 ); + NameId = Smt_PrsCreateNode( pNtk, Type, fSigned, Range, vFanins, pName ); + Vec_IntFree( vFanins ); + return NameId; + } } - return Type; } -Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_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, fSigned, nBits = 0; + Vec_Int_t * vFans, * vFans2, * vFans3; + Vec_Int_t * vAsserts = Vec_IntAlloc(100); + char * pName, * pRange, * pValue; + int i, k, Fan, Fan3, iObj, Status, Range, NameId, nBits = 0; + // issue warnings about unknown dirs + vFans = Vec_WecEntry( &p->vObjs, 0 ); + Vec_IntForEachEntry( vFans, Fan, i ) + { + assert( !Smt_EntryIsName(Fan) ); + vFans2 = Smt_VecEntryNode( p, vFans, i ); + Fan = Vec_IntEntry(vFans2, 0); + assert( Smt_EntryIsName(Fan) ); + if ( Abc_Lit2Var(Fan) >= SMT_PRS_END ) + printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) ); + } // start network and create primary inputs - pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 ); + pNtk = Wlc_NtkAlloc( p->pName, 1000 ); pNtk->pManName = Abc_NamStart( 1000, 24 ); - for ( i = 0; i < Vec_IntSize(&p->vData) - 1; ) + Smt_ManForEachDir( p, SMT_PRS_DECLARE_FUN, vFans, i ) { - assert( Vec_IntEntry(&p->vData, i) == 0 ); - if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT ) + assert( Vec_IntSize(vFans) == 4 ); + assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) ); + // get name + Fan = Vec_IntEntry(vFans, 1); + assert( Smt_EntryIsName(Fan) ); + pName = Smt_EntryName(p, Fan); + // skip () + Fan = Vec_IntEntry(vFans, 2); + assert( !Smt_EntryIsName(Fan) ); + // check type (Bool or BitVec) + Fan = Vec_IntEntry(vFans, 3); + if ( Smt_EntryIsName(Fan) ) { - 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 ); - // save values - Vec_IntPush( &pNtk->vValues, NameId ); - Vec_IntPush( &pNtk->vValues, nBits ); - Vec_IntPush( &pNtk->vValues, atoi(pBits) ); - nBits += atoi(pBits); + //(declare-fun s1 () Bool) + assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); + Range = 1; } - while ( Vec_IntEntry(&p->vData, ++i) ); + else + { + // (declare-fun s1 () (_ BitVec 64)) + // get range + Fan = Vec_IntEntry(vFans, 3); + assert( !Smt_EntryIsName(Fan) ); + vFans2 = Smt_EntryNode(p, Fan); + assert( Vec_IntSize(vFans2) == 3 ); + assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) ); + assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); + Fan = Vec_IntEntry(vFans2, 2); + assert( Smt_EntryIsName(Fan) ); + pRange = Smt_EntryName(p, Fan); + Range = atoi(pRange); + } + // create node + iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, Range-1, 0 ); + NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, NULL ); + assert( iObj == NameId ); + // save values + Vec_IntPush( &pNtk->vValues, NameId ); + Vec_IntPush( &pNtk->vValues, nBits ); + Vec_IntPush( &pNtk->vValues, Range ); + nBits += Range; } - // create logic nodes - for ( i = 0; i < Vec_IntSize(&p->vData) - 1; ) + // create constants + Smt_ManForEachDir( p, SMT_PRS_DEFINE_FUN, vFans, i ) { - assert( Vec_IntEntry(&p->vData, i) == 0 ); - Entry = Vec_IntEntry(&p->vData, ++i); - if ( Entry == PRS_SMT_INPUT ) - {} - else if ( Entry == PRS_SMT_CONST ) + assert( Vec_IntSize(vFans) == 5 ); + assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); + // get name + Fan = Vec_IntEntry(vFans, 1); + assert( Smt_EntryIsName(Fan) ); + pName = Smt_EntryName(p, Fan); + // skip () + Fan = Vec_IntEntry(vFans, 2); + assert( !Smt_EntryIsName(Fan) ); + // check type (Bool or BitVec) + Fan = Vec_IntEntry(vFans, 3); + if ( Smt_EntryIsName(Fan) ) { - 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; + // (define-fun s_2 () Bool false) + assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); + Range = 1; + pValue = Smt_VecEntryName(p, vFans, 4); + if ( !strcmp("false", pValue) ) + pValue = "#b0"; + else if ( !strcmp("true", pValue) ) + pValue = "#b1"; + else assert( 0 ); + Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName ); } - else if ( Entry == PRS_SMT_LET ) + else { - pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); - Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range, &fSigned ); - 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 ); - if ( fSigned ) - { - Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; - if ( Vec_IntSize(vFanins) > 0 ) - Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned; - if ( Vec_IntSize(vFanins) > 1 ) - Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned; - } - // add node's name - NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); - assert( !fFound ); - assert( iObj == NameId ); + // (define-fun s702 () (_ BitVec 4) #xe) + // (define-fun s1 () (_ BitVec 8) (bvneg #x7f)) + // get range + Fan = Vec_IntEntry(vFans, 3); + assert( !Smt_EntryIsName(Fan) ); + vFans2 = Smt_VecEntryNode(p, vFans, 3); + assert( Vec_IntSize(vFans2) == 3 ); + assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) ); + assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); + // get range + Fan = Vec_IntEntry(vFans2, 2); + assert( Smt_EntryIsName(Fan) ); + pRange = Smt_EntryName(p, Fan); + Range = atoi(pRange); + // get constant + Fan = Vec_IntEntry(vFans, 4); + Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName ); + } + if ( !Status ) + { + Wlc_NtkFree( pNtk ); pNtk = NULL; + goto finish; } - else if ( Entry == PRS_SMT_ASSERT ) + } + // process let-statements + Smt_ManForEachDir( p, SMT_PRS_LET, vFans, i ) + { + // let ((s35550 (bvor s48 s35549))) + assert( Vec_IntSize(vFans) == 3 ); + assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_LET) ); + // get parts + Fan = Vec_IntEntry(vFans, 1); + assert( !Smt_EntryIsName(Fan) ); + vFans2 = Smt_EntryNode(p, Fan); + if ( Smt_VecEntryIsType(vFans2, 0, SMT_PRS_LET) ) + continue; + // iterate through the parts + Vec_IntForEachEntry( vFans2, Fan, k ) { - Type = WLC_OBJ_BUF; - Vec_IntClear( vFanins ); - pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); - if ( !strcmp(pName, "not") ) + // s35550 (bvor s48 s35549) + Fan = Vec_IntEntry(vFans2, 0); + assert( !Smt_EntryIsName(Fan) ); + vFans3 = Smt_EntryNode(p, Fan); + // get the name + Fan3 = Vec_IntEntry(vFans3, 0); + assert( Smt_EntryIsName(Fan3) ); + pName = Smt_EntryName(p, Fan3); + // get function + Fan3 = Vec_IntEntry(vFans3, 1); + assert( !Smt_EntryIsName(Fan3) ); + Status = Smt_PrsBuildNode( pNtk, p, Fan3, -1, pName ); + if ( !Status ) { - Type = WLC_OBJ_LOGIC_NOT; - pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); - Range = 1; + Wlc_NtkFree( pNtk ); pNtk = NULL; + goto finish; } - // add fanin - NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); - assert( fFound ); - Vec_IntPush( vFanins, NameId ); - // find range - if ( Type == WLC_OBJ_BUF ) + } + } + // process assert-statements + Vec_IntClear( vAsserts ); + Smt_ManForEachDir( p, SMT_PRS_ASSERT, vFans, i ) + { + //(assert ; no quantifiers + // (let ((s2 (bvsge s0 s1))) + // (not s2))) + //(assert (not (= s0 #x00))) + assert( Vec_IntSize(vFans) == 2 ); + assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) ); + // get second directive + Fan = Vec_IntEntry(vFans, 1); + if ( !Smt_EntryIsName(Fan) ) + { + // find the final let-statement + vFans2 = Smt_VecEntryNode(p, vFans, 1); + while ( Smt_VecEntryIsType(vFans2, 0, SMT_PRS_LET) ) { - // find range - iObj = Vec_IntEntry(vFanins, 0); - Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ); - assert( Range == 1 ); + Fan = Vec_IntEntry(vFans2, 2); + if ( Smt_EntryIsName(Fan) ) + break; + vFans2 = Smt_VecEntryNode(p, vFans2, 2); } - // 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) ); + // find name or create node + iObj = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL ); + if ( !iObj ) + { + Wlc_NtkFree( pNtk ); pNtk = NULL; + goto finish; + } + Vec_IntPush( vAsserts, iObj ); } - Vec_IntFree( vFanins ); + // build AND of asserts + if ( Vec_IntSize(vAsserts) == 1 ) + iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter_output" ); + else + { + iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL ); + Vec_IntFill( vAsserts, 1, iObj ); + iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter_output" ); + } + Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 ); // create nameIDs - vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) ); - Vec_IntAppend( &pNtk->vNameIds, vFanins ); - Vec_IntFree( vFanins ); + vFans = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) ); + Vec_IntAppend( &pNtk->vNameIds, vFans ); + Vec_IntFree( vFans ); //Wlc_NtkReport( pNtk, NULL ); +finish: + // cleanup + Vec_IntFree(vAsserts); return pNtk; } + + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +// create error message +static inline int Smt_PrsErrorSet( Smt_Prs_t * p, char * pError, int Value ) +{ + assert( !p->ErrorStr[0] ); + sprintf( p->ErrorStr, "%s", pError ); + return Value; +} +// print error message +static inline int Smt_PrsErrorPrint( Smt_Prs_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 * Smt_PrsLoadFile( 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 int Smt_PrsRemoveComments( char * pBuffer, char * pLimit ) +{ + char * pTemp; int nCount1 = 0, nCount2 = 0; + for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ ) + { + if ( *pTemp == '(' ) + nCount1++; + else if ( *pTemp == ')' ) + nCount2++; + else if ( *pTemp == ';' ) + while ( *pTemp && *pTemp != '\n' ) + *pTemp++ = ' '; + } + if ( nCount1 != nCount2 ) + printf( "The input SMTLIB file has different number of opening and closing parentheses (%d and %d).\n", nCount1, nCount2 ); + else if ( nCount1 == 0 ) + printf( "The input SMTLIB file has no opening or closing parentheses.\n" ); + return nCount1 == nCount2 ? nCount1 : 0; +} +static inline Smt_Prs_t * Smt_PrsAlloc( char * pFileName, char * pBuffer, char * pLimit, int nObjs ) +{ + Smt_Prs_t * p; + if ( nObjs == 0 ) + return NULL; + p = ABC_CALLOC( Smt_Prs_t, 1 ); + p->pName = pFileName; + p->pBuffer = pBuffer; + p->pLimit = pLimit; + p->pCur = pBuffer; + p->pStrs = Abc_NamStart( 1000, 24 ); + Smt_AddTypes( p->pStrs ); + Vec_IntGrow( &p->vStack, 100 ); + //Vec_WecGrow( &p->vDepth, 100 ); + Vec_WecGrow( &p->vObjs, nObjs+1 ); + return p; +} +static inline void Smt_PrsFree( Smt_Prs_t * p ) +{ + if ( p->pStrs ) + Abc_NamDeref( p->pStrs ); + Vec_IntErase( &p->vStack ); + //Vec_WecErase( &p->vDepth ); + Vec_WecErase( &p->vObjs ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Smt_PrsIsSpace( char c ) +{ + return c == ' ' || c == '\t' || c == '\r' || c == '\n'; +} +static inline void Smt_PrsSkipSpaces( Smt_Prs_t * p ) +{ + while ( Smt_PrsIsSpace(*p->pCur) ) + p->pCur++; +} +static inline void Smt_PrsSkipNonSpaces( Smt_Prs_t * p ) +{ + while ( p->pCur < p->pLimit && !Smt_PrsIsSpace(*p->pCur) && *p->pCur != '(' && *p->pCur != ')' ) + p->pCur++; +} +void Smt_PrsReadLines( Smt_Prs_t * p ) +{ + assert( Vec_IntSize(&p->vStack) == 0 ); + //assert( Vec_WecSize(&p->vDepth) == 0 ); + assert( Vec_WecSize(&p->vObjs) == 0 ); + // add top node at level 0 + //Vec_WecPushLevel( &p->vDepth ); + //Vec_WecPush( &p->vDepth, Vec_IntSize(&p->vStack), Vec_WecSize(&p->vObjs) ); + // add top node + Vec_IntPush( &p->vStack, Vec_WecSize(&p->vObjs) ); + Vec_WecPushLevel( &p->vObjs ); + // add other nodes + for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ ) + { + Smt_PrsSkipSpaces( p ); + if ( *p->pCur == '(' ) + { + // add new node at this depth + //assert( Vec_WecSize(&p->vDepth) >= Vec_IntSize(&p->vStack) ); + //if ( Vec_WecSize(&p->vDepth) == Vec_IntSize(&p->vStack) ) + // Vec_WecPushLevel(&p->vDepth); + //Vec_WecPush( &p->vDepth, Vec_IntSize(&p->vStack), Vec_WecSize(&p->vObjs) ); + // add fanin to node on the previous level + Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(Vec_WecSize(&p->vObjs), 0) ); + // add node to the stack + Vec_IntPush( &p->vStack, Vec_WecSize(&p->vObjs) ); + Vec_WecPushLevel( &p->vObjs ); + } + else if ( *p->pCur == ')' ) + { + Vec_IntPop( &p->vStack ); + } + else // token + { + char * pStart = p->pCur; + Smt_PrsSkipNonSpaces( p ); + if ( p->pCur < p->pLimit ) + { + // add fanin + int iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL ); + Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) ); + } + } + } + assert( Vec_IntSize(&p->vStack) == 1 ); + assert( Vec_WecSize(&p->vObjs) == Vec_WecCap(&p->vObjs) ); +} +void Smt_PrsPrintParser_rec( Smt_Prs_t * p, int iObj, int Depth ) +{ + Vec_Int_t * vFans; int i, Fan; + printf( "%*s(\n", Depth, "" ); + vFans = Vec_WecEntry( &p->vObjs, iObj ); + Vec_IntForEachEntry( vFans, Fan, i ) + { + if ( Abc_LitIsCompl(Fan) ) + { + printf( "%*s", Depth+2, "" ); + printf( "%s\n", Abc_NamStr(p->pStrs, Abc_Lit2Var(Fan)) ); + } + else + Smt_PrsPrintParser_rec( p, Abc_Lit2Var(Fan), Depth+4 ); + } + printf( "%*s)\n", Depth, "" ); +} +void Smt_PrsPrintParser( Smt_Prs_t * p ) +{ +// Vec_WecPrint( &p->vDepth, 0 ); + Smt_PrsPrintParser_rec( p, 0, 0 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ) { Wlc_Ntk_t * pNtk = NULL; - Prs_Smt_t * p = Prs_SmtAlloc( pFileName, pBuffer, pLimit ); + int nCount = Smt_PrsRemoveComments( pBuffer, pLimit ); + Smt_Prs_t * p = Smt_PrsAlloc( pFileName, pBuffer, pLimit, nCount ); 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 ); + Smt_PrsReadLines( p ); + //Smt_PrsPrintParser( p ); + if ( Smt_PrsErrorPrint(p) ) + pNtk = Smt_PrsBuild( p ); + Smt_PrsFree( p ); return pNtk; } Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) { Wlc_Ntk_t * pNtk = NULL; - char * pBuffer, * pLimit; - pBuffer = Prs_SmtLoadFile( pFileName, &pLimit ); + char * pBuffer, * pLimit; + pBuffer = Smt_PrsLoadFile( pFileName, &pLimit ); if ( pBuffer == NULL ) return NULL; pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit ); @@ -744,6 +893,7 @@ Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) return pNtk; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3