From dd96bb7477fc568ef8fc8d86d330af22c8fa2f26 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 10 Feb 2017 18:53:39 -0800 Subject: Adding PDR with abstraction. --- src/proof/pdr/pdrCore.c | 13 ++++++++----- src/proof/pdr/pdrInt.h | 3 +++ src/proof/pdr/pdrInv.c | 8 +++++--- src/proof/pdr/pdrMan.c | 11 +++++++---- src/proof/pdr/pdrTsim.c | 17 ++++++++++++++++- 5 files changed, 39 insertions(+), 13 deletions(-) diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index fb35269d..5aa689f5 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -861,7 +861,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManCreateSolver( p, (iFrame = 0) ); while ( 1 ) { - if ( p->pPars->fUseAbs && iFrame == 2 ) + int fRefined = 0; + if ( p->pPars->fUseAbs && iFrame == 3 ) { int i, Prio; assert( p->vAbsFlops == NULL ); @@ -872,9 +873,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( Prio >> p->nPrioShift ) Vec_IntWriteEntry( p->vAbsFlops, i, 1 ); } - if ( p->pPars->fUseAbs && p->vAbsFlops ) - printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) ); - + //if ( p->pPars->fUseAbs && p->vAbsFlops ) + // printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) ); p->nFrames = iFrame; assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); p->iUseFrame = Abc_MaxInt(iFrame, 1); @@ -1000,12 +1000,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pPars->iFrame = iFrame; if ( !p->pPars->fSolveAll ) { + abctime clk = Abc_Clock(); Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p); + p->tAbs += Abc_Clock() - clk; if ( pCex == NULL ) { assert( p->pPars->fUseAbs ); Pdr_QueueClean( p ); pCube = NULL; + fRefined = 1; break; // keep solving } p->pAig->pSeqModel = pCex; @@ -1058,7 +1061,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 2ee4ae09..a6d249e8 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -96,6 +96,8 @@ struct Pdr_Man_t_ Vec_Int_t * vAbsFlops; // flops currently used Vec_Int_t * vMapFf2Ppi; Vec_Int_t * vMapPpi2Ff; + int nCexes; + int nCexesTotal; // terminary simulation Txs_Man_t * pTxs; // internal use @@ -142,6 +144,7 @@ struct Pdr_Man_t_ abctime tTsim; abctime tContain; abctime tCnf; + abctime tAbs; abctime tTotal; }; diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 7a8a66d6..e3233a3a 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -80,8 +80,10 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) } for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); - Abc_Print( 1, "%6d", p->nQueMax ); - Abc_Print( 1, "%6d", p->nAbsFlops ); + Abc_Print( 1, "%5d", p->nQueMax ); + Abc_Print( 1, "%5d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); + if ( p->pPars->fUseAbs ) + Abc_Print( 1, "%5d", p->nCexes ); Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); if ( p->pPars->fSolveAll ) Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); @@ -89,7 +91,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts ); Abc_Print( 1, "%s", fClose ? "\n":"\r" ); if ( fClose ) - p->nQueMax = 0; + p->nQueMax = 0, p->nCexes = 0; fflush( stdout ); } diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index e2807c92..c19041ee 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -324,8 +324,8 @@ void Pdr_ManStop( Pdr_Man_t * p ) Aig_ManCleanMarkAB( p->pAig ); if ( p->pPars->fVerbose ) { - Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n", - p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts ); + Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Cex =%4d Start =%4d\n", + p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nCexesTotal, p->nStarts ); ABC_PRTP( "SAT solving", p->tSat, p->tTotal ); ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal ); ABC_PRTP( " sat ", p->tSatSat, p->tTotal ); @@ -334,6 +334,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) ABC_PRTP( "Ternary sim", p->tTsim, p->tTotal ); ABC_PRTP( "Containment", p->tContain, p->tTotal ); ABC_PRTP( "CNF compute", p->tCnf, p->tTotal ); + ABC_PRTP( "Refinement ", p->tAbs, p->tTotal ); ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal ); fflush( stdout ); } @@ -503,7 +504,7 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p ) assert( f == nFrames ); // perform CEX minimization pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi ); - pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 1, 1 ); + pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 ); Gia_ManStop( pAbs ); assert( pCexCare->nPis == pCex->nPis ); Abc_CexFree( pCex ); @@ -520,7 +521,9 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p ) Abc_CexFree( pCexCare ); if ( nFfRefined == 0 ) // no refinement -- this is a real CEX return Pdr_ManDeriveCex(p); - printf( "CEX-based refinement refined %d flops.\n", nFfRefined ); + //printf( "CEX-based refinement refined %d flops.\n", nFfRefined ); + p->nCexesTotal++; + p->nCexes++; return NULL; } diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 1cff03c7..283a0e1d 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -476,7 +476,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); // move abstracted literals from flops to inputs if ( p->pPars->fUseAbs && p->vAbsFlops ) { - int i, iLit, k = 0, fAllNegs = 1; + int i, iLit, Used, k = 0, fAllNegs = 1; Vec_IntForEachEntry( vRes, iLit, i ) { if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop @@ -501,6 +501,21 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); break; } } + // add any flop that is not in the cone + if ( i == Vec_IntSize(vCiObjs) ) + { + Vec_IntForEachEntry( p->vAbsFlops, Used, i ) + { + if ( !Used ) + continue; + if ( Vec_IntFind( vRes, Abc_Var2Lit(i, 1) ) >= 0 ) + continue; + Vec_IntPush( vRes, Abc_Var2Lit(i, 0) ); + //Vec_IntPrint( vRes ); + break; + } + assert( i < Vec_IntSize(p->vAbsFlops) ); + } } } pRes = Pdr_SetCreate( vRes, vPiLits ); -- cgit v1.2.3