From c2a1a9ef372419844d6fad0fbbc35790c873e1c0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 10 Dec 2011 14:55:33 -0800 Subject: Implementing rollback in the updated solver. --- src/sat/bsat/satSolver2.c | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 93dd9d01..e2bea751 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1322,7 +1322,8 @@ void sat_solver2_delete(sat_solver2* s) veci_delete( pCore ); ABC_FREE( pCore ); */ -// Sat_ProofCheck( s ); +// if ( s->fProofLogging ) +// Sat_ProofCheck( s ); // delete vectors veci_delete(&s->order); @@ -1516,17 +1517,17 @@ void solver2_reducedb(sat_solver2* s) { pArray = veci_begin(&s->wlists[i]); for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) - if ( pArray[k] & 1 ) + if ( !(pArray[k] & 1) ) // problem clause pArray[j++] = pArray[k]; - else if ( !(c = clause_read(s, pArray[k]))->mark ) - pArray[j++] = c->Id; + else if ( !(c = clause_read(s, pArray[k]))->mark ) // useful learned clause + pArray[j++] = (c->Id << 1) | 1; veci_resize(&s->wlists[i],j); } // compact units if ( s->fProofLogging ) for ( i = 0; i < s->size; i++ ) if ( s->units[i] && (s->units[i] & 1) ) - s->units[i] = clause_read(s, s->units[i])->Id; + s->units[i] = (clause_read(s, s->units[i])->Id << 1) | 1; // compact clauses satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) { -- cgit v1.2.3