From c985e17d1f62597924a3e12a2a5e54df41e089e4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 8 Dec 2011 15:06:26 -0800 Subject: Proof-logging in the updated solver. --- src/sat/bsat/satSolver2.h | 10 ++++++---- 1 file changed, 6 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 d77c0141..01216146 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -103,8 +103,8 @@ struct sat_solver2_t // clauses veci clauses; // clause memory veci* wlists; // watcher lists (for each literal) - int iLearntFirst; // the first learnt clause - int iLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) + int hLearntFirst; // the first learnt clause + int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) // activities #ifdef USE_FLOAT_ACTIVITY @@ -139,10 +139,10 @@ struct sat_solver2_t veci mark_levels; // temporary storage for labeled levels veci min_lit_order; // ordering of removable literals veci min_step_order; // ordering of resolution steps - veci glob_vars; // global variables + veci learnt_live; // remaining clauses after reduce DB // proof logging - veci proof_clas; // sequence of proof clauses + veci proofs; // sequence of proof records int iStartChain; // temporary variable to remember beginning of the current chain in proof logging int nUnits; // the total number of unit clauses @@ -178,6 +178,8 @@ static inline void satset_print (satset * c) { #define satset_foreach_entry( p, c, h, s ) \ for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) ) +#define satset_foreach_entry_vec( pVec, p, c, i ) \ + for ( i = 0; (i < veci_size(pVec)) && ((c) = satset_read(p, veci_begin(pVec)[i])); i++ ) #define satset_foreach_var( p, var, i, start ) \ for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ ) -- cgit v1.2.3