diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-15 17:16:19 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-15 17:16:19 -0800 |
| commit | ab387953ab3a50200384f5619cf999e3f729f28f (patch) | |
| tree | 3828dbe0c485d691c470288972b0573bd3dc4266 /src/proof/pdr/pdrInv.c | |
| parent | cb1ab7030fcd6964d4feb7441bf594829583d5ba (diff) | |
| download | abc-ab387953ab3a50200384f5619cf999e3f729f28f.tar.gz abc-ab387953ab3a50200384f5619cf999e3f729f28f.tar.bz2 abc-ab387953ab3a50200384f5619cf999e3f729f28f.zip | |
Word-level abstraction engine.
Diffstat (limited to 'src/proof/pdr/pdrInv.c')
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 554add9b..baade033 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -50,7 +50,16 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) Vec_Ptr_t * vVec; int i, ThisSize, Length, LengthStart; if ( Vec_PtrSize(p->vSolvers) < 2 ) + { + printf( "Frame " ); + printf( "Clauses " ); + printf( "Max Queue " ); + printf( "Flops " ); + printf( "Cex " ); + printf( "Time" ); + printf( "\n" ); return; + } if ( Abc_FrameIsBatchMode() && !fClose ) return; // count the total length of the printout @@ -81,9 +90,9 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); Abc_Print( 1, "%5d", p->nQueMax ); - Abc_Print( 1, "%5d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); + Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); if ( p->pPars->fUseAbs ) - Abc_Print( 1, "%5d", p->nCexes ); + Abc_Print( 1, "%4d", 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 ); |