summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/wlc/wlcAbc.c54
-rw-r--r--src/base/wlc/wlcBlast.c11
-rw-r--r--src/base/wlc/wlcCom.c4
-rw-r--r--src/proof/pdr/pdrInv.c2
4 files changed, 53 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;
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 8130d0a3..95adb10c 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -756,6 +756,8 @@ int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver
// check if this cube intersects with the complement of other cubes in the solver
// if it does not intersect, then it is redundant and can be skipped
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+ if ( status != l_True && fVerbose )
+ printf( "Finished checking clause %d (out of %d)...\r", i, pList[0] );
if ( status == l_Undef ) // timeout
break;
if ( status == l_False ) // unsat -- correct
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 11:59:42 +0000