summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-11-04 20:25:36 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2013-11-04 20:25:36 -0800
commit2076d38ea3c552c47967a6c2e08376560baf6cb5 (patch)
tree3edee33eaeae11b56e86137e3d94560f9fd14a74 /src/sat
parenta0529ec5c80482253d451b90c00b6c22d664dfb2 (diff)
downloadabc-2076d38ea3c552c47967a6c2e08376560baf6cb5.tar.gz
abc-2076d38ea3c552c47967a6c2e08376560baf6cb5.tar.bz2
abc-2076d38ea3c552c47967a6c2e08376560baf6cb5.zip
Added sharing of counter-examples across multiple failed properties in 'bmc3 -a'.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmcBmc3.c127
1 files changed, 84 insertions, 43 deletions
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
@@ -1350,6 +1350,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.]
Description []
@@ -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
{