diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bsat/satProof.c | 35 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 294 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 8 |
3 files changed, 127 insertions, 210 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 111b3ece..b8420014 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -447,9 +447,13 @@ void Sat_ProofCheck( sat_solver2 * s ) Vec_Int_t * vUsed, * vTemp; satset * pSet, * pSet0, * pSet1; int i, k, hRoot, Handle, Counter = 0, clk = clock(); - if ( s->hLearntLast < 0 ) +// if ( s->hLearntLast < 0 ) +// return; +// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; + hRoot = s->hProofLast; + if ( hRoot == -1 ) return; - hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; + // collect visited clauses vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); Proof_CleanCollected( vProof, vUsed ); @@ -490,7 +494,7 @@ void Sat_ProofCheck( sat_solver2 * s ) Synopsis [Collects nodes belonging to the UNSAT core.] - Description [The resulting array contains 0-based IDs of root clauses.] + Description [The resulting array contains 1-based IDs of root clauses.] SideEffects [] @@ -518,7 +522,8 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ { pNode->mark = 0; if ( fUseIds ) - Vec_IntWriteEntry( vCore, i, pNode->Id - 1 ); +// Vec_IntWriteEntry( vCore, i, pNode->Id - 1 ); + Vec_IntWriteEntry( vCore, i, pNode->Id ); } return vCore; } @@ -592,9 +597,12 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) Aig_Man_t * pAig; Aig_Obj_t * pObj; int i, k, iVar, Lit, Entry, hRoot; - if ( s->hLearntLast < 0 ) +// if ( s->hLearntLast < 0 ) +// return NULL; +// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; + hRoot = s->hProofLast; + if ( hRoot == -1 ) return NULL; - hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; Sat_ProofInterpolantCheckVars( s, vGlobVars ); @@ -693,9 +701,12 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) word * pRes = ABC_ALLOC( word, nWords ); int i, k, iVar, Lit, Entry, hRoot; assert( nVars > 0 && nVars <= 16 ); - if ( s->hLearntLast < 0 ) +// if ( s->hLearntLast < 0 ) +// return NULL; +// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; + hRoot = s->hProofLast; + if ( hRoot == -1 ) return NULL; - hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; Sat_ProofInterpolantCheckVars( s, vGlobVars ); @@ -794,9 +805,13 @@ void * Sat_ProofCore( sat_solver2 * s ) Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; Vec_Int_t * vCore, * vUsed; int hRoot; - if ( s->hLearntLast < 0 ) +// if ( s->hLearntLast < 0 ) +// return NULL; +// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; + hRoot = s->hProofLast; + if ( hRoot == -1 ) return NULL; - hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; + // collect visited clauses vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); // collect core clauses diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 37ae7354..25ba35c3 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -28,7 +28,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_IMPL_START -#define SAT_USE_ANALYZE_FINAL #define SAT_USE_PROOF_LOGGING //================================================================================================= @@ -150,7 +149,9 @@ static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1 static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; } static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; } static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause_read(s, s->units[v]); } -static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } +static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ + assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; +} //static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; } // these two only work after creating a clause before the solver is called @@ -501,13 +502,8 @@ static void solver2_canceluntil(sat_solver2* s, int level) { int bound; int lastLev; int c, x; - - if ( level == 0 ) - { - int ss = 0; - } - if (solver2_dlevel(s) <= level) + if (solver2_dlevel(s) < level) return; trail = s->trail; @@ -532,7 +528,7 @@ static void solver2_canceluntil(sat_solver2* s, int level) { } -static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUnit) +static void solver2_record(sat_solver2* s, veci* cls, int proof_id) { lit* begin = veci_begin(cls); lit* end = begin + veci_size(cls); @@ -540,7 +536,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUni assert(veci_size(cls) > 0); if ( veci_size(cls) == 1 ) { - if ( s->fProofLogging && !fSkipUnit) + if ( s->fProofLogging ) var_set_unit_clause(s, lit_var(begin[0]), Cid); Cid = 0; } @@ -610,14 +606,12 @@ void Solver::analyzeFinal(satset* confl, bool skip_first) } */ -#ifdef SAT_USE_ANALYZE_FINAL - static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) { int i, j, x;//, start; veci_resize(&s->conf_final,0); if ( s->root_level == 0 ) - return -1; + return s->hProofLast; proof_chain_start( s, conf ); assert( veci_size(&s->tagged) == 0 ); satset_foreach_var( conf, x, i, skip_first ){ @@ -650,9 +644,6 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) return proof_chain_stop( s ); } -#endif - - static int solver2_lit_removable_rec(sat_solver2* s, int v) { // tag[0]: True if original conflict clause literal. @@ -916,8 +907,6 @@ satset* solver2_propagate(sat_solver2* s) end = begin + veci_size(ws); s->stats.propagations++; - s->simpdb_props--; - for (i = j = begin; i < end; ){ c = clause_read(s,*i); lits = c->pEnts; @@ -968,7 +957,8 @@ satset* solver2_propagate(sat_solver2* s) proof_chain_start( s, clause_read(s,Cid) ); proof_chain_resolve( s, NULL, Var ); proof_id = proof_chain_stop( s ); - clause_create_new( s, &Lit, &Lit, 1, proof_id ); + s->hProofLast = proof_id; +// clause_create_new( s, &Lit, &Lit, 1, proof_id ); } } @@ -990,71 +980,10 @@ WatchFound: i++; return confl; } - -/* -static void clause_remove(sat_solver2* s, satset* c) -{ - assert(lit_neg(c->pEnts[0]) < s->size*2); - assert(lit_neg(c->pEnts[1]) < s->size*2); - - veci_remove(solver2_wlist(s,lit_neg(c->pEnts[0])),clause_handle(s,c)); - veci_remove(solver2_wlist(s,lit_neg(c->pEnts[1])),clause_handle(s,c)); - - if (c->learnt){ - s->stats.learnts--; - s->stats.learnts_literals -= c->nEnts; - }else{ - s->stats.clauses--; - s->stats.clauses_literals -= c->nEnts; - } -} -*/ - -static lbool clause_simplify(sat_solver2* s, satset* c) -{ - int i, x; - assert(solver2_dlevel(s) == 0); - satset_foreach_var( c, x, i, 0 ) - if (var_value(s, x) == lit_sign(c->pEnts[i])) - return l_True; - return l_False; -} - int sat_solver2_simplify(sat_solver2* s) { - int TailOld = s->qtail; -// int type; - int Counter = 0; assert(solver2_dlevel(s) == 0); - // reset the head - s->qhead = 0; - if (solver2_propagate(s) != 0) - return false; -// printf( "Tail moved from %d to %d.\n", TailOld, s->qtail ); - - if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) - return true; -/* - for (type = 0; type < 2; type++){ - veci* cs = type ? &s->learnts : &s->clauses; - int* cls = (int*)veci_begin(cs); - int i, j; - for (j = i = 0; i < veci_size(cs); i++){ - satset* c = clause_read(s,cls[i]); - if (lit_reason(s,c->pEnts[0]) != cls[i] && - clause_simplify(s,c) == l_True) - clause_remove(s,c), Counter++; - else - cls[j++] = cls[i]; - } - veci_resize(cs,j); - } -*/ -//printf( "Simplification removed %d clauses (out of %d)...\n", Counter, s->stats.clauses ); - s->simpdb_assigns = s->qhead; - // (shouldn't depend on 'stats' really, but it will do for now) - s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); - return true; + return (solver2_propagate(s) == NULL); } /* @@ -1123,11 +1052,10 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) #endif s->stats.conflicts++; conflictC++; if (solver2_dlevel(s) <= s->root_level){ -#ifdef SAT_USE_ANALYZE_FINAL proof_id = solver2_analyze_final(s, confl, 0); assert( proof_id > 0 ); - solver2_record(s,&s->conf_final, proof_id, 0); -#endif +// solver2_record(s,&s->conf_final, proof_id); + s->hProofLast = proof_id; veci_delete(&learnt_clause); return l_False; } @@ -1137,13 +1065,11 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level; blevel = s->root_level > blevel ? s->root_level : blevel; solver2_canceluntil(s,blevel); - solver2_record(s,&learnt_clause, proof_id, 0); -#ifdef SAT_USE_ANALYZE_FINAL + solver2_record(s,&learnt_clause, proof_id); // if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions) if ( learnt_clause.size == 1 ) var_set_level( s, lit_var(learnt_clause.ptr[0]), 0 ); -#endif act_var_decay(s); act_clause_decay(s); @@ -1169,9 +1095,9 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) return l_Undef; } - if (solver2_dlevel(s) == 0 && !s->fSkipSimplify) +// if (solver2_dlevel(s) == 0 && !s->fSkipSimplify) // Simplify the set of problem clauses: - sat_solver2_simplify(s); +// sat_solver2_simplify(s); // New variable decision: s->stats.decisions++; @@ -1267,9 +1193,12 @@ sat_solver2* sat_solver2_new(void) veci_push(&s->proofs, -1); } // initialize clause pointers - s->hClausePivot = 1; - s->hLearntPivot = 1; s->hLearntLast = -1; // the last learnt clause + s->hProofLast = -1; // the last proof ID + s->hClausePivot = 1; // the pivot among clauses + s->hLearntPivot = 1; // the pivot moang learned clauses + s->iVarPivot = 0; // the pivot among the variables + s->iSimpPivot = 0; // marker of unit-clauses return s; } @@ -1381,17 +1310,13 @@ void sat_solver2_delete(sat_solver2* s) } -int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) +int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) { - lit *i,*j; - int maxvar; - lit last; - - if (begin == end) - { - assert( 0 ); - return false; - } + cla Cid; + lit *i,*j,*iFree = NULL; + int maxvar, count, temp; + assert( solver2_dlevel(s) == 0 ); + assert( begin < end ); // copy clause into storage veci_resize( &s->temp_clause, 0 ); @@ -1400,7 +1325,6 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) begin = veci_begin( &s->temp_clause ); end = begin + veci_size( &s->temp_clause ); - //printlits(begin,end); printf("\n"); // insertion sort maxvar = lit_var(*begin); for (i = begin + 1; i < end; i++){ @@ -1412,67 +1336,58 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) } sat_solver2_setnvars(s,maxvar+1); - // delete duplicates - last = lit_Undef; - for (i = j = begin; i < end; i++){ - //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -var_value(s, lit_var(*i)) : var_value(s, lit_var(*i)))); - if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i)) - return true; // tautology - else if (*i != last && var_value(s, lit_var(*i)) == varX) - last = *j++ = *i; - } - //printf("final: "); printlits(begin,j); printf("\n"); - if (j == begin) // empty clause + // coount the number of 0-literals + count = 0; + for ( i = begin; i < end; i++ ) { - assert( 0 ); - return false; + // make sure all literals are unique + assert( i == begin || lit_var(*(i-1)) != lit_var(*i) ); + // consider the value of this literal + if ( var_value(s, lit_var(*i)) == lit_sign(*i) ) // this clause is always true + return clause_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count + if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal + iFree = i; + else + count++; // literal is 0 } + assert( count < end-begin ); // the clause cannot be UNSAT - if (j - begin == 1) // unit clause - return solver2_enqueue(s,*begin,0); - - // create new clause - return clause_create_new(s,begin,j,0,0); -} - -int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) -{ - cla Cid; - lit *i,*j; - int maxvar; - assert( begin < end ); - - // copy clause into storage - veci_resize( &s->temp_clause, 0 ); - for ( i = begin; i < end; i++ ) - veci_push( &s->temp_clause, *i ); - begin = veci_begin( &s->temp_clause ); - end = begin + veci_size( &s->temp_clause ); - - // insertion sort - maxvar = lit_var(*begin); - for (i = begin + 1; i < end; i++){ - lit l = *i; - maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; - for (j = i; j > begin && *(j-1) > l; j--) - *j = *(j-1); - *j = l; - } - sat_solver2_setnvars(s,maxvar+1); + // swap variables to make sure the clause is watched using unassigned variable + temp = *iFree; + *iFree = *begin; + *begin = temp; // create a new clause Cid = clause_create_new( s, begin, end, 0, 0 ); + // handle unit clause - if ( begin + 1 == end ) + if ( count+1 == end-begin ) { -// printf( "Adding unit clause %d\n", begin[0] ); -// solver2_canceluntil(s, 0); if ( s->fProofLogging ) - var_set_unit_clause( s, lit_var(begin[0]), Cid ); - if ( !solver2_enqueue(s,begin[0],0) ) - assert( 0 ); + { + if ( count == 0 ) // original learned clause + { + var_set_unit_clause( s, lit_var(begin[0]), Cid ); + if ( !solver2_enqueue(s,begin[0],0) ) + assert( 0 ); + } + else + { + // Log production of top-level unit clause: + int x, k, proof_id, CidNew; + satset* c = clause_read(s, Cid); + proof_chain_start( s, c ); + satset_foreach_var( c, x, k, 1 ) + proof_chain_resolve( s, NULL, x ); + proof_id = proof_chain_stop( s ); + // generate a new clause + CidNew = clause_create_new( s, begin, begin+1, 1, proof_id ); + var_set_unit_clause( s, lit_var(begin[0]), CidNew ); + if ( !solver2_enqueue(s,begin[0],Cid) ) + assert( 0 ); + } + } } -//satset_print( clause_read(s, Cid) ); return Cid; } @@ -1571,6 +1486,7 @@ void solver2_reducedb(sat_solver2* s) void sat_solver2_rollback( sat_solver2* s ) { int i, k, j; + assert( s->qhead == s->qtail ); assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) ); assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) ); assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); @@ -1596,34 +1512,37 @@ void sat_solver2_rollback( sat_solver2* s ) veci_resize(&s->wlists[i],j); } // compact units - if ( s->fProofLogging ) - for ( i = 0; i < s->size; i++ ) - if ( s->units[i] && !clause_is_used(s, s->units[i]) ) - s->units[i] = 0; + if ( s->fProofLogging ) { + for ( i = 0; i < s->size; i++ ) + if ( s->units[i] && !clause_is_used(s, s->units[i]) ) + { + var_set_value(s, i, varX); + s->reasons[i] = 0; + s->units[i] = 0; + } + } } // reset implication queue - assert( (&s->trail_lim)->ptr[0] == s->simpdb_assigns ); - assert( s->simpdb_assigns >= s->iSimpPivot ); + assert( (&s->trail_lim)->ptr[0] >= s->iSimpPivot ); (&s->trail_lim)->ptr[0] = s->iSimpPivot; - s->simpdb_assigns = s->iSimpPivot; solver2_canceluntil( s, 0 ); // reset problem clauses if ( s->hClausePivot < veci_size(&s->clauses) ) { satset* first = satset_read(&s->clauses, s->hClausePivot); - s->stats.clauses = first->Id; + s->stats.clauses = first->Id-1; veci_resize(&s->clauses, s->hClausePivot); } // resetn learned clauses if ( s->hLearntPivot < veci_size(&s->learnts) ) { satset* first = satset_read(&s->learnts, s->hLearntPivot); - veci_resize(&s->claActs, first->Id+1); + veci_resize(&s->claActs, first->Id); if ( s->fProofLogging ) { - veci_resize(&s->claProofs, first->Id+1); + veci_resize(&s->claProofs, first->Id); Sat_ProofReduce( s ); } - s->stats.learnts = first->Id; + s->stats.learnts = first->Id-1; veci_resize(&s->learnts, s->hLearntPivot); } // reset watcher lists @@ -1647,8 +1566,6 @@ void sat_solver2_rollback( sat_solver2* s ) s->cla_inc = (1 << 11); #endif s->root_level = 0; - s->simpdb_assigns = 0; - s->simpdb_props = 0; s->random_seed = 91648253; s->progress_estimate = 0; s->verbosity = 0; @@ -1664,9 +1581,12 @@ void sat_solver2_rollback( sat_solver2* s ) s->stats.learnts_literals = 0; s->stats.tot_literals = 0; // initialize clause pointers - s->hClausePivot = 1; - s->hLearntPivot = 1; s->hLearntLast = -1; // the last learnt clause + s->hProofLast = -1; // the last proof ID + s->hClausePivot = 1; // the pivot among clauses + s->hLearntPivot = 1; // the pivot moang learned clauses + s->iVarPivot = 0; // the pivot among the variables + s->iSimpPivot = 0; // marker of unit-clauses } } @@ -1717,10 +1637,10 @@ void sat_solver2_verify( sat_solver2* s ) Counter++; } } - if ( Counter == 0 ) - printf( "Verification passed.\n" ); - else + if ( Counter != 0 ) printf( "Verification failed!\n" ); +// else +// printf( "Verification passed.\n" ); } @@ -1734,6 +1654,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim lit * i; s->hLearntLast = -1; + s->hProofLast = -1; // set the external limits // s->nCalls++; @@ -1750,27 +1671,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) s->nInsLimit = nInsLimitGlobal; -#ifndef SAT_USE_ANALYZE_FINAL - - //printf("solve: "); printlits(begin, end); printf("\n"); - for (i = begin; i < end; i++){ - switch (var_value(s, *i)) { - case var1: // l_True: - break; - case varX: // l_Undef - solver2_assume(s, *i); - if (solver2_propagate(s) == NULL) - break; - // fallthrough - case var0: // l_False - solver2_canceluntil(s, 0); - return l_False; - } - } - s->root_level = solver2_dlevel(s); - -#endif - /* // Perform assumptions: root_level = assumps.size(); @@ -1803,7 +1703,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim assert(root_level == decisionLevel()); */ -#ifdef SAT_USE_ANALYZE_FINAL // Perform assumptions: s->root_level = end - begin; for ( i = begin; i < end; i++ ) @@ -1822,6 +1721,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } else { + assert( 0 ); proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions) veci_resize(&s->conf_final,0); veci_push(&s->conf_final, lit_neg(p)); @@ -1829,7 +1729,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (var_level(s, lit_var(p)) > 0) veci_push(&s->conf_final, p); } - solver2_record(s, &s->conf_final, proof_id, 1); +// solver2_record(s, &s->conf_final, proof_id, 1); + s->hProofLast = proof_id; solver2_canceluntil(s, 0); return l_False; } @@ -1839,14 +1740,14 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (confl != NULL){ proof_id = solver2_analyze_final(s, confl, 0); assert(s->conf_final.size > 0); +// solver2_record(s,&s->conf_final, proof_id, 1); + s->hProofLast = proof_id; solver2_canceluntil(s, 0); - solver2_record(s,&s->conf_final, proof_id, 1); return l_False; } } } assert(s->root_level == solver2_dlevel(s)); -#endif if (s->verbosity >= 1){ printf("==================================[MINISAT]===================================\n"); @@ -1891,6 +1792,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim printf("==============================================================================\n"); solver2_canceluntil(s,0); + assert( s->qhead == s->qtail ); // if ( status == l_True ) // sat_solver2_verify( s ); return status; 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 ) |