diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-17 22:48:05 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-17 22:48:05 -0700 |
| commit | af0ff7e6fa668b507bfb78baf1bcb1fa9d5e81bf (patch) | |
| tree | 72c8f3fccf909243001edd37ef511f0e9fb1f0af /src/sat/bmc | |
| parent | 455ecb6accf2ce3c000cc04454e97f04ba20c6c1 (diff) | |
| download | abc-af0ff7e6fa668b507bfb78baf1bcb1fa9d5e81bf.tar.gz abc-af0ff7e6fa668b507bfb78baf1bcb1fa9d5e81bf.tar.bz2 abc-af0ff7e6fa668b507bfb78baf1bcb1fa9d5e81bf.zip | |
Adding progress report to 'bmc3'.
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index bee14df2..8e983a2d 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -68,6 +68,14 @@ struct Gia_ManBmc_t_ 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 /// //////////////////////////////////////////////////////////////////////// @@ -1565,6 +1573,8 @@ nTimeUnsat += Abc_Clock() - clk2; // propagate units sat_solver_compress( p->pSat ); } + if ( p->pPars->fUseBridge ) + Gia_ManReportProgress( stdout, i, f ); } else if ( status == l_True ) { |