Eneabled writing/reading pAbc->nFrames into/from status files.

4 files changed, 21 insertions, 21 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 6dcb3881..3357ff46 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -646,7 +646,7 @@ extern ABC_DLL Abc_Ntk_t *        Abc_LibFindModelByName( Abc_Lib_t * pLib, char
 extern ABC_DLL int                Abc_LibFindTopLevelModels( Abc_Lib_t * pLib );
 extern ABC_DLL Abc_Ntk_t *        Abc_LibDeriveRoot( Abc_Lib_t * pLib );
 /*=== abcLog.c ==========================================================*/
-extern ABC_DLL void               Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pSeqCex, int Status, char * pCommand );
+extern ABC_DLL void               Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pSeqCex, int Status, int nFrames, char * pCommand );
 /*=== abcMiter.c ==========================================================*/
 extern ABC_DLL int                Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NodeMinimumBase( Abc_Obj_t * pNode );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index efdf3c94..32618e76 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6780,7 +6780,7 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "reach" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "reach" );
     return 0;
 
 usage:
@@ -16884,7 +16884,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar );
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "dprove" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "dprove" );
 
     // read back the resulting unsolved reduced sequential miter
     if ( pSecPar->fReadUnsolved && pSecPar->nSMnumber >= 0 )
@@ -18132,7 +18132,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = iFrames;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "bmc" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc" );
     return 0;
 
 usage:
@@ -18316,7 +18316,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = iFrames;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "bmc2" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc2" );
     return 0;
 
 usage:
@@ -18450,7 +18450,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "bmc3" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" );
     if ( pPars->fSolveAll && pPars->fDropSatOuts )
     {
         if ( pNtk->pSeqModelVec == NULL )
@@ -18662,7 +18662,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     }
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "int" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "int" );
     return 0;
 
 usage:
@@ -24182,7 +24182,7 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
         pAbc->Status = -1;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
 //    if ( pLogFileName )
-//        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&sim" );
+//        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&sim" );
     return 0;
 
 usage:
@@ -27594,7 +27594,7 @@ int Abc_CommandAbc9ReachM( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachm" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachm" );
     return 0;
 
 usage:
@@ -27742,7 +27742,7 @@ int Abc_CommandAbc9ReachP( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachp" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachp" );
     Aig_ManStop( pMan );
     return 0;
 
@@ -27870,7 +27870,7 @@ int Abc_CommandAbc9ReachN( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachn" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachn" );
     Aig_ManStop( pMan );
     return 0;
 
diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c
index acdfc79b..615584a1 100644
--- a/src/base/abci/abcLog.c
+++ b/src/base/abci/abcLog.c
@@ -64,7 +64,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char * pCommand )
+void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nFrames, char * pCommand )
 {
     FILE * pFile;
     int i;
@@ -85,7 +85,7 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char *
         printf( "Abc_NtkWriteLogFile(): Cannot recognize solving status.\n" );
     fprintf( pFile, " " );
     // write <cyc>
-    fprintf( pFile, "%d", pCex ? pCex->iFrame + 1 : -1 );
+    fprintf( pFile, "%d", pCex ? pCex->iFrame + 1 : nFrames );
     fprintf( pFile, " " );
     // write <engine_name>
     fprintf( pFile, "%s", pCommand ? pCommand : "unknown" );
@@ -125,12 +125,12 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char *
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex )
+int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
 {
+    FILE * pFile;
     Abc_Cex_t * pCex;
     Vec_Int_t * vNums;
     char Buffer[1000], * pToken;
-    FILE * pFile;
     int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1;
     pFile = fopen( pFileName, "r" );
     if ( pFile == NULL )
@@ -210,6 +210,8 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex )
         else
             ABC_FREE( pCex );
     }
+    if ( pnFrames )
+        *pnFrames = nFrames;
     return Status;
 }
 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index eab865d8..46cbb33a 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1210,7 +1210,7 @@ int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pFileName;
     FILE * pFile;
     int c;
-    extern int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex );
+    extern int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
@@ -1239,9 +1239,7 @@ int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set the new network
     Abc_FrameClearVerifStatus( pAbc );
-    pAbc->Status = Abc_NtkReadLogFile( pFileName, &pAbc->pCex );
-    if ( pAbc->pCex )
-        pAbc->nFrames = pAbc->pCex->iFrame;
+    pAbc->Status = Abc_NtkReadLogFile( pFileName, &pAbc->pCex, &pAbc->nFrames );
     return 0;
 
 usage:
@@ -2534,7 +2532,7 @@ int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
     int c;
-    extern void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char * pCommand );
+    extern void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nFrames, char * pCommand );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
@@ -2551,7 +2549,7 @@ int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv )
         goto usage;
     // get the input file name
     pFileName = argv[globalUtilOptind];
-    Abc_NtkWriteLogFile( pFileName, pAbc->pCex, pAbc->Status, NULL );
+    Abc_NtkWriteLogFile( pFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, NULL );
     return 0;
 
 usage: