diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2010-12-03 09:26:08 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2010-12-03 09:26:08 -0800 |
| commit | f4066b5be3b5473f5c64ab71d1983df6ca7aec76 (patch) | |
| tree | 9beb56d7a62a0e735c2ca451403597751fe88b95 /src/sat/bsat | |
| parent | 002ad0f9844f4706b409e7b8e6f0d63a5b3e0eb9 (diff) | |
| download | abc-f4066b5be3b5473f5c64ab71d1983df6ca7aec76.tar.gz abc-f4066b5be3b5473f5c64ab71d1983df6ca7aec76.tar.bz2 abc-f4066b5be3b5473f5c64ab71d1983df6ca7aec76.zip | |
Initial implementation of AnalyseFinal
Diffstat (limited to 'src/sat/bsat')
| -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 |