Skip to content

A
abc
Commit 34c5ac88 by Alan Mishchenko
Options

Improving SMT-LIB parser.

parent 7b570b62
Showing with 88 additions and 83 deletions
src/base/wlc/wlc.h
...@@ -61,6 +61,8 @@ typedef enum { ...@@ -61,6 +61,8 @@ 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_NOR, // 17: bitwise OR
WLC_OBJ_BIT_NXOR, // 19: bitwise NXOR WLC_OBJ_BIT_NXOR, // 19: bitwise NXOR
WLC_OBJ_BIT_SELECT, // 20: bit selection WLC_OBJ_BIT_SELECT, // 20: bit selection
WLC_OBJ_BIT_CONCAT, // 21: bit concatenation WLC_OBJ_BIT_CONCAT, // 21: bit concatenation
......
src/base/wlc/wlcBlast.c
...@@ -946,21 +946,21 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple ...@@ -946,21 +946,21 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
for ( k = 0; k < nRange; k++ ) for ( k = 0; k < nRange; k++ )
Vec_IntPush( vRes, Abc_LitNot(pArg0[k]) ); Vec_IntPush( vRes, Abc_LitNot(pArg0[k]) );
} }
else if ( pObj->Type == WLC_OBJ_BIT_AND ) else if ( pObj->Type == WLC_OBJ_BIT_AND || pObj->Type == WLC_OBJ_BIT_NAND )
{ {
int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) ); int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) ); int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) ); int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
for ( k = 0; k < nRange; k++ ) for ( k = 0; k < nRange; k++ )
Vec_IntPush( vRes, Gia_ManHashAnd(pNew, pArg0[k], pArg1[k]) ); Vec_IntPush( vRes, Abc_LitNotCond(Gia_ManHashAnd(pNew, pArg0[k], pArg1[k]), pObj->Type == WLC_OBJ_BIT_NAND) );
} }
else if ( pObj->Type == WLC_OBJ_BIT_OR ) else if ( pObj->Type == WLC_OBJ_BIT_OR || pObj->Type == WLC_OBJ_BIT_NOR )
{ {
int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) ); int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) ); int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) ); int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
for ( k = 0; k < nRange; k++ ) for ( k = 0; k < nRange; k++ )
Vec_IntPush( vRes, Gia_ManHashOr(pNew, pArg0[k], pArg1[k]) ); Vec_IntPush( vRes, Abc_LitNotCond(Gia_ManHashOr(pNew, pArg0[k], pArg1[k]), pObj->Type == WLC_OBJ_BIT_NOR) );
} }
else if ( pObj->Type == WLC_OBJ_BIT_XOR || pObj->Type == WLC_OBJ_BIT_NXOR ) else if ( pObj->Type == WLC_OBJ_BIT_XOR || pObj->Type == WLC_OBJ_BIT_NXOR )
{ {
......
src/base/wlc/wlcNtk.c
...@@ -50,6 +50,8 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = { ...@@ -50,6 +50,8 @@ 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
"~|", // 17: bitwise NOR
"~^", // 19: bitwise NXOR "~^", // 19: bitwise NXOR
"[:]", // 20: bit selection "[:]", // 20: bit selection
"{,}", // 21: bit concatenation "{,}", // 21: bit concatenation
...@@ -362,6 +364,10 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose ) ...@@ -362,6 +364,10 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_OR, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) ); Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_OR, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
else if ( pObj->Type == WLC_OBJ_BIT_XOR ) else if ( pObj->Type == WLC_OBJ_BIT_XOR )
Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_XOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) ); Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_XOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
else if ( pObj->Type == WLC_OBJ_BIT_NAND )
Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_NAND, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
else if ( pObj->Type == WLC_OBJ_BIT_NOR )
Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_NOR, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
else if ( pObj->Type == WLC_OBJ_BIT_NXOR ) else if ( pObj->Type == WLC_OBJ_BIT_NXOR )
Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_NXOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) ); Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_NXOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
else if ( pObj->Type == WLC_OBJ_BIT_SELECT ) else if ( pObj->Type == WLC_OBJ_BIT_SELECT )
......
src/base/wlc/wlcReadSmt.c
...@@ -153,6 +153,12 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) ...@@ -153,6 +153,12 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
Type = WLC_OBJ_BIT_OR; // 17: bitwise OR Type = WLC_OBJ_BIT_OR; // 17: bitwise OR
else if ( !strcmp(pName, "bvxor") ) else if ( !strcmp(pName, "bvxor") )
Type = WLC_OBJ_BIT_XOR; // 18: bitwise XOR Type = WLC_OBJ_BIT_XOR; // 18: bitwise XOR
else if ( !strcmp(pName, "bvnand") )
Type = WLC_OBJ_BIT_NAND; // 16: bitwise NAND
else if ( !strcmp(pName, "bvnor") )
Type = WLC_OBJ_BIT_NOR; // 17: bitwise NOR
else if ( !strcmp(pName, "bvnxor") )
Type = WLC_OBJ_BIT_NXOR; // 18: bitwise NXOR
else if ( !strcmp(pName, "extract") ) else if ( !strcmp(pName, "extract") )
Type = WLC_OBJ_BIT_SELECT; // 19: bit selection Type = WLC_OBJ_BIT_SELECT; // 19: bit selection
else if ( !strcmp(pName, "concat") ) else if ( !strcmp(pName, "concat") )
...@@ -169,7 +175,7 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) ...@@ -169,7 +175,7 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
Type = WLC_OBJ_LOGIC_OR; // 25: logic OR Type = WLC_OBJ_LOGIC_OR; // 25: logic OR
else if ( !strcmp(pName, "xor") ) else if ( !strcmp(pName, "xor") )
Type = WLC_OBJ_LOGIC_XOR; // 26: logic OR Type = WLC_OBJ_LOGIC_XOR; // 26: logic OR
else if ( !strcmp(pName, "bvcomp") ) else if ( !strcmp(pName, "bvcomp") || !strcmp(pName, "=") )
Type = WLC_OBJ_COMP_EQU; // 27: compare equal Type = WLC_OBJ_COMP_EQU; // 27: compare equal
else if ( !strcmp(pName, "distinct") ) else if ( !strcmp(pName, "distinct") )
Type = WLC_OBJ_COMP_NOTEQU; // 28: compare not equal Type = WLC_OBJ_COMP_NOTEQU; // 28: compare not equal
...@@ -221,7 +227,6 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) ...@@ -221,7 +227,6 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
{ {
printf( "The following operations is currently not supported (%s)\n", pName ); printf( "The following operations is currently not supported (%s)\n", pName );
fflush( stdout ); fflush( stdout );
assert( 0 );
} }
return Type; return Type;
} }
...@@ -295,10 +300,15 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits ...@@ -295,10 +300,15 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits
{ {
if ( pStr[0] >= '0' && pStr[0] <= '9' ) if ( pStr[0] >= '0' && pStr[0] <= '9' )
{ {
int Number = atoi( pStr ); int w, nWords, Number = atoi( pStr );
nBits = Abc_Base2Log( Number+1 ); if ( nBits == -1 )
assert( nBits < 32 ); {
Vec_IntPush( vFanins, Number ); nBits = Abc_Base2Log( Number+1 );
assert( nBits < 32 );
}
nWords = Abc_BitWordNum( nBits );
for ( w = 0; w < nWords; w++ )
Vec_IntPush( vFanins, w ? 0 : Number );
} }
else else
{ {
...@@ -362,7 +372,7 @@ int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut, ...@@ -362,7 +372,7 @@ int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut,
// (_ bv1 32) // (_ bv1 32)
char * pStr2 = Smt_VecEntryName( p, vFans, 2 ); char * pStr2 = Smt_VecEntryName( p, vFans, 2 );
assert( Vec_IntSize(vFans) == 3 ); assert( Vec_IntSize(vFans) == 3 );
return Smt_PrsBuildConstant( pNtk, pStr2+2, atoi(pStr2), pName ); return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), pName );
} }
else if ( pStr0 && pStr0[0] == '=' ) else if ( pStr0 && pStr0[0] == '=' )
{ {
...@@ -691,55 +701,31 @@ char * Smt_PrsGenName( Smt_Prs_t * p ) ...@@ -691,55 +701,31 @@ 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 Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev )
{ {
if ( Smt_EntryIsName(iNode) ) if ( Smt_EntryIsName(iNode) )
{ {
int fFound, iObj;
char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
if ( pStr[0] == '#' ) if ( pStr[0] == '#' )
return Smt_PrsBuildConstant( pNtk, pStr, -1, Smt_PrsGenName(p) );
else
{ {
int i, nDigits, nBits = -1, iObj = -1; int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
Vec_IntClear( &p->vTempFans ); assert( fFound );
if ( pStr[1] == 'b' ) // binary
{
nBits = strlen(pStr+2);
Vec_IntFill( &p->vTempFans, Abc_BitWordNum(nBits), 0 );
for ( i = 0; i < nBits; i++ )
if ( pStr[2+i] == '1' )
Abc_InfoSetBit( (unsigned *)Vec_IntArray(&p->vTempFans), nBits-1-i );
else if ( pStr[2+i] != '0' )
return 0;
}
else if ( pStr[1] == 'x' ) // hexadecimal
{
nBits = strlen(pStr+2)*4;
Vec_IntFill( &p->vTempFans, Abc_BitWordNum(nBits), 0 );
nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(&p->vTempFans), pStr+2 );
if ( nDigits != (nBits + 3)/4 )
return 0;
}
else return 0;
// create constant node
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_CONST, 0, nBits, &p->vTempFans, Smt_PrsGenName(p) );
return iObj; return iObj;
} }
iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
assert( fFound );
return iObj;
} }
else else
{ {
Vec_Int_t * vRoots, * vRoots1, * vFans3; Vec_Int_t * vRoots, * vRoots1, * vFans3;
int iRoot0, iRoot1, Fan, Fan3, k; int iObj, iRoot0, iRoot1, iRoot2, Fan, Fan3, k;
assert( !Smt_EntryIsName(iNode) ); assert( !Smt_EntryIsName(iNode) );
vRoots = Smt_EntryNode( p, iNode ); vRoots = Smt_EntryNode( p, iNode );
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 * pName, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0));
int iObj; if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET )
if ( pStr0[0] == 'l' && pStr0[1] == 'e' && pStr0[2] == 't' && pStr0[3] == '\0' )
{ {
// let ((s35550 (bvor s48 s35549))) // let ((s35550 (bvor s48 s35549)))
assert( Vec_IntSize(vRoots) == 3 ); assert( Vec_IntSize(vRoots) == 3 );
...@@ -748,16 +734,13 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode ) ...@@ -748,16 +734,13 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
iRoot1 = Vec_IntEntry(vRoots, 1); iRoot1 = Vec_IntEntry(vRoots, 1);
assert( !Smt_EntryIsName(iRoot1) ); assert( !Smt_EntryIsName(iRoot1) );
vRoots1 = Smt_EntryNode(p, iRoot1); vRoots1 = Smt_EntryNode(p, iRoot1);
//if ( Smt_VecEntryIsType(vRoots1, 0, SMT_PRS_LET) )
// continue;
// iterate through the parts // iterate through the parts
Vec_IntForEachEntry( vRoots1, Fan, k ) Vec_IntForEachEntry( vRoots1, Fan, k )
{ {
// s35550 (bvor s48 s35549) // s35550 (bvor s48 s35549)
Fan = Vec_IntEntry(vRoots1, 0);
assert( !Smt_EntryIsName(Fan) ); assert( !Smt_EntryIsName(Fan) );
vFans3 = Smt_EntryNode(p, Fan); vFans3 = Smt_EntryNode(p, Fan);
assert( Vec_IntSize(vFans3) == 2 );
// get the name // get the name
Fan3 = Vec_IntEntry(vFans3, 0); Fan3 = Vec_IntEntry(vFans3, 0);
assert( Smt_EntryIsName(Fan3) ); assert( Smt_EntryIsName(Fan3) );
...@@ -766,41 +749,43 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode ) ...@@ -766,41 +749,43 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
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 ); iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1 );
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 );
return Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, &p->vTempFans, pName ); Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, &p->vTempFans, pName );
} }
// pricess the final part of let
iRoot2 = Vec_IntEntry(vRoots, 2);
return Smt_PrsBuild2_rec( pNtk, p, iRoot2, -1 );
} }
else if ( pStr0[0] == '_' ) else if ( pStr0[0] == '_' )
{ {
int iRoot1 = Vec_IntEntry( vRoots, 1 ); char * pStr1 = Smt_VecEntryName( p, vRoots, 1 );
char * pStr1 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot1));
if ( pStr1[0] == 'b' && pStr1[1] == 'v' ) if ( pStr1[0] == 'b' && pStr1[1] == 'v' )
{ {
int iObj = 0; // (_ bv1 32)
return iObj; char * pStr2 = Smt_VecEntryName( p, vRoots, 2 );
assert( Vec_IntSize(vRoots) == 3 );
return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), Smt_PrsGenName(p) );
} }
else else
{ {
int Type1, Range = -1, fSigned = 0; int Type1, fSigned = 0, Range = -1;
// call the other branch assert( iObjPrev != -1 );
assert( Vec_IntSize(vRoots) == 2 ); Type1 = Smt_StrToType( pStr1, &fSigned );
iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1) ); if ( Type1 == 0 )
if ( iObj == 0 )
return 0; return 0;
Vec_IntFill( &p->vTempFans, 1, iObj ); Vec_IntFill( &p->vTempFans, 1, iObjPrev );
// find out this branch // find out this branch
Type1 = Abc_Lit2Var(iRoot1);
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, iObj) ); Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) );
Vec_IntPush( &p->vTempFans, Num ); Vec_IntPush( &p->vTempFans, Num );
} }
else if ( Type1 == WLC_OBJ_BIT_SELECT ) else if ( Type1 == WLC_OBJ_BIT_SELECT )
...@@ -813,7 +798,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode ) ...@@ -813,7 +798,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
int Num2 = atoi( pStr3 ); int Num2 = atoi( pStr3 );
assert( Num1 >= Num2 ); assert( Num1 >= Num2 );
fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT); fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
Range = (Num1 - Num2 + 1) + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ); Range = Num1 - Num2 + 1;
Vec_IntPushTwo( &p->vTempFans, Num1, Num2 ); Vec_IntPushTwo( &p->vTempFans, Num1, Num2 );
} }
else assert( 0 ); else assert( 0 );
...@@ -826,15 +811,18 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode ) ...@@ -826,15 +811,18 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
Vec_Int_t * vFanins; Vec_Int_t * vFanins;
int i, Fan, fSigned = 0, Range, Type0; int i, Fan, fSigned = 0, Range, Type0;
int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 ); int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 );
if ( iObj > 0 ) if ( iObj )
return iObj; return iObj;
Type0 = Smt_StrToType( pStr0, &fSigned ); Type0 = Smt_StrToType( pStr0, &fSigned );
if ( Type0 == 0 )
return 0;
assert( Type0 != WLC_OBJ_BIT_SIGNEXT && Type0 != WLC_OBJ_BIT_ZEROPAD && Type0 != WLC_OBJ_BIT_SELECT && Type0 != WLC_OBJ_ROTATE_R && Type0 != WLC_OBJ_ROTATE_L );
// collect fanins // collect fanins
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 ); iObj = Smt_PrsBuild2_rec( pNtk, p, Fan, -1 );
if ( iObj == 0 ) if ( iObj == 0 )
{ {
Vec_IntFree( vFanins ); Vec_IntFree( vFanins );
...@@ -842,8 +830,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode ) ...@@ -842,8 +830,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
} }
Vec_IntPush( vFanins, iObj ); Vec_IntPush( vFanins, iObj );
} }
// update specialized nodes
assert( Type0 != WLC_OBJ_BIT_SIGNEXT && Type0 != WLC_OBJ_BIT_ZEROPAD && Type0 != WLC_OBJ_BIT_SELECT && Type0 != WLC_OBJ_ROTATE_R && Type0 != WLC_OBJ_ROTATE_L );
// find range // find range
Range = 0; Range = 0;
if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR ) if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR )
...@@ -873,6 +859,13 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode ) ...@@ -873,6 +859,13 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
return iObj; return iObj;
} }
} }
else if ( Vec_IntSize(vRoots) == 2 ) // possible ((_ extract 48 16) (bvmul ?v_5 ?v_12))
{
int iObjPrev = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1), -1 );
if ( iObjPrev == 0 )
return 0;
return Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 0), iObjPrev );
}
else assert( 0 ); // return Smt_PrsBuild2_rec( pNtk, p, iRoot0 ); else assert( 0 ); // return Smt_PrsBuild2_rec( pNtk, p, iRoot0 );
return 0; return 0;
} }
...@@ -882,16 +875,16 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -882,16 +875,16 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
Wlc_Ntk_t * pNtk; Wlc_Ntk_t * pNtk;
Vec_Int_t * vFansRoot, * vFans, * vFans2; Vec_Int_t * vFansRoot, * vFans, * vFans2;
Vec_Int_t * vAsserts = Vec_IntAlloc(100); Vec_Int_t * vAsserts = Vec_IntAlloc(100);
int i, Fan, iObj, NameId, Range, Status, nBits = 0; int i, Root, Fan, iObj, NameId, Range, Status, nBits = 0;
char * pName, * pRange, * pValue; char * pName, * pRange, * pValue;
// start network and create primary inputs // start network and create primary inputs
pNtk = Wlc_NtkAlloc( p->pName, 1000 ); pNtk = Wlc_NtkAlloc( p->pName, 1000 );
pNtk->pManName = Abc_NamStart( 1000, 24 ); pNtk->pManName = Abc_NamStart( 1000, 24 );
// collect top-level asserts // collect top-level asserts
vFansRoot = Vec_WecEntry( &p->vObjs, 0 ); vFansRoot = Vec_WecEntry( &p->vObjs, 0 );
Vec_IntForEachEntry( vFansRoot, Fan, i ) Vec_IntForEachEntry( vFansRoot, Root, i )
{ {
assert( !Smt_EntryIsName(Fan) ); assert( !Smt_EntryIsName(Root) );
vFans = Smt_VecEntryNode( p, vFansRoot, i ); vFans = Smt_VecEntryNode( p, vFansRoot, i );
Fan = Vec_IntEntry(vFans, 0); Fan = Vec_IntEntry(vFans, 0);
assert( Smt_EntryIsName(Fan) ); assert( Smt_EntryIsName(Fan) );
...@@ -910,15 +903,12 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -910,15 +903,12 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// check type (Bool or BitVec) // check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3); Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) ) if ( Smt_EntryIsName(Fan) )
{ { //(declare-fun s1 () Bool)
//(declare-fun s1 () Bool)
assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
Range = 1; Range = 1;
} }
else else
{ { // (declare-fun s1 () (_ BitVec 64))
// (declare-fun s1 () (_ BitVec 64))
// get range
Fan = Vec_IntEntry(vFans, 3); Fan = Vec_IntEntry(vFans, 3);
assert( !Smt_EntryIsName(Fan) ); assert( !Smt_EntryIsName(Fan) );
vFans2 = Smt_EntryNode(p, Fan); vFans2 = Smt_EntryNode(p, Fan);
...@@ -1002,7 +992,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1002,7 +992,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) ); iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1 );
if ( iObj == 0 ) if ( iObj == 0 )
{ {
Wlc_NtkFree( pNtk ); pNtk = NULL; Wlc_NtkFree( pNtk ); pNtk = NULL;
...@@ -1012,19 +1002,16 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1012,19 +1002,16 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
} }
// issue warnings about unknown dirs // issue warnings about unknown dirs
else if ( Abc_Lit2Var(Fan) >= SMT_PRS_END ) else if ( Abc_Lit2Var(Fan) >= SMT_PRS_END )
{
printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) ); printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) );
continue;
}
} }
// build AND of asserts // build AND of asserts
if ( Vec_IntSize(vAsserts) == 1 ) if ( Vec_IntSize(vAsserts) == 1 )
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter_output" ); iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter" );
else else
{ {
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL ); iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL );
Vec_IntFill( vAsserts, 1, iObj ); Vec_IntFill( vAsserts, 1, iObj );
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter_output" ); iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter" );
} }
Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 ); Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 );
// create nameIDs // create nameIDs
...@@ -1212,6 +1199,7 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) ...@@ -1212,6 +1199,7 @@ void Smt_PrsReadLines( Smt_Prs_t * p )
} }
assert( Vec_IntSize(&p->vStack) == 1 ); assert( Vec_IntSize(&p->vStack) == 1 );
assert( Vec_WecSize(&p->vObjs) == Vec_WecCap(&p->vObjs) ); assert( Vec_WecSize(&p->vObjs) == Vec_WecCap(&p->vObjs) );
p->nDigits = Abc_Base16Log( Vec_WecSize(&p->vObjs) );
} }
void Smt_PrsPrintParser_rec( Smt_Prs_t * p, int iObj, int Depth ) void Smt_PrsPrintParser_rec( Smt_Prs_t * p, int iObj, int Depth )
{ {
...@@ -1234,7 +1222,6 @@ void Smt_PrsPrintParser( Smt_Prs_t * p ) ...@@ -1234,7 +1222,6 @@ void Smt_PrsPrintParser( Smt_Prs_t * p )
{ {
// Vec_WecPrint( &p->vDepth, 0 ); // Vec_WecPrint( &p->vDepth, 0 );
Smt_PrsPrintParser_rec( p, 0, 0 ); Smt_PrsPrintParser_rec( p, 0, 0 );
p->nDigits = Abc_Base16Log( Vec_WecSize(&p->vObjs) );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1258,7 +1245,7 @@ Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ) ...@@ -1258,7 +1245,7 @@ Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
Smt_PrsReadLines( p ); Smt_PrsReadLines( p );
//Smt_PrsPrintParser( p ); //Smt_PrsPrintParser( p );
if ( Smt_PrsErrorPrint(p) ) if ( Smt_PrsErrorPrint(p) )
pNtk = Smt_PrsBuild( p ); pNtk = Smt_PrsBuild2( p );
Smt_PrsFree( p ); Smt_PrsFree( p );
return pNtk; return pNtk;
} }
......
src/base/wlc/wlcReadVer.c
...@@ -778,9 +778,12 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t * ...@@ -778,9 +778,12 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
else if ( pStr[0] == '&' && pStr[1] != '&' ) pStr += 1, Type = WLC_OBJ_BIT_AND; else if ( pStr[0] == '&' && pStr[1] != '&' ) pStr += 1, Type = WLC_OBJ_BIT_AND;
else if ( pStr[0] == '|' && pStr[1] != '|' ) pStr += 1, Type = WLC_OBJ_BIT_OR; else if ( pStr[0] == '|' && pStr[1] != '|' ) pStr += 1, Type = WLC_OBJ_BIT_OR;
else if ( pStr[0] == '^' && pStr[1] != '^' ) pStr += 1, Type = WLC_OBJ_BIT_XOR; else if ( pStr[0] == '^' && pStr[1] != '^' ) pStr += 1, Type = WLC_OBJ_BIT_XOR;
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_BIT_NXOR;
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_COMP_EQU; else if ( pStr[0] == '=' && pStr[1] == '=' ) pStr += 2, Type = WLC_OBJ_COMP_EQU;
else if ( pStr[0] == '!' && pStr[1] == '=' ) pStr += 2, Type = WLC_OBJ_COMP_NOTEQU; else if ( pStr[0] == '!' && pStr[1] == '=' ) pStr += 2, Type = WLC_OBJ_COMP_NOTEQU;
else if ( pStr[0] == '<' && pStr[1] != '=' ) pStr += 1, Type = WLC_OBJ_COMP_LESS; else if ( pStr[0] == '<' && pStr[1] != '=' ) pStr += 1, Type = WLC_OBJ_COMP_LESS;
......
src/base/wlc/wlcWriteVer.c
...@@ -308,12 +308,18 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) ...@@ -308,12 +308,18 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
fprintf( pFile, "|" ); fprintf( pFile, "|" );
else if ( pObj->Type == WLC_OBJ_BIT_XOR ) else if ( pObj->Type == WLC_OBJ_BIT_XOR )
fprintf( pFile, "^" ); fprintf( pFile, "^" );
else if ( pObj->Type == WLC_OBJ_BIT_NAND )
fprintf( pFile, "~&" );
else if ( pObj->Type == WLC_OBJ_BIT_NOR )
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_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 )
fprintf( pFile, "||" ); fprintf( pFile, "||" );
else if ( pObj->Type == WLC_OBJ_LOGIC_XOR )
fprintf( pFile, "^^" );
else if ( pObj->Type == WLC_OBJ_COMP_EQU ) else if ( pObj->Type == WLC_OBJ_COMP_EQU )
fprintf( pFile, "==" ); fprintf( pFile, "==" );
else if ( pObj->Type == WLC_OBJ_COMP_NOTEQU ) else if ( pObj->Type == WLC_OBJ_COMP_NOTEQU )
...@@ -333,7 +339,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) ...@@ -333,7 +339,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
else if ( pObj->Type == WLC_OBJ_ARI_MULTI ) else if ( pObj->Type == WLC_OBJ_ARI_MULTI )
fprintf( pFile, "*" ); fprintf( pFile, "*" );
else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE ) else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE )
fprintf( pFile, "//" ); fprintf( pFile, "/" );
else if ( pObj->Type == WLC_OBJ_ARI_MODULUS ) else if ( pObj->Type == WLC_OBJ_ARI_MODULUS )
fprintf( pFile, "%%" ); fprintf( pFile, "%%" );
else if ( pObj->Type == WLC_OBJ_ARI_POWER ) else if ( pObj->Type == WLC_OBJ_ARI_POWER )
...@@ -343,6 +349,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) ...@@ -343,6 +349,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
else if ( pObj->Type == WLC_OBJ_ARI_SQUARE ) else if ( pObj->Type == WLC_OBJ_ARI_SQUARE )
fprintf( pFile, "#" ); fprintf( pFile, "#" );
else assert( 0 ); else assert( 0 );
//fprintf( pFile, "???" );
fprintf( pFile, " %s", Wlc_ObjName(p, Wlc_ObjFaninId(pObj, 1)) ); fprintf( pFile, " %s", Wlc_ObjName(p, Wlc_ObjFaninId(pObj, 1)) );
} }
} }
......
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