Skip to content

A
abc
Commit c688d1b1 by Alan Mishchenko
Options

Improving SMT-LIB parser.

parent 0f29f0ae
Showing with 38 additions and 27 deletions
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]; }
......
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);
......
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) )
......
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 )
......
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)) )
......
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) );
......
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