diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/wlc/wlcReadSmt.c | 13 | ||||
-rw-r--r-- | src/base/wlc/wlcStdin.c | 32 |
2 files changed, 18 insertions, 27 deletions
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index a3614dde..49463aae 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -612,7 +612,7 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) Wlc_Ntk_t * pNtk; char * pName, * pBits, * pConst; 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 pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 ); pNtk->pManName = Abc_NamStart( 1000, 24 ); @@ -629,14 +629,9 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) assert( !fFound ); assert( iObj == NameId ); // save values - Vec_IntForEachEntry( &p->vValues, Entry, k ) - if ( Entry == NameOld ) - { - Vec_IntPush( &pNtk->vValues, NameId ); - Vec_IntPush( &pNtk->vValues, nBits ); - Vec_IntPush( &pNtk->vValues, atoi(pBits) ); - break; - } + Vec_IntPush( &pNtk->vValues, NameId ); + Vec_IntPush( &pNtk->vValues, nBits ); + Vec_IntPush( &pNtk->vValues, atoi(pBits) ); nBits += atoi(pBits); } while ( Vec_IntEntry(&p->vData, ++i) ); diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c index bb9c9614..fa2a3217 100644 --- a/src/base/wlc/wlcStdin.c +++ b/src/base/wlc/wlcStdin.c @@ -65,14 +65,15 @@ Vec_Str_t * Wlc_ConvertToRadix( unsigned * pBits, int Start, int nBits, int Radi Vec_Str_t * vSum = Vec_StrStart( nBits ); char * pRes = Vec_StrArray( vRes ); char * pSum = Vec_StrArray( vSum ); int i; - assert( Radix > 2 && Radix < 36 ); + assert( Radix >= 2 && Radix < 36 ); pSum[0] = 1; // compute number for ( i = 0; i < nBits; i++ ) { if ( Abc_InfoHasBit(pBits, Start + i) ) Wlc_ComputeSum( pRes, pSum, nBits, Radix ); - Wlc_ComputeSum( pSum, pSum, nBits, Radix ); + if ( i < nBits - 1 ) + Wlc_ComputeSum( pSum, pSum, nBits, Radix ); } Vec_StrFree( vSum ); // remove zeros @@ -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 ) { Vec_Str_t * vNum; - Wlc_Obj_t * pObj; - int i, ObjId, Start, nBits = -1; + int i, NameId, Name, Start, nBits = -1; assert( pCex->nRegs == 0 ); - // get the node ID - ObjId = Abc_NamStrFind( p->pManName, pName ); - if ( ObjId <= 0 ) + // get the name ID + NameId = Abc_NamStrFind( p->pManName, pName ); + if ( NameId <= 0 ) { printf( "Cannot find \"%s\" among nodes of the network.\n", pName ); return; } - // find the PI - Start = 0; - Wlc_NtkForEachPi( p, pObj, i ) - { - nBits = Wlc_ObjRange( pObj ); - if ( Wlc_ObjId(p, pObj) == ObjId ) + // get the primary input + Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i ) + if ( Name == NameId ) break; - Start += nBits; - } - if ( i == Wlc_NtkPiNum(p) ) + // find the PI + if ( i == Vec_IntSize(&p->vValues) ) { printf( "Cannot find \"%s\" among primary inputs of the network.\n", pName ); return; } // print value - assert( Radix == 10 || Radix == 16 ); + assert( Radix == 2 || Radix == 10 || Radix == 16 ); 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 ); } |