From d40af538e2b7dc644fa427c37965a9721b64b12d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Sep 2012 20:46:34 -0700 Subject: Unified print-out of property failures produced by all engines. --- src/aig/gia/giaAbsOut.c | 2 +- src/aig/gia/giaEra2.c | 5 ++--- src/aig/gia/giaSim.c | 2 +- src/aig/gia/giaSim2.c | 2 +- src/aig/saig/saigAbs.c | 4 ++-- src/aig/saig/saigBmc2.c | 6 +++--- src/aig/saig/saigBmc3.c | 4 ++-- src/base/abci/abcDar.c | 10 +++++----- src/proof/bbr/bbrReach.c | 4 ++-- src/proof/llb/llb1Reach.c | 4 ++-- src/proof/llb/llb2Core.c | 4 ++-- src/proof/llb/llb3Nonlin.c | 4 ++-- src/proof/llb/llb4Nonlin.c | 2 +- src/proof/ssw/sswRarity.c | 4 ++-- 14 files changed, 28 insertions(+), 29 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaAbsOut.c b/src/aig/gia/giaAbsOut.c index f7204307..0b303355 100644 --- a/src/aig/gia/giaAbsOut.c +++ b/src/aig/gia/giaAbsOut.c @@ -73,7 +73,7 @@ Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPi else { Abc_Print( 1, "Counter-example verification is successful.\n" ); - Abc_Print( 1, "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame ); } return pCex; } diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c index b0823ee8..060c83a5 100644 --- a/src/aig/gia/giaEra2.c +++ b/src/aig/gia/giaEra2.c @@ -1736,9 +1736,8 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos Gia_ManAreDepth(p, p->iStaCur-1) ); ABC_PRT( "Time", clock() - clk ); if ( pAig->pCexSeq != NULL ) -// printf( "Miter FAILED in state %d at frame %d (use \"&write_counter\" to dump a witness)\n", - printf( "Miter FAILED in state %d at frame %d (the cex is available for refinement)\n", - p->iStaCur, Gia_ManAreDepth(p, p->iStaCur)-1 ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", + p->iStaCur, pAig->pName, Gia_ManAreDepth(p, p->iStaCur)-1 ); if ( fVerbose ) { ABC_PRTP( "Cofactoring", p->timeAig - p->timeCube, clock() - clk ); diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 8d22e699..da6ac33e 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -631,7 +631,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) Gia_ManResetRandom( pPars ); pPars->iOutFail = iOut; pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids ); - Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", iOut, pAig->pName, i ); if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) { // Abc_Print( 1, "\n" ); diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c index 897eff98..85428769 100644 --- a/src/aig/gia/giaSim2.c +++ b/src/aig/gia/giaSim2.c @@ -663,7 +663,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) Gia_ManResetRandom( pPars ); pPars->iOutFail = iOut; pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat ); - Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", iOut, pAig->pName, i ); if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) { // Abc_Print( 1, "\n" ); diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index ffb17db8..f30963a8 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -118,8 +118,8 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA } else { - printf( "Counter-example verification is successful.\n" ); - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); + Abc_Print( 1, "Counter-example verification is successful.\n" ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame ); } return pCex; } diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index f70a0015..ed15c635 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -829,8 +829,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax { assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved ); if ( !fSilent ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", - p->iOutputFail, p->iFrameFail ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", + p->iOutputFail, p->pAig->pName, p->iFrameFail ); Status = 0; if ( piFrames ) *piFrames = p->iFrameFail; @@ -838,7 +838,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax else // if ( RetValue == l_False || RetValue == l_Undef ) { if ( !fSilent ) - printf( "No output was asserted in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) ); + Abc_Print( 1, "No output failed in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) ); if ( piFrames ) { if ( p->iOutputLast > 0 ) diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index bb59f677..75014158 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1413,7 +1413,7 @@ clkOther += clock() - clk2; return 0; } pPars->nFailOuts++; - printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); @@ -1486,7 +1486,7 @@ clkOther += clock() - clk2; return 0; } pPars->nFailOuts++; - printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 97385b91..85377956 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1899,7 +1899,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int else // if ( RetValue == 0 ) { Abc_Cex_t * pCex = pNtk->pSeqModel; - Abc_Print( 1, "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame ); } ABC_PRT( "Time", clock() - clk ); } @@ -1988,7 +1988,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp ) if ( !pPars->fSolveAll ) { Abc_Cex_t * pCex = pNtk->pSeqModel; - Abc_Print( 1, "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame ); } else { @@ -2120,7 +2120,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man if ( RetValue == 1 ) Abc_Print( 1, "Property proved. " ); else if ( RetValue == 0 ) - Abc_Print( 1, "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness). ", iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel ? pMan->pSeqModel->iPo : -1, pMan->pName, iFrame ); else if ( RetValue == -1 ) Abc_Print( 1, "Property UNDECIDED. " ); else @@ -2445,7 +2445,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i if ( pNtk->pSeqModel ) { Abc_Cex_t * pCex = pNtk->pSeqModel; - Abc_Print( 1, "Output %d asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, pNtk->pName, pCex->iFrame ); if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) ) Abc_Print( 1, "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" ); } @@ -2580,7 +2580,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) if ( RetValue == 1 ) Abc_Print( 1, "Property proved. " ); else if ( RetValue == 0 ) - Abc_Print( 1, "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness). ", ppCex? (*ppCex)->iFrame : -1 ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", (*ppCex)->iPo, pNtk->pName, ppCex? (*ppCex)->iFrame : -1 ); else if ( RetValue == -1 ) Abc_Print( 1, "Property UNDECIDED. " ); else diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c index 19d87bc2..13f4f558 100644 --- a/src/proof/bbr/bbrReach.c +++ b/src/proof/bbr/bbrReach.c @@ -336,7 +336,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); Cudd_RecursiveDeref( dd, bIntersect ); if ( !pPars->fSilent ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", i, Vec_PtrSize(vOnionRings) ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, Vec_PtrSize(vOnionRings) ); Cudd_RecursiveDeref( dd, bReached ); bReached = NULL; pPars->iFrame = nIters; @@ -488,7 +488,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars ) vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); Cudd_RecursiveDeref( dd, bIntersect ); if ( !pPars->fSilent ) - printf( "The miter output %d is proved REACHABLE in the initial state (use \"write_counter\" to dump a witness). ", i ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, -1 ); RetValue = 0; break; } diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c index fed0389a..b7d79994 100644 --- a/src/proof/llb/llb1Reach.c +++ b/src/proof/llb/llb1Reach.c @@ -699,9 +699,9 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo if ( !p->pPars->fSilent ) { if ( !p->pPars->fBackward ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAigGlo->pSeqModel->iPo, nIters ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAigGlo->pSeqModel->iPo, p->pAigGlo->pName, p->pAigGlo->pName, nIters ); else - printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); + Abc_Print( 1, "Output ??? of miter \"%s\" was asserted in frame %d (counter-example is not produced). ", p->pAigGlo->pName, nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } p->pPars->iFrame = nIters - 1; diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c index f19f757e..a6f16aeb 100644 --- a/src/proof/llb/llb2Core.c +++ b/src/proof/llb/llb2Core.c @@ -323,9 +323,9 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ if ( !p->pPars->fSilent ) { if ( !p->pPars->fBackward ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pInit->pSeqModel->iPo, nIters ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, p->pInit->pName, nIters ); else - printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); + Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } p->pPars->iFrame = nIters - 1; diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c index 8badc61d..22e23337 100644 --- a/src/proof/llb/llb3Nonlin.c +++ b/src/proof/llb/llb3Nonlin.c @@ -504,9 +504,9 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) if ( !p->pPars->fSilent ) { if ( !p->pPars->fBackward ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pInit->pSeqModel->iPo, nIters ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, nIters ); else - printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); + Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } p->pPars->iFrame = nIters - 1; diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c index f2973922..51f9d602 100644 --- a/src/proof/llb/llb4Nonlin.c +++ b/src/proof/llb/llb4Nonlin.c @@ -759,7 +759,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) Vec_PtrFreeP( &vStates ); if ( !p->pPars->fSilent ) { - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAig->pSeqModel->iPo, nIters ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAig->pSeqModel->iPo, p->pAig->pName, nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } p->pPars->iFrame = nIters - 1; diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index d13e82ee..73a65d88 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -946,7 +946,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in printf( "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, fVerbose ); // print final report - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pAig->pSeqModel->iPo, pAig->pSeqModel->iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); RetValue = 0; goto finish; @@ -1106,7 +1106,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize Abc_CexFree( pAig->pSeqModel ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 ); // print final report - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pAig->pSeqModel->iPo, pAig->pSeqModel->iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); RetValue = 0; goto finish; -- cgit v1.2.3