Skip to content

A
abc
Commit 467f8b65 by Alan Mishchenko
Options

Making 'bmc3' with switch '-a' not save CEXes.

parent 7adc34ad
Showing with 6 additions and 6 deletions
src/sat/bmc/bmcBmc3.c
...@@ -1425,9 +1425,9 @@ clkOther += clock() - clk2; ...@@ -1425,9 +1425,9 @@ clkOther += clock() - clk2;
continue; continue;
if ( Lit == 1 ) if ( Lit == 1 )
{ {
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
if ( !pPars->fSolveAll ) if ( !pPars->fSolveAll )
{ {
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
printf( "Output %d is trivially SAT in frame %d.\n", i, f ); printf( "Output %d is trivially SAT in frame %d.\n", i, f );
ABC_FREE( pAig->pSeqModel ); ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = pCex; pAig->pSeqModel = pCex;
...@@ -1440,7 +1440,7 @@ clkOther += clock() - clk2; ...@@ -1440,7 +1440,7 @@ clkOther += clock() - clk2;
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL ) if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex ); Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
RetValue = 0; RetValue = 0;
pPars->timeLastSolved = clock(); pPars->timeLastSolved = clock();
continue; continue;
...@@ -1471,6 +1471,9 @@ clkOther += clock() - clk2; ...@@ -1471,6 +1471,9 @@ clkOther += clock() - clk2;
} }
else if ( status == l_True ) else if ( status == l_True )
{ {
fFirst = 0;
if ( !pPars->fSolveAll )
{
Aig_Obj_t * pObjPi; Aig_Obj_t * pObjPi;
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
int j, iBit = Saig_ManRegNum(pAig); int j, iBit = Saig_ManRegNum(pAig);
...@@ -1481,9 +1484,6 @@ clkOther += clock() - clk2; ...@@ -1481,9 +1484,6 @@ clkOther += clock() - clk2;
if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) ) if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k ); Abc_InfoSetBit( pCex->pData, iBit + k );
} }
fFirst = 0;
if ( !pPars->fSolveAll )
{
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "%4d %s : ", f, fUnfinished ? "-" : "+" ); printf( "%4d %s : ", f, fUnfinished ? "-" : "+" );
...@@ -1515,7 +1515,7 @@ clkOther += clock() - clk2; ...@@ -1515,7 +1515,7 @@ clkOther += clock() - clk2;
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL ) if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex ); Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
RetValue = 0; RetValue = 0;
pPars->timeLastSolved = clock(); pPars->timeLastSolved = clock();
} }
......
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