From ca710b3dda0848e552b4b13d72bb261b5089819c Mon Sep 17 00:00:00 2001
From: Tobias Wiersema <tobias.wiersema@uni-paderborn.de>
Date: Thu, 19 Aug 2021 17:23:03 +0200
Subject: Add inv_get -f to read flop names from GIA

---
 src/base/wlc/wlcAbc.c | 12 +++++++++---
 src/base/wlc/wlcCom.c | 36 +++++++++++++++++++++++++++++++-----
 2 files changed, 40 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index e1b06ffd..be254bb2 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -140,7 +140,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Ptr_t * vNamesIn )
 {
     extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
     extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
@@ -166,8 +166,14 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
             if ( Entry == 0 )
                 continue;
             pMainObj = Abc_NtkCreatePi( pMainNtk );
-            sprintf( Buffer, "pi%d", i );
-            Abc_ObjAssignName( pMainObj, Buffer, NULL );
+            if (vNamesIn != NULL && i < Vec_PtrSize(vNamesIn)) {
+                Abc_ObjAssignName( pMainObj, (char *)Vec_PtrEntry(vNamesIn, i), NULL );
+            }
+            else
+            {
+                sprintf( Buffer, "pi%d", i );
+                Abc_ObjAssignName( pMainObj, Buffer, NULL );
+            }
         }
         if ( Abc_NtkPiNum(pMainNtk) != nInputs )
         {
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 666a8776..cf9805c5 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -1727,15 +1727,19 @@ usage:
 ******************************************************************************/
 int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv );
+    extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Ptr_t * vNamesIn );
     Abc_Ntk_t * pMainNtk;
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
-    int c, fVerbose  = 0;
+    int c, i, fVerbose = 0, fFlopNamesFromGia = 0;
+    Vec_Ptr_t * vNamesIn = NULL;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'f':
+                fFlopNamesFromGia ^= 1;
+                break;
             case 'v':
                 fVerbose ^= 1;
                 break;
@@ -1750,16 +1754,38 @@ int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
         return 0;
     }
+    // See if we shall and can copy the PI names from the current GIA
+    if ( fFlopNamesFromGia )
+    {
+        if ( pAbc->pGia == NULL )
+        {
+            Abc_Print( 1, "Abc_CommandInvGet(): No network in &-space, cannot copy names.\n" );
+            fFlopNamesFromGia = 0;
+        }
+        else
+        {
+            vNamesIn = Vec_PtrStart( Gia_ManRegNum(pAbc->pGia) );
+            for ( i = 0; i < Gia_ManRegNum(pAbc->pGia); ++i )
+            {
+                // Only the registers
+                Vec_PtrSetEntry( vNamesIn, i, Extra_UtilStrsav( (const char*)Vec_PtrEntry( pAbc->pGia->vNamesIn, Gia_ManPiNum(pAbc->pGia)+i ) ) );
+            }
+        }
+    }
     // derive the network
-    pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) );
+    pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), vNamesIn );
+    // Delete names
+    if (vNamesIn)
+        Vec_PtrFree( vNamesIn );
     // replace the current network
     if ( pMainNtk )
         Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: inv_get [-vh]\n" );
+    Abc_Print( -2, "usage: inv_get [-fvh]\n" );
     Abc_Print( -2, "\t         places invariant found by PDR as the current network in the main-space\n" );
     Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
+    Abc_Print( -2, "\t-f     : toggle reading flop names from the &-space [default = %s]\n", fFlopNamesFromGia? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
-- 
cgit v1.2.3