From 51d5055e68f5eb0e4ee222c8ffe20c00e1cd1b0f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 30 Jul 2012 12:02:30 -0700 Subject: Saving variable activity during rollback. --- src/sat/bsat/satSolver2.c | 3 +++ src/sat/bsat/satSolver2.h | 4 ++++ 2 files changed, 7 insertions(+) diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index c6da6237..47c7b72f 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1562,7 +1562,10 @@ void sat_solver2_rollback( sat_solver2* s ) if ( s->iVarPivot < s->size ) { if ( s->activity2 ) + { + s->var_inc = s->var_inc2; memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot ); + } veci_resize(&s->order, 0); for ( i = 0; i < s->iVarPivot; i++ ) { diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index f2cc1552..bed774ef 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -98,6 +98,7 @@ struct sat_solver2_t double* activity; // A heuristic measurement of the activity of a variable. #else int var_inc; // Amount to bump next variable with. + int var_inc2; // Amount to bump next variable with. int cla_inc; // Amount to bump next clause with. unsigned* activity; // A heuristic measurement of the activity of a variable unsigned* activity2; // backup variable activity @@ -242,7 +243,10 @@ static inline void sat_solver2_bookmark(sat_solver2* s) s->hProofPivot = Vec_SetHandCurrent(s->pPrf1); Sat_MemBookMark( &s->Mem ); if ( s->activity2 ) + { + s->var_inc2 = s->var_inc; memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot ); + } } static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark, int Id ) -- cgit v1.2.3