From 58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Dec 2012 14:46:16 -0800 Subject: Enabling multi-output solving in 'pdr'. --- src/base/abci/abc.c | 51 ++++++++++++++++++++++------------------------- src/base/abci/abcDar.c | 47 +++++++++++++++++-------------------------- src/misc/util/utilCex.c | 7 ++++--- src/proof/abs/absOldRef.c | 10 +++++----- src/proof/abs/absPth.c | 3 +-- src/proof/fra/fraSec.c | 10 +++------- src/proof/pdr/pdr.h | 2 +- src/proof/pdr/pdrCore.c | 25 +++++++++++++---------- src/proof/pdr/pdrInt.h | 1 + src/proof/pdr/pdrMan.c | 2 ++ src/proof/pdr/pdrUtil.c | 18 +++++++++++++++++ 11 files changed, 91 insertions(+), 85 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e7fe63e9..4b7f21bd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2292,13 +2292,21 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) } } Abc_Print( 1,"Status = %d Frames = %d ", pAbc->Status, pAbc->nFrames ); - if ( pAbc->pCex == NULL ) + if ( pAbc->pCex == NULL && pAbc->vCexVec == NULL ) Abc_Print( 1,"Cex is not defined.\n" ); else - Abc_Print( 1,"Cex: PIs = %d Regs = %d PO = %d Frame = %d Bits = %d\n", - pAbc->pCex->nPis, pAbc->pCex->nRegs, - pAbc->pCex->iPo, pAbc->pCex->iFrame, - pAbc->pCex->nBits ); + { + if ( pAbc->pCex ) + Abc_CexPrintStats( pAbc->pCex ); + if ( pAbc->vCexVec ) + { + Abc_Cex_t * pTemp; + printf( "\n" ); + Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c ) + if ( pTemp ) + Abc_CexPrintStats( pTemp ); + } + } return 0; usage: @@ -20920,7 +20928,10 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) } } if ( pNtk->vSeqModelVec ) + { Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + pAbc->nFrames = -1; + } return 0; usage: @@ -22314,10 +22325,9 @@ usage: ***********************************************************************/ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ); + extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); Pdr_Par_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); - Abc_Cex_t * pCex = NULL; int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); @@ -22437,28 +22447,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); return 0; } -/* - if ( pPars->iOutput != -1 && (pPars->iOutput < 0 || pPars->iOutput >= Abc_NtkPoNum(pNtk)) ) - { - Abc_Print( -2, "Output index (%d) is incorrect (can be 0 through %d).\n", - pPars->iOutput, Abc_NtkPoNum(pNtk)-1 ); - return 0; - } -*/ -/* - if ( Abc_NtkPoNum(pNtk) != 1 && pPars->fVerbose ) - { - if ( pPars->iOutput == -1 ) - Abc_Print( -2, "The %d property outputs are ORed together.\n", Abc_NtkPoNum(pNtk) ); - else - Abc_Print( -2, "Working on the primary output with zero-based number %d (out of %d).\n", - pPars->iOutput, Abc_NtkPoNum(pNtk) ); - } -*/ // run the procedure - pAbc->Status = Abc_NtkDarPdr( pNtk, pPars, &pCex ); + pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); pAbc->nFrames = pPars->iFrame; - Abc_FrameReplaceCex( pAbc, &pCex ); + Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + if ( pNtk->vSeqModelVec ) + { + Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + pAbc->nFrames = -1; + } return 0; usage: diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 496855c2..742f90bb 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2705,57 +2705,46 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar ) SeeAlso [] ***********************************************************************/ -int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) +int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ) { int RetValue = -1; clock_t clk = clock(); Aig_Man_t * pMan; - *ppCex = NULL; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) { Abc_Print( 1, "Converting network into AIG has failed.\n" ); return -1; } -/* - // perform ORing the primary outputs - if ( pPars->iOutput == -1 ) - { - Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan ); - RetValue = Pdr_ManSolve( pTemp, pPars, ppCex ); - if ( RetValue == 0 ) - (*ppCex)->iPo = Saig_ManFindFailedPoCex( pMan, *ppCex ); - Aig_ManStop( pTemp ); - } - else - RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); -*/ - RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); - - // output the result + RetValue = Pdr_ManSolve( pMan, pPars ); if ( !pPars->fSilent ) { if ( RetValue == 1 ) Abc_Print( 1, "Property proved. " ); else if ( RetValue == 0 ) - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame ); + { + if ( pMan->pSeqModel == NULL ) + Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" ); + else + { + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame ); + if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) ) + Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" ); + } + } else if ( RetValue == -1 ) Abc_Print( 1, "Property UNDECIDED. " ); else assert( 0 ); ABC_PRT( "Time", clock() - clk ); } - -// ABC_FREE( pNtk->pSeqModel ); -// pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - if ( ppCex ) - *ppCex = pMan->pSeqModel; - else - ABC_FREE( pMan->pSeqModel ); + ABC_FREE( pNtk->pSeqModel ); + pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - - if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) ) - Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" ); + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; + pMan->vSeqModelVec = NULL; Aig_ManStop( pMan ); return RetValue; } diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 2f205d2e..75b99492 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -261,8 +261,9 @@ void Abc_CexPrintStats( Abc_Cex_t * p ) } for ( k = 0; k < p->nBits; k++ ) Counter += Abc_InfoHasBit(p->pData, k); - printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits =%8d nOnes =%8d (%5.2f %%)\n", - p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs) ); + printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%)\n", + p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, + Counter, 100.0 * Counter / (p->nBits - p->nRegs) ); } void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs ) { @@ -278,7 +279,7 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs ) if ( (k - p->nRegs) % p->nPis < nInputs ) Counter2 += Abc_InfoHasBit(p->pData, k); } - printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits =%8d nOnes =%8d (%5.2f %%) nOnesIn =%8d (%5.2f %%)\n", + printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%) 1sIn =%8d (%5.2f %%)\n", p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs), Counter2, 100.0 * Counter2 / (p->nBits - p->nRegs - (p->iFrame + 1) * (p->nPis - nInputs)) ); diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c index eb9b84fa..0b99ab40 100644 --- a/src/proof/abs/absOldRef.c +++ b/src/proof/abs/absOldRef.c @@ -134,7 +134,6 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo pSecPar->fVerbose = fVerbose; RetValue = Fra_FraigSec( pAbs, pSecPar, NULL ); */ - Abc_Cex_t * pCex = NULL; Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs ); Pdr_Par_t Pars, * pPars = &Pars; Pdr_ManSetDefaultParams( pPars ); @@ -142,11 +141,12 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo pPars->fVerbose = fVerbose; if ( pPars->fVerbose ) printf( "Running property directed reachability...\n" ); - RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex ); - if ( pCex ) - pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex ); + RetValue = Pdr_ManSolve( pAbsOrpos, pPars ); + if ( pAbsOrpos->pSeqModel ) + pAbsOrpos->pSeqModel->iPo = Saig_ManFindFailedPoCex( pAbs, pAbsOrpos->pSeqModel ); + pAbs->pSeqModel = pAbsOrpos->pSeqModel; + pAbsOrpos->pSeqModel = NULL; Aig_ManStop( pAbsOrpos ); - pAbs->pSeqModel = pCex; if ( RetValue ) *piRetValue = 1; diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c index 3c24d83e..ef38369c 100644 --- a/src/proof/abs/absPth.c +++ b/src/proof/abs/absPth.c @@ -107,8 +107,7 @@ void * Abs_ProverThread( void * pArg ) pPars->fSilent = 1; pPars->RunId = pThData->RunId; pPars->pFuncStop = Abs_CallBackToStop; - RetValue = Pdr_ManSolve( pThData->pAig, pPars, NULL ); -// RetValue = Pdr_ManSolve_test( pAig, pPars, NULL ); + RetValue = Pdr_ManSolve( pThData->pAig, pPars ); // update the result if ( RetValue == 1 ) { diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c index c43fc4dd..04c9d668 100644 --- a/src/proof/fra/fraSec.c +++ b/src/proof/fra/fraSec.c @@ -589,19 +589,15 @@ ABC_PRT( "Time", clock() - clk ); // try PDR if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 ) { - Abc_Cex_t * pCex = NULL; - Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew ); Pdr_Par_t Pars, * pPars = &Pars; Pdr_ManSetDefaultParams( pPars ); pPars->nTimeOut = pParSec->nPdrTimeout; pPars->fVerbose = pParSec->fVerbose; if ( pParSec->fVerbose ) printf( "Running property directed reachability...\n" ); - RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex ); - if ( pCex ) - pCex->iPo = Saig_ManFindFailedPoCex( pNew, pCex ); - Aig_ManStop( pNewOrpos ); - pNew->pSeqModel = pCex; + RetValue = Pdr_ManSolve( pNew, pPars ); + if ( pNew->pSeqModel ) + pNew->pSeqModel->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ); } finish: 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 @@ -499,6 +499,24 @@ Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p ) return pRes; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_QueueClean( Pdr_Man_t * p ) +{ + Pdr_Obl_t * pThis; + while ( (pThis = Pdr_QueuePop(p)) ) + Pdr_OblDeref( pThis ); +} + /**Function************************************************************* Synopsis [] -- cgit v1.2.3