Skip to content

A
abc
Commit d40af538 by Alan Mishchenko
Options

Unified print-out of property failures produced by all engines.

parent 71d7c9e6
Showing with 28 additions and 29 deletions
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;
}
......
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 );
......
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" );
......
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" );
......
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;
}
......
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 )
......
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) );
......
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
......
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;
}
......
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;
......
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;
......
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;
......
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;
......
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;
......
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