diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 14:46:16 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 14:46:16 -0800 |
commit | 58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2 (patch) | |
tree | 871796cca031fc63f082a66277cd9c2de1e71e5b /src/proof/pdr | |
parent | 9f396a0d7e652c420f4af74e4c8db06068bea862 (diff) | |
download | abc-58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2.tar.gz abc-58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2.tar.bz2 abc-58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2.zip |
Enabling multi-output solving in 'pdr'.
Diffstat (limited to 'src/proof/pdr')
-rw-r--r-- | src/proof/pdr/pdr.h | 2 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 25 | ||||
-rw-r--r-- | src/proof/pdr/pdrInt.h | 1 | ||||
-rw-r--r-- | src/proof/pdr/pdrMan.c | 2 | ||||
-rw-r--r-- | src/proof/pdr/pdrUtil.c | 18 |
5 files changed, 36 insertions, 12 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 3c40d2d5..a815bb30 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -71,7 +71,7 @@ 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 int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars ); ABC_NAMESPACE_HEADER_END diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index f72983da..76d6f788 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -635,7 +635,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( !p->pPars->fSolveAll ) { - p->pAig->pSeqModel = Pdr_ManDeriveCex( p ); + p->pAig->pSeqModel = Pdr_ManDeriveCex(p); return 0; // SAT } p->pPars->nFailOuts++; @@ -647,6 +647,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT + Pdr_QueueClean( p ); + pCube = NULL; + break; // keep solving } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 0, clock() - clkStart ); @@ -735,7 +738,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) +int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) { Pdr_Man_t * p; int RetValue; @@ -743,16 +746,19 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) if ( pPars->fVerbose ) { // Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); - Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", - pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut ); - Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", - pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" ); + Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ", + pPars->nRecycle, + pPars->nFrameMax, + pPars->nRestLimit, + pPars->nTimeOut ); + Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n", + pPars->fMonoCnf ? "yes" : "no", + pPars->fSkipGeneral ? "yes" : "no", + pPars->fSolveAll ? "yes" : "no" ); } ABC_FREE( pAig->pSeqModel ); p = Pdr_ManStart( pAig, pPars, NULL ); RetValue = Pdr_ManSolveInt( p ); -// if ( ppCex ) -// *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p ); if ( RetValue == 0 ) assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); if ( p->vCexes ) @@ -763,9 +769,6 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) } if ( p->pPars->fDumpInv ) Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 ); -// if ( *ppCex && pPars->fVerbose ) -// Abc_Print( 1, "Found counter-example in frame %d after exploring %d frames.\n", -// (*ppCex)->iFrame, p->nFrames ); p->tTotal += clock() - clk; Pdr_ManStop( p ); pPars->iFrame--; diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index abc8f12b..f6d3d170 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -187,6 +187,7 @@ extern void Pdr_OblDeref( Pdr_Obl_t * p ); extern int Pdr_QueueIsEmpty( Pdr_Man_t * p ); extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p ); extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p ); +extern void Pdr_QueueClean( Pdr_Man_t * p ); extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl ); extern void Pdr_QueuePrint( Pdr_Man_t * p ); extern void Pdr_QueueStop( Pdr_Man_t * p ); diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 78aa2b69..95e7641b 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -188,6 +188,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) ); } assert( f == nFrames ); + if ( !Saig_ManVerifyCex(p->pAig, pCex) ) + printf( "CEX for output %d is not valid.\n", p->iOutCur ); return pCex; } diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index a47bc9f0..c70554e3 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -510,6 +510,24 @@ Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Pdr_QueueClean( Pdr_Man_t * p ) +{ + Pdr_Obl_t * pThis; + while ( (pThis = Pdr_QueuePop(p)) ) + Pdr_OblDeref( pThis ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl ) { Pdr_Obl_t * pTemp, ** ppPrev; |