diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-12 23:42:19 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-12 23:42:19 -0800 |
| commit | b695e3334cd033083c7b9e80942e23b9e0d3010c (patch) | |
| tree | bf16e81b2c12b325570b079a3b0a407e68d620f7 /src | |
| parent | 30ea50a3b4618f0217d89b812535fdeb617893d4 (diff) | |
| download | abc-b695e3334cd033083c7b9e80942e23b9e0d3010c.tar.gz abc-b695e3334cd033083c7b9e80942e23b9e0d3010c.tar.bz2 abc-b695e3334cd033083c7b9e80942e23b9e0d3010c.zip | |
Setting the number of completed time frames.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaAbs.c | 13 | ||||
| -rw-r--r-- | src/aig/saig/saigGlaCba.c | 3 |
2 files changed, 13 insertions, 3 deletions
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 16fe9c35..0a8652ad 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -291,6 +291,8 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ) // update flop classes Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd ); Vec_IntFree( vAbsFfsToAdd ); + if ( p->fVerbose ) + Gia_ManPrintStats( pGia, 0 ); return -1; } @@ -362,6 +364,8 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit RetValue = -1; } Aig_ManStop( pAig ); + if ( fVerbose ) + Gia_ManPrintStats( pGia, 0 ); return RetValue; } @@ -379,7 +383,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit ***********************************************************************/ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) { - extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose ); + extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame ); Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; Vec_Int_t * vGateClasses, * vGateClassesOld = NULL; Aig_Man_t * pAig; @@ -395,14 +399,17 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) } // perform abstraction + p->iFrame = -1; pAig = Gia_ManToAigSimple( pGia ); assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) ); - vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose ); + vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose, &p->iFrame ); Aig_ManStop( pAig ); // update the map Vec_IntFreeP( &vGateClassesOld ); pGia->vGateClasses = vGateClasses; + if ( p->fVerbose ) + Gia_ManPrintStats( pGia, 0 ); return 1; } @@ -476,6 +483,8 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ) Vec_IntFreeP( &pGia->vGateClasses ); pGia->vGateClasses = vGateClasses; } + if ( p->fVerbose ) + Gia_ManPrintStats( pGia, 0 ); return 1; } diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c index 9140c7bf..eae9a3c2 100644 --- a/src/aig/saig/saigGlaCba.c +++ b/src/aig/saig/saigGlaCba.c @@ -676,7 +676,7 @@ void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose ) +Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame ) { Vec_Int_t * vResult = NULL; Aig_Gla1Man_t * p; @@ -812,6 +812,7 @@ Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, i printf( "The problem is SAT in frame %d. The CEX is currently not produced.\n", f ); else printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f ); + *piFrame = i; // print stats if ( fVerbose ) { |