From 3c8c807ac16dbfc9b1960f77dd49fd244e3d718d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 26 Jan 2017 11:56:17 -0800 Subject: Improvements to SMT-LIB parser. --- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcNtk.c | 6 +- src/base/wlc/wlcReadSmt.c | 320 ++++++++++++++++++++++++++++++++++------------ 3 files changed, 243 insertions(+), 84 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 1df3e5e9..6f64b47a 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -140,6 +140,7 @@ struct Wlc_Ntk_t_ int nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type int nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting int fSmtLib; // the network comes from an SMT-LIB file + int nAssert; // the number of asserts // memory for objects Wlc_Obj_t * pObjs; int iObj; diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 6f396771..a0799ba0 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -195,14 +195,14 @@ void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins ) { assert( pObj->nFanins == 0 ); pObj->nFanins = Vec_IntSize(vFanins); - if ( Wlc_ObjHasArray(pObj) ) - pObj->pFanins[0] = (int *)Mem_FlexEntryFetch( p->pMemFanin, Vec_IntSize(vFanins) * sizeof(int) ); - memcpy( Wlc_ObjFanins(pObj), Vec_IntArray(vFanins), sizeof(int) * Vec_IntSize(vFanins) ); // special treatment of CONST, SELECT and TABLE if ( pObj->Type == WLC_OBJ_CONST ) pObj->nFanins = 0; else if ( pObj->Type == WLC_OBJ_BIT_SELECT || pObj->Type == WLC_OBJ_TABLE ) pObj->nFanins = 1; + if ( Wlc_ObjHasArray(pObj) ) + pObj->pFanins[0] = (int *)Mem_FlexEntryFetch( p->pMemFanin, Vec_IntSize(vFanins) * sizeof(int) ); + memcpy( Wlc_ObjFanins(pObj), Vec_IntArray(vFanins), sizeof(int) * Vec_IntSize(vFanins) ); } void Wlc_NtkFree( Wlc_Ntk_t * p ) { diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index d07a54c4..61d0bca8 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -219,6 +219,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) Type = WLC_OBJ_ARI_REM, *pfSigned = 1; // 40: arithmetic remainder else if ( !strcmp(pName, "bvsmod") ) Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus + else if ( !strcmp(pName, "=") ) + Type = WLC_OBJ_COMP_EQU; // 40: arithmetic modulus // else if ( !strcmp(pName, "") ) // Type = WLC_OBJ_ARI_POWER; // 41: arithmetic power else if ( !strcmp(pName, "bvneg") ) @@ -255,6 +257,8 @@ static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int } } +static inline int Smt_StrType( char * str ) { return Smt_StrToType(str, NULL); } + /**Function************************************************************* Synopsis [] @@ -274,20 +278,27 @@ static inline int Smt_PrsCreateNodeOld( Wlc_Ntk_t * pNtk, int Type, int fSigned, assert( Type > 0 ); assert( Range >= 0 ); assert( fSigned >= 0 ); - Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); - if ( fSigned ) - Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; - if ( Type == WLC_OBJ_SHIFT_RA ) - Wlc_NtkObj(pNtk, iObj)->Signed = 1; + + // add node's name if ( pName == NULL ) { sprintf( Buffer, "_n%d_", iObj ); pName = Buffer; } - // add node's name NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); assert( !fFound ); assert( iObj == NameId ); + + 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; + } + return iObj; } static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) @@ -302,8 +313,7 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in assert( Range >= 0 ); assert( fSigned >= 0 ); - // allow more than 2 fanins for specific operators - // if (Vec_IntSize(vFanins)<=2 || Type == WLC_OBJ_BIT_CONCAT || Type == WLC_OBJ_MUX ) + //if (Vec_IntSize(vFanins)<=2 || Type == WLC_OBJ_BIT_CONCAT || Type == WLC_OBJ_MUX ) // explicitely secify allowed multi operators if (Vec_IntSize(vFanins)<=2 || !( Type == WLC_OBJ_BIT_AND || // 16:`` bitwise AND @@ -362,17 +372,17 @@ FINISHED_WITH_FANINS: Vec_IntFree(v2Fanins); - // to deal with long shifts create extra bit select (ROTATE as well ??) + //added to deal with long shifts create extra bit select (ROTATE as well ??) // this is a temporary hack - // basically we keep only 32 bits. - // bits 0 - 30 are kept same as original - // bit 31 will be the reduction or of all bits from 31 to Range-1 + // basically we keep only 32 bits. + // bit[31] will be the copy of original MSB (sign bit, just in case) UPDATE: assume it is unsigned first???? + // bit[31] will be the reduction or of any bits from [31] to Range if (Type == WLC_OBJ_SHIFT_R || Type == WLC_OBJ_SHIFT_RA || Type == WLC_OBJ_SHIFT_L) { - int iFanin1 = Vec_IntEntry(vFanins,1); - int range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) ); - int iObj1, iObj2, iObj3; + int range1, iObj1, iObj2, iObj3; assert(Vec_IntSize(vFanins)>=2); + iFanin1 = Vec_IntEntry(vFanins,1); + range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) ); if (range1>32) { Vec_Int_t * newFanins = Vec_IntAlloc(10); @@ -389,6 +399,8 @@ FINISHED_WITH_FANINS: Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj1), newFanins ); + //printf("obj1: %d\n",iObj1); + // bit select of larger bits Vec_IntPop(newFanins); Vec_IntPop(newFanins); @@ -402,6 +414,7 @@ FINISHED_WITH_FANINS: assert( iObj2 == NameId ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj2), newFanins ); + //printf("obj2: %d\n",iObj2); // reduction or Vec_IntPop( newFanins ); @@ -416,6 +429,7 @@ FINISHED_WITH_FANINS: assert( iObj3 == NameId ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj3), newFanins ); + //printf("obj3: %d\n",iObj3); // concat all together Vec_IntWriteEntry( newFanins, 0, iObj3 ); @@ -429,6 +443,7 @@ FINISHED_WITH_FANINS: assert( iObj == NameId ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), newFanins ); + //printf("obj: %d\n",iObj); // pushing the new node Vec_IntWriteEntry(vFanins, 1, iObj); @@ -461,34 +476,22 @@ FINISHED_WITH_FANINS: return iObj; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ static inline char * Smt_GetHexFromDecimalString(char * pStr) { int i,k=0, nDigits = strlen(pStr); int digit, carry = 0; - int metNonZeroBit; - int nBits; - char * hex; + int metNonZeroBit = 0; Vec_Int_t * decimal = Vec_IntAlloc(nDigits); Vec_Int_t * rev; + int nBits; + char * hex; for (i=0;i= '0' && pStr[0] <= '9' ) { + // added: sanity check for large constants + /* + Vec_Int_t * temp = Vec_IntAlloc(10); + int fullBits = -1; + Smt_GetBinaryFromDecimalString(pStr,temp,&fullBits); + Vec_IntFree(temp); + assert(fullBits < 32);*/ + + char * pHex = Smt_GetHexFromDecimalString(pStr); + + if ( nBits == -1 ) + nBits = strlen(pHex)*4; + + //printf("nbits: %d\n",nBits); + + Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); + nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pHex ); + ABC_FREE( pHex ); + /* int w, nWords, Number = atoi( pStr ); if ( nBits == -1 ) @@ -589,15 +616,6 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits for ( w = 0; w < nWords; w++ ) Vec_IntPush( vFanins, w ? 0 : Number ); */ - - // convert decimal to hex to parse large constants - char * pHex = Smt_GetHexFromDecimalString(pStr); - - if ( nBits == -1 ) - nBits = strlen(pHex)*4; - - Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); - nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pHex ); } else { @@ -648,12 +666,6 @@ int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut, // s3087 int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); assert( fFound ); - // create buffer if the name of the fanin has different name - if ( pName && strcmp(pStr, pName) ) - { - Vec_IntFill( &p->vTempFans, 1, iObj ); - iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, RangeOut, &p->vTempFans, pName ); - } return iObj; } } @@ -804,13 +816,6 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p ) // skip () Fan = Vec_IntEntry(vFans, 2); assert( !Smt_EntryIsName(Fan) ); - vFans2 = Smt_VecEntryNode(p, vFans, 2); - if ( Vec_IntSize(vFans2) > 0 ) - { - printf( "File parsing error: Uninterpreted functions are not supported.\n" ); - Wlc_NtkFree( pNtk ); pNtk = NULL; - goto finish; - } // check type (Bool or BitVec) Fan = Vec_IntEntry(vFans, 3); if ( Smt_EntryIsName(Fan) ) @@ -1006,6 +1011,14 @@ char * Smt_PrsGenName( Smt_Prs_t * p ) } int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, char * pName ) { + char suffix[100]; + sprintf(suffix,"_as%d",pNtk->nAssert); + + //char * prepStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); + //printf("prestr: %s\n",prepStr); + + //printf("inode: %d %d\n",iNode,Smt_EntryIsName(iNode)); + if ( Smt_EntryIsName(iNode) ) { char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); @@ -1018,7 +1031,27 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, return Smt_PrsBuildConstant( pNtk, pStr, -1, pName ? pName : Smt_PrsGenName(p) ); else { - int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); + int fFound, iObj; + // look either for global DECLARE-FUN variable or local LET + char * pStr_glb = (char *)malloc(strlen(pStr) + 4 +1); //glb + char * pStr_loc = (char *)malloc(strlen(pStr) + strlen(suffix) +1); + strcpy(pStr_glb,pStr); + strcat(pStr_glb,"_glb"); + strcpy(pStr_loc,pStr); + strcat(pStr_loc,suffix); + + fFound = Abc_NamStrFind( pNtk->pManName, pStr_glb ); + + if (fFound) + pStr = pStr_glb; + else + { + assert( Abc_NamStrFind( pNtk->pManName, pStr_loc )); + pStr = pStr_loc; + } + // FIXME: delete memory of pStr + + iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); assert( fFound ); // create buffer if the name of the fanin has different name if ( pName && strcmp(Wlc_ObjName(pNtk, iObj), pName) ) @@ -1026,9 +1059,11 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, Vec_IntFill( &p->vTempFans, 1, iObj ); iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName ); } + ABC_FREE( pStr_glb ); + ABC_FREE( pStr_loc ); return iObj; } - } + } else { Vec_Int_t * vRoots, * vRoots1, * vFans3; @@ -1039,7 +1074,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, if ( Smt_EntryIsName(iRoot0) ) { char * pName2, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0)); - if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET ) + if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET || Abc_Lit2Var(iRoot0) == SMT_PRS_DEFINE_FUN) //added define-fun is similar to let { // let ((s35550 (bvor s48 s35549))) assert( Vec_IntSize(vRoots) == 3 ); @@ -1051,6 +1086,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, // iterate through the parts Vec_IntForEachEntry( vRoots1, Fan, k ) { + char * temp; // s35550 (bvor s48 s35549) assert( !Smt_EntryIsName(Fan) ); vFans3 = Smt_EntryNode(p, Fan); @@ -1059,11 +1095,26 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, Fan3 = Vec_IntEntry(vFans3, 0); assert( Smt_EntryIsName(Fan3) ); pName2 = Smt_EntryName(p, Fan3); + // create a local name with suffix + if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET ) + { + temp = (char *)malloc(strlen(pName2) + strlen(suffix) + 1); + strcpy(temp, pName2); + strcat(temp,suffix); + } + else + { temp = (char *)malloc(strlen(pName2) + 4 + 1); + strcpy(temp, pName2); + strcat(temp,"_glb"); + } + // FIXME: need to delete memory of pName2 + pName2 = temp; // get function Fan3 = Vec_IntEntry(vFans3, 1); //assert( !Smt_EntryIsName(Fan3) ); // solve the problem iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1, pName2 ); // NULL ); //pName2 ); + ABC_FREE( temp ); if ( iObj == 0 ) return 0; // create buffer @@ -1133,7 +1184,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 ); if ( iObj ) return iObj; - Type0 = Smt_StrToType( pStr0, &fSigned ); if ( Type0 == 0 ) return 0; @@ -1151,7 +1201,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, } Vec_IntPush( vFanins, iObj ); } - // find range Range = 0; if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR ) @@ -1197,7 +1246,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) Wlc_Ntk_t * pNtk; Vec_Int_t * vFansRoot, * vFans, * vFans2; Vec_Int_t * vAsserts = Vec_IntAlloc(100); - int i, Root, Fan, iObj, NameId, Range, Status, nBits = 0; + int i, Root, Fan, iObj, NameId, Range, nBits = 0; char * pName, * pRange; // start network and create primary inputs pNtk = Wlc_NtkAlloc( p->pName, 1000 ); @@ -1214,22 +1263,22 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) // create variables if ( Abc_Lit2Var(Fan) == SMT_PRS_DECLARE_FUN ) { + char * pName_glb; 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); + // added: giving a global suffix + pName_glb = (char *) malloc(strlen(pName) + 4 + 1); + strcpy(pName_glb,pName); + strcat(pName_glb,"_glb"); + // FIXME: delete memory of pName + pName = pName_glb; // skip () Fan = Vec_IntEntry(vFans, 2); assert( !Smt_EntryIsName(Fan) ); - vFans2 = Smt_VecEntryNode(p, vFans, 2); - if ( Vec_IntSize(vFans2) > 0 ) - { - printf( "File parsing error: Uninterpreted functions are not supported.\n" ); - Wlc_NtkFree( pNtk ); pNtk = NULL; - goto finish; - } // check type (Bool or BitVec) Fan = Vec_IntEntry(vFans, 3); if ( Smt_EntryIsName(Fan) ) @@ -1259,9 +1308,11 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) Vec_IntPush( &pNtk->vValues, nBits ); Vec_IntPush( &pNtk->vValues, Range ); nBits += Range; + ABC_FREE( pName_glb ); } // create constants - else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) + /* + else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) // added: we parse DEFINE_FUN in LET { assert( Vec_IntSize(vFans) == 5 ); assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); @@ -1269,6 +1320,14 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) Fan = Vec_IntEntry(vFans, 1); assert( Smt_EntryIsName(Fan) ); pName = Smt_EntryName(p, Fan); + + // added: giving a global suffix + char * pName_glb = (char *) malloc(strlen(pName) + 4 + 1); + strcpy(pName_glb,pName); + strcat(pName_glb,"_glb"); + // FIXME: delete memory of pName + pName = pName_glb; + // skip () Fan = Vec_IntEntry(vFans, 2); assert( !Smt_EntryIsName(Fan) ); @@ -1278,13 +1337,17 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) { // (define-fun s_2 () Bool false) assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); - iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), -1, pName ); - if ( iObj == 0 ) - { - Wlc_NtkFree( pNtk ); pNtk = NULL; - goto finish; - } - continue; + Range = 1; + pValue = Smt_VecEntryName(p, vFans, 4); + + //printf("value: %s\n",pValue); + + if ( !strcmp("false", pValue) ) + pValue = "#b0"; + else if ( !strcmp("true", pValue) ) + pValue = "#b1"; + else assert( 0 ); + Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName ); } else { @@ -1292,6 +1355,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) // (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 ); @@ -1299,11 +1363,24 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) 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); + + // added: can parse functions too + Vec_Int_t * vFans3 = Smt_VecEntryNode(p, vFans, 4); + Fan = Vec_IntEntry(vFans3, 0); + // get constant - Fan = Vec_IntEntry(vFans, 4); + //Fan = Vec_IntEntry(vFans, 4); + + //printf("fan3: %s\n",Fan); + //printf("fan0: %s\n",Smt_VecEntryName(p, vFans3, 0)); + //printf("fan1: %s\n",Smt_VecEntryName(p, vFans3, 1)); + //printf("fan2: %s\n",Smt_VecEntryName(p, vFans3, 2)); + //printf("fan3: %s\n",Smt_VecEntryName(p, vFans3, 3)); + Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName ); } if ( !Status ) @@ -1312,6 +1389,57 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) goto finish; } } + */ + // added: new way to parse define-fun + // create constants + else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) + { + char * pName_glb; + // (define-fun def_16001 () Bool (or def_15999 def_16000)) + // (define-fun def_15990 () (_ BitVec 24) (concat def_15988 def_15989)) + assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); + assert( Vec_IntSize(vFans) == 5 ); // const or definition + + // get name + Fan = Vec_IntEntry(vFans, 1); + assert( Smt_EntryIsName(Fan) ); + pName = Smt_EntryName(p, Fan); + // added: giving a global suffix + pName_glb = (char *) malloc(strlen(pName) + 4 + 1); + strcpy(pName_glb,pName); + strcat(pName_glb,"_glb"); + // FIXME: delete memory of pName + pName = pName_glb; + + //get range + Fan = Vec_IntEntry(vFans, 3); + if ( Smt_EntryIsName(Fan) ) + { + // (define-fun s_2 () Bool false) + assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); + Range = 1; + } + else + { + // (define-fun s702 () (_ BitVec 4) #xe) + // (define-fun s1 () (_ BitVec 8) (bvneg #x7f)) + 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); + } + + iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), Range, pName ); + assert( iObj ); + ABC_FREE( pName_glb ); + } + // collect assertion outputs else if ( Abc_Lit2Var(Fan) == SMT_PRS_ASSERT ) { @@ -1321,6 +1449,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) //(assert (not (= s0 #x00))) assert( Vec_IntSize(vFans) == 2 ); assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) ); + pNtk->nAssert++; // added iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL ); if ( iObj == 0 ) { @@ -1336,6 +1465,9 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) // build AND of asserts if ( Vec_IntSize(vAsserts) == 1 ) iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter" ); + // added: 0 asserts + else if ( Vec_IntSize(vAsserts) == 0 ) + iObj = Smt_PrsBuildConstant( pNtk, "#b1", 1, "miter" ); else { iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL ); @@ -1413,18 +1545,35 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit ) static inline int Smt_PrsRemoveComments( char * pBuffer, char * pLimit ) { char * pTemp; int nCount1 = 0, nCount2 = 0, fHaveBar = 0; + int backslash = 0; for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ ) { if ( *pTemp == '(' ) - nCount1++; + { if ( !fHaveBar ) nCount1++; } else if ( *pTemp == ')' ) - nCount2++; + { if ( !fHaveBar ) nCount2++; } else if ( *pTemp == '|' ) fHaveBar ^= 1; else if ( *pTemp == ';' && !fHaveBar ) while ( *pTemp && *pTemp != '\n' ) *pTemp++ = ' '; + // added: hack to remove quotes + else if ( *pTemp == '\"' && *(pTemp-1) != '\\' && !fHaveBar ) + { + *pTemp++ = ' '; + while ( *pTemp && (*pTemp != '\"' || backslash)) + { + if (*pTemp == '\\') + backslash = 1; + else + backslash = 0; + *pTemp++ = ' '; + } + // remove the last quote symbol + *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 ) @@ -1455,7 +1604,6 @@ static inline void Smt_PrsFree( Smt_Prs_t * p ) Vec_IntErase( &p->vStack ); Vec_IntErase( &p->vTempFans ); //Vec_WecErase( &p->vDepth ); - Vec_WecErase( &p->vObjs ); ABC_FREE( p ); } @@ -1499,6 +1647,15 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ ) { Smt_PrsSkipSpaces( p ); + if ( *p->pCur == '|' ) + { + *p->pCur = ' '; + while ( *p->pCur && *p->pCur != '|' ) + *p->pCur++ = ' '; + if ( *p->pCur == '|' ) + *p->pCur = ' '; + continue; + } if ( *p->pCur == '(' ) { // add new node at this depth @@ -1524,12 +1681,13 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) { // remove strange characters (this can lead to name clashes) int iToken; + /* commented out for SMT comp char * pTemp; if ( *pStart == '?' ) *pStart = '_'; for ( pTemp = pStart; pTemp < p->pCur; pTemp++ ) if ( *pTemp == '.' ) - *pTemp = '_'; + *pTemp = '_';*/ // create and save token for this string iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL ); Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) ); -- cgit v1.2.3