diff options
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 82 |
1 files changed, 44 insertions, 38 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 4fbf7c70..d662f376 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2138,56 +2138,62 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp ) ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - if ( RetValue == 1 ) - { - Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) ); - } - else if ( RetValue == -1 ) + if ( !pPars->fSilent ) { - if ( pPars->nFailOuts == 0 ) + if ( RetValue == 1 ) { - Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) ); - if ( nTimeOut && Abc_Clock() > nTimeOut ) - Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut ); - else - Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit ); + Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) ); } - else + else if ( RetValue == -1 ) { - Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame ); - if ( Abc_Clock() > nTimeOut ) - Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut ); + if ( pPars->nFailOuts == 0 ) + { + Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) ); + if ( nTimeOut && Abc_Clock() > nTimeOut ) + Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut ); + else + Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit ); + } else - Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit ); - } - } - else // if ( RetValue == 0 ) - { - if ( !pPars->fSolveAll ) - { - Abc_Cex_t * pCex = pNtk->pSeqModel; - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame ); + { + Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame ); + if ( Abc_Clock() > nTimeOut ) + Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut ); + else + Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit ); + } } - else + else // if ( RetValue == 0 ) { - int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan); - if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs ) - Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs ); - else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 ) - Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs ); + if ( !pPars->fSolveAll ) + { + Abc_Cex_t * pCex = pNtk->pSeqModel; + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame ); + } else { - Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs ); - if ( pPars->nDropOuts ) - Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs ); - Abc_Print( 1, ". " ); + int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan); + if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs ) + Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs ); + else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 ) + Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs ); + else + { + Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs ); + if ( pPars->nDropOuts ) + Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs ); + Abc_Print( 1, ". " ); + } } - if ( pNtk->vSeqModelVec ) - Vec_PtrFreeFree( pNtk->vSeqModelVec ); - pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; } + ABC_PRT( "Time", Abc_Clock() - clk ); + } + if ( RetValue == 0 && pPars->fSolveAll ) + { + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; } - ABC_PRT( "Time", Abc_Clock() - clk ); if ( pNtk->pSeqModel ) { status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel ); |