summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/wlc/wlc.h18
-rw-r--r--src/base/wlc/wlcBlast.c2
-rw-r--r--src/base/wlc/wlcNtk.c19
-rw-r--r--src/base/wlc/wlcReadSmt.c18
-rw-r--r--src/base/wlc/wlcReadVer.c2
-rw-r--r--src/base/wlc/wlcWriteVer.c6
6 files changed, 38 insertions, 27 deletions
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) );
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 14:12:15 +0000