diff options
| -rw-r--r-- | src/base/wlc/wlc.h | 73 | ||||
| -rw-r--r-- | src/base/wlc/wlcBlast.c | 14 | ||||
| -rw-r--r-- | src/base/wlc/wlcCom.c | 16 | ||||
| -rw-r--r-- | src/base/wlc/wlcNtk.c | 71 | ||||
| -rw-r--r-- | src/base/wlc/wlcReadSmt.c | 92 | ||||
| -rw-r--r-- | src/base/wlc/wlcReadVer.c | 1 | ||||
| -rw-r--r-- | src/base/wlc/wlcStdin.c | 2 | ||||
| -rw-r--r-- | src/base/wlc/wlcWriteVer.c | 2 |
8 files changed, 164 insertions, 107 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 305a896d..b12e239c 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -61,40 +61,41 @@ typedef enum { WLC_OBJ_BIT_AND, // 16: bitwise AND WLC_OBJ_BIT_OR, // 17: bitwise OR WLC_OBJ_BIT_XOR, // 18: bitwise XOR - WLC_OBJ_BIT_NAND, // 16: bitwise AND - WLC_OBJ_BIT_NOR, // 17: bitwise OR - WLC_OBJ_BIT_NXOR, // 19: bitwise NXOR - WLC_OBJ_BIT_SELECT, // 20: bit selection - WLC_OBJ_BIT_CONCAT, // 21: bit concatenation - WLC_OBJ_BIT_ZEROPAD, // 22: zero padding - WLC_OBJ_BIT_SIGNEXT, // 23: sign extension - WLC_OBJ_LOGIC_NOT, // 24: logic NOT - WLC_OBJ_LOGIC_AND, // 25: logic AND - WLC_OBJ_LOGIC_OR, // 27: logic OR - WLC_OBJ_LOGIC_XOR, // 28: logic XOR - WLC_OBJ_COMP_EQU, // 29: compare equal - WLC_OBJ_COMP_NOTEQU, // 30: compare not equal - WLC_OBJ_COMP_LESS, // 31: compare less - WLC_OBJ_COMP_MORE, // 32: compare more - WLC_OBJ_COMP_LESSEQU, // 33: compare less or equal - WLC_OBJ_COMP_MOREEQU, // 34: compare more or equal - WLC_OBJ_REDUCT_AND, // 35: reduction AND - WLC_OBJ_REDUCT_OR, // 36: reduction OR - WLC_OBJ_REDUCT_XOR, // 37: reduction XOR - WLC_OBJ_REDUCT_NAND, // 38: reduction NAND - WLC_OBJ_REDUCT_NOR, // 39: reduction NOR - WLC_OBJ_REDUCT_NXOR, // 40: reduction NXOR - WLC_OBJ_ARI_ADD, // 41: arithmetic addition - WLC_OBJ_ARI_SUB, // 42: arithmetic subtraction - WLC_OBJ_ARI_MULTI, // 43: arithmetic multiplier - WLC_OBJ_ARI_DIVIDE, // 44: arithmetic division - WLC_OBJ_ARI_MODULUS, // 45: arithmetic modulus - WLC_OBJ_ARI_POWER, // 46: arithmetic power - WLC_OBJ_ARI_MINUS, // 47: arithmetic minus - WLC_OBJ_ARI_SQRT, // 48: integer square root - WLC_OBJ_ARI_SQUARE, // 49: integer square - WLC_OBJ_TABLE, // 50: bit table - WLC_OBJ_NUMBER // 51: unused + WLC_OBJ_BIT_NAND, // 19: bitwise AND + WLC_OBJ_BIT_NOR, // 20: bitwise OR + WLC_OBJ_BIT_NXOR, // 21: bitwise NXOR + WLC_OBJ_BIT_SELECT, // 22: bit selection + WLC_OBJ_BIT_CONCAT, // 23: bit concatenation + WLC_OBJ_BIT_ZEROPAD, // 24: zero padding + WLC_OBJ_BIT_SIGNEXT, // 25: sign extension + WLC_OBJ_LOGIC_NOT, // 26: logic NOT + WLC_OBJ_LOGIC_IMPL, // 27: logic implication + WLC_OBJ_LOGIC_AND, // 28: logic AND + WLC_OBJ_LOGIC_OR, // 29: logic OR + WLC_OBJ_LOGIC_XOR, // 30: logic XOR + WLC_OBJ_COMP_EQU, // 31: compare equal + WLC_OBJ_COMP_NOTEQU, // 32: compare not equal + WLC_OBJ_COMP_LESS, // 33: compare less + WLC_OBJ_COMP_MORE, // 34: compare more + WLC_OBJ_COMP_LESSEQU, // 35: compare less or equal + WLC_OBJ_COMP_MOREEQU, // 36: compare more or equal + WLC_OBJ_REDUCT_AND, // 37: reduction AND + WLC_OBJ_REDUCT_OR, // 38: reduction OR + WLC_OBJ_REDUCT_XOR, // 39: reduction XOR + WLC_OBJ_REDUCT_NAND, // 40: reduction NAND + WLC_OBJ_REDUCT_NOR, // 41: reduction NOR + WLC_OBJ_REDUCT_NXOR, // 42: reduction NXOR + WLC_OBJ_ARI_ADD, // 43: arithmetic addition + WLC_OBJ_ARI_SUB, // 44: arithmetic subtraction + WLC_OBJ_ARI_MULTI, // 45: arithmetic multiplier + WLC_OBJ_ARI_DIVIDE, // 46: arithmetic division + WLC_OBJ_ARI_MODULUS, // 47: arithmetic modulus + WLC_OBJ_ARI_POWER, // 48: arithmetic power + WLC_OBJ_ARI_MINUS, // 49: arithmetic minus + WLC_OBJ_ARI_SQRT, // 50: integer square root + WLC_OBJ_ARI_SQUARE, // 51: integer square + WLC_OBJ_TABLE, // 52: bit table + WLC_OBJ_NUMBER // 53: unused } Wlc_ObjType_t; // when adding new types, remember to update table Wlc_Names in "wlcNtk.c" @@ -273,8 +274,8 @@ extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ); extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p ); /*=== wlcReadSmt.c ========================================================*/ -extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ); -extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ); +extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree ); +extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree ); /*=== wlcSim.c ========================================================*/ extern Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int nFrames ); extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p ); diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 16044e67..5ef7ef14 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -777,7 +777,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple // blast in the topological order Wlc_NtkForEachObj( p, pObj, i ) { -// char * pName = Wlc_ObjName(p, i); +// char * pName1 = Wlc_ObjName(p, i); +// char * pName2 = Wlc_ObjFaninNum(pObj) ? Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) : NULL; + nAndPrev = Gia_ManAndNum(pNew); nRange = Wlc_ObjRange( pObj ); nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1; @@ -1007,7 +1009,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple else if ( pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT ) { int Pad = pObj->Type == WLC_OBJ_BIT_ZEROPAD ? 0 : pFans0[nRange0-1]; - assert( nRange0 < nRange ); + assert( nRange0 <= nRange ); for ( k = 0; k < nRange0; k++ ) Vec_IntPush( vRes, pFans0[k] ); for ( ; k < nRange; k++ ) @@ -1020,6 +1022,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple for ( k = 1; k < nRange; k++ ) Vec_IntPush( vRes, 0 ); } + else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL ) + { + int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR ); + int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR ); + Vec_IntFill( vRes, 1, Gia_ManHashOr(pNew, Abc_LitNot(iLit0), iLit1) ); + for ( k = 1; k < nRange; k++ ) + Vec_IntPush( vRes, 0 ); + } else if ( pObj->Type == WLC_OBJ_LOGIC_AND ) { int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR ); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index bbb897ea..4bdb66c2 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -119,12 +119,20 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pFile; Wlc_Ntk_t * pNtk = NULL; char * pFileName = NULL; + int fOldParser = 0; + int fPrintTree = 0; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF ) { switch ( c ) { + case 'o': + fPrintTree ^= 1; + break; + case 'p': + fOldParser ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -155,7 +163,7 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) pNtk = Wlc_ReadVer( pFileName ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" ) || !strcmp( Extra_FileNameExtension(pFileName), "smt2" ) ) - pNtk = Wlc_ReadSmt( pFileName ); + pNtk = Wlc_ReadSmt( pFileName, fOldParser, fPrintTree ); else { printf( "Abc_CommandReadWlc(): Unknown file extension.\n" ); @@ -164,8 +172,10 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_AbcUpdateNtk( pAbc, pNtk ); return 0; usage: - Abc_Print( -2, "usage: %%read [-vh] <file_name>\n" ); + Abc_Print( -2, "usage: %%read [-opvh] <file_name>\n" ); Abc_Print( -2, "\t reads word-level design from Verilog file\n" ); + Abc_Print( -2, "\t-o : toggle using old SMT-LIB parser [default = %s]\n", fOldParser? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle printing parse SMT-LIB tree [default = %s]\n", fPrintTree? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index c4f9ac70..726e7bf8 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -50,40 +50,41 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = { "&", // 16: bitwise AND "|", // 17: bitwise OR "^", // 18: bitwise XOR - "~&", // 16: bitwise NAND - "~|", // 17: bitwise NOR - "~^", // 19: bitwise NXOR - "[:]", // 20: bit selection - "{,}", // 21: bit concatenation - "zeroPad", // 22: zero padding - "signExt", // 23: sign extension - "!", // 24: logic NOT - "&&", // 25: logic AND - "||", // 27: logic OR - "^^", // 28: logic XOR - "==", // 29: compare equal - "!=", // 30: compare not equal - "<", // 31: compare less - ">", // 32: compare more - "<=", // 33: compare less or equal - ">=", // 34: compare more or equal - "&", // 35: reduction AND - "|", // 36: reduction OR - "^", // 37: reduction XOR - "~&", // 38: reduction NAND - "~|", // 39: reduction NOR - "~^", // 40: reduction NXOR - "+", // 41: arithmetic addition - "-", // 42: arithmetic subtraction - "*", // 43: arithmetic multiplier - "/", // 44: arithmetic division - "%", // 45: arithmetic modulus - "**", // 46: arithmetic power - "-", // 47: arithmetic minus - "sqrt", // 48: integer square root - "square", // 49: integer square - "table", // 50: bit table - NULL // 51: unused + "~&", // 19: bitwise NAND + "~|", // 20: bitwise NOR + "~^", // 21: bitwise NXOR + "[:]", // 22: bit selection + "{,}", // 23: bit concatenation + "zeroPad", // 24: zero padding + "signExt", // 25: sign extension + "!", // 26: logic NOT + "=>", // 27: logic implication + "&&", // 28: logic AND + "||", // 29: logic OR + "^^", // 30: logic XOR + "==", // 31: compare equal + "!=", // 32: compare not equal + "<", // 33: compare less + ">", // 34: compare more + "<=", // 35: compare less or equal + ">=", // 36: compare more or equal + "&", // 37: reduction AND + "|", // 38: reduction OR + "^", // 39: reduction XOR + "~&", // 40: reduction NAND + "~|", // 41: reduction NOR + "~^", // 42: reduction NXOR + "+", // 43: arithmetic addition + "-", // 44: arithmetic subtraction + "*", // 45: arithmetic multiplier + "/", // 46: arithmetic division + "%", // 47: arithmetic modulus + "**", // 48: arithmetic power + "-", // 49: arithmetic minus + "sqrt", // 50: integer square root + "square", // 51: integer square + "table", // 52: bit table + NULL // 53: unused }; //////////////////////////////////////////////////////////////////////// @@ -380,6 +381,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose ) Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_SIGNEXT, 0 ); else if ( pObj->Type == WLC_OBJ_LOGIC_NOT ) Vec_IntAddToEntry( vAnds, WLC_OBJ_LOGIC_NOT, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 ); + else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL ) + Vec_IntAddToEntry( vAnds, WLC_OBJ_LOGIC_IMPL, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) + Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)) - 1 ); else if ( pObj->Type == WLC_OBJ_LOGIC_AND ) Vec_IntAddToEntry( vAnds, WLC_OBJ_LOGIC_AND, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) + Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)) - 1 ); else if ( pObj->Type == WLC_OBJ_LOGIC_OR ) diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 3a782257..d68688c4 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -169,6 +169,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) Type = WLC_OBJ_BIT_SIGNEXT, *pfSigned = 1; // 22: sign extension else if ( !strcmp(pName, "not") ) Type = WLC_OBJ_LOGIC_NOT; // 23: logic NOT + else if ( !strcmp(pName, "=>") ) + Type = WLC_OBJ_LOGIC_IMPL; // 24: logic AND else if ( !strcmp(pName, "and") ) Type = WLC_OBJ_LOGIC_AND; // 24: logic AND else if ( !strcmp(pName, "or") ) @@ -701,17 +703,28 @@ char * Smt_PrsGenName( Smt_Prs_t * p ) sprintf( Buffer, "_%0*X_", p->nDigits, ++p->NameCount ); return Buffer; } -int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev ) +int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, char * pName ) { if ( Smt_EntryIsName(iNode) ) { char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); + // handle built-in constants + if ( !strcmp(pStr, "false") ) + pStr = "#b0"; + else if ( !strcmp(pStr, "true") ) + pStr = "#b1"; if ( pStr[0] == '#' ) - return Smt_PrsBuildConstant( pNtk, pStr, -1, Smt_PrsGenName(p) ); + return Smt_PrsBuildConstant( pNtk, pStr, -1, pName ? pName : Smt_PrsGenName(p) ); else { 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(Wlc_ObjName(pNtk, iObj), pName) ) + { + Vec_IntFill( &p->vTempFans, 1, iObj ); + iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName ); + } return iObj; } } @@ -724,7 +737,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev iRoot0 = Vec_IntEntry( vRoots, 0 ); if ( Smt_EntryIsName(iRoot0) ) { - char * pName, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0)); + char * pName2, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0)); if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET ) { // let ((s35550 (bvor s48 s35549))) @@ -744,21 +757,21 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev // get the name Fan3 = Vec_IntEntry(vFans3, 0); assert( Smt_EntryIsName(Fan3) ); - pName = Smt_EntryName(p, Fan3); + pName2 = Smt_EntryName(p, Fan3); // get function Fan3 = Vec_IntEntry(vFans3, 1); - assert( !Smt_EntryIsName(Fan3) ); + //assert( !Smt_EntryIsName(Fan3) ); // solve the problem - iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1 ); + iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1, pName2 ); // NULL ); //pName2 ); if ( iObj == 0 ) return 0; // create buffer - Vec_IntFill( &p->vTempFans, 1, iObj ); - Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, &p->vTempFans, pName ); + //Vec_IntFill( &p->vTempFans, 1, iObj ); + //Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName2 ); } - // pricess the final part of let + // process the final part of let iRoot2 = Vec_IntEntry(vRoots, 2); - return Smt_PrsBuild2_rec( pNtk, p, iRoot2, -1 ); + return Smt_PrsBuild2_rec( pNtk, p, iRoot2, -1, pName ); } else if ( pStr0[0] == '_' ) { @@ -768,7 +781,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev // (_ bv1 32) char * pStr2 = Smt_VecEntryName( p, vRoots, 2 ); assert( Vec_IntSize(vRoots) == 3 ); - return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), Smt_PrsGenName(p) ); + return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), pName ? pName : Smt_PrsGenName(p) ); } else { @@ -777,16 +790,23 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev Type1 = Smt_StrToType( pStr1, &fSigned ); if ( Type1 == 0 ) return 0; - Vec_IntFill( &p->vTempFans, 1, iObjPrev ); // find out this branch + Vec_IntFill( &p->vTempFans, 1, iObjPrev ); if ( Type1 == WLC_OBJ_BIT_SIGNEXT || Type1 == WLC_OBJ_BIT_ZEROPAD || Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L ) { int iRoot2 = Vec_IntEntry(vRoots, 2); char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2)); int Num = atoi( pStr2 ); fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT); - Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) ); - Vec_IntPush( &p->vTempFans, Num ); + if ( Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L ) + { + int iConst = Smt_PrsBuildConstant( pNtk, pStr2, -1, Smt_PrsGenName(p) ); + Vec_IntClear( &p->vTempFans ); + Vec_IntPushTwo( &p->vTempFans, iObjPrev, iConst ); + Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) ); + } + else + Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) ); } else if ( Type1 == WLC_OBJ_BIT_SELECT ) { @@ -797,12 +817,11 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev int Num1 = atoi( pStr2 ); int Num2 = atoi( pStr3 ); assert( Num1 >= Num2 ); - fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT); Range = Num1 - Num2 + 1; Vec_IntPushTwo( &p->vTempFans, Num1, Num2 ); } else assert( 0 ); - iObj = Smt_PrsCreateNode( pNtk, Type1, fSigned, Range, &p->vTempFans, Smt_PrsGenName(p) ); + iObj = Smt_PrsCreateNode( pNtk, Type1, fSigned, Range, &p->vTempFans, pName ? pName : Smt_PrsGenName(p) ); return iObj; } } @@ -822,7 +841,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev vFanins = Vec_IntAlloc( 100 ); Vec_IntForEachEntryStart( vRoots, Fan, i, 1 ) { - iObj = Smt_PrsBuild2_rec( pNtk, p, Fan, -1 ); + iObj = Smt_PrsBuild2_rec( pNtk, p, Fan, -1, NULL ); if ( iObj == 0 ) { Vec_IntFree( vFanins ); @@ -854,17 +873,17 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev } // create node assert( Range > 0 ); - iObj = Smt_PrsCreateNode( pNtk, Type0, fSigned, Range, vFanins, Smt_PrsGenName(p) ); + iObj = Smt_PrsCreateNode( pNtk, Type0, fSigned, Range, vFanins, pName ? pName : Smt_PrsGenName(p) ); Vec_IntFree( vFanins ); return iObj; } } - else if ( Vec_IntSize(vRoots) == 2 ) // possible ((_ extract 48 16) (bvmul ?v_5 ?v_12)) + else if ( Vec_IntSize(vRoots) == 2 ) // could be ((_ extract 48 16) (bvmul ?v_5 ?v_12)) { - int iObjPrev = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1), -1 ); + int iObjPrev = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1), -1, NULL ); if ( iObjPrev == 0 ) return 0; - return Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 0), iObjPrev ); + return Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 0), iObjPrev, pName ); } else assert( 0 ); // return Smt_PrsBuild2_rec( pNtk, p, iRoot0 ); return 0; @@ -992,7 +1011,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) ); - iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1 ); + iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL ); if ( iObj == 0 ) { Wlc_NtkFree( pNtk ); pNtk = NULL; @@ -1083,14 +1102,16 @@ 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; + char * pTemp; int nCount1 = 0, nCount2 = 0, fHaveBar = 0; for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ ) { if ( *pTemp == '(' ) nCount1++; else if ( *pTemp == ')' ) nCount2++; - else if ( *pTemp == ';' ) + else if ( *pTemp == '|' ) + fHaveBar ^= 1; + else if ( *pTemp == ';' && !fHaveBar ) while ( *pTemp && *pTemp != '\n' ) *pTemp++ = ' '; } @@ -1191,8 +1212,16 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) Smt_PrsSkipNonSpaces( p ); if ( p->pCur < p->pLimit ) { - // add fanin - int iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL ); + // remove strange characters (this can lead to name clashes) + int iToken; + char * pTemp; + if ( *pStart == '?' ) + *pStart = '_'; + for ( pTemp = pStart; pTemp < p->pCur; pTemp++ ) + if ( *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) ); } } @@ -1235,7 +1264,7 @@ void Smt_PrsPrintParser( Smt_Prs_t * p ) SeeAlso [] ***********************************************************************/ -Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ) +Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree ) { Wlc_Ntk_t * pNtk = NULL; int nCount = Smt_PrsRemoveComments( pBuffer, pLimit ); @@ -1243,20 +1272,21 @@ Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ) if ( p == NULL ) return NULL; Smt_PrsReadLines( p ); - //Smt_PrsPrintParser( p ); + if ( fPrintTree ) + Smt_PrsPrintParser( p ); if ( Smt_PrsErrorPrint(p) ) - pNtk = Smt_PrsBuild2( p ); + pNtk = fOldParser ? Smt_PrsBuild(p) : Smt_PrsBuild2(p); Smt_PrsFree( p ); return pNtk; } -Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) +Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree ) { Wlc_Ntk_t * pNtk = NULL; char * pBuffer, * pLimit; pBuffer = Smt_PrsLoadFile( pFileName, &pLimit ); if ( pBuffer == NULL ) return NULL; - pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit ); + pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit, fOldParser, fPrintTree ); ABC_FREE( pBuffer ); return pNtk; } diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index e42fac42..7683f8a6 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -781,6 +781,7 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t * else if ( pStr[0] == '~' && pStr[1] == '&' ) pStr += 2, Type = WLC_OBJ_BIT_NAND; else if ( pStr[0] == '~' && pStr[1] == '|' ) pStr += 2, Type = WLC_OBJ_BIT_NOR; else if ( pStr[0] == '~' && pStr[1] == '^' ) pStr += 2, Type = WLC_OBJ_BIT_NXOR; + else if ( pStr[0] == '=' && pStr[1] == '>' ) pStr += 2, Type = WLC_OBJ_LOGIC_IMPL; else if ( pStr[0] == '&' && pStr[1] == '&' ) pStr += 2, Type = WLC_OBJ_LOGIC_AND; else if ( pStr[0] == '|' && pStr[1] == '|' ) pStr += 2, Type = WLC_OBJ_LOGIC_OR; else if ( pStr[0] == '^' && pStr[1] == '^' ) pStr += 2, Type = WLC_OBJ_LOGIC_XOR; diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c index d0249d1e..86092f95 100644 --- a/src/base/wlc/wlcStdin.c +++ b/src/base/wlc/wlcStdin.c @@ -192,7 +192,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd ) // collect stdin until (check-sat) Vec_Str_t * vInput = Wlc_StdinCollectProblem( "(check-sat)" ); // parse input - Wlc_Ntk_t * pNtk = Wlc_ReadSmtBuffer( NULL, Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput) ); + Wlc_Ntk_t * pNtk = Wlc_ReadSmtBuffer( NULL, Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput), 0, 0 ); Vec_StrFree( vInput ); // install current network Wlc_SetNtk( pAbc, pNtk ); diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c index 5f99f81b..b15d3d38 100644 --- a/src/base/wlc/wlcWriteVer.c +++ b/src/base/wlc/wlcWriteVer.c @@ -314,6 +314,8 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) fprintf( pFile, "~|" ); else if ( pObj->Type == WLC_OBJ_BIT_NXOR ) fprintf( pFile, "~^" ); + else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL ) + fprintf( pFile, "=>" ); else if ( pObj->Type == WLC_OBJ_LOGIC_AND ) fprintf( pFile, "&&" ); else if ( pObj->Type == WLC_OBJ_LOGIC_OR ) |