diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-09 16:26:28 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-09 16:26:28 -0700 |
| commit | 4876f1e21cd395e94435aaafeaeec05839a32181 (patch) | |
| tree | 07dc3c5b9416cfae41599b5affcfee8c4dd208bc /src/proof/pdr | |
| parent | f1cd8797861e5a47d1f7cc9de0616bbc2d532f43 (diff) | |
| download | abc-4876f1e21cd395e94435aaafeaeec05839a32181.tar.gz abc-4876f1e21cd395e94435aaafeaeec05839a32181.tar.bz2 abc-4876f1e21cd395e94435aaafeaeec05839a32181.zip | |
Added switch '-x' to save CEXes in 'bmc3' and 'pdr' in multi-output mode.
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 8 |
2 files changed, 4 insertions, 5 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index e55eebb6..6e157aad 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -57,6 +57,7 @@ struct Pdr_Par_t_ int fNotVerbose; // not printing line by line progress int fSilent; // totally silent execution int fSolveAll; // do not stop when found a SAT output + int fStoreCex; // enable storing counter-examples in MO mode int nFailOuts; // the number of failed outputs int iFrame; // explored up to this frame int RunId; // PDR id in this run diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index a7c4dc35..eb21edfc 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -590,7 +590,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); - Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) ); + Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT p->pPars->timeLastSolved = clock(); @@ -640,7 +640,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } if ( RetValue == 0 ) { - Abc_Cex_t * pCex; if ( fPrintClauses ) { Abc_Print( 1, "*** Clauses after frame %d:\n", k ); @@ -659,11 +658,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); - pCex = Pdr_ManDeriveCex(p); - Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex ); + Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 ); if ( !p->pPars->fNotVerbose ) Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", - nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT Pdr_QueueClean( p ); |