Experiments with SAT sweeping.

3 files changed, 11 insertions, 1 deletions

diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 3e5fc8ee..3738129b 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -364,6 +364,7 @@ static inline void solver_analyze_final(solver_t *s, unsigned lit)
 {
     int i;
 
+    vec_uint_clear(s->final_conflict);
     vec_uint_push_back(s->final_conflict, lit);
     if (solver_dlevel(s) == 0)
         return;
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index e4fd88b7..f758a1ef 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -356,10 +356,15 @@ void satoko_rollback(satoko_t *s)
     vec_uint_shrink(s->originals, s->book_cl_orig);
     vec_uint_shrink(s->learnts, s->book_cl_lrnt);
     /* Shrink variable related vectors */
+    for (i = s->book_vars; i < 2 * vec_char_size(s->assigns); i++)
+        vec_wl_at(s->watches, i)->size = 0;
+    s->watches->size = s->book_vars;
     vec_act_shrink(s->activity, s->book_vars);
     vec_uint_shrink(s->levels, s->book_vars);
     vec_uint_shrink(s->reasons, s->book_vars);
+    vec_uint_shrink(s->stamps, s->book_vars);
     vec_char_shrink(s->assigns, s->book_vars);
+    vec_char_shrink(s->seen, s->book_vars);
     vec_char_shrink(s->polarity, s->book_vars);
     solver_rebuild_order(s);
     /* Rewind solver and cancel level 0 assignments to the trail */
@@ -369,6 +374,10 @@ void satoko_rollback(satoko_t *s)
     s->book_cl_lrnt = 0;
     s->book_vars = 0;
     s->book_trail = 0;
+    if (!s->book_vars) {
+        s->all_clauses->size = 0;
+        s->all_clauses->wasted = 0;
+    }
 }
 
 void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h
index 49f419f2..a36ab2bb 100644
--- a/src/sat/satoko/watch_list.h
+++ b/src/sat/satoko/watch_list.h
@@ -154,7 +154,7 @@ static inline vec_wl_t *vec_wl_alloc(unsigned cap)
 static inline void vec_wl_free(vec_wl_t *vec_wl)
 {
     unsigned i;
-    for (i = 0; i < vec_wl->size; i++)
+    for (i = 0; i < vec_wl->cap; i++)
         watch_list_free(vec_wl->watch_lists + i);
     satoko_free(vec_wl->watch_lists);
     satoko_free(vec_wl);