diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-10 18:53:39 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-10 18:53:39 -0800 |
| commit | dd96bb7477fc568ef8fc8d86d330af22c8fa2f26 (patch) | |
| tree | 33744ec4f77423b3d117fd0788bd9062583f6365 /src/proof/pdr/pdrInv.c | |
| parent | 5d717256d3b856d8f29c4a5e442af624f0b0bb69 (diff) | |
| download | abc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.tar.gz abc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.tar.bz2 abc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.zip | |
Adding PDR with abstraction.
Diffstat (limited to 'src/proof/pdr/pdrInv.c')
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 7a8a66d6..e3233a3a 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -80,8 +80,10 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) } for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); - Abc_Print( 1, "%6d", p->nQueMax ); - Abc_Print( 1, "%6d", p->nAbsFlops ); + Abc_Print( 1, "%5d", p->nQueMax ); + Abc_Print( 1, "%5d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); + if ( p->pPars->fUseAbs ) + Abc_Print( 1, "%5d", p->nCexes ); Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); if ( p->pPars->fSolveAll ) Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); @@ -89,7 +91,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts ); Abc_Print( 1, "%s", fClose ? "\n":"\r" ); if ( fClose ) - p->nQueMax = 0; + p->nQueMax = 0, p->nCexes = 0; fflush( stdout ); } |