diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-11 22:48:20 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-11 22:48:20 -0800 |
| commit | 3fb058a35562ceeafb2967f0991215ad47a23b0f (patch) | |
| tree | a6425be23c78f699fd78bcedb3149bd732331b92 /src/proof/pdr/pdrCore.c | |
| parent | 4abb1ce8a45d115567a125c6b2b00d48f6776aff (diff) | |
| download | abc-3fb058a35562ceeafb2967f0991215ad47a23b0f.tar.gz abc-3fb058a35562ceeafb2967f0991215ad47a23b0f.tar.bz2 abc-3fb058a35562ceeafb2967f0991215ad47a23b0f.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, 10 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index f77bc05f..568f7642 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -874,7 +874,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) 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) ); + // printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) ); p->nFrames = iFrame; assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); p->iUseFrame = Abc_MaxInt(iFrame, 1); @@ -1061,10 +1061,19 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->timeToStopOne = 0; } } + if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined ) + { + int i, Used; + Vec_IntForEachEntry( p->vAbsFlops, Used, i ) + if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 ) + Vec_IntWriteEntry( p->vAbsFlops, i, 0 ); + } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); if ( fRefined ) continue; + //if ( p->pPars->fUseAbs && p->vAbsFlops ) + // printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) ); // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); |