diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-23 10:42:53 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-23 10:42:53 -0700 |
| commit | c688d1b158170b83d15dd9005b0534c42957f507 (patch) | |
| tree | 4f155dd7d5b9e234a40fc74be88e1ca954758a9c /src/base/wlc/wlcWriteVer.c | |
| parent | 0f29f0aec9b6b8fe3a0b83ed52cb1dda38819650 (diff) | |
| download | abc-c688d1b158170b83d15dd9005b0534c42957f507.tar.gz abc-c688d1b158170b83d15dd9005b0534c42957f507.tar.bz2 abc-c688d1b158170b83d15dd9005b0534c42957f507.zip | |
Improving SMT-LIB parser.
Diffstat (limited to 'src/base/wlc/wlcWriteVer.c')
| -rw-r--r-- | src/base/wlc/wlcWriteVer.c | 6 |
1 files changed, 4 insertions, 2 deletions
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) ); |