luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Setting the number of completed time frames.

This commit is contained in:
Alan Mishchenko 2011-11-12 23:42:19 -08:00
parent 30ea50a3b4
commit b695e3334c
2 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/aig/gia/giaAbs.c
View File

@ -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;
}

3
src/aig/saig/saigGlaCba.c
View File

@ -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 )
{