diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-10-09 15:42:25 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-10-09 15:42:25 -0700 |
| commit | daeffe791cb2f6690a23f4cf4d0d3101a5ac54b5 (patch) | |
| tree | 25cfc25fa019bf143410c3cb672c8c518a3489f5 | |
| parent | fed18333e2bb055cf253244da9362f862c2be091 (diff) | |
| download | abc-daeffe791cb2f6690a23f4cf4d0d3101a5ac54b5.tar.gz abc-daeffe791cb2f6690a23f4cf4d0d3101a5ac54b5.tar.bz2 abc-daeffe791cb2f6690a23f4cf4d0d3101a5ac54b5.zip | |
Making report about the number of correcty covered frames consistent across the engines.
| -rw-r--r-- | src/aig/saig/saigBmc2.c | 6 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 2 | ||||
| -rw-r--r-- | src/proof/int/intCore.c | 4 | ||||
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 1 |
4 files changed, 7 insertions, 6 deletions
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index ed15c635..7d4bfdd2 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -833,7 +833,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax p->iOutputFail, p->pAig->pName, p->iFrameFail ); Status = 0; if ( piFrames ) - *piFrames = p->iFrameFail; + *piFrames = p->iFrameFail - 1; } else // if ( RetValue == l_False || RetValue == l_Undef ) { @@ -842,9 +842,9 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax if ( piFrames ) { if ( p->iOutputLast > 0 ) - *piFrames = p->iFramePrev - 1; + *piFrames = p->iFramePrev - 2; else - *piFrames = p->iFramePrev; + *piFrames = p->iFramePrev - 1; } } if ( !fSilent ) diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 294f6b64..c8ed7e5a 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1551,7 +1551,7 @@ clkOther += clock() - clk2; if ( nJumpFrame && pPars->nStart == 0 ) pPars->iFrame = nJumpFrame - pPars->nFramesJump; else if ( RetValue == -1 && pPars->nStart == 0 ) - pPars->iFrame = f; + pPars->iFrame = f-1; //ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) { diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c index 7891fa69..f563eea2 100644 --- a/src/proof/int/intCore.c +++ b/src/proof/int/intCore.c @@ -97,7 +97,7 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, if ( Inter_ManCheckInitialState(pAig) ) { - *piFrame = 0; + *piFrame = -1; printf( "Property trivially fails in the initial state.\n" ); return 0; } @@ -223,7 +223,7 @@ p->timeEqu += clock() - clk; ABC_PRT( "Time", clock() - clk ); } // remember the number of timeframes completed - pPars->iFrameMax = i + 1 + p->nFrames; + pPars->iFrameMax = i - 1 + p->nFrames; if ( RetValue == 0 ) // found a (spurious?) counter-example { if ( i == 0 ) // real counterexample diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 5cb05143..ca2ca5a0 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -709,6 +709,7 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, p->vPrio = NULL; } Pdr_ManStop( p ); + pPars->iFrame--; return RetValue; } |