From 68636887891036a2ebd77fa0397afd7da91a551a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 23 Jan 2013 12:37:44 +0700 Subject: Enabled detecting CEXes in multiple POs without stopping (sim3 -a). --- src/proof/pdr/pdr.h | 1 + src/proof/pdr/pdrCore.c | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) (limited to 'src/proof/pdr') diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index a815bb30..c2243761 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -53,6 +53,7 @@ struct Pdr_Par_t_ int fSkipGeneral; // skips expensive generalization step int fVerbose; // verbose output` int fVeryVerbose; // very verbose output + int fNotVerbose; // not printing line by line progress int fSilent; // totally silent execution int fSolveAll; // do not stop when found a SAT output int nFailOuts; // the number of failed outputs diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 46288925..314784d7 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -57,6 +57,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->fShortest = 0; // forces bug traces to be shortest pPars->fVerbose = 0; // verbose output pPars->fVeryVerbose = 0; // very verbose output + pPars->fNotVerbose = 0; // not printing line-by-line progress pPars->iFrame = -1; // explored up to this frame } @@ -645,8 +646,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); pCex = Pdr_ManDeriveCex(p); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex ); - Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", - nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + if ( !p->pPars->fNotVerbose ) + Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", + nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT Pdr_QueueClean( p ); -- cgit v1.2.3