diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 8 |
2 files changed, 9 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 10dea1e3..1f02adec 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -976,7 +976,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT #endif s->stats.conflicts++; conflictC++; if (sat_solver_dlevel(s) == s->root_level){ -// lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0]; + lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0]; // sat_solver_analyze_final(s, lit_neg(p), &s->conf_final); veci_delete(&learnt_clause); return l_False; diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 2e435c59..f474fc1d 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -85,6 +85,8 @@ extern int sat_solver_nconflicts(sat_solver* s); extern void sat_solver_setnvars(sat_solver* s,int n); +extern int sat_solver_final(sat_solver* s, int ** ppArray); + struct stats_t { ABC_INT64_T starts, decisions, propagations, inspects, conflicts; @@ -214,6 +216,12 @@ static void sat_solver_compress(sat_solver* s) } } +static int sat_solver_final(sat_solver* s, int ** ppArray) +{ + *ppArray = s->conf_final.ptr; + return s->conf_final.size; +} + ABC_NAMESPACE_HEADER_END |