diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-30 11:47:24 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-30 11:47:24 -0700 |
| commit | a22db31d6de27dfd1f8de47a4fa425372f4a1d0d (patch) | |
| tree | fd96d827035bfda0e80eb59bd18a914148983b5f /src/sat/bsat | |
| parent | ed564664f1ab86611cc05245745a22501f8414c2 (diff) | |
| download | abc-a22db31d6de27dfd1f8de47a4fa425372f4a1d0d.tar.gz abc-a22db31d6de27dfd1f8de47a4fa425372f4a1d0d.tar.bz2 abc-a22db31d6de27dfd1f8de47a4fa425372f4a1d0d.zip | |
Saving variable activity during rollback.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 6 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 5 |
2 files changed, 10 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 934f1be1..c6da6237 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1168,6 +1168,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n) s->activity = ABC_REALLOC(double, s->activity, s->cap); #else s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); + s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap); #endif s->model = ABC_REALLOC(int, s->model, s->cap); memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) ); @@ -1253,6 +1254,7 @@ void sat_solver2_delete(sat_solver2* s) ABC_FREE(s->reasons ); ABC_FREE(s->units ); ABC_FREE(s->activity ); + ABC_FREE(s->activity2); ABC_FREE(s->model ); } ABC_FREE(s); @@ -1559,6 +1561,8 @@ void sat_solver2_rollback( sat_solver2* s ) // update order if ( s->iVarPivot < s->size ) { + if ( s->activity2 ) + memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot ); veci_resize(&s->order, 0); for ( i = 0; i < s->iVarPivot; i++ ) { @@ -1665,6 +1669,8 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) Mem += s->cap * sizeof(double); // ABC_FREE(s->activity ); #else Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity ); + if ( s->activity2 ) + Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity2); #endif Mem += s->cap * sizeof(lit); // ABC_FREE(s->trail ); Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos ); diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 1682ab6e..f2cc1552 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -99,7 +99,8 @@ struct sat_solver2_t #else int var_inc; // 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* activity; // A heuristic measurement of the activity of a variable + unsigned* activity2; // backup variable activity #endif int nUnits; // the total number of unit clauses @@ -240,6 +241,8 @@ static inline void sat_solver2_bookmark(sat_solver2* s) if ( s->pPrf1 ) s->hProofPivot = Vec_SetHandCurrent(s->pPrf1); Sat_MemBookMark( &s->Mem ); + if ( s->activity2 ) + 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 ) |