Skip to content

A
abc
Commit 82e9de90 by Alan Mishchenko
Options

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

parent e5fb4fe5
Showing with 21 additions and 21 deletions
src/base/abc/abc.h
...@@ -646,7 +646,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_LibFindModelByName( Abc_Lib_t * pLib, char ...@@ -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 int Abc_LibFindTopLevelModels( Abc_Lib_t * pLib );
extern ABC_DLL Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib ); extern ABC_DLL Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib );
/*=== abcLog.c ==========================================================*/ /*=== 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 ==========================================================*/ /*=== abcMiter.c ==========================================================*/
extern ABC_DLL int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NodeMinimumBase( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeMinimumBase( Abc_Obj_t * pNode );
......
src/base/abci/abc.c
...@@ -6780,7 +6780,7 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6780,7 +6780,7 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->nFrames = pPars->iFrame; pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pLogFileName ) if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "reach" ); Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "reach" );
return 0; return 0;
usage: usage:
...@@ -16884,7 +16884,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -16884,7 +16884,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar ); pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar );
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pLogFileName ) 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 // read back the resulting unsolved reduced sequential miter
if ( pSecPar->fReadUnsolved && pSecPar->nSMnumber >= 0 ) if ( pSecPar->fReadUnsolved && pSecPar->nSMnumber >= 0 )
...@@ -18132,7 +18132,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18132,7 +18132,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->nFrames = iFrames; pAbc->nFrames = iFrames;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pLogFileName ) if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "bmc" ); Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc" );
return 0; return 0;
usage: usage:
...@@ -18316,7 +18316,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18316,7 +18316,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->nFrames = iFrames; pAbc->nFrames = iFrames;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pLogFileName ) if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "bmc2" ); Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc2" );
return 0; return 0;
usage: usage:
...@@ -18450,7 +18450,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18450,7 +18450,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->nFrames = pPars->iFrame; pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pLogFileName ) 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 ( pPars->fSolveAll && pPars->fDropSatOuts )
{ {
if ( pNtk->pSeqModelVec == NULL ) if ( pNtk->pSeqModelVec == NULL )
...@@ -18662,7 +18662,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18662,7 +18662,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
} }
if ( pLogFileName ) if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "int" ); Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "int" );
return 0; return 0;
usage: usage:
...@@ -24182,7 +24182,7 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -24182,7 +24182,7 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->Status = -1; pAbc->Status = -1;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
// if ( pLogFileName ) // if ( pLogFileName )
// Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&sim" ); // Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&sim" );
return 0; return 0;
usage: usage:
...@@ -27594,7 +27594,7 @@ int Abc_CommandAbc9ReachM( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27594,7 +27594,7 @@ int Abc_CommandAbc9ReachM( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->nFrames = pPars->iFrame; pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
if ( pLogFileName ) if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachm" ); Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachm" );
return 0; return 0;
usage: usage:
...@@ -27742,7 +27742,7 @@ int Abc_CommandAbc9ReachP( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27742,7 +27742,7 @@ int Abc_CommandAbc9ReachP( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->nFrames = pPars->iFrame; pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
if ( pLogFileName ) if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachp" ); Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachp" );
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return 0; return 0;
...@@ -27870,7 +27870,7 @@ int Abc_CommandAbc9ReachN( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27870,7 +27870,7 @@ int Abc_CommandAbc9ReachN( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->nFrames = pPars->iFrame; pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
if ( pLogFileName ) if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachn" ); Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachn" );
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return 0; return 0;
......
src/base/abci/abcLog.c
...@@ -64,7 +64,7 @@ ABC_NAMESPACE_IMPL_START ...@@ -64,7 +64,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] 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; FILE * pFile;
int i; int i;
...@@ -85,7 +85,7 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char * ...@@ -85,7 +85,7 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char *
printf( "Abc_NtkWriteLogFile(): Cannot recognize solving status.\n" ); printf( "Abc_NtkWriteLogFile(): Cannot recognize solving status.\n" );
fprintf( pFile, " " ); fprintf( pFile, " " );
// write <cyc> // write <cyc>
fprintf( pFile, "%d", pCex ? pCex->iFrame + 1 : -1 ); fprintf( pFile, "%d", pCex ? pCex->iFrame + 1 : nFrames );
fprintf( pFile, " " ); fprintf( pFile, " " );
// write <engine_name> // write <engine_name>
fprintf( pFile, "%s", pCommand ? pCommand : "unknown" ); fprintf( pFile, "%s", pCommand ? pCommand : "unknown" );
...@@ -125,12 +125,12 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char * ...@@ -125,12 +125,12 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char *
SeeAlso [] 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; Abc_Cex_t * pCex;
Vec_Int_t * vNums; Vec_Int_t * vNums;
char Buffer[1000], * pToken; char Buffer[1000], * pToken;
FILE * pFile;
int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1; int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1;
pFile = fopen( pFileName, "r" ); pFile = fopen( pFileName, "r" );
if ( pFile == NULL ) if ( pFile == NULL )
...@@ -210,6 +210,8 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex ) ...@@ -210,6 +210,8 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex )
else else
ABC_FREE( pCex ); ABC_FREE( pCex );
} }
if ( pnFrames )
*pnFrames = nFrames;
return Status; return Status;
} }
......
src/base/io/io.c
...@@ -1210,7 +1210,7 @@ int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -1210,7 +1210,7 @@ int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
char * pFileName; char * pFileName;
FILE * pFile; FILE * pFile;
int c; 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(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
...@@ -1239,9 +1239,7 @@ int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -1239,9 +1239,7 @@ int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
// set the new network // set the new network
Abc_FrameClearVerifStatus( pAbc ); Abc_FrameClearVerifStatus( pAbc );
pAbc->Status = Abc_NtkReadLogFile( pFileName, &pAbc->pCex ); pAbc->Status = Abc_NtkReadLogFile( pFileName, &pAbc->pCex, &pAbc->nFrames );
if ( pAbc->pCex )
pAbc->nFrames = pAbc->pCex->iFrame;
return 0; return 0;
usage: usage:
...@@ -2534,7 +2532,7 @@ int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -2534,7 +2532,7 @@ int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv )
{ {
char * pFileName; char * pFileName;
int c; 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(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
...@@ -2551,7 +2549,7 @@ int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -2551,7 +2549,7 @@ int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv )
goto usage; goto usage;
// get the input file name // get the input file name
pFileName = argv[globalUtilOptind]; pFileName = argv[globalUtilOptind];
Abc_NtkWriteLogFile( pFileName, pAbc->pCex, pAbc->Status, NULL ); Abc_NtkWriteLogFile( pFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, NULL );
return 0; return 0;
usage: usage:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment