From c688d1b158170b83d15dd9005b0534c42957f507 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 23 May 2016 10:42:53 -0700 Subject: Improving SMT-LIB parser. --- src/base/wlc/wlc.h | 18 ++++++++++-------- src/base/wlc/wlcBlast.c | 2 +- src/base/wlc/wlcNtk.c | 19 ++++++++++++------- src/base/wlc/wlcReadSmt.c | 18 ++++++++++-------- src/base/wlc/wlcReadVer.c | 2 +- src/base/wlc/wlcWriteVer.c | 6 ++++-- 6 files changed, 38 insertions(+), 27 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index b12e239c..0165a0a4 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -89,13 +89,14 @@ typedef enum { 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_OBJ_ARI_REM, // 47: arithmetic remainder + WLC_OBJ_ARI_MODULUS, // 48: arithmetic modulus + WLC_OBJ_ARI_POWER, // 49: arithmetic power + WLC_OBJ_ARI_MINUS, // 50: arithmetic minus + WLC_OBJ_ARI_SQRT, // 51: integer square root + WLC_OBJ_ARI_SQUARE, // 52: integer square + WLC_OBJ_TABLE, // 53: bit table + WLC_OBJ_NUMBER // 54: unused } Wlc_ObjType_t; // when adding new types, remember to update table Wlc_Names in "wlcNtk.c" @@ -138,6 +139,7 @@ struct Wlc_Ntk_t_ char * pInits; // initial values int nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type int nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting + int fSmtLib; // the network comes from an SMT-LIB file // memory for objects Wlc_Obj_t * pObjs; int iObj; @@ -196,7 +198,7 @@ static inline int Wlc_ObjRangeBeg( Wlc_Obj_t * p ) static inline int Wlc_ObjRangeIsReversed( Wlc_Obj_t * p ) { return p->End < p->Beg; } static inline int Wlc_ObjIsSigned( Wlc_Obj_t * p ) { return p->Signed; } -static inline int Wlc_ObjIsSignedFanin01( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ){ return Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed; } +static inline int Wlc_ObjIsSignedFanin01( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ){ return p->fSmtLib ? Wlc_ObjIsSigned(pObj) : (Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed); } static inline int Wlc_ObjSign( Wlc_Obj_t * p ) { return Abc_Var2Lit( Wlc_ObjRange(p), Wlc_ObjIsSigned(p) ); } static inline int * Wlc_ObjConstValue( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_CONST); return Wlc_ObjFanins(p); } static inline int Wlc_ObjTableId( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_TABLE); return p->Fanins[1]; } diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 5ef7ef14..f6cd9310 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1130,7 +1130,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple assert( Vec_IntSize(vRes) == nRange ); } } - else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_MODULUS ) + else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) { int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) ); int fSigned = Wlc_ObjIsSignedFanin01(p, pObj); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 726e7bf8..5a08cd99 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -78,13 +78,14 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = { "-", // 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 + "%", // 47: arithmetic reminder + "mod", // 48: arithmetic modulus + "**", // 49: arithmetic power + "-", // 50: arithmetic minus + "sqrt", // 51: integer square root + "square", // 52: integer square + "table", // 53: bit table + NULL // 54: unused }; //////////////////////////////////////////////////////////////////////// @@ -421,6 +422,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose ) Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_MULTI, 9 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)) ); else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE ) Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_DIVIDE, 13 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 19 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) + 10 ); + else if ( pObj->Type == WLC_OBJ_ARI_REM ) + Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_REM, 13 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 7 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 2 ); else if ( pObj->Type == WLC_OBJ_ARI_MODULUS ) Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_MODULUS, 13 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 7 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 2 ); else if ( pObj->Type == WLC_OBJ_ARI_POWER ) @@ -586,6 +589,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ) Wlc_NtkCleanCopy( p ); vFanins = Vec_IntAlloc( 100 ); pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc ); + pNew->fSmtLib = p->fSmtLib; Wlc_NtkForEachCi( p, pObj, i ) Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); Wlc_NtkForEachCo( p, pObj, i ) @@ -645,6 +649,7 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p ) Wlc_NtkCleanCopy( p ); vFanins = Vec_IntAlloc( 100 ); pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc ); + pNew->fSmtLib = p->fSmtLib; Wlc_NtkForEachObj( p, pObj, i ) { if ( Wlc_ObjIsCi(pObj) ) diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index d68688c4..9ebecb73 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -166,7 +166,7 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) else if ( !strcmp(pName, "zero_extend") ) Type = WLC_OBJ_BIT_ZEROPAD; // 21: zero padding else if ( !strcmp(pName, "sign_extend") ) - Type = WLC_OBJ_BIT_SIGNEXT, *pfSigned = 1; // 22: sign extension + Type = WLC_OBJ_BIT_SIGNEXT; // 22: sign extension else if ( !strcmp(pName, "not") ) Type = WLC_OBJ_LOGIC_NOT; // 23: logic NOT else if ( !strcmp(pName, "=>") ) @@ -212,11 +212,11 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) else if ( !strcmp(pName, "bvudiv") ) Type = WLC_OBJ_ARI_DIVIDE; // 39: arithmetic division else if ( !strcmp(pName, "bvurem") ) - Type = WLC_OBJ_ARI_MODULUS; // 40: arithmetic modulus + Type = WLC_OBJ_ARI_REM; // 40: arithmetic remainder else if ( !strcmp(pName, "bvsdiv") ) Type = WLC_OBJ_ARI_DIVIDE, *pfSigned = 1; // 39: arithmetic division else if ( !strcmp(pName, "bvsrem") ) - Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus + Type = WLC_OBJ_ARI_REM, *pfSigned = 1; // 40: arithmetic remainder else if ( !strcmp(pName, "bvsmod") ) Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus // else if ( !strcmp(pName, "") ) @@ -278,10 +278,10 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in 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; +// 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; } if ( pName == NULL ) { @@ -499,6 +499,7 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p ) // start network and create primary inputs pNtk = Wlc_NtkAlloc( p->pName, 1000 ); pNtk->pManName = Abc_NamStart( 1000, 24 ); + pNtk->fSmtLib = 1; Smt_ManForEachDir( p, SMT_PRS_DECLARE_FUN, vFans, i ) { assert( Vec_IntSize(vFans) == 4 ); @@ -797,7 +798,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, 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); + //fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT); if ( Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L ) { int iConst = Smt_PrsBuildConstant( pNtk, pStr2, -1, Smt_PrsGenName(p) ); @@ -899,6 +900,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) // start network and create primary inputs pNtk = Wlc_NtkAlloc( p->pName, 1000 ); pNtk->pManName = Abc_NamStart( 1000, 24 ); + pNtk->fSmtLib = 1; // collect top-level asserts vFansRoot = Vec_WecEntry( &p->vObjs, 0 ); Vec_IntForEachEntry( vFansRoot, Root, i ) diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index 7683f8a6..7753d24d 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -795,7 +795,7 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t * else if ( pStr[0] == '-' ) pStr += 1, Type = WLC_OBJ_ARI_SUB; else if ( pStr[0] == '*' && pStr[1] != '*' ) pStr += 1, Type = WLC_OBJ_ARI_MULTI; else if ( pStr[0] == '/' ) pStr += 1, Type = WLC_OBJ_ARI_DIVIDE; - else if ( pStr[0] == '%' ) pStr += 1, Type = WLC_OBJ_ARI_MODULUS; + else if ( pStr[0] == '%' ) pStr += 1, Type = WLC_OBJ_ARI_REM; else if ( pStr[0] == '*' && pStr[1] == '*' ) pStr += 2, Type = WLC_OBJ_ARI_POWER; else return Wlc_PrsWriteErrorMessage( p, pStr, "Unsupported operation (%c).", pStr[0] ); if ( !(pStr = Wlc_PrsReadName(p, pStr+1, vFanins)) ) diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c index b15d3d38..cf0e528f 100644 --- a/src/base/wlc/wlcWriteVer.c +++ b/src/base/wlc/wlcWriteVer.c @@ -171,7 +171,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) pObj->Mark = 0; continue; } - sprintf( Range, "%s[%d:%d]%*s", Wlc_ObjIsSigned(pObj) ? "signed ":" ", pObj->End, pObj->Beg, 8-nDigits, "" ); + sprintf( Range, "%s[%d:%d]%*s", (!p->fSmtLib && Wlc_ObjIsSigned(pObj)) ? "signed ":" ", pObj->End, pObj->Beg, 8-nDigits, "" ); fprintf( pFile, " " ); if ( pObj->Type == WLC_OBJ_PI || (fNoFlops && pObj->Type == WLC_OBJ_FO) ) fprintf( pFile, "input " ); @@ -342,6 +342,8 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) fprintf( pFile, "*" ); else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE ) fprintf( pFile, "/" ); + else if ( pObj->Type == WLC_OBJ_ARI_REM ) + fprintf( pFile, "%%" ); else if ( pObj->Type == WLC_OBJ_ARI_MODULUS ) fprintf( pFile, "%%" ); else if ( pObj->Type == WLC_OBJ_ARI_POWER ) @@ -355,7 +357,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) fprintf( pFile, " %s", Wlc_ObjName(p, Wlc_ObjFaninId(pObj, 1)) ); } } - fprintf( pFile, " ;\n" ); + fprintf( pFile, " ;%s\n", (p->fSmtLib && Wlc_ObjIsSigned(pObj)) ? " // signed SMT-LIB operator" : "" ); } iFanin = 0; assert( !p->vInits || Wlc_NtkFfNum(p) == Vec_IntSize(p->vInits) ); -- cgit v1.2.3