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/satSolver2.h | |
| 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/satSolver2.h')
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 5 |
1 files changed, 4 insertions, 1 deletions
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 ) |