From 2076d38ea3c552c47967a6c2e08376560baf6cb5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 4 Nov 2013 20:25:36 -0800 Subject: Added sharing of counter-examples across multiple failed properties in 'bmc3 -a'. --- src/sat/bmc/bmcBmc3.c | 127 +++++++++++++++++++++++++++++++++----------------- 1 file changed, 84 insertions(+), 43 deletions(-) (limited to 'src/sat/bmc/bmcBmc3.c') diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 16ed2b0b..5d0a05e9 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1348,6 +1348,26 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit ) +{ + if ( Lit == 0 ) + return l_False; + if ( Lit == 1 ) + return l_True; + return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +} + /**Function************************************************************* Synopsis [Bounded model checking engine.] @@ -1363,7 +1383,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) { Gia_ManBmc_t * p; Aig_Obj_t * pObj; - Abc_Cex_t * pCexNew; + Abc_Cex_t * pCexNew, * pCexNew0; unsigned * pInfo; int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) ); @@ -1446,6 +1466,37 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) } if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) ) continue; + // create CNF upfront + if ( pPars->fSolveAll ) + { + Saig_ManForEachPo( pAig, pObj, i ) + { + if ( i >= Saig_ManPoNum(pAig) ) + break; + // check for timeout + if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC ) + { + Abc_Print( 1, "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap ); + goto finish; + } + if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + { + if ( !pPars->fSilent ) + Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut ); + goto finish; + } + // skip solved outputs + if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) + continue; + // skip output whose time has run out + if ( p->pTime4Outs && p->pTime4Outs[i] == 0 ) + continue; + // add constraints for this output +clk2 = Abc_Clock(); + Saig_ManBmcCreateCnf( p, pObj, f ); +clkOther += Abc_Clock() - clk2; + } + } // solve SAT clk = Abc_Clock(); Saig_ManForEachPo( pAig, pObj, i ) @@ -1474,45 +1525,6 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) clk2 = Abc_Clock(); Lit = Saig_ManBmcCreateCnf( p, pObj, f ); clkOther += Abc_Clock() - clk2; - if ( Lit == 0 ) - continue; - if ( Lit == 1 ) - { - RetValue = 0; - if ( !pPars->fSolveAll ) - { - Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); - Abc_Print( 1, "Output %d is trivially SAT in frame %d.\n", i, f ); - ABC_FREE( pAig->pSeqModel ); - pAig->pSeqModel = pCex; - goto finish; - } - pPars->nFailOuts++; - if ( !pPars->fNotVerbose ) - Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", - nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); - if ( p->vCexes == NULL ) - p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); - pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; - if ( p->pPars->fUseBridge ) - { - Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); - Abc_CexFree( pCexNew ); - pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1; - } - Vec_PtrWriteEntry( p->vCexes, i, pCexNew ); - if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) ) - { - Abc_Print( 1, "Quitting due to callback on fail.\n" ); - goto finish; - } - // reset the timeout - pPars->timeLastSolved = Abc_Clock(); - nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); - if ( nTimeToStop ) - sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); - continue; - } // solve this output fUnfinished = 0; sat_solver_compress( p->pSat ); @@ -1523,7 +1535,8 @@ clk2 = Abc_Clock(); clkOne = Abc_Clock(); sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() ); } - status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +// status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + status = Saig_ManCallSolver( p, Lit ); if ( p->pTime4Outs ) { abctime timeSince = Abc_Clock() - clkOne; @@ -1535,7 +1548,7 @@ clk2 = Abc_Clock(); if ( status == l_False ) { nTimeUnsat += Abc_Clock() - clk2; - if ( 1 ) + if ( Lit != 0 ) { // add final unit clause Lit = lit_neg( Lit ); @@ -1591,15 +1604,18 @@ nTimeSat += Abc_Clock() - clk2; if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + pCexNew0 = NULL; if ( p->pPars->fUseBridge ) { Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); - Abc_CexFree( pCexNew ); + //Abc_CexFree( pCexNew ); + pCexNew0 = pCexNew; pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1; } Vec_PtrWriteEntry( p->vCexes, i, pCexNew ); if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) ) { + Abc_CexFreeP( &pCexNew0 ); Abc_Print( 1, "Quitting due to callback on fail.\n" ); goto finish; } @@ -1608,6 +1624,31 @@ nTimeSat += Abc_Clock() - clk2; nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); if ( nTimeToStop ) sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); + + // check if other outputs failed under the same counter-example + Saig_ManForEachPo( pAig, pObj, k ) + { + if ( k >= Saig_ManPoNum(pAig) ) + break; + // skip solved outputs + if ( p->vCexes && Vec_PtrEntry(p->vCexes, k) ) + continue; + // check if this output is solved + Lit = Saig_ManBmcCreateCnf( p, pObj, f ); + if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) + continue; + // write entry + pPars->nFailOuts++; + if ( !pPars->fNotVerbose ) + Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); + // report to the bridge + if ( p->pPars->fUseBridge ) + Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo ); + // remember solved output + Vec_PtrWriteEntry( p->vCexes, k, pCexNew ); + } + Abc_CexFreeP( &pCexNew0 ); } else { -- cgit v1.2.3