diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-17 20:46:14 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-17 20:46:14 -0700 |
| commit | bdae7c625afaff6f9313f201096dcb7d591c2486 (patch) | |
| tree | e9185e4988afe65adf7de7e1cc1bd5dda19c2a3d /src/proof/pdr/pdrCore.c | |
| parent | 7808ee8e70b4ece98ed045aa50fe21bf6e3065b3 (diff) | |
| download | abc-bdae7c625afaff6f9313f201096dcb7d591c2486.tar.gz abc-bdae7c625afaff6f9313f201096dcb7d591c2486.tar.bz2 abc-bdae7c625afaff6f9313f201096dcb7d591c2486.zip | |
Adding callback to bmc3, sim3, pdr in the multi-output mode.
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index eb21edfc..3df1d7de 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -591,6 +591,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 ); + if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Quitting due to callback on fail.\n" ); + p->pPars->iFrame = k; + return -1; + } if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT p->pPars->timeLastSolved = clock(); @@ -659,6 +668,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 ); + if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Quitting due to callback on fail.\n" ); + p->pPars->iFrame = k; + return -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, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); |