Adding new utility procedures.

6 files changed, 159 insertions, 45 deletions

diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h
index cfe090bb..0a188d0f 100644
--- a/src/base/acb/acb.h
+++ b/src/base/acb/acb.h
@@ -1023,7 +1023,7 @@ extern Vec_Int_t * Acb_ObjCollectTfiVec( Acb_Ntk_t * p, Vec_Int_t * vObjs );
 extern Vec_Int_t * Acb_ObjCollectTfoVec( Acb_Ntk_t * p, Vec_Int_t * vObjs );
 extern int         Acb_NtkCountPiBuffers( Acb_Ntk_t * p, Vec_Int_t * vObjs );
 extern int         Acb_NtkCountPoDrivers( Acb_Ntk_t * p, Vec_Int_t * vObjs );
-extern int         Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjs, int nGates[5] );
+extern int         Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjsRefed, Vec_Int_t * vObjsDerefed, int nGates[5] );
 
 extern int         Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj );
 extern int         Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo );
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index 4af33903..565dbb06 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -1905,6 +1905,42 @@ Vec_Int_t * Acb_GetUsedDivs( Vec_Int_t * vDivs, Vec_Int_t * vUsed )
         Vec_IntPush( vRes, iObj );
     return vRes;
 }
+Vec_Int_t * Acb_GetDerefedNodes( Acb_Ntk_t * p )
+{
+    Vec_Ptr_t * vNames = Abc_FrameReadSignalNames();
+    if ( vNames != NULL )
+    {
+        Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
+        Vec_Int_t * vMap   = Vec_IntStartFull( Abc_NamObjNumMax(p->pDesign->pStrs) );
+        int i, iObj; char * pName;
+        Acb_NtkForEachObj( p, iObj )
+            if ( Acb_ObjName(p, iObj) )
+                Vec_IntWriteEntry( vMap, Acb_ObjName(p, iObj), iObj );
+        Vec_PtrForEachEntry( char *, vNames, pName, i )
+        {
+            int NameId = Abc_NamStrFindOrAdd( p->pDesign->pStrs, pName, NULL );
+            if ( NameId == 0 )
+            {
+                printf( "Cannot find name ID for name %s\n", pName );
+                Vec_IntFree( vMap );
+                Vec_IntFree( vNodes );
+                return NULL;
+            }
+            else if ( Vec_IntEntry(vMap, NameId) == -1 )
+            {
+                printf( "Cannot find obj ID for name %s\n", pName );
+                Vec_IntFree( vMap );
+                Vec_IntFree( vNodes );
+                return NULL;
+            }
+            else
+                Vec_IntPush( vNodes, Vec_IntEntry(vMap, NameId) );
+        }
+        Vec_IntFree( vMap );
+        return vNodes;
+    }
+    return NULL;
+}
 Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Ptr_t * vSops, Vec_Ptr_t * vGias, Vec_Int_t * vTars )
 {
     extern Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops );
@@ -1912,15 +1948,19 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
     Vec_Wec_t * vGates = vGias ? Abc_GiaSynthesize(vGias, NULL) : Abc_SopSynthesize(vSops);  Vec_Int_t * vGate;
     int nOuts = vGias ? Vec_PtrSize(vGias) : Vec_PtrSize(vSops);
     int i, k, iObj, nWires = Vec_WecSize(vGates) - Vec_IntSize(vUsed) - nOuts, fFirst = 1;
-    int nGates[5] = {0}, nInvs = 0, nBufs = 0, nNodes = 0, nConst[2] = {0};
+    int nGates1[5] = {0}, nGates0[5] = {0};
     Vec_Ptr_t * vNames = Acb_GenerateSignalNames( p, vDivs, vUsed, nWires, vTars, vGates );
     Vec_Str_t * vStr = Vec_StrAlloc( 100 );
     Vec_Int_t * vSup = Acb_GetUsedDivs( vDivs, vUsed );
+    Vec_Int_t * vDrf = Acb_GetDerefedNodes( p );
     Vec_Int_t * vTfi = Acb_ObjCollectTfiVec( p, vSup );
     Vec_Int_t * vTfo = Acb_ObjCollectTfoVec( p, vTars );
     int nPiCount = Acb_NtkCountPiBuffers( p, vSup );
     int nPoCount = Acb_NtkCountPoDrivers( p, vTars );
-    int nMffc    = Acb_NtkFindMffcSize( p, vSup, nGates );
+    int nMffc    = vDrf ? Vec_IntSize(vTars) + Acb_NtkFindMffcSize( p, vSup, vDrf, nGates1 ) : 0;
+    int * pCounts = Abc_FrameReadGateCounts();
+    for ( i = 0; i < 5; i++ )
+        nGates1[i] += pCounts[i];
     Vec_IntFree( vSup );
     Vec_WecForEachLevelStartStop( vGates, vGate, i, Vec_IntSize(vUsed), Vec_IntSize(vUsed)+nWires )
     {
@@ -1928,20 +1968,23 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
         {
             char * pName = Acb_Oper2Name(Vec_IntEntry(vGate, 0));
             if ( !strcmp(pName, "buf") )
-                nBufs++;
+                nGates0[2]++;
             else if ( !strcmp(pName, "not") )
-                nInvs++;
+                nGates0[3]++;
             else
-                nNodes += Vec_IntSize(vGate) - 3;
+                nGates0[4] += Vec_IntSize(vGate) - 3;
         }
         else
-            nConst[Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T]++;
+            nGates0[Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T]++;
     }
 
     Vec_StrPrintF( vStr, "// Patch   : in = %d  out = %d : pi_in = %d  po_out = %d : tfi = %d  tfo = %d\n", Vec_IntSize(vUsed), nOuts, nPiCount, nPoCount, Vec_IntSize(vTfi), Vec_IntSize(vTfo) );
-    Vec_StrPrintF( vStr, "// Added   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires,       nConst[0], nConst[1], nBufs,     nInvs,     nNodes ); 
-    Vec_StrPrintF( vStr, "// Removed : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nMffc,        nGates[0], nGates[1], nGates[2], nGates[3], nGates[4] ); 
-    Vec_StrPrintF( vStr, "// TOTAL   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n\n", nWires-nMffc, nConst[0]-nGates[0],  nConst[1]-nGates[1],  nBufs-nGates[2], nInvs-nGates[3], nNodes-nGates[4] ); 
+    Vec_StrPrintF( vStr, "// Added   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires,         nGates0[0], nGates0[1], nGates0[2], nGates0[3], nGates0[4] ); 
+    if ( vDrf != NULL )
+    Vec_StrPrintF( vStr, "// Removed : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nMffc,          nGates1[0], nGates1[1], nGates1[2], nGates1[3], nGates1[4] ); 
+    if ( vDrf != NULL )
+    Vec_StrPrintF( vStr, "// TOTAL   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires-nMffc, nGates0[0]-nGates1[0],  nGates0[1]-nGates1[1],  nGates0[2]-nGates1[2], nGates0[3]-nGates1[3], nGates0[4]-nGates1[4] ); 
+    Vec_StrPrintF( vStr, "\n" );
 
     Vec_StrAppend( vStr, "module patch (" );
 
@@ -2003,9 +2046,13 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
 //    printf( "Summary of the results\n" );
     printf( "\n" );
     printf( "Patch   : in = %d  out = %d : pi_in = %d  po_out = %d : tfi = %d  tfo = %d\n", Vec_IntSize(vUsed), nOuts, nPiCount, nPoCount, Vec_IntSize(vTfi), Vec_IntSize(vTfo) );
-    printf( "Added   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires,       nConst[0], nConst[1], nBufs,     nInvs,     nNodes ); 
-    printf( "Removed : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nMffc,        nGates[0], nGates[1], nGates[2], nGates[3], nGates[4] ); 
-    printf( "TOTAL   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires-nMffc, nConst[0]-nGates[0],  nConst[1]-nGates[1],  nBufs-nGates[2], nInvs-nGates[3], nNodes-nGates[4] ); 
+    printf( "Added   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires,         nGates0[0], nGates0[1], nGates0[2], nGates0[3], nGates0[4] ); 
+    if ( vDrf != NULL )
+    printf( "Removed : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nMffc,          nGates1[0], nGates1[1], nGates1[2], nGates1[3], nGates1[4] ); 
+    if ( vDrf != NULL )
+    printf( "TOTAL   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires-nMffc,   nGates0[0]-nGates1[0],  nGates0[1]-nGates1[1],  nGates0[2]-nGates1[2], nGates0[3]-nGates1[3], nGates0[4]-nGates1[4] ); 
+    printf( "\n" );
+    Vec_IntFreeP( &vDrf );
     return vStr;
 }
 
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index 680dca12..d707d136 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -21,6 +21,7 @@
 #include "acb.h"
 #include "base/abc/abc.h"
 #include "base/io/ioAbc.h"
+#include "base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -166,67 +167,65 @@ int Acb_NtkCountPoDrivers( Acb_Ntk_t * p, Vec_Int_t * vObjs )
   SeeAlso     []
 
 ***********************************************************************/
-int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5] )
+int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj )
 {
     int i, Fanin, * pFanins, Counter = 1;
     if ( Acb_ObjIsCi(p, iObj) )
         return 0;
-    if ( nGates )
-    {
-        int Type = Acb_ObjType( p, iObj );
-        if ( Type == ABC_OPER_CONST_F ) 
-            nGates[0]++;
-        if ( Type == ABC_OPER_CONST_T ) 
-            nGates[1]++;
-        if ( Type == ABC_OPER_BIT_BUF ) 
-            nGates[2]++;
-        if ( Type == ABC_OPER_BIT_INV ) 
-            nGates[3]++;
-        else
-            nGates[4] += Acb_ObjFaninNum(p, iObj)-1;
-    }
     Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
     {
         assert( Vec_IntEntry(vRefs, Fanin) > 0 );
         Vec_IntAddToEntry( vRefs, Fanin, -1 );
         if ( Vec_IntEntry(vRefs, Fanin) == 0 )
-            Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin, nGates );
+            Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin );
     }
     return Counter;
 }
-int Acb_NtkNodeRef_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj )
+int Acb_NtkNodeRef_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5] )
 {
     int i, Fanin, * pFanins, Counter = 1;
     if ( Acb_ObjIsCi(p, iObj) )
         return 0;
+    if ( nGates )
+    {
+        int nFan = Acb_ObjFaninNum(p, iObj);
+        int Type = Acb_ObjType( p, iObj );
+        if ( Type == ABC_OPER_CONST_F ) 
+            nGates[0]++;
+        else if ( Type == ABC_OPER_CONST_T ) 
+            nGates[1]++;
+        else if ( Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_CO ) 
+            nGates[2]++;
+        else if ( Type == ABC_OPER_BIT_INV ) 
+            nGates[3]++;
+        else
+        {
+            assert( nFan >= 2 );
+            nGates[4] += Acb_ObjFaninNum(p, iObj)-1;
+        }
+    }
     Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
     {
         if ( Vec_IntEntry(vRefs, Fanin) == 0 )
-            Counter += Acb_NtkNodeRef_rec( vRefs, p, Fanin );
+            Counter += Acb_NtkNodeRef_rec( vRefs, p, Fanin, nGates );
         Vec_IntAddToEntry( vRefs, Fanin, 1 );
     }
     return Counter;
 }
-int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjs, int nGates[5] )
+int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjsRefed, Vec_Int_t * vObjsDerefed, int nGates[5] )
 {
     Vec_Int_t * vRefs = Vec_IntStart( Acb_NtkObjNumMax(p) );
-    int i, iObj, Fanin, * pFanins, Count1 = 0, Count2 = 0;
+    int i, iObj, Fanin, * pFanins, Count2 = 0;
     Acb_NtkForEachObj( p, iObj )
         Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
             Vec_IntAddToEntry( vRefs, Fanin, 1 );
-    //Vec_IntForEachEntry( vObjs, iObj, i )
-    //    assert( Vec_IntEntry(vRefs, iObj) > 0 );
-    Vec_IntForEachEntry( vObjs, iObj, i )
-        Vec_IntAddToEntry( vRefs, iObj, 1 );
-    Vec_IntForEachEntry( vObjs, iObj, i )
-        Count1 += Acb_NtkNodeDeref_rec( vRefs, p, iObj, nGates );
-    Vec_IntForEachEntry( vObjs, iObj, i )
-        Count2 += Acb_NtkNodeRef_rec( vRefs, p, iObj );
-    Vec_IntForEachEntry( vObjs, iObj, i )
-        Vec_IntAddToEntry( vRefs, iObj, -1 );
-    assert( Count1 == Count2 );
+    Vec_IntForEachEntry( vObjsRefed, iObj, i )
+        Acb_NtkNodeRef_rec( vRefs, p, iObj, NULL );
+    Vec_IntForEachEntry( vObjsDerefed, iObj, i )
+        if ( Vec_IntEntry(vRefs, iObj) == 0 )
+            Count2 += Acb_NtkNodeRef_rec( vRefs, p, iObj, nGates );
     Vec_IntFree( vRefs );
-    return Count1;
+    return Count2;
 }
 
 /**Function*************************************************************
@@ -942,6 +941,63 @@ int Abc_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
   SeeAlso     []
 
 ***********************************************************************/
+void Acb_NtkFindNamesInPlaces( char * pBuffer, Vec_Int_t * vPlaces, Vec_Ptr_t * vPivots )
+{
+    int * pCounts = Abc_FrameReadGateCounts();
+    Vec_Ptr_t * vNames = Vec_PtrAlloc( 100 );
+    int i, k, iObj, Pos;
+    for ( i = 0; i < 5; i++ )
+        pCounts[i] = 0;
+    Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
+    {
+        int nFanins = 0;
+        char pLocal[1000], * pTemp, * pName, * pSpot;
+        char * pPivot = (char *)Vec_PtrEntry(vPivots, iObj);
+        for ( k = 0; k < 1000; k++ )
+        {
+            if ( pBuffer[Pos+k] == '\n' )
+            {
+                pLocal[k] = 0;
+                break;
+            }
+            else
+                pLocal[k] = pBuffer[Pos+k];
+        }
+        assert( k < 1000 );
+        pSpot = strstr( pLocal, pPivot );
+        if ( pSpot == NULL )
+        {
+            printf( "Cannot find location of signal \"%s\" in this line.\n", pPivot );
+            continue;
+        }
+        pTemp = strtok( pLocal, " \r\n\t,;()" );
+        while ( pTemp )
+        {
+            if ( !strcmp(pTemp, "1\'b0") )
+                pCounts[0]++;
+            else if ( !strcmp(pTemp, "1\'b1") )
+                pCounts[1]++;
+            else if ( !strcmp(pTemp, "buf") || !strcmp(pTemp, "assign") )
+                pCounts[2]++;
+            else if ( !strcmp(pTemp, "not") )
+                pCounts[3]++;
+            else if ( strcmp(pTemp, pPivot) && pTemp > pSpot )
+            {
+                nFanins++;
+                Vec_PtrForEachEntry( char *, vNames, pName, k )
+                    if ( !strcmp(pName, pTemp) )
+                        break;
+                if ( k == Vec_PtrSize(vNames) )
+                    Vec_PtrPush( vNames, Abc_UtilStrsav(pTemp) );
+            }
+            pTemp = strtok( NULL, " \r\n\t,;()" );
+        }
+        if ( nFanins > 1 )
+            pCounts[4] += nFanins-1;
+    }
+    //printf( "Found %d names\n", Vec_PtrSize(vNames) );
+    Abc_FrameSetSignalNames( vNames );
+}
 Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames )
 {
     Vec_Int_t * vPlaces; int First = 1, Pos = -1, fComment = 0;
@@ -1002,6 +1058,7 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames,
         return;
     }
     vPlaces = Acb_NtkPlaces( pFileNameIn, vNames );
+    Acb_NtkFindNamesInPlaces( pBuffer, vPlaces, vNames );
     Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
     {
         for ( k = Prev; k < Pos; k++ )
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 2efb3358..9ef8b6ff 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -105,6 +105,8 @@ extern ABC_DLL void *          Abc_FrameReadManDd();
 extern ABC_DLL void *          Abc_FrameReadManDec();                    
 extern ABC_DLL void *          Abc_FrameReadManDsd();           
 extern ABC_DLL void *          Abc_FrameReadManDsd2();           
+extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadSignalNames();
+extern ABC_DLL int *           Abc_FrameReadGateCounts();
          
 extern ABC_DLL char *          Abc_FrameReadFlag( char * pFlag ); 
 extern ABC_DLL int             Abc_FrameIsFlagEnabled( char * pFlag );
@@ -147,6 +149,7 @@ extern ABC_DLL void            Abc_FrameSetCnf( Vec_Int_t * vInv );
 extern ABC_DLL void            Abc_FrameSetStr( Vec_Str_t * vInv );
 extern ABC_DLL void            Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs );
 extern ABC_DLL void            Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs );
+extern ABC_DLL void            Abc_FrameSetSignalNames( Vec_Ptr_t * vNames );
 
 extern ABC_DLL int             Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 1d54f4e4..2743a90a 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -67,6 +67,8 @@ void *      Abc_FrameReadManDec()                            { if ( s_GlobalFram
 void *      Abc_FrameReadManDsd()                            { return s_GlobalFrame->pManDsd;      } 
 void *      Abc_FrameReadManDsd2()                           { return s_GlobalFrame->pManDsd2;     }
 char *      Abc_FrameReadFlag( char * pFlag )                { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );   }
+Vec_Ptr_t * Abc_FrameReadSignalNames()                       { return s_GlobalFrame->vSignalNames; }
+int *       Abc_FrameReadGateCounts()                        { return s_GlobalFrame->pGateCounts;  }
 
 int         Abc_FrameReadBmcFrames( Abc_Frame_t * p )        { return s_GlobalFrame->nFrames;      }               
 int         Abc_FrameReadProbStatus( Abc_Frame_t * p )       { return s_GlobalFrame->Status;       }               
@@ -102,6 +104,7 @@ void        Abc_FrameSetManDsd2( void * pMan )               { if (s_GlobalFrame
 void        Abc_FrameSetInv( Vec_Int_t * vInv )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
 void        Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs )        { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
 void        Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs )        { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
+void        Abc_FrameSetSignalNames( Vec_Ptr_t * vNames )    { if ( s_GlobalFrame->vSignalNames ) Vec_PtrFreeFree( s_GlobalFrame->vSignalNames ); s_GlobalFrame->vSignalNames = vNames; }
 
 int         Abc_FrameIsBatchMode()                           { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0;              } 
 
@@ -231,6 +234,8 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     }
     Vec_IntFreeP( &p->vIndFlops );
     Vec_PtrFreeP( &p->vLTLProperties_global );
+    if ( p->vSignalNames )
+    Vec_PtrFreeFree( p->vSignalNames );
     Abc_FrameDeleteAllNetworks( p );
     ABC_FREE( p->pDrivingCell );
     ABC_FREE( p->pCex2 );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index bc57ad2a..9eaa03d1 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -133,6 +133,8 @@ struct Abc_Frame_t_
     int             nFrames;               // the number of time frames completed by BMC
     Vec_Ptr_t *     vPlugInComBinPairs;    // pairs of command and its binary name
     Vec_Ptr_t *     vLTLProperties_global; // related to LTL
+    Vec_Ptr_t *     vSignalNames;  // temporary storage for signal names
+    int             pGateCounts[5];// temporary gate counts
     void *          pSave1; 
     void *          pSave2; 
     void *          pSave3;