diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 86ba6ed5..cb6199ec 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1717,6 +1717,43 @@ void sat_solver2_verify( sat_solver2* s ) // Abc_Print(1, "Verification passed.\n" ); } */ +// checks how many watched clauses are satisfied by 0-level assignments +// (this procedure may be called before setting up a new bookmark for rollback) +int sat_solver2_check_watched( sat_solver2* s ) +{ + clause * c; + int i, k, j, m; + int claSat[2] = {0}; + // update watches + for ( i = 0; i < s->size*2; i++ ) + { + int * pArray = veci_begin(&s->wlists[i]); + for ( m = k = 0; k < veci_size(&s->wlists[i]); k++ ) + { + c = clause2_read(s, pArray[k]); + for ( j = 0; j < (int)c->size; j++ ) + if ( var_value(s, lit_var(c->lits[j])) == lit_sign(c->lits[j]) ) // true lit + break; + if ( j == (int)c->size ) + { + pArray[m++] = pArray[k]; + continue; + } + claSat[c->lrn]++; + } + veci_resize(&s->wlists[i],m); + if ( m == 0 ) + { +// s->wlists[i].cap = 0; +// s->wlists[i].size = 0; +// ABC_FREE( s->wlists[i].ptr ); + } + } +// printf( "\nClauses = %d (Sat = %d). Learned = %d (Sat = %d).\n", +// s->stats.clauses, claSat[0], s->stats.learnts, claSat[1] ); + return 0; +} + int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) { |