From df3e23ae3a20d0f6b8a1d3512e322b98057eb136 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 12 Nov 2011 17:50:41 -0800 Subject: Enabled skipping random decisions in PBA, which are performed by default. --- src/aig/gia/giaAbs.c | 8 ++++---- src/aig/saig/saig.h | 1 + src/aig/saig/saigGlaCba.c | 2 +- src/aig/saig/saigGlaPba.c | 3 ++- src/base/abci/abc.c | 9 +++++++-- src/sat/bsat/satSolver.c | 2 +- src/sat/bsat/satSolver.h | 8 ++++++++ 7 files changed, 24 insertions(+), 9 deletions(-) (limited to 'src') 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 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 diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ed23abfd..81b82f73 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29093,8 +29093,9 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0; pPars->nFramesMax = 10; //pPars->nStart + 10; pPars->nConfLimit = 0; + pPars->fSkipRand = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrvh" ) ) != EOF ) { switch ( c ) { @@ -29142,6 +29143,9 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nTimeOut < 0 ) goto usage; break; + case 'r': + pPars->fSkipRand ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -29185,12 +29189,13 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-vh]\n" ); + Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rvh]\n" ); Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-r : toggle using random decisiont during SAT solving [default = %s]\n", !pPars->fSkipRand? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index ac2202dc..d4726b81 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -967,7 +967,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT int* levels = s->levels; double var_decay = 0.95; double clause_decay = 0.999; - double random_var_freq = 0.02; + double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; ABC_INT64_T conflictC = 0; veci learnt_clause; diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index a33c7240..a67e829a 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -175,6 +175,7 @@ struct sat_solver_t Sat_MmStep_t * pMem; int fSkipSimplify; // set to one to skip simplification of the clause database + int fNotUseRandom; // do not allow random decisions with a fixed probability int * pGlobalVars; // for experiments with global vars during interpolation // clause store @@ -228,6 +229,13 @@ static int sat_solver_set_runtime_limit(sat_solver* s, int Limit) return nRuntimeLimit; } +static int sat_solver_set_random(sat_solver* s, int fNotUseRandom) +{ + int fNotUseRandomOld = s->fNotUseRandom; + s->fNotUseRandom = fNotUseRandom; + return fNotUseRandomOld; +} + ABC_NAMESPACE_HEADER_END #endif -- cgit v1.2.3