Skip to content

A
abc
Commit 0f29f0ae by Alan Mishchenko
Options

Improving SMT-LIB parser.

parent 34c5ac88
Showing with 164 additions and 107 deletions
src/base/wlc/wlc.h
...@@ -61,40 +61,41 @@ typedef enum { ...@@ -61,40 +61,41 @@ typedef enum {
WLC_OBJ_BIT_AND, // 16: bitwise AND WLC_OBJ_BIT_AND, // 16: bitwise AND
WLC_OBJ_BIT_OR, // 17: bitwise OR WLC_OBJ_BIT_OR, // 17: bitwise OR
WLC_OBJ_BIT_XOR, // 18: bitwise XOR WLC_OBJ_BIT_XOR, // 18: bitwise XOR
WLC_OBJ_BIT_NAND, // 16: bitwise AND WLC_OBJ_BIT_NAND, // 19: bitwise AND
WLC_OBJ_BIT_NOR, // 17: bitwise OR WLC_OBJ_BIT_NOR, // 20: bitwise OR
WLC_OBJ_BIT_NXOR, // 19: bitwise NXOR WLC_OBJ_BIT_NXOR, // 21: bitwise NXOR
WLC_OBJ_BIT_SELECT, // 20: bit selection WLC_OBJ_BIT_SELECT, // 22: bit selection
WLC_OBJ_BIT_CONCAT, // 21: bit concatenation WLC_OBJ_BIT_CONCAT, // 23: bit concatenation
WLC_OBJ_BIT_ZEROPAD, // 22: zero padding WLC_OBJ_BIT_ZEROPAD, // 24: zero padding
WLC_OBJ_BIT_SIGNEXT, // 23: sign extension WLC_OBJ_BIT_SIGNEXT, // 25: sign extension
WLC_OBJ_LOGIC_NOT, // 24: logic NOT WLC_OBJ_LOGIC_NOT, // 26: logic NOT
WLC_OBJ_LOGIC_AND, // 25: logic AND WLC_OBJ_LOGIC_IMPL, // 27: logic implication
WLC_OBJ_LOGIC_OR, // 27: logic OR WLC_OBJ_LOGIC_AND, // 28: logic AND
WLC_OBJ_LOGIC_XOR, // 28: logic XOR WLC_OBJ_LOGIC_OR, // 29: logic OR
WLC_OBJ_COMP_EQU, // 29: compare equal WLC_OBJ_LOGIC_XOR, // 30: logic XOR
WLC_OBJ_COMP_NOTEQU, // 30: compare not equal WLC_OBJ_COMP_EQU, // 31: compare equal
WLC_OBJ_COMP_LESS, // 31: compare less WLC_OBJ_COMP_NOTEQU, // 32: compare not equal
WLC_OBJ_COMP_MORE, // 32: compare more WLC_OBJ_COMP_LESS, // 33: compare less
WLC_OBJ_COMP_LESSEQU, // 33: compare less or equal WLC_OBJ_COMP_MORE, // 34: compare more
WLC_OBJ_COMP_MOREEQU, // 34: compare more or equal WLC_OBJ_COMP_LESSEQU, // 35: compare less or equal
WLC_OBJ_REDUCT_AND, // 35: reduction AND WLC_OBJ_COMP_MOREEQU, // 36: compare more or equal
WLC_OBJ_REDUCT_OR, // 36: reduction OR WLC_OBJ_REDUCT_AND, // 37: reduction AND
WLC_OBJ_REDUCT_XOR, // 37: reduction XOR WLC_OBJ_REDUCT_OR, // 38: reduction OR
WLC_OBJ_REDUCT_NAND, // 38: reduction NAND WLC_OBJ_REDUCT_XOR, // 39: reduction XOR
WLC_OBJ_REDUCT_NOR, // 39: reduction NOR WLC_OBJ_REDUCT_NAND, // 40: reduction NAND
WLC_OBJ_REDUCT_NXOR, // 40: reduction NXOR WLC_OBJ_REDUCT_NOR, // 41: reduction NOR
WLC_OBJ_ARI_ADD, // 41: arithmetic addition WLC_OBJ_REDUCT_NXOR, // 42: reduction NXOR
WLC_OBJ_ARI_SUB, // 42: arithmetic subtraction WLC_OBJ_ARI_ADD, // 43: arithmetic addition
WLC_OBJ_ARI_MULTI, // 43: arithmetic multiplier WLC_OBJ_ARI_SUB, // 44: arithmetic subtraction
WLC_OBJ_ARI_DIVIDE, // 44: arithmetic division WLC_OBJ_ARI_MULTI, // 45: arithmetic multiplier
WLC_OBJ_ARI_MODULUS, // 45: arithmetic modulus WLC_OBJ_ARI_DIVIDE, // 46: arithmetic division
WLC_OBJ_ARI_POWER, // 46: arithmetic power WLC_OBJ_ARI_MODULUS, // 47: arithmetic modulus
WLC_OBJ_ARI_MINUS, // 47: arithmetic minus WLC_OBJ_ARI_POWER, // 48: arithmetic power
WLC_OBJ_ARI_SQRT, // 48: integer square root WLC_OBJ_ARI_MINUS, // 49: arithmetic minus
WLC_OBJ_ARI_SQUARE, // 49: integer square WLC_OBJ_ARI_SQRT, // 50: integer square root
WLC_OBJ_TABLE, // 50: bit table WLC_OBJ_ARI_SQUARE, // 51: integer square
WLC_OBJ_NUMBER // 51: unused WLC_OBJ_TABLE, // 52: bit table
WLC_OBJ_NUMBER // 53: unused
} Wlc_ObjType_t; } Wlc_ObjType_t;
// when adding new types, remember to update table Wlc_Names in "wlcNtk.c" // 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 ); ...@@ -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 void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p ); extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p );
/*=== wlcReadSmt.c ========================================================*/ /*=== wlcReadSmt.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ); extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ); extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree );
/*=== wlcSim.c ========================================================*/ /*=== wlcSim.c ========================================================*/
extern Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int nFrames ); 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 ); extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p );
......
src/base/wlc/wlcBlast.c
...@@ -777,7 +777,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple ...@@ -777,7 +777,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
// blast in the topological order // blast in the topological order
Wlc_NtkForEachObj( p, pObj, i ) 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); nAndPrev = Gia_ManAndNum(pNew);
nRange = Wlc_ObjRange( pObj ); nRange = Wlc_ObjRange( pObj );
nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1; 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 ...@@ -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 ) 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]; int Pad = pObj->Type == WLC_OBJ_BIT_ZEROPAD ? 0 : pFans0[nRange0-1];
assert( nRange0 < nRange ); assert( nRange0 <= nRange );
for ( k = 0; k < nRange0; k++ ) for ( k = 0; k < nRange0; k++ )
Vec_IntPush( vRes, pFans0[k] ); Vec_IntPush( vRes, pFans0[k] );
for ( ; k < nRange; k++ ) for ( ; k < nRange; k++ )
...@@ -1020,6 +1022,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple ...@@ -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++ ) for ( k = 1; k < nRange; k++ )
Vec_IntPush( vRes, 0 ); 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 ) else if ( pObj->Type == WLC_OBJ_LOGIC_AND )
{ {
int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR ); int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
......
src/base/wlc/wlcCom.c
...@@ -119,12 +119,20 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -119,12 +119,20 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pFile; FILE * pFile;
Wlc_Ntk_t * pNtk = NULL; Wlc_Ntk_t * pNtk = NULL;
char * pFileName = NULL; char * pFileName = NULL;
int fOldParser = 0;
int fPrintTree = 0;
int c, fVerbose = 0; int c, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'o':
fPrintTree ^= 1;
break;
case 'p':
fOldParser ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
...@@ -155,7 +163,7 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -155,7 +163,7 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
pNtk = Wlc_ReadVer( pFileName ); pNtk = Wlc_ReadVer( pFileName );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" ) || !strcmp( Extra_FileNameExtension(pFileName), "smt2" ) ) else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" ) || !strcmp( Extra_FileNameExtension(pFileName), "smt2" ) )
pNtk = Wlc_ReadSmt( pFileName ); pNtk = Wlc_ReadSmt( pFileName, fOldParser, fPrintTree );
else else
{ {
printf( "Abc_CommandReadWlc(): Unknown file extension.\n" ); printf( "Abc_CommandReadWlc(): Unknown file extension.\n" );
...@@ -164,8 +172,10 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -164,8 +172,10 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_AbcUpdateNtk( pAbc, pNtk ); Wlc_AbcUpdateNtk( pAbc, pNtk );
return 0; return 0;
usage: 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 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-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
......
src/base/wlc/wlcNtk.c
...@@ -50,40 +50,41 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = { ...@@ -50,40 +50,41 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
"&", // 16: bitwise AND "&", // 16: bitwise AND
"|", // 17: bitwise OR "|", // 17: bitwise OR
"^", // 18: bitwise XOR "^", // 18: bitwise XOR
"~&", // 16: bitwise NAND "~&", // 19: bitwise NAND
"~|", // 17: bitwise NOR "~|", // 20: bitwise NOR
"~^", // 19: bitwise NXOR "~^", // 21: bitwise NXOR
"[:]", // 20: bit selection "[:]", // 22: bit selection
"{,}", // 21: bit concatenation "{,}", // 23: bit concatenation
"zeroPad", // 22: zero padding "zeroPad", // 24: zero padding
"signExt", // 23: sign extension "signExt", // 25: sign extension
"!", // 24: logic NOT "!", // 26: logic NOT
"&&", // 25: logic AND "=>", // 27: logic implication
"||", // 27: logic OR "&&", // 28: logic AND
"^^", // 28: logic XOR "||", // 29: logic OR
"==", // 29: compare equal "^^", // 30: logic XOR
"!=", // 30: compare not equal "==", // 31: compare equal
"<", // 31: compare less "!=", // 32: compare not equal
">", // 32: compare more "<", // 33: compare less
"<=", // 33: compare less or equal ">", // 34: compare more
">=", // 34: compare more or equal "<=", // 35: compare less or equal
"&", // 35: reduction AND ">=", // 36: compare more or equal
"|", // 36: reduction OR "&", // 37: reduction AND
"^", // 37: reduction XOR "|", // 38: reduction OR
"~&", // 38: reduction NAND "^", // 39: reduction XOR
"~|", // 39: reduction NOR "~&", // 40: reduction NAND
"~^", // 40: reduction NXOR "~|", // 41: reduction NOR
"+", // 41: arithmetic addition "~^", // 42: reduction NXOR
"-", // 42: arithmetic subtraction "+", // 43: arithmetic addition
"*", // 43: arithmetic multiplier "-", // 44: arithmetic subtraction
"/", // 44: arithmetic division "*", // 45: arithmetic multiplier
"%", // 45: arithmetic modulus "/", // 46: arithmetic division
"**", // 46: arithmetic power "%", // 47: arithmetic modulus
"-", // 47: arithmetic minus "**", // 48: arithmetic power
"sqrt", // 48: integer square root "-", // 49: arithmetic minus
"square", // 49: integer square "sqrt", // 50: integer square root
"table", // 50: bit table "square", // 51: integer square
NULL // 51: unused "table", // 52: bit table
NULL // 53: unused
}; };
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -380,6 +381,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose ) ...@@ -380,6 +381,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_SIGNEXT, 0 ); Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_SIGNEXT, 0 );
else if ( pObj->Type == WLC_OBJ_LOGIC_NOT ) else if ( pObj->Type == WLC_OBJ_LOGIC_NOT )
Vec_IntAddToEntry( vAnds, WLC_OBJ_LOGIC_NOT, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 ); 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 ) 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 ); 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 ) else if ( pObj->Type == WLC_OBJ_LOGIC_OR )
......
src/base/wlc/wlcReadSmt.c
...@@ -169,6 +169,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) ...@@ -169,6 +169,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
Type = WLC_OBJ_BIT_SIGNEXT, *pfSigned = 1; // 22: sign extension Type = WLC_OBJ_BIT_SIGNEXT, *pfSigned = 1; // 22: sign extension
else if ( !strcmp(pName, "not") ) else if ( !strcmp(pName, "not") )
Type = WLC_OBJ_LOGIC_NOT; // 23: logic 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") ) else if ( !strcmp(pName, "and") )
Type = WLC_OBJ_LOGIC_AND; // 24: logic AND Type = WLC_OBJ_LOGIC_AND; // 24: logic AND
else if ( !strcmp(pName, "or") ) else if ( !strcmp(pName, "or") )
...@@ -701,17 +703,28 @@ char * Smt_PrsGenName( Smt_Prs_t * p ) ...@@ -701,17 +703,28 @@ char * Smt_PrsGenName( Smt_Prs_t * p )
sprintf( Buffer, "_%0*X_", p->nDigits, ++p->NameCount ); sprintf( Buffer, "_%0*X_", p->nDigits, ++p->NameCount );
return Buffer; 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) ) if ( Smt_EntryIsName(iNode) )
{ {
char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(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] == '#' ) if ( pStr[0] == '#' )
return Smt_PrsBuildConstant( pNtk, pStr, -1, Smt_PrsGenName(p) ); return Smt_PrsBuildConstant( pNtk, pStr, -1, pName ? pName : Smt_PrsGenName(p) );
else else
{ {
int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
assert( 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; return iObj;
} }
} }
...@@ -724,7 +737,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev ...@@ -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 ); iRoot0 = Vec_IntEntry( vRoots, 0 );
if ( Smt_EntryIsName(iRoot0) ) 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 ) if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET )
{ {
// let ((s35550 (bvor s48 s35549))) // 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 ...@@ -744,21 +757,21 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
// get the name // get the name
Fan3 = Vec_IntEntry(vFans3, 0); Fan3 = Vec_IntEntry(vFans3, 0);
assert( Smt_EntryIsName(Fan3) ); assert( Smt_EntryIsName(Fan3) );
pName = Smt_EntryName(p, Fan3); pName2 = Smt_EntryName(p, Fan3);
// get function // get function
Fan3 = Vec_IntEntry(vFans3, 1); Fan3 = Vec_IntEntry(vFans3, 1);
assert( !Smt_EntryIsName(Fan3) ); //assert( !Smt_EntryIsName(Fan3) );
// solve the problem // 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 ) if ( iObj == 0 )
return 0; return 0;
// create buffer // create buffer
Vec_IntFill( &p->vTempFans, 1, iObj ); //Vec_IntFill( &p->vTempFans, 1, iObj );
Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, &p->vTempFans, pName ); //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); 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] == '_' ) else if ( pStr0[0] == '_' )
{ {
...@@ -768,7 +781,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev ...@@ -768,7 +781,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
// (_ bv1 32) // (_ bv1 32)
char * pStr2 = Smt_VecEntryName( p, vRoots, 2 ); char * pStr2 = Smt_VecEntryName( p, vRoots, 2 );
assert( Vec_IntSize(vRoots) == 3 ); 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 else
{ {
...@@ -777,16 +790,23 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev ...@@ -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 ); Type1 = Smt_StrToType( pStr1, &fSigned );
if ( Type1 == 0 ) if ( Type1 == 0 )
return 0; return 0;
Vec_IntFill( &p->vTempFans, 1, iObjPrev );
// find out this branch // 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 ) 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); int iRoot2 = Vec_IntEntry(vRoots, 2);
char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2)); char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2));
int Num = atoi( pStr2 ); int Num = atoi( pStr2 );
fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT); fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) ); if ( Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L )
Vec_IntPush( &p->vTempFans, Num ); {
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 ) 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 ...@@ -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 Num1 = atoi( pStr2 );
int Num2 = atoi( pStr3 ); int Num2 = atoi( pStr3 );
assert( Num1 >= Num2 ); assert( Num1 >= Num2 );
fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
Range = Num1 - Num2 + 1; Range = Num1 - Num2 + 1;
Vec_IntPushTwo( &p->vTempFans, Num1, Num2 ); Vec_IntPushTwo( &p->vTempFans, Num1, Num2 );
} }
else assert( 0 ); 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; return iObj;
} }
} }
...@@ -822,7 +841,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev ...@@ -822,7 +841,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
vFanins = Vec_IntAlloc( 100 ); vFanins = Vec_IntAlloc( 100 );
Vec_IntForEachEntryStart( vRoots, Fan, i, 1 ) 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 ) if ( iObj == 0 )
{ {
Vec_IntFree( vFanins ); Vec_IntFree( vFanins );
...@@ -854,17 +873,17 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev ...@@ -854,17 +873,17 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
} }
// create node // create node
assert( Range > 0 ); 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 ); Vec_IntFree( vFanins );
return iObj; 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 ) if ( iObjPrev == 0 )
return 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 ); else assert( 0 ); // return Smt_PrsBuild2_rec( pNtk, p, iRoot0 );
return 0; return 0;
...@@ -992,7 +1011,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -992,7 +1011,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
//(assert (not (= s0 #x00))) //(assert (not (= s0 #x00)))
assert( Vec_IntSize(vFans) == 2 ); assert( Vec_IntSize(vFans) == 2 );
assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) ); 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 ) if ( iObj == 0 )
{ {
Wlc_NtkFree( pNtk ); pNtk = NULL; Wlc_NtkFree( pNtk ); pNtk = NULL;
...@@ -1083,14 +1102,16 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit ) ...@@ -1083,14 +1102,16 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit )
} }
static inline int Smt_PrsRemoveComments( char * pBuffer, char * pLimit ) 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++ ) for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
{ {
if ( *pTemp == '(' ) if ( *pTemp == '(' )
nCount1++; nCount1++;
else if ( *pTemp == ')' ) else if ( *pTemp == ')' )
nCount2++; nCount2++;
else if ( *pTemp == ';' ) else if ( *pTemp == '|' )
fHaveBar ^= 1;
else if ( *pTemp == ';' && !fHaveBar )
while ( *pTemp && *pTemp != '\n' ) while ( *pTemp && *pTemp != '\n' )
*pTemp++ = ' '; *pTemp++ = ' ';
} }
...@@ -1191,8 +1212,16 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) ...@@ -1191,8 +1212,16 @@ void Smt_PrsReadLines( Smt_Prs_t * p )
Smt_PrsSkipNonSpaces( p ); Smt_PrsSkipNonSpaces( p );
if ( p->pCur < p->pLimit ) if ( p->pCur < p->pLimit )
{ {
// add fanin // remove strange characters (this can lead to name clashes)
int iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL ); 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) ); 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 ) ...@@ -1235,7 +1264,7 @@ void Smt_PrsPrintParser( Smt_Prs_t * p )
SeeAlso [] 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; Wlc_Ntk_t * pNtk = NULL;
int nCount = Smt_PrsRemoveComments( pBuffer, pLimit ); int nCount = Smt_PrsRemoveComments( pBuffer, pLimit );
...@@ -1243,20 +1272,21 @@ Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ) ...@@ -1243,20 +1272,21 @@ Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
if ( p == NULL ) if ( p == NULL )
return NULL; return NULL;
Smt_PrsReadLines( p ); Smt_PrsReadLines( p );
//Smt_PrsPrintParser( p ); if ( fPrintTree )
Smt_PrsPrintParser( p );
if ( Smt_PrsErrorPrint(p) ) if ( Smt_PrsErrorPrint(p) )
pNtk = Smt_PrsBuild2( p ); pNtk = fOldParser ? Smt_PrsBuild(p) : Smt_PrsBuild2(p);
Smt_PrsFree( p ); Smt_PrsFree( p );
return pNtk; 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; Wlc_Ntk_t * pNtk = NULL;
char * pBuffer, * pLimit; char * pBuffer, * pLimit;
pBuffer = Smt_PrsLoadFile( pFileName, &pLimit ); pBuffer = Smt_PrsLoadFile( pFileName, &pLimit );
if ( pBuffer == NULL ) if ( pBuffer == NULL )
return NULL; return NULL;
pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit ); pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit, fOldParser, fPrintTree );
ABC_FREE( pBuffer ); ABC_FREE( pBuffer );
return pNtk; return pNtk;
} }
......
src/base/wlc/wlcReadVer.c
...@@ -781,6 +781,7 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t * ...@@ -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_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_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_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_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_OR;
else if ( pStr[0] == '^' && pStr[1] == '^' ) pStr += 2, Type = WLC_OBJ_LOGIC_XOR; else if ( pStr[0] == '^' && pStr[1] == '^' ) pStr += 2, Type = WLC_OBJ_LOGIC_XOR;
......
src/base/wlc/wlcStdin.c
...@@ -192,7 +192,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd ) ...@@ -192,7 +192,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd )
// collect stdin until (check-sat) // collect stdin until (check-sat)
Vec_Str_t * vInput = Wlc_StdinCollectProblem( "(check-sat)" ); Vec_Str_t * vInput = Wlc_StdinCollectProblem( "(check-sat)" );
// parse input // 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 ); Vec_StrFree( vInput );
// install current network // install current network
Wlc_SetNtk( pAbc, pNtk ); Wlc_SetNtk( pAbc, pNtk );
......
src/base/wlc/wlcWriteVer.c
...@@ -314,6 +314,8 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) ...@@ -314,6 +314,8 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
fprintf( pFile, "~|" ); fprintf( pFile, "~|" );
else if ( pObj->Type == WLC_OBJ_BIT_NXOR ) else if ( pObj->Type == WLC_OBJ_BIT_NXOR )
fprintf( pFile, "~^" ); fprintf( pFile, "~^" );
else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL )
fprintf( pFile, "=>" );
else if ( pObj->Type == WLC_OBJ_LOGIC_AND ) else if ( pObj->Type == WLC_OBJ_LOGIC_AND )
fprintf( pFile, "&&" ); fprintf( pFile, "&&" );
else if ( pObj->Type == WLC_OBJ_LOGIC_OR ) else if ( pObj->Type == WLC_OBJ_LOGIC_OR )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment