diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-12 13:34:06 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-12 13:34:06 -0700 |
| commit | 3b76bc2792e3e0b717d2eca5fc3469d5dfaaab0c (patch) | |
| tree | 16a598bca13e4d18ba4bc6247adda81b5dfb9727 | |
| parent | 4ffc14fd56b0f32351adffeec062c9086c5b9cb5 (diff) | |
| download | abc-3b76bc2792e3e0b717d2eca5fc3469d5dfaaab0c.tar.gz abc-3b76bc2792e3e0b717d2eca5fc3469d5dfaaab0c.tar.bz2 abc-3b76bc2792e3e0b717d2eca5fc3469d5dfaaab0c.zip | |
Bug-fix in SMT-LIB parser (incorrect handling of arithmetic right-shift).
| -rw-r--r-- | src/base/wlc/wlcCom.c | 4 | ||||
| -rw-r--r-- | src/base/wlc/wlcReadSmt.c | 22 |
2 files changed, 18 insertions, 8 deletions
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 77bf36ba..5f62f757 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -128,10 +128,10 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv ) switch ( c ) { case 'o': - fPrintTree ^= 1; + fOldParser ^= 1; break; case 'p': - fOldParser ^= 1; + fPrintTree ^= 1; break; case 'v': fVerbose ^= 1; diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index ed6092a5..fcd47274 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -276,13 +276,9 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in assert( fSigned >= 0 ); 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; - } + if ( Type == WLC_OBJ_SHIFT_RA ) + Wlc_NtkObj(pNtk, iObj)->Signed = 1; if ( pName == NULL ) { sprintf( Buffer, "_n%d_", iObj ); @@ -511,6 +507,13 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p ) // skip () Fan = Vec_IntEntry(vFans, 2); 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) Fan = Vec_IntEntry(vFans, 3); if ( Smt_EntryIsName(Fan) ) @@ -921,6 +924,13 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) // skip () Fan = Vec_IntEntry(vFans, 2); 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) Fan = Vec_IntEntry(vFans, 3); if ( Smt_EntryIsName(Fan) ) |