Skip to content

A
abc
Commit 3c8c807a by Alan Mishchenko
Options

Improvements to SMT-LIB parser.

parent 57286e8a
Showing with 243 additions and 84 deletions
src/base/wlc/wlc.h
...@@ -140,6 +140,7 @@ struct Wlc_Ntk_t_ ...@@ -140,6 +140,7 @@ struct Wlc_Ntk_t_
int nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type int nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type
int nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting int nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting
int fSmtLib; // the network comes from an SMT-LIB file int fSmtLib; // the network comes from an SMT-LIB file
int nAssert; // the number of asserts
// memory for objects // memory for objects
Wlc_Obj_t * pObjs; Wlc_Obj_t * pObjs;
int iObj; int iObj;
......
src/base/wlc/wlcNtk.c
...@@ -195,14 +195,14 @@ void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins ) ...@@ -195,14 +195,14 @@ void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins )
{ {
assert( pObj->nFanins == 0 ); assert( pObj->nFanins == 0 );
pObj->nFanins = Vec_IntSize(vFanins); 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 // special treatment of CONST, SELECT and TABLE
if ( pObj->Type == WLC_OBJ_CONST ) if ( pObj->Type == WLC_OBJ_CONST )
pObj->nFanins = 0; pObj->nFanins = 0;
else if ( pObj->Type == WLC_OBJ_BIT_SELECT || pObj->Type == WLC_OBJ_TABLE ) else if ( pObj->Type == WLC_OBJ_BIT_SELECT || pObj->Type == WLC_OBJ_TABLE )
pObj->nFanins = 1; 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 ) void Wlc_NtkFree( Wlc_Ntk_t * p )
{ {
......
src/base/wlc/wlcReadSmt.c
...@@ -219,6 +219,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) ...@@ -219,6 +219,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
Type = WLC_OBJ_ARI_REM, *pfSigned = 1; // 40: arithmetic remainder Type = WLC_OBJ_ARI_REM, *pfSigned = 1; // 40: arithmetic remainder
else if ( !strcmp(pName, "bvsmod") ) else if ( !strcmp(pName, "bvsmod") )
Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus 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, "") ) // else if ( !strcmp(pName, "") )
// Type = WLC_OBJ_ARI_POWER; // 41: arithmetic power // Type = WLC_OBJ_ARI_POWER; // 41: arithmetic power
else if ( !strcmp(pName, "bvneg") ) else if ( !strcmp(pName, "bvneg") )
...@@ -255,6 +257,8 @@ static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int ...@@ -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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
...@@ -274,20 +278,27 @@ static inline int Smt_PrsCreateNodeOld( Wlc_Ntk_t * pNtk, int Type, int fSigned, ...@@ -274,20 +278,27 @@ static inline int Smt_PrsCreateNodeOld( Wlc_Ntk_t * pNtk, int Type, int fSigned,
assert( Type > 0 ); assert( Type > 0 );
assert( Range >= 0 ); assert( Range >= 0 );
assert( fSigned >= 0 ); assert( fSigned >= 0 );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
if ( fSigned ) // add node's name
Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
if ( Type == WLC_OBJ_SHIFT_RA )
Wlc_NtkObj(pNtk, iObj)->Signed = 1;
if ( pName == NULL ) if ( pName == NULL )
{ {
sprintf( Buffer, "_n%d_", iObj ); sprintf( Buffer, "_n%d_", iObj );
pName = Buffer; pName = Buffer;
} }
// add node's name
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
assert( !fFound ); assert( !fFound );
assert( iObj == NameId ); 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; return iObj;
} }
static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) 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 ...@@ -302,8 +313,7 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in
assert( Range >= 0 ); assert( Range >= 0 );
assert( fSigned >= 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 // explicitely secify allowed multi operators
if (Vec_IntSize(vFanins)<=2 || if (Vec_IntSize(vFanins)<=2 ||
!( Type == WLC_OBJ_BIT_AND || // 16:`` bitwise AND !( Type == WLC_OBJ_BIT_AND || // 16:`` bitwise AND
...@@ -362,17 +372,17 @@ FINISHED_WITH_FANINS: ...@@ -362,17 +372,17 @@ FINISHED_WITH_FANINS:
Vec_IntFree(v2Fanins); 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 // this is a temporary hack
// basically we keep only 32 bits. // basically we keep only 32 bits.
// bits 0 - 30 are kept same as original // 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 all bits from 31 to Range-1 // 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) if (Type == WLC_OBJ_SHIFT_R || Type == WLC_OBJ_SHIFT_RA || Type == WLC_OBJ_SHIFT_L)
{ {
int iFanin1 = Vec_IntEntry(vFanins,1); int range1, iObj1, iObj2, iObj3;
int range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) );
int iObj1, iObj2, iObj3;
assert(Vec_IntSize(vFanins)>=2); assert(Vec_IntSize(vFanins)>=2);
iFanin1 = Vec_IntEntry(vFanins,1);
range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) );
if (range1>32) if (range1>32)
{ {
Vec_Int_t * newFanins = Vec_IntAlloc(10); Vec_Int_t * newFanins = Vec_IntAlloc(10);
...@@ -389,6 +399,8 @@ FINISHED_WITH_FANINS: ...@@ -389,6 +399,8 @@ FINISHED_WITH_FANINS:
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj1), newFanins ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj1), newFanins );
//printf("obj1: %d\n",iObj1);
// bit select of larger bits // bit select of larger bits
Vec_IntPop(newFanins); Vec_IntPop(newFanins);
Vec_IntPop(newFanins); Vec_IntPop(newFanins);
...@@ -402,6 +414,7 @@ FINISHED_WITH_FANINS: ...@@ -402,6 +414,7 @@ FINISHED_WITH_FANINS:
assert( iObj2 == NameId ); assert( iObj2 == NameId );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj2), newFanins ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj2), newFanins );
//printf("obj2: %d\n",iObj2);
// reduction or // reduction or
Vec_IntPop( newFanins ); Vec_IntPop( newFanins );
...@@ -416,6 +429,7 @@ FINISHED_WITH_FANINS: ...@@ -416,6 +429,7 @@ FINISHED_WITH_FANINS:
assert( iObj3 == NameId ); assert( iObj3 == NameId );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj3), newFanins ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj3), newFanins );
//printf("obj3: %d\n",iObj3);
// concat all together // concat all together
Vec_IntWriteEntry( newFanins, 0, iObj3 ); Vec_IntWriteEntry( newFanins, 0, iObj3 );
...@@ -429,6 +443,7 @@ FINISHED_WITH_FANINS: ...@@ -429,6 +443,7 @@ FINISHED_WITH_FANINS:
assert( iObj == NameId ); assert( iObj == NameId );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), newFanins ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), newFanins );
//printf("obj: %d\n",iObj);
// pushing the new node // pushing the new node
Vec_IntWriteEntry(vFanins, 1, iObj); Vec_IntWriteEntry(vFanins, 1, iObj);
...@@ -461,34 +476,22 @@ FINISHED_WITH_FANINS: ...@@ -461,34 +476,22 @@ FINISHED_WITH_FANINS:
return iObj; return iObj;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline char * Smt_GetHexFromDecimalString(char * pStr) static inline char * Smt_GetHexFromDecimalString(char * pStr)
{ {
int i,k=0, nDigits = strlen(pStr); int i,k=0, nDigits = strlen(pStr);
int digit, carry = 0; int digit, carry = 0;
int metNonZeroBit; int metNonZeroBit = 0;
int nBits;
char * hex;
Vec_Int_t * decimal = Vec_IntAlloc(nDigits); Vec_Int_t * decimal = Vec_IntAlloc(nDigits);
Vec_Int_t * rev; Vec_Int_t * rev;
int nBits;
char * hex;
for (i=0;i<nDigits;i++) for (i=0;i<nDigits;i++)
Vec_IntPush(decimal,pStr[i]-'0'); Vec_IntPush(decimal,pStr[i]-'0');
// firstly fill-in the reversed vector // firstly fillin the reversed vector
rev = Vec_IntAlloc(10); rev = Vec_IntAlloc(10);
metNonZeroBit = 0;
while(k<nDigits) while(k<nDigits)
{ {
digit = Vec_IntEntry(decimal,k); digit = Vec_IntEntry(decimal,k);
...@@ -501,7 +504,7 @@ static inline char * Smt_GetHexFromDecimalString(char * pStr) ...@@ -501,7 +504,7 @@ static inline char * Smt_GetHexFromDecimalString(char * pStr)
break; break;
else else
{ {
Vec_IntPush(rev,carry); Vec_IntPush(rev,carry);
carry = 0; carry = 0;
k = 0; k = 0;
metNonZeroBit = 0; metNonZeroBit = 0;
...@@ -564,12 +567,17 @@ static inline char * Smt_GetHexFromDecimalString(char * pStr) ...@@ -564,12 +567,17 @@ static inline char * Smt_GetHexFromDecimalString(char * pStr)
default: assert(0); default: assert(0);
} }
hex[nBits/4-1-k] = letter; hex[nBits/4-1-k] = letter;
//if (k<Vec_IntSize(rev))
// Vec_IntPush(vFanins,Vec_IntEntry(rev,k));
//else
// Vec_IntPush(vFanins,0);
} }
hex[nBits/4] = '\0'; hex[nBits/4] = '\0';
Vec_IntFree(rev); Vec_IntFree(rev);
return hex; return hex;
} }
static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, char * pName ) static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, char * pName )
{ {
int i, nDigits, iObj; int i, nDigits, iObj;
...@@ -578,6 +586,25 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits ...@@ -578,6 +586,25 @@ 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' )
{ {
// 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 ); int w, nWords, Number = atoi( pStr );
if ( nBits == -1 ) if ( nBits == -1 )
...@@ -589,15 +616,6 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits ...@@ -589,15 +616,6 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits
for ( w = 0; w < nWords; w++ ) for ( w = 0; w < nWords; w++ )
Vec_IntPush( vFanins, w ? 0 : Number ); 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 else
{ {
...@@ -648,12 +666,6 @@ int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut, ...@@ -648,12 +666,6 @@ int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut,
// s3087 // s3087
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(pStr, pName) )
{
Vec_IntFill( &p->vTempFans, 1, iObj );
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, RangeOut, &p->vTempFans, pName );
}
return iObj; return iObj;
} }
} }
...@@ -804,13 +816,6 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p ) ...@@ -804,13 +816,6 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p )
// skip () // skip ()
Fan = Vec_IntEntry(vFans, 2); Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) ); 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) // check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3); Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) ) if ( Smt_EntryIsName(Fan) )
...@@ -1006,6 +1011,14 @@ char * Smt_PrsGenName( Smt_Prs_t * p ) ...@@ -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 ) 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) ) if ( Smt_EntryIsName(iNode) )
{ {
char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(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, ...@@ -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) ); 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;
// 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 ); assert( fFound );
// create buffer if the name of the fanin has different name // create buffer if the name of the fanin has different name
if ( pName && strcmp(Wlc_ObjName(pNtk, iObj), pName) ) 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, ...@@ -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 ); Vec_IntFill( &p->vTempFans, 1, iObj );
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName ); 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; return iObj;
} }
} }
else else
{ {
Vec_Int_t * vRoots, * vRoots1, * vFans3; 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, ...@@ -1039,7 +1074,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
if ( Smt_EntryIsName(iRoot0) ) if ( Smt_EntryIsName(iRoot0) )
{ {
char * pName2, * 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 || Abc_Lit2Var(iRoot0) == SMT_PRS_DEFINE_FUN) //added define-fun is similar to let
{ {
// let ((s35550 (bvor s48 s35549))) // let ((s35550 (bvor s48 s35549)))
assert( Vec_IntSize(vRoots) == 3 ); 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, ...@@ -1051,6 +1086,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
// iterate through the parts // iterate through the parts
Vec_IntForEachEntry( vRoots1, Fan, k ) Vec_IntForEachEntry( vRoots1, Fan, k )
{ {
char * temp;
// s35550 (bvor s48 s35549) // s35550 (bvor s48 s35549)
assert( !Smt_EntryIsName(Fan) ); assert( !Smt_EntryIsName(Fan) );
vFans3 = Smt_EntryNode(p, 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, ...@@ -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); Fan3 = Vec_IntEntry(vFans3, 0);
assert( Smt_EntryIsName(Fan3) ); assert( Smt_EntryIsName(Fan3) );
pName2 = Smt_EntryName(p, 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 // 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, pName2 ); // NULL ); //pName2 ); iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1, pName2 ); // NULL ); //pName2 );
ABC_FREE( temp );
if ( iObj == 0 ) if ( iObj == 0 )
return 0; return 0;
// create buffer // create buffer
...@@ -1133,7 +1184,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, ...@@ -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 ); int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 );
if ( iObj ) if ( iObj )
return iObj; return iObj;
Type0 = Smt_StrToType( pStr0, &fSigned ); Type0 = Smt_StrToType( pStr0, &fSigned );
if ( Type0 == 0 ) if ( Type0 == 0 )
return 0; return 0;
...@@ -1151,7 +1201,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, ...@@ -1151,7 +1201,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
} }
Vec_IntPush( vFanins, iObj ); Vec_IntPush( vFanins, iObj );
} }
// 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 )
...@@ -1197,7 +1246,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1197,7 +1246,7 @@ 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, Root, Fan, iObj, NameId, Range, Status, nBits = 0; int i, Root, Fan, iObj, NameId, Range, nBits = 0;
char * pName, * pRange; char * pName, * pRange;
// start network and create primary inputs // start network and create primary inputs
pNtk = Wlc_NtkAlloc( p->pName, 1000 ); pNtk = Wlc_NtkAlloc( p->pName, 1000 );
...@@ -1214,22 +1263,22 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1214,22 +1263,22 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// create variables // create variables
if ( Abc_Lit2Var(Fan) == SMT_PRS_DECLARE_FUN ) if ( Abc_Lit2Var(Fan) == SMT_PRS_DECLARE_FUN )
{ {
char * pName_glb;
assert( Vec_IntSize(vFans) == 4 ); assert( Vec_IntSize(vFans) == 4 );
assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) ); assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) );
// get name // get name
Fan = Vec_IntEntry(vFans, 1); Fan = Vec_IntEntry(vFans, 1);
assert( Smt_EntryIsName(Fan) ); assert( Smt_EntryIsName(Fan) );
pName = Smt_EntryName(p, 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 () // skip ()
Fan = Vec_IntEntry(vFans, 2); Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) ); 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) // check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3); Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) ) if ( Smt_EntryIsName(Fan) )
...@@ -1259,9 +1308,11 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1259,9 +1308,11 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
Vec_IntPush( &pNtk->vValues, nBits ); Vec_IntPush( &pNtk->vValues, nBits );
Vec_IntPush( &pNtk->vValues, Range ); Vec_IntPush( &pNtk->vValues, Range );
nBits += Range; nBits += Range;
ABC_FREE( pName_glb );
} }
// create constants // 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( Vec_IntSize(vFans) == 5 );
assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) );
...@@ -1269,6 +1320,14 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1269,6 +1320,14 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
Fan = Vec_IntEntry(vFans, 1); Fan = Vec_IntEntry(vFans, 1);
assert( Smt_EntryIsName(Fan) ); assert( Smt_EntryIsName(Fan) );
pName = Smt_EntryName(p, 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 () // skip ()
Fan = Vec_IntEntry(vFans, 2); Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) ); assert( !Smt_EntryIsName(Fan) );
...@@ -1278,13 +1337,17 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1278,13 +1337,17 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
{ {
// (define-fun s_2 () Bool false) // (define-fun s_2 () Bool false)
assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), -1, pName ); Range = 1;
if ( iObj == 0 ) pValue = Smt_VecEntryName(p, vFans, 4);
{
Wlc_NtkFree( pNtk ); pNtk = NULL; //printf("value: %s\n",pValue);
goto finish;
} if ( !strcmp("false", pValue) )
continue; pValue = "#b0";
else if ( !strcmp("true", pValue) )
pValue = "#b1";
else assert( 0 );
Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName );
} }
else else
{ {
...@@ -1292,6 +1355,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1292,6 +1355,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// (define-fun s1 () (_ BitVec 8) (bvneg #x7f)) // (define-fun s1 () (_ BitVec 8) (bvneg #x7f))
// get range // get range
Fan = Vec_IntEntry(vFans, 3); Fan = Vec_IntEntry(vFans, 3);
assert( !Smt_EntryIsName(Fan) ); assert( !Smt_EntryIsName(Fan) );
vFans2 = Smt_VecEntryNode(p, vFans, 3); vFans2 = Smt_VecEntryNode(p, vFans, 3);
assert( Vec_IntSize(vFans2) == 3 ); assert( Vec_IntSize(vFans2) == 3 );
...@@ -1299,11 +1363,24 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1299,11 +1363,24 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
// get range // get range
Fan = Vec_IntEntry(vFans2, 2); Fan = Vec_IntEntry(vFans2, 2);
assert( Smt_EntryIsName(Fan) ); assert( Smt_EntryIsName(Fan) );
pRange = Smt_EntryName(p, Fan); pRange = Smt_EntryName(p, Fan);
Range = atoi(pRange); Range = atoi(pRange);
// added: can parse functions too
Vec_Int_t * vFans3 = Smt_VecEntryNode(p, vFans, 4);
Fan = Vec_IntEntry(vFans3, 0);
// get constant // 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 ); Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName );
} }
if ( !Status ) if ( !Status )
...@@ -1312,6 +1389,57 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1312,6 +1389,57 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
goto finish; 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 // collect assertion outputs
else if ( Abc_Lit2Var(Fan) == SMT_PRS_ASSERT ) else if ( Abc_Lit2Var(Fan) == SMT_PRS_ASSERT )
{ {
...@@ -1321,6 +1449,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1321,6 +1449,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) );
pNtk->nAssert++; // added
iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL ); iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL );
if ( iObj == 0 ) if ( iObj == 0 )
{ {
...@@ -1336,6 +1465,9 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) ...@@ -1336,6 +1465,9 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// 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" ); 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 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 );
...@@ -1413,18 +1545,35 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit ) ...@@ -1413,18 +1545,35 @@ 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, fHaveBar = 0; char * pTemp; int nCount1 = 0, nCount2 = 0, fHaveBar = 0;
int backslash = 0;
for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ ) for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
{ {
if ( *pTemp == '(' ) if ( *pTemp == '(' )
nCount1++; { if ( !fHaveBar ) nCount1++; }
else if ( *pTemp == ')' ) else if ( *pTemp == ')' )
nCount2++; { if ( !fHaveBar ) nCount2++; }
else if ( *pTemp == '|' ) else if ( *pTemp == '|' )
fHaveBar ^= 1; fHaveBar ^= 1;
else if ( *pTemp == ';' && !fHaveBar ) else if ( *pTemp == ';' && !fHaveBar )
while ( *pTemp && *pTemp != '\n' ) while ( *pTemp && *pTemp != '\n' )
*pTemp++ = ' '; *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 ) if ( nCount1 != nCount2 )
printf( "The input SMTLIB file has different number of opening and closing parentheses (%d and %d).\n", 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 ) else if ( nCount1 == 0 )
...@@ -1455,7 +1604,6 @@ static inline void Smt_PrsFree( Smt_Prs_t * p ) ...@@ -1455,7 +1604,6 @@ static inline void Smt_PrsFree( Smt_Prs_t * p )
Vec_IntErase( &p->vStack ); Vec_IntErase( &p->vStack );
Vec_IntErase( &p->vTempFans ); Vec_IntErase( &p->vTempFans );
//Vec_WecErase( &p->vDepth ); //Vec_WecErase( &p->vDepth );
Vec_WecErase( &p->vObjs );
ABC_FREE( p ); ABC_FREE( p );
} }
...@@ -1499,6 +1647,15 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) ...@@ -1499,6 +1647,15 @@ void Smt_PrsReadLines( Smt_Prs_t * p )
for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ ) for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ )
{ {
Smt_PrsSkipSpaces( p ); Smt_PrsSkipSpaces( p );
if ( *p->pCur == '|' )
{
*p->pCur = ' ';
while ( *p->pCur && *p->pCur != '|' )
*p->pCur++ = ' ';
if ( *p->pCur == '|' )
*p->pCur = ' ';
continue;
}
if ( *p->pCur == '(' ) if ( *p->pCur == '(' )
{ {
// add new node at this depth // add new node at this depth
...@@ -1524,12 +1681,13 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) ...@@ -1524,12 +1681,13 @@ void Smt_PrsReadLines( Smt_Prs_t * p )
{ {
// remove strange characters (this can lead to name clashes) // remove strange characters (this can lead to name clashes)
int iToken; int iToken;
/* commented out for SMT comp
char * pTemp; char * pTemp;
if ( *pStart == '?' ) if ( *pStart == '?' )
*pStart = '_'; *pStart = '_';
for ( pTemp = pStart; pTemp < p->pCur; pTemp++ ) for ( pTemp = pStart; pTemp < p->pCur; pTemp++ )
if ( *pTemp == '.' ) if ( *pTemp == '.' )
*pTemp = '_'; *pTemp = '_';*/
// create and save token for this string // create and save token for this string
iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL ); 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) );
......
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