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

Modifications to read SMTLIB file from stdin.

This commit is contained in:
Alan Mishchenko 2015-02-18 21:02:17 -08:00
parent d5cfb39a48
commit 4cd7895d6c
2 changed files with 18 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -612,7 +612,7 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
Wlc_Ntk_t * pNtk; Wlc_Ntk_t * pNtk;
char * pName, * pBits, * pConst; char * pName, * pBits, * pConst;
Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); Vec_Int_t * vFanins = Vec_IntAlloc( 100 );
int i, k, iObj, Type, Entry, NameId, fFound, Range, fSigned, nBits = 0; int i, iObj, Type, Entry, NameId, fFound, Range, fSigned, nBits = 0;
// start network and create primary inputs // start network and create primary inputs
pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 ); pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 );
pNtk->pManName = Abc_NamStart( 1000, 24 ); pNtk->pManName = Abc_NamStart( 1000, 24 );
@ -629,14 +629,9 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
assert( !fFound ); assert( !fFound );
assert( iObj == NameId ); assert( iObj == NameId );
// save values // save values
Vec_IntForEachEntry( &p->vValues, Entry, k )
if ( Entry == NameOld )
{
Vec_IntPush( &pNtk->vValues, NameId ); Vec_IntPush( &pNtk->vValues, NameId );
Vec_IntPush( &pNtk->vValues, nBits ); Vec_IntPush( &pNtk->vValues, nBits );
Vec_IntPush( &pNtk->vValues, atoi(pBits) ); Vec_IntPush( &pNtk->vValues, atoi(pBits) );
break;
}
nBits += atoi(pBits); nBits += atoi(pBits);
} }
while ( Vec_IntEntry(&p->vData, ++i) ); while ( Vec_IntEntry(&p->vData, ++i) );

30
src/base/wlc/wlcStdin.c
View File

@ -65,13 +65,14 @@ Vec_Str_t * Wlc_ConvertToRadix( unsigned * pBits, int Start, int nBits, int Radi
Vec_Str_t * vSum = Vec_StrStart( nBits ); Vec_Str_t * vSum = Vec_StrStart( nBits );
char * pRes = Vec_StrArray( vRes ); char * pRes = Vec_StrArray( vRes );
char * pSum = Vec_StrArray( vSum ); int i; char * pSum = Vec_StrArray( vSum ); int i;
assert( Radix > 2 && Radix < 36 ); assert( Radix >= 2 && Radix < 36 );
pSum[0] = 1; pSum[0] = 1;
// compute number // compute number
for ( i = 0; i < nBits; i++ ) for ( i = 0; i < nBits; i++ )
{ {
if ( Abc_InfoHasBit(pBits, Start + i) ) if ( Abc_InfoHasBit(pBits, Start + i) )
Wlc_ComputeSum( pRes, pSum, nBits, Radix ); Wlc_ComputeSum( pRes, pSum, nBits, Radix );
if ( i < nBits - 1 )
Wlc_ComputeSum( pSum, pSum, nBits, Radix ); Wlc_ComputeSum( pSum, pSum, nBits, Radix );
} }
Vec_StrFree( vSum ); Vec_StrFree( vSum );
@ -109,34 +110,29 @@ Vec_Str_t * Wlc_ConvertToRadix( unsigned * pBits, int Start, int nBits, int Radi
void Wlc_NtkReport( Wlc_Ntk_t * p, Abc_Cex_t * pCex, char * pName, int Radix ) void Wlc_NtkReport( Wlc_Ntk_t * p, Abc_Cex_t * pCex, char * pName, int Radix )
{ {
Vec_Str_t * vNum; Vec_Str_t * vNum;
Wlc_Obj_t * pObj; int i, NameId, Name, Start, nBits = -1;
int i, ObjId, Start, nBits = -1;
assert( pCex->nRegs == 0 ); assert( pCex->nRegs == 0 );
// get the node ID // get the name ID
ObjId = Abc_NamStrFind( p->pManName, pName ); NameId = Abc_NamStrFind( p->pManName, pName );
if ( ObjId <= 0 ) if ( NameId <= 0 )
{ {
printf( "Cannot find \"%s\" among nodes of the network.\n", pName ); printf( "Cannot find \"%s\" among nodes of the network.\n", pName );
return; return;
} }
// find the PI // get the primary input
Start = 0; Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i )
Wlc_NtkForEachPi( p, pObj, i ) if ( Name == NameId )
{
nBits = Wlc_ObjRange( pObj );
if ( Wlc_ObjId(p, pObj) == ObjId )
break; break;
Start += nBits; // find the PI
} if ( i == Vec_IntSize(&p->vValues) )
if ( i == Wlc_NtkPiNum(p) )
{ {
printf( "Cannot find \"%s\" among primary inputs of the network.\n", pName ); printf( "Cannot find \"%s\" among primary inputs of the network.\n", pName );
return; return;
} }
// print value // print value
assert( Radix == 10 || Radix == 16 ); assert( Radix == 2 || Radix == 10 || Radix == 16 );
vNum = Wlc_ConvertToRadix( pCex->pData, Start, nBits, Radix ); vNum = Wlc_ConvertToRadix( pCex->pData, Start, nBits, Radix );
printf( "((%s %s%s))\n", pName, Radix == 16 ? "#x" : "", Vec_StrArray(vNum) ); printf( "((%s %s%s))\n", pName, Radix == 16 ? "#x" : (Radix == 2 ? "#b" : ""), Vec_StrArray(vNum) );
Vec_StrFree( vNum ); Vec_StrFree( vNum );
} }