From a22db31d6de27dfd1f8de47a4fa425372f4a1d0d Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 30 Jul 2012 11:47:24 -0700
Subject: [PATCH] Saving variable activity during rollback.
---
src/sat/bsat/satSolver2.c | 6 ++++++
src/sat/bsat/satSolver2.h | 5 ++++-
2 files changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 934f1be..c6da623 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 1682ab6..f2cc155 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 )
--
libgit2 0.26.0