diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-10 14:55:33 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-10 14:55:33 -0800 |
| commit | c2a1a9ef372419844d6fad0fbbc35790c873e1c0 (patch) | |
| tree | fb3a732a04d5c84ed61f233940e163869667b700 /src/sat | |
| parent | a2228ee09b76bd6b33156c5bc4ad1fcd5cfe13a6 (diff) | |
| download | abc-c2a1a9ef372419844d6fad0fbbc35790c873e1c0.tar.gz abc-c2a1a9ef372419844d6fad0fbbc35790c873e1c0.tar.bz2 abc-c2a1a9ef372419844d6fad0fbbc35790c873e1c0.zip | |
Implementing rollback in the updated solver.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 11 |
1 files changed, 6 insertions, 5 deletions
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 ) { |