luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Saving variable activity during rollback.

This commit is contained in:
Alan Mishchenko 2012-07-30 12:02:30 -07:00
parent a22db31d6d
commit 51d5055e68
2 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/sat/bsat/satSolver2.c
View File

@ -1562,7 +1562,10 @@ void sat_solver2_rollback( sat_solver2* s )
if ( s->iVarPivot < s->size ) if ( s->iVarPivot < s->size )
{ {
if ( s->activity2 ) if ( s->activity2 )
{
s->var_inc = s->var_inc2;
memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot ); memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot );
}
veci_resize(&s->order, 0); veci_resize(&s->order, 0);
for ( i = 0; i < s->iVarPivot; i++ ) for ( i = 0; i < s->iVarPivot; i++ )
{ {

4
src/sat/bsat/satSolver2.h
View File

@ -98,6 +98,7 @@ struct sat_solver2_t
double* activity; // A heuristic measurement of the activity of a variable. double* activity; // A heuristic measurement of the activity of a variable.
#else #else
int var_inc; // Amount to bump next variable with. 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. 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 unsigned* activity2; // backup variable activity
@ -242,8 +243,11 @@ static inline void sat_solver2_bookmark(sat_solver2* s)
s->hProofPivot = Vec_SetHandCurrent(s->pPrf1); s->hProofPivot = Vec_SetHandCurrent(s->pPrf1);
Sat_MemBookMark( &s->Mem ); Sat_MemBookMark( &s->Mem );
if ( s->activity2 ) if ( s->activity2 )
{
s->var_inc2 = s->var_inc;
memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot ); 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 ) static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark, int Id )
{ {