Making sure 'inv_out' can match flops by name.

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