summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/wlc/wlcAbc.c54
-rw-r--r--src/base/wlc/wlcBlast.c11
-rw-r--r--src/base/wlc/wlcCom.c4
3 files changed, 51 insertions, 18 deletions
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index 1f10d7b0..e19aaaec 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -185,8 +185,9 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs )
+Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia )
{
+ int nRegs = Gia_ManRegNum(pGia);
Vec_Int_t * vRes = NULL;
if ( Abc_NtkPoNum(pNtk) != 1 )
printf( "The number of outputs is other than 1.\n" );
@@ -194,26 +195,57 @@ Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs )
printf( "The number of internal nodes is other than 1.\n" );
else
{
- Abc_Obj_t * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
+ Abc_Nam_t * pNames = NULL;
+ Abc_Obj_t * pFanin, * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
char * pName, * pCube, * pSop = (char *)pNode->pData;
Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
- Abc_Obj_t * pFanin; int i, k, Value, nLits;
+ int i, k, Value, nLits, Counter = 0;
+ if ( pGia->vNamesIn )
+ {
+ // hash the names
+ pNames = Abc_NamStart( 100, 16 );
+ Vec_PtrForEachEntry( char *, pGia->vNamesIn, pName, i )
+ {
+ Value = Abc_NamStrFindOrAdd( pNames, pName, NULL );
+ assert( Value == i+1 );
+ //printf( "%s(%d) ", pName, i );
+ }
+ //printf( "\n" );
+ }
Abc_ObjForEachFanin( pNode, pFanin, i )
{
assert( Abc_ObjIsCi(pFanin) );
pName = Abc_ObjName(pFanin);
- for ( k = (int)strlen(pName)-1; k >= 0; k-- )
- if ( pName[k] < '0' || pName[k] > '9' )
- break;
- if ( k == (int)strlen(pName)-1 )
+ if ( pNames )
+ {
+ Value = Abc_NamStrFind(pNames, pName) - 1;
+ if ( Value == -1 )
+ {
+ if ( Counter++ == 0 )
+ printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
+ Value = i;
+ }
+ }
+ else
{
- printf( "Cannot read input name of fanin %d.\n", i );
- Value = i;
+ for ( k = (int)strlen(pName)-1; k >= 0; k-- )
+ if ( pName[k] < '0' || pName[k] > '9' )
+ break;
+ if ( k == (int)strlen(pName)-1 )
+ {
+ if ( Counter++ == 0 )
+ printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
+ Value = i;
+ }
+ else
+ Value = atoi(pName + k + 1);
}
- else
- Value = atoi(pName + k + 1);
Vec_IntPush( vFanins, Value );
}
+ if ( Counter )
+ printf( "Cannot read names for %d inputs of the invariant.\n", Counter );
+ if ( pNames )
+ Abc_NamStop( pNames );
assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
vRes = Vec_IntAlloc( 1000 );
Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index b49c2dd7..67d7c902 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -872,6 +872,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
int fVerbose = 0;
int fUseOldMultiplierBlasting = 0;
+ int fSkipBitRange = 0;
Tim_Man_t * pManTime = NULL;
Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
Wlc_Obj_t * pObj;
@@ -1448,7 +1449,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1475,7 +1476,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1498,7 +1499,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1513,7 +1514,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1532,7 +1533,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 3bbe843f..cc69c636 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -1051,7 +1051,7 @@ usage:
******************************************************************************/
int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs );
+ extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia );
Vec_Int_t * vInv = NULL;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c, fVerbose = 0;
@@ -1080,7 +1080,7 @@ int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// derive the network
- vInv = Wlc_NtkGetPut( pNtk, Gia_ManRegNum(pAbc->pGia) );
+ vInv = Wlc_NtkGetPut( pNtk, pAbc->pGia );
if ( vInv )
Abc_FrameSetInv( vInv );
return 0;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 14:06:31 +0000