diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-14 13:31:29 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-14 13:31:29 -0700 |
commit | 3b14c7b490cf0cdd93f47f9697c700b19cdda895 (patch) | |
tree | e30f5e754d5304d879d357a6730dfa24cec30133 /src/proof | |
parent | 19c28cae94cd2fe94d7cc7d9542d0fbacd9be95b (diff) | |
download | abc-3b14c7b490cf0cdd93f47f9697c700b19cdda895.tar.gz abc-3b14c7b490cf0cdd93f47f9697c700b19cdda895.tar.bz2 abc-3b14c7b490cf0cdd93f47f9697c700b19cdda895.zip |
Prepared &gla to try abstracting and proving concurrently.
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/pdr/pdr.h | 35 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 39 |
2 files changed, 48 insertions, 26 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index d245b467..491477dd 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -40,20 +40,23 @@ ABC_NAMESPACE_HEADER_START typedef struct Pdr_Par_t_ Pdr_Par_t; struct Pdr_Par_t_ { - int iOutput; // zero-based number of primary output to solve - int nRecycle; // limit on vars for recycling - int nFrameMax; // limit on frame count - int nConfLimit; // limit on SAT solver conflicts - int nRestLimit; // limit on the number of proof-obligations - int nTimeOut; // timeout in seconds - int fTwoRounds; // use two rounds for generalization - int fMonoCnf; // monolythic CNF - int fDumpInv; // dump inductive invariant - int fShortest; // forces bug traces to be shortest - int fSkipGeneral; // skips expensive generalization step - int fVerbose; // verbose output - int fVeryVerbose; // very verbose output - int iFrame; // explored up to this frame + int iOutput; // zero-based number of primary output to solve + int nRecycle; // limit on vars for recycling + int nFrameMax; // limit on frame count + int nConfLimit; // limit on SAT solver conflicts + int nRestLimit; // limit on the number of proof-obligations + int nTimeOut; // timeout in seconds + int fTwoRounds; // use two rounds for generalization + int fMonoCnf; // monolythic CNF + int fDumpInv; // dump inductive invariant + int fShortest; // forces bug traces to be shortest + int fSkipGeneral; // skips expensive generalization step + int fVerbose; // verbose output` + int fVeryVerbose; // very verbose output + int fSilent; // totally silent execution + int iFrame; // explored up to this frame + int RunId; // PDR id in this run + int(*pFuncStop)(int); // callback to terminate }; //////////////////////////////////////////////////////////////////////// @@ -65,8 +68,8 @@ struct Pdr_Par_t_ //////////////////////////////////////////////////////////////////////// /*=== pdrCore.c ==========================================================*/ -extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); -extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ); +extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); +extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ); ABC_NAMESPACE_HEADER_END diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 765894e3..5cb05143 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -528,7 +528,9 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) Pdr_QueuePush( p, pThis ); } - // check the timeout + // check termination + if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) ) + return -1; if ( p->timeToStop && clock() > p->timeToStop ) return -1; } @@ -565,7 +567,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + if ( p->pPars->nConfLimit ) + Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + else if ( p->pPars->fVerbose ) + Abc_Print( 1, "Computation cancelled by the callback.\n" ); p->pPars->iFrame = k; return -1; } @@ -576,7 +581,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + if ( p->pPars->nConfLimit ) + Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + else if ( p->pPars->fVerbose ) + Abc_Print( 1, "Computation cancelled by the callback.\n" ); p->pPars->iFrame = k; return -1; } @@ -615,7 +623,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); p->pPars->iFrame = k; return -1; } @@ -623,8 +632,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - Pdr_ManReportInvariant( p ); - Pdr_ManVerifyInvariant( p ); + if ( !p->pPars->fSilent ) + Pdr_ManReportInvariant( p ); + if ( !p->pPars->fSilent ) + Pdr_ManVerifyInvariant( p ); p->pPars->iFrame = k; return 1; // UNSAT } @@ -633,7 +644,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // clkStart = clock(); } - // check the timeout + // check termination + if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) ) + { + p->pPars->iFrame = k; + return -1; + } if ( p->timeToStop && clock() > p->timeToStop ) { if ( fPrintClauses ) @@ -643,7 +659,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); p->pPars->iFrame = k; return -1; } @@ -651,7 +668,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax ); p->pPars->iFrame = k; return -1; } @@ -677,7 +695,8 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, clock_t clk = clock(); p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL ); RetValue = Pdr_ManSolveInt( p ); - *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p ); + if ( ppCex ) + *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p ); if ( p->pPars->fDumpInv ) Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 ); // if ( *ppCex && pPars->fVerbose ) |