diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-23 10:54:53 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-23 10:54:53 -0800 |
| commit | ca0bdde9b35a004303a843953e37c3bbe3bcc3f1 (patch) | |
| tree | ec79a2e18ce44a7eae5b10b188379e7bc32e9360 | |
| parent | d5bbf9188c4ea4ded22afe67b18290b148bf1d88 (diff) | |
| download | abc-ca0bdde9b35a004303a843953e37c3bbe3bcc3f1.tar.gz abc-ca0bdde9b35a004303a843953e37c3bbe3bcc3f1.tar.bz2 abc-ca0bdde9b35a004303a843953e37c3bbe3bcc3f1.zip | |
changed how pdr -t cleans up abs flops
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 7bca217f..8ca8e29e 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -468,6 +468,9 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) break; // keep solving } p->pAig->pSeqModel = pCex; + + if ( p->pPars->fVerbose && p->pPars->fUseAbs ) + Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); return 0; // SAT } p->pPars->nFailOuts++; @@ -517,6 +520,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) p->timeToStopOne = 0; } } + /* if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined ) { int i, Used; @@ -524,6 +528,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 ) Vec_IntWriteEntry( p->vAbsFlops, i, 0 ); } + */ + if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined ) + { + Pdr_Set_t * pSet; + int i, j, k; + Vec_IntFill( p->vAbsFlops, Vec_IntSize( p->vAbsFlops ), 0 ); + Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j ) + for ( k = 0; k < pSet->nLits; k++ ) + Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 ); + } + if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); if ( fRefined ) |