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/pdrCore.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/pdrCore.c')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index fb35269d..5aa689f5 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -861,7 +861,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManCreateSolver( p, (iFrame = 0) ); while ( 1 ) { - if ( p->pPars->fUseAbs && iFrame == 2 ) + int fRefined = 0; + if ( p->pPars->fUseAbs && iFrame == 3 ) { int i, Prio; assert( p->vAbsFlops == NULL ); @@ -872,9 +873,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( Prio >> p->nPrioShift ) Vec_IntWriteEntry( p->vAbsFlops, i, 1 ); } - if ( p->pPars->fUseAbs && p->vAbsFlops ) - printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) ); - + //if ( p->pPars->fUseAbs && p->vAbsFlops ) + // printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) ); p->nFrames = iFrame; assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); p->iUseFrame = Abc_MaxInt(iFrame, 1); @@ -1000,12 +1000,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pPars->iFrame = iFrame; if ( !p->pPars->fSolveAll ) { + abctime clk = Abc_Clock(); Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p); + p->tAbs += Abc_Clock() - clk; if ( pCex == NULL ) { assert( p->pPars->fUseAbs ); Pdr_QueueClean( p ); pCube = NULL; + fRefined = 1; break; // keep solving } p->pAig->pSeqModel = pCex; @@ -1058,7 +1061,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); |