luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Bug-fix in SMT-LIB parser (incorrect handling of arithmetic right-shift).

This commit is contained in:
Alan Mishchenko 2016-07-12 13:34:06 -07:00
parent 4ffc14fd56
commit 3b76bc2792
2 changed files with 18 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/wlc/wlcCom.c
View File

@ -128,10 +128,10 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
switch ( c ) switch ( c )
{ {
case 'o': case 'o':
fPrintTree ^= 1; fOldParser ^= 1;
break; break;
case 'p': case 'p':
fOldParser ^= 1; fPrintTree ^= 1;
break; break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;

22
src/base/wlc/wlcReadSmt.c
View File

@ -276,13 +276,9 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in
assert( fSigned >= 0 ); assert( fSigned >= 0 );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
if ( fSigned ) if ( fSigned )
{
Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
// if ( Vec_IntSize(vFanins) > 0 ) if ( Type == WLC_OBJ_SHIFT_RA )
// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned; Wlc_NtkObj(pNtk, iObj)->Signed = 1;
// if ( Vec_IntSize(vFanins) > 1 )
// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned;
}
if ( pName == NULL ) if ( pName == NULL )
{ {
sprintf( Buffer, "_n%d_", iObj ); sprintf( Buffer, "_n%d_", iObj );
@ -511,6 +507,13 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p )
// skip () // skip ()
Fan = Vec_IntEntry(vFans, 2); Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) ); 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) // check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3); Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) ) if ( Smt_EntryIsName(Fan) )
@ -921,6 +924,13 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// skip () // skip ()
Fan = Vec_IntEntry(vFans, 2); Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) ); 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) // check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3); Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) ) if ( Smt_EntryIsName(Fan) )