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/saig | |
| 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/saig')
| -rw-r--r-- | src/aig/saig/saig.h | 1 | ||||
| -rw-r--r-- | src/aig/saig/saigGlaCba.c | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigGlaPba.c | 3 |
3 files changed, 4 insertions, 2 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 9f98a8f9..99928a66 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -68,6 +68,7 @@ struct Saig_ParBmc_t_ int fSolveAll; // does not stop at the first SAT output int fDropSatOuts; // replace sat outputs by constant 0 int nFfToAddMax; // max number of flops to add during CBA + int fSkipRand; // skip random decisions int fVerbose; // verbose int iFrame; // explored up to this frame int nFailOuts; // the number of failed outputs diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c index d0fd2db3..9140c7bf 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_Gla1ManTest( 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 ) { Vec_Int_t * vResult = NULL; Aig_Gla1Man_t * p; diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index 00e04346..fce2372f 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -553,7 +553,7 @@ Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose ) +Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ) { Aig_Gla2Man_t * p; Vec_Int_t * vCore, * vResult; @@ -578,6 +578,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int n Aig_Gla2ManStop( p ); return NULL; } + sat_solver_set_random( p->pSat, fSkipRand ); p->timePre += Abc_Clock(1,0); // set runtime limit |