Skip to content

A
abc
Commit 017c35ba by Alan Mishchenko
Options

Updating bmc3 printout to show the number of failed outputs.

parent 900bdfac
Showing with 12 additions and 14 deletions
src/sat/bmc/bmcBmc3.c
...@@ -1382,14 +1382,14 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) ...@@ -1382,14 +1382,14 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
// stop BMC after exploring all reachable states // stop BMC after exploring all reachable states
if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) ) if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) )
{ {
Saig_Bmc3ManStop( p ); RetValue = pPars->nFailOuts ? 0 : 1;
return pPars->nFailOuts ? 0 : 1; goto finish;
} }
// stop BMC if all targets are solved // stop BMC if all targets are solved
if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) ) if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) )
{ {
Saig_Bmc3ManStop( p ); RetValue = 0;
return 0; goto finish;
} }
// consider the next timeframe // consider the next timeframe
if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame ) if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
...@@ -1432,14 +1432,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) ...@@ -1432,14 +1432,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
if ( pPars->nTimeOutGap && pPars->timeLastSolved && clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC ) if ( pPars->nTimeOutGap && pPars->timeLastSolved && clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
{ {
printf( "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap ); printf( "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap );
Saig_Bmc3ManStop( p ); goto finish;
return RetValue;
} }
if ( nTimeToStop && clock() > nTimeToStop ) if ( nTimeToStop && clock() > nTimeToStop )
{ {
printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut ); printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut );
Saig_Bmc3ManStop( p ); goto finish;
return RetValue;
} }
// skip solved outputs // skip solved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
...@@ -1458,8 +1456,8 @@ clkOther += clock() - clk2; ...@@ -1458,8 +1456,8 @@ clkOther += clock() - clk2;
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;
Saig_Bmc3ManStop( p ); RetValue = 0;
return 0; goto finish;
} }
pPars->nFailOuts++; pPars->nFailOuts++;
if ( !pPars->fNotVerbose ) if ( !pPars->fNotVerbose )
...@@ -1540,8 +1538,8 @@ nTimeSat += clock() - clk2; ...@@ -1540,8 +1538,8 @@ nTimeSat += clock() - clk2;
} }
ABC_FREE( pAig->pSeqModel ); ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = pCex; pAig->pSeqModel = pCex;
Saig_Bmc3ManStop( p ); RetValue = 0;
return 0; goto finish;
} }
pPars->nFailOuts++; pPars->nFailOuts++;
if ( !pPars->fNotVerbose ) if ( !pPars->fNotVerbose )
...@@ -1568,8 +1566,7 @@ nTimeUndec += clock() - clk2; ...@@ -1568,8 +1566,7 @@ nTimeUndec += clock() - clk2;
fUnfinished = 1; fUnfinished = 1;
break; break;
} }
Saig_Bmc3ManStop( p ); goto finish;
return RetValue;
} }
} }
if ( pPars->fVerbose ) if ( pPars->fVerbose )
...@@ -1608,6 +1605,7 @@ nTimeUndec += clock() - clk2; ...@@ -1608,6 +1605,7 @@ nTimeUndec += clock() - clk2;
else if ( RetValue == -1 && pPars->nStart == 0 ) else if ( RetValue == -1 && pPars->nStart == 0 )
pPars->iFrame = f-1; pPars->iFrame = f-1;
//ABC_PRT( "CNF generation runtime", clkOther ); //ABC_PRT( "CNF generation runtime", clkOther );
finish:
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "Runtime: " ); printf( "Runtime: " );
......
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