From ce0e8caf79b596423272aa5d9d4aeb931aa88259 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 27 Jan 2012 00:48:06 -0800 Subject: Variable timeframe abstraction. --- src/sat/bsat/satSolver2.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/sat/bsat/satSolver2.h') diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 2c5f8bf4..63fc9755 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -85,8 +85,6 @@ struct sat_solver2_t int qtail; // Tail index of queue. int root_level; // Level of first proper decision. - int simpdb_assigns; // Number of top-level assignments at last 'simplifyDB()'. - int simpdb_props; // Number of propagations before next 'simplifyDB()'. double random_seed; double progress_estimate; int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything // activities @@ -111,9 +109,10 @@ struct sat_solver2_t veci clauses; // clause memory veci learnts; // learnt memory veci* wlists; // watcher lists (for each literal) + int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) + int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) int hClausePivot; // the pivot among problem clause int hLearntPivot; // the pivot among learned clause - int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) int iVarPivot; // the pivot among the variables int iSimpPivot; // marker of unit-clauses @@ -247,10 +246,11 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) static inline void sat_solver2_bookmark(sat_solver2* s) { + assert( s->qhead == s->qtail ); s->hLearntPivot = veci_size(&s->learnts); s->hClausePivot = veci_size(&s->clauses); s->iVarPivot = s->size; - s->iSimpPivot = s->simpdb_assigns; + s->iSimpPivot = s->qhead; } static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) -- cgit v1.2.3