Initial implementation of AnalyseFinal

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;

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