From dd96bb7477fc568ef8fc8d86d330af22c8fa2f26 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 10 Feb 2017 18:53:39 -0800 Subject: Adding PDR with abstraction. --- src/proof/pdr/pdrInv.c | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src/proof/pdr/pdrInv.c') 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 ); } -- cgit v1.2.3