diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-11 21:00:37 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-11 21:00:37 -0800 |
| commit | ae521b66019623fd6ed51d89bef8244650227876 (patch) | |
| tree | 5a5519c3069931cb0881ce497fb21d004b42c52f /src/proof/pdr/pdrCore.c | |
| parent | 2a5fa67d36393ab3ddb14e5bf542b0f29c8634e1 (diff) | |
| download | abc-ae521b66019623fd6ed51d89bef8244650227876.tar.gz abc-ae521b66019623fd6ed51d89bef8244650227876.tar.bz2 abc-ae521b66019623fd6ed51d89bef8244650227876.zip | |
Adding PDR with abstraction.
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 5aa689f5..f77bc05f 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -706,7 +706,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) { Counter++; pThis = Pdr_QueueHead( p ); - if ( pThis->iFrame == 0 ) + if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) ) return 0; // SAT if ( pThis->iFrame > kMax ) // finished this level return 1; @@ -862,7 +862,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) while ( 1 ) { int fRefined = 0; - if ( p->pPars->fUseAbs && iFrame == 3 ) + if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 2 ) { int i, Prio; assert( p->vAbsFlops == NULL ); @@ -995,7 +995,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } - if ( p->pPars->fVerbose ) + if ( p->pPars->fVerbose && !p->pPars->fUseAbs ) Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); p->pPars->iFrame = iFrame; if ( !p->pPars->fSolveAll ) @@ -1043,6 +1043,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart ); } } + if ( fRefined ) + break; if ( p->pTime4Outs ) { abctime timeSince = Abc_Clock() - clkOne; @@ -1059,9 +1061,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->timeToStopOne = 0; } } - if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); + if ( fRefined ) + continue; // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); |