diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-30 17:43:15 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-30 17:43:15 -0700 |
| commit | 017c35baf22da739f29bcafbda2063640bd1e82d (patch) | |
| tree | f0fba5fa18d87885d99ae98961cc0e4114e978f3 /src/sat | |
| parent | 900bdfac1750e5ab0690b77f47be9e24a7e79c21 (diff) | |
| download | abc-017c35baf22da739f29bcafbda2063640bd1e82d.tar.gz abc-017c35baf22da739f29bcafbda2063640bd1e82d.tar.bz2 abc-017c35baf22da739f29bcafbda2063640bd1e82d.zip | |
Updating bmc3 printout to show the number of failed outputs.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 26 |
1 files changed, 12 insertions, 14 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 48028f76..28bb7729 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1382,14 +1382,14 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) // stop BMC after exploring all reachable states if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) ) { - Saig_Bmc3ManStop( p ); - return pPars->nFailOuts ? 0 : 1; + RetValue = pPars->nFailOuts ? 0 : 1; + goto finish; } // stop BMC if all targets are solved if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) ) { - Saig_Bmc3ManStop( p ); - return 0; + RetValue = 0; + goto finish; } // consider the next timeframe if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame ) @@ -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 ) { printf( "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap ); - Saig_Bmc3ManStop( p ); - return RetValue; + goto finish; } if ( nTimeToStop && clock() > nTimeToStop ) { printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut ); - Saig_Bmc3ManStop( p ); - return RetValue; + goto finish; } // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) @@ -1458,8 +1456,8 @@ clkOther += clock() - clk2; printf( "Output %d is trivially SAT in frame %d.\n", i, f ); ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = pCex; - Saig_Bmc3ManStop( p ); - return 0; + RetValue = 0; + goto finish; } pPars->nFailOuts++; if ( !pPars->fNotVerbose ) @@ -1540,8 +1538,8 @@ nTimeSat += clock() - clk2; } ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = pCex; - Saig_Bmc3ManStop( p ); - return 0; + RetValue = 0; + goto finish; } pPars->nFailOuts++; if ( !pPars->fNotVerbose ) @@ -1568,8 +1566,7 @@ nTimeUndec += clock() - clk2; fUnfinished = 1; break; } - Saig_Bmc3ManStop( p ); - return RetValue; + goto finish; } } if ( pPars->fVerbose ) @@ -1608,6 +1605,7 @@ nTimeUndec += clock() - clk2; else if ( RetValue == -1 && pPars->nStart == 0 ) pPars->iFrame = f-1; //ABC_PRT( "CNF generation runtime", clkOther ); +finish: if ( pPars->fVerbose ) { printf( "Runtime: " ); |