Adding new command to reset Satoko.

Small fixes in watching list data structure.

6 files changed, 63 insertions, 9 deletions

diff --git a/src/sat/satoko/cdb.h b/src/sat/satoko/cdb.h
index 28686ff2..32b0bf93 100644
--- a/src/sat/satoko/cdb.h
+++ b/src/sat/satoko/cdb.h
@@ -81,6 +81,12 @@ static inline void cdb_remove(struct cdb *p, struct clause *clause)
     p->wasted += clause->size;
 }
 
+static inline void cdb_clear(struct cdb *p)
+{
+    p->wasted = 0;
+    p->size = 0;
+}
+
 static inline unsigned cdb_capacity(struct cdb *p)
 {
     return p->cap;
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index 2d3e056e..a0c4d216 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -80,6 +80,8 @@ struct satoko_stats {
 //===------------------------------------------------------------------------===
 extern satoko_t *satoko_create(void);
 extern void satoko_destroy(satoko_t *);
+extern void satoko_reset(satoko_t *);
+
 extern void satoko_default_opts(satoko_opts_t *);
 extern void satoko_configure(satoko_t *, satoko_opts_t *);
 extern int  satoko_parse_dimacs(char *, satoko_t **);
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index f758a1ef..90d04cfd 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -334,6 +334,41 @@ void satoko_unbookmark(satoko_t *s)
     s->book_trail = 0;
 }
 
+void satoko_reset(satoko_t *s)
+{
+    vec_uint_clear(s->assumptions);
+    vec_uint_clear(s->final_conflict);
+    cdb_clear(s->all_clauses);
+    vec_uint_clear(s->originals);
+    vec_uint_clear(s->learnts);
+    vec_wl_clean(s->watches);
+    vec_act_clear(s->activity);
+    heap_clear(s->var_order);
+    vec_uint_clear(s->levels);
+    vec_uint_clear(s->reasons);
+    vec_char_clear(s->assigns);
+    vec_char_clear(s->polarity);
+    vec_uint_clear(s->trail);
+    vec_uint_clear(s->trail_lim);
+    b_queue_clean(s->bq_lbd);
+    b_queue_clean(s->bq_trail);
+    vec_uint_clear(s->temp_lits);
+    vec_char_clear(s->seen);
+    vec_uint_clear(s->tagged);
+    vec_uint_clear(s->stack);
+    vec_uint_clear(s->last_dlevel);
+    vec_uint_clear(s->stamps);
+    s->var_act_inc = VAR_ACT_INIT_INC;
+    s->clause_act_inc = CLAUSE_ACT_INIT_INC;
+    s->n_confl_bfr_reduce = s->opts.n_conf_fst_reduce;
+    s->RC1 = 1;
+    s->RC2 = s->opts.n_conf_fst_reduce;
+    s->book_cl_orig = 0;
+    s->book_cl_lrnt = 0;
+    s->book_vars = 0;
+    s->book_trail = 0;
+}
+
 void satoko_rollback(satoko_t *s)
 {
     unsigned i, cref;
@@ -342,6 +377,11 @@ void satoko_rollback(satoko_t *s)
     struct clause **cl_to_remove;
 
     assert(solver_dlevel(s) == 0);
+    if (!s->book_vars) {
+        satoko_reset(s);
+        return;
+    }
+
     cl_to_remove = satoko_alloc(struct clause *, n_originals + n_learnts);
     /* Mark clauses */
     vec_uint_foreach_start(s->originals, cref, i, s->book_cl_orig)
@@ -356,8 +396,10 @@ 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++)
+    for (i = s->book_vars; i < 2 * vec_char_size(s->assigns); i++) {
         vec_wl_at(s->watches, i)->size = 0;
+        vec_wl_at(s->watches, i)->n_bin = 0;
+    }
     s->watches->size = s->book_vars;
     vec_act_shrink(s->activity, s->book_vars);
     vec_uint_shrink(s->levels, s->book_vars);
@@ -374,10 +416,6 @@ 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/types.h b/src/sat/satoko/types.h
index 9c47ca7c..06c190ab 100644
--- a/src/sat/satoko/types.h
+++ b/src/sat/satoko/types.h
@@ -26,6 +26,7 @@ typedef vec_sdbl_t vec_act_t ;
 #define vec_act_free(vec) vec_sdbl_free(vec)
 #define vec_act_size(vec) vec_sdbl_size(vec)
 #define vec_act_data(vec) vec_sdbl_data(vec)
+#define vec_act_clear(vec) vec_sdbl_clear(vec)
 #define vec_act_shrink(vec, size) vec_sdbl_shrink(vec, size)
 #define vec_act_at(vec, idx) vec_sdbl_at(vec, idx)
 #define vec_act_push_back(vec, value) vec_sdbl_push_back(vec, value)
diff --git a/src/sat/satoko/utils/heap.h b/src/sat/satoko/utils/heap.h
index 8b1d8f4b..391b8a7e 100644
--- a/src/sat/satoko/utils/heap.h
+++ b/src/sat/satoko/utils/heap.h
@@ -158,10 +158,7 @@ static inline void heap_build(heap_t *p, vec_uint_t *entries)
 
 static inline void heap_clear(heap_t *p)
 {
-    unsigned i;
-    int entry;
-    vec_int_foreach(p->indices, entry, i)
-        vec_int_assign(p->indices, i, -1);
+    vec_int_clear(p->indices);
     vec_uint_clear(p->data);
 }
 
diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h
index a36ab2bb..1bcbf3b4 100644
--- a/src/sat/satoko/watch_list.h
+++ b/src/sat/satoko/watch_list.h
@@ -160,6 +160,16 @@ static inline void vec_wl_free(vec_wl_t *vec_wl)
     satoko_free(vec_wl);
 }
 
+static inline void vec_wl_clean(vec_wl_t *vec_wl)
+{
+    unsigned i;
+    for (i = 0; i < vec_wl->size; i++) {
+        vec_wl->watch_lists[i].size = 0;
+        vec_wl->watch_lists[i].n_bin = 0;
+    }
+    vec_wl->size = 0;
+}
+
 static inline void vec_wl_push(vec_wl_t *vec_wl)
 {
     if (vec_wl->size == vec_wl->cap) {