From 6b2fe00cd82f0229777a6beb2390858834551399 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 1 Nov 2019 00:58:12 +0200 Subject: Changes to several APIs. --- src/sat/bsat/satSolver.c | 28 ++++++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 31ae8dae..2f3a84db 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -217,16 +217,32 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars) { int i; - assert( s->VarActType == 1 ); for (i = 0; i < s->size; i++) s->activity[i] = 0; - s->var_inc = Abc_Dbl2Word(1); - for ( i = 0; i < nVars; i++ ) + if ( s->VarActType == 0 ) { - int iVar = pVars ? pVars[i] : i; - s->activity[iVar] = Abc_Dbl2Word(nVars-i); - order_update( s, iVar ); + s->var_inc = (1 << 5); + s->var_decay = -1; + for ( i = 0; i < nVars; i++ ) + { + int iVar = pVars ? pVars[i] : i; + s->activity[iVar] = s->var_inc*(nVars-i); + if (s->orderpos[iVar] != -1) + order_update( s, iVar ); + } } + else if ( s->VarActType == 1 ) + { + s->var_inc = Abc_Dbl2Word(1); + for ( i = 0; i < nVars; i++ ) + { + int iVar = pVars ? pVars[i] : i; + s->activity[iVar] = Abc_Dbl2Word(nVars-i); + if (s->orderpos[iVar] != -1) + order_update( s, iVar ); + } + } + else assert( 0 ); } //================================================================================================= -- cgit v1.2.3