diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-12 17:50:41 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-12 17:50:41 -0800 |
| commit | df3e23ae3a20d0f6b8a1d3512e322b98057eb136 (patch) | |
| tree | 5ee7c1c6a2618fad81211dd4312dfa9b9a923bb2 /src/aig/gia/giaAbs.c | |
| parent | fa96b8d7988da75e38d45b719d21a64e5ecbdb9c (diff) | |
| download | abc-df3e23ae3a20d0f6b8a1d3512e322b98057eb136.tar.gz abc-df3e23ae3a20d0f6b8a1d3512e322b98057eb136.tar.bz2 abc-df3e23ae3a20d0f6b8a1d3512e322b98057eb136.zip | |
Enabled skipping random decisions in PBA, which are performed by default.
Diffstat (limited to 'src/aig/gia/giaAbs.c')
| -rw-r--r-- | src/aig/gia/giaAbs.c | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 2432bdbf..16fe9c35 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -379,7 +379,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_Gla1ManTest( 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 ); Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; Vec_Int_t * vGateClasses, * vGateClassesOld = NULL; Aig_Man_t * pAig; @@ -397,7 +397,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) // perform abstraction pAig = Gia_ManToAigSimple( pGia ); assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) ); - vGateClasses = Aig_Gla1ManTest( 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 ); Aig_ManStop( pAig ); // update the map @@ -419,7 +419,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) ***********************************************************************/ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ) { - extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose ); + extern Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ); Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; Vec_Int_t * vGateClasses; Aig_Man_t * pAig; @@ -440,7 +440,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ) } // perform abstraction - vGateClasses = Aig_Gla2ManTest( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose ); + vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose ); Aig_ManStop( pAig ); // update the BMC depth |