From f6b67d78464a10705d02a7491ca5ef78624f209c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 4 Sep 2012 23:57:58 -0700 Subject: Added new command &gla_shrink. --- src/aig/saig/saig.h | 2 +- src/aig/saig/saigAbsStart.c | 4 ++-- src/aig/saig/saigBmc2.c | 48 +++++++++++++++++++++++++-------------------- src/aig/saig/saigTempor.c | 2 +- 4 files changed, 31 insertions(+), 25 deletions(-) (limited to 'src/aig/saig') diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index ec33b3eb..e7cdea90 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -147,7 +147,7 @@ extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlop extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); -extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames ); +extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); /*=== saigBmc3.c ==========================================================*/ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index 51033dee..90efef26 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -72,7 +72,7 @@ int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) ***********************************************************************/ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames ) { - extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames ); + extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); Vec_Int_t * vFlopsNew; int i, Entry, RetValue; *piRetValue = -1; @@ -119,7 +119,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo } else { - Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames ); + Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0 ); } if ( pAbs->pSeqModel == NULL ) return NULL; diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index a1dee6e4..f70a0015 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -754,7 +754,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames ) +int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ) { Saig_Bmc_t * p; Aig_Man_t * pNew; @@ -817,7 +817,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax // check the timeout if ( nTimeOut && clock() > nTimeToStop ) { - printf( "Reached timeout (%d seconds).\n", nTimeOut ); + if ( !fSilent ) + printf( "Reached timeout (%d seconds).\n", nTimeOut ); if ( piFrames ) *piFrames = p->iFrameLast-1; Saig_BmcManStop( p ); @@ -827,15 +828,17 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax if ( RetValue == l_True ) { assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved ); - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", - p->iOutputFail, p->iFrameFail ); + if ( !fSilent ) + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", + p->iOutputFail, p->iFrameFail ); Status = 0; if ( piFrames ) *piFrames = p->iFrameFail; } else // if ( RetValue == l_False || RetValue == l_Undef ) { - printf( "No output was asserted in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) ); + if ( !fSilent ) + printf( "No output was asserted in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) ); if ( piFrames ) { if ( p->iOutputLast > 0 ) @@ -844,24 +847,27 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax *piFrames = p->iFramePrev; } } - if ( fVerbOverwrite ) + if ( !fSilent ) { - ABC_PRTr( "Time", clock() - clk ); - } - else - { - ABC_PRT( "Time", clock() - clk ); - } - if ( RetValue != l_True ) - { - if ( p->iFrameLast >= p->nFramesMax ) - printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); - else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll ) - printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); - else if ( nTimeOut && clock() > nTimeToStop ) - printf( "Reached timeout (%d seconds).\n", nTimeOut ); + if ( fVerbOverwrite ) + { + ABC_PRTr( "Time", clock() - clk ); + } else - printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); + { + ABC_PRT( "Time", clock() - clk ); + } + if ( RetValue != l_True ) + { + if ( p->iFrameLast >= p->nFramesMax ) + printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); + else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll ) + printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); + else if ( nTimeOut && clock() > nTimeToStop ) + printf( "Reached timeout (%d seconds).\n", nTimeOut ); + else + printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); + } } Saig_BmcManStop( p ); fflush( stdout ); diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c index c8c33680..040df1f9 100644 --- a/src/aig/saig/saigTempor.c +++ b/src/aig/saig/saigTempor.c @@ -222,7 +222,7 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon // run BMC2 if ( fUseBmc ) { - RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished ); + RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0 ); if ( RetValue == 0 ) { Vec_IntFreeP( &vTransSigs ); -- cgit v1.2.3