Skip to content

A
abc
Commit 2076d38e by Alan Mishchenko
Options

Added sharing of counter-examples across multiple failed properties in 'bmc3 -a'.

parent a0529ec5
Showing with 79 additions and 38 deletions
src/sat/bmc/bmcBmc3.c
...@@ -1350,6 +1350,26 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i ) ...@@ -1350,6 +1350,26 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
/**Function************************************************************* /**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.] Synopsis [Bounded model checking engine.]
Description [] Description []
...@@ -1363,7 +1383,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) ...@@ -1363,7 +1383,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{ {
Gia_ManBmc_t * p; Gia_ManBmc_t * p;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
Abc_Cex_t * pCexNew; Abc_Cex_t * pCexNew, * pCexNew0;
unsigned * pInfo; unsigned * pInfo;
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0; int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) ); int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
...@@ -1446,8 +1466,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) ...@@ -1446,8 +1466,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
} }
if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) ) if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
continue; continue;
// solve SAT // create CNF upfront
clk = Abc_Clock(); if ( pPars->fSolveAll )
{
Saig_ManForEachPo( pAig, pObj, i ) Saig_ManForEachPo( pAig, pObj, i )
{ {
if ( i >= Saig_ManPoNum(pAig) ) if ( i >= Saig_ManPoNum(pAig) )
...@@ -1472,47 +1493,38 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) ...@@ -1472,47 +1493,38 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
continue; continue;
// add constraints for this output // add constraints for this output
clk2 = Abc_Clock(); clk2 = Abc_Clock();
Lit = Saig_ManBmcCreateCnf( p, pObj, f ); Saig_ManBmcCreateCnf( p, pObj, f );
clkOther += Abc_Clock() - clk2; clkOther += Abc_Clock() - clk2;
if ( Lit == 0 ) }
continue; }
if ( Lit == 1 ) // solve SAT
clk = Abc_Clock();
Saig_ManForEachPo( pAig, pObj, i )
{ {
RetValue = 0; if ( i >= Saig_ManPoNum(pAig) )
if ( !pPars->fSolveAll ) break;
// check for timeout
if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
{ {
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); Abc_Print( 1, "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap );
Abc_Print( 1, "Output %d is trivially SAT in frame %d.\n", i, f );
ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = pCex;
goto finish; goto finish;
} }
pPars->nFailOuts++; if ( nTimeToStop && Abc_Clock() > nTimeToStop )
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" ); if ( !pPars->fSilent )
Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
goto finish; goto finish;
} }
// reset the timeout // skip solved outputs
pPars->timeLastSolved = Abc_Clock(); if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
if ( nTimeToStop )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
continue; continue;
} // skip output whose time has run out
if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
continue;
// add constraints for this output
clk2 = Abc_Clock();
Lit = Saig_ManBmcCreateCnf( p, pObj, f );
clkOther += Abc_Clock() - clk2;
// solve this output // solve this output
fUnfinished = 0; fUnfinished = 0;
sat_solver_compress( p->pSat ); sat_solver_compress( p->pSat );
...@@ -1523,7 +1535,8 @@ clk2 = Abc_Clock(); ...@@ -1523,7 +1535,8 @@ clk2 = Abc_Clock();
clkOne = Abc_Clock(); clkOne = Abc_Clock();
sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + 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 ) if ( p->pTime4Outs )
{ {
abctime timeSince = Abc_Clock() - clkOne; abctime timeSince = Abc_Clock() - clkOne;
...@@ -1535,7 +1548,7 @@ clk2 = Abc_Clock(); ...@@ -1535,7 +1548,7 @@ clk2 = Abc_Clock();
if ( status == l_False ) if ( status == l_False )
{ {
nTimeUnsat += Abc_Clock() - clk2; nTimeUnsat += Abc_Clock() - clk2;
if ( 1 ) if ( Lit != 0 )
{ {
// add final unit clause // add final unit clause
Lit = lit_neg( Lit ); Lit = lit_neg( Lit );
...@@ -1591,15 +1604,18 @@ nTimeSat += Abc_Clock() - clk2; ...@@ -1591,15 +1604,18 @@ nTimeSat += Abc_Clock() - clk2;
if ( p->vCexes == NULL ) if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); 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; pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
pCexNew0 = NULL;
if ( p->pPars->fUseBridge ) if ( p->pPars->fUseBridge )
{ {
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
Abc_CexFree( pCexNew ); //Abc_CexFree( pCexNew );
pCexNew0 = pCexNew;
pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1; pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1;
} }
Vec_PtrWriteEntry( p->vCexes, i, pCexNew ); Vec_PtrWriteEntry( p->vCexes, i, pCexNew );
if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) ) 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" ); Abc_Print( 1, "Quitting due to callback on fail.\n" );
goto finish; goto finish;
} }
...@@ -1608,6 +1624,31 @@ nTimeSat += Abc_Clock() - clk2; ...@@ -1608,6 +1624,31 @@ nTimeSat += Abc_Clock() - clk2;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
if ( nTimeToStop ) if ( nTimeToStop )
sat_solver_set_runtime_limit( p->pSat, 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 else
{ {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment