luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding progress report to 'bmc3'.

This commit is contained in:
Alan Mishchenko 2014-03-17 22:48:05 -07:00
parent 455ecb6acc
commit af0ff7e6fa
1 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/sat/bmc/bmcBmc3.c
View File

@ -68,6 +68,14 @@ struct Gia_ManBmc_t_
extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved ); extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
void Gia_ManReportProgress( FILE * pFile, int prop_no, int depth )
{
extern int Gia_ManToBridgeProgress( FILE * pFile, int Size, unsigned char * pBuffer );
char buf[100];
sprintf(buf, "property: safe<%d>\nbug-free-depth: %d\n", prop_no, depth);
Gia_ManToBridgeProgress(pFile, strlen(buf), buf);
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -1565,6 +1573,8 @@ nTimeUnsat += Abc_Clock() - clk2;
// propagate units // propagate units
sat_solver_compress( p->pSat ); sat_solver_compress( p->pSat );
} }
if ( p->pPars->fUseBridge )
Gia_ManReportProgress( stdout, i, f );
} }
else if ( status == l_True ) else if ( status == l_True )
{ {