summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2010-12-03 09:26:08 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2010-12-03 09:26:08 -0800
commitf4066b5be3b5473f5c64ab71d1983df6ca7aec76 (patch)
tree9beb56d7a62a0e735c2ca451403597751fe88b95
parent002ad0f9844f4706b409e7b8e6f0d63a5b3e0eb9 (diff)
downloadabc-f4066b5be3b5473f5c64ab71d1983df6ca7aec76.tar.gz
abc-f4066b5be3b5473f5c64ab71d1983df6ca7aec76.tar.bz2
abc-f4066b5be3b5473f5c64ab71d1983df6ca7aec76.zip
Initial implementation of AnalyseFinal
-rw-r--r--src/sat/bsat/satSolver.c2
-rw-r--r--src/sat/bsat/satSolver.h8
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