- Small changes to the watch lists behavior.

- Implementation of bookmark, unbookmark and rollback procedures.
- Minor changes.

src/sat/satoko/satoko.h

@@ -89,9 +89,12 @@ extern void satoko_assump_push(satoko_t *s, unsigned);
 extern void satoko_assump_pop(satoko_t *s);
 extern int  satoko_simplify(satoko_t *);
 extern int  satoko_solve(satoko_t *);
-extern void satoko_mark_cone(satoko_t *s, int * pvars, int nvars);
-extern void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars);
+extern void satoko_mark_cone(satoko_t *, int *, int);
+extern void satoko_unmark_cone(satoko_t *, int *, int);
 
+extern void satoko_rollback(satoko_t *);
+extern void satoko_bookmark(satoko_t *);
+extern void satoko_unbookmark(satoko_t *);
 /* If problem is unsatisfiable under assumptions, this function is used to
  * obtain the final conflict clause expressed in the assumptions.
  *

src/sat/satoko/solver.c

@@ -402,6 +402,7 @@ static inline void solver_garbage_collect(solver_t *s)
             clause_realloc(new_cdb, s->all_clauses, &(w->cref));
     }
 
+    /* Update CREFS */
     for (i = 0; i < vec_uint_size(s->trail); i++)
         if (lit_reason(s, vec_uint_at(s->trail, i)) != UNDEF)
             clause_realloc(new_cdb, s->all_clauses, &(vec_uint_data(s->reasons)[lit2var(vec_uint_at(s->trail, i))]));
@@ -427,7 +428,7 @@ static inline void solver_reduce_cdb(solver_t *s)
     struct clause **learnts_cls;
 
     learnts_cls = satoko_alloc(struct clause *, n_learnts);
-    vec_uint_foreach(s->learnts, cref, i)
+    vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt)
         learnts_cls[i] = clause_read(s, cref);
 
     limit = (unsigned)(n_learnts * s->opts.learnt_ratio);
@@ -504,7 +505,7 @@ unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt)
     return cref;
 }
 
-void solver_cancel_until(solver_t * s, unsigned level)
+void solver_cancel_until(solver_t *s, unsigned level)
 {
     int i;
 

src/sat/satoko/solver.h

@@ -92,6 +92,12 @@ struct solver_t_ {
     vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and
                  * clauses minimization with binary resolution */
 
+    /* Bookmark */
+    unsigned book_cl_orig; /* Bookmark for orignal problem clauses vector */
+    unsigned book_cl_lrnt; /* Bookmark for learnt clauses vector */
+    unsigned book_vars;    /* Bookmark number of variables */
+    unsigned book_trail;   /* Bookmark trail size */
+
     /* Temporary data used for solving cones */
     vec_char_t *marks;
 

src/sat/satoko/solver_api.c

@@ -229,7 +229,8 @@ void satoko_add_variable(solver_t *s, char sign)
     vec_uint_push_back(s->stamps, 0);
     vec_char_push_back(s->seen, 0);
     heap_insert(s->var_order, var);
-    if (s->marks) vec_char_push_back(s->marks, 0);
+    if (s->marks)
+        vec_char_push_back(s->marks, 0);
 }
 
 int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
@@ -315,6 +316,59 @@ satoko_stats_t satoko_stats(satoko_t *s)
     return s->stats;
 }
 
+void satoko_bookmark(satoko_t *s)
+{
+    assert(solver_dlevel(s) == 0);
+    s->book_cl_orig = vec_uint_size(s->originals);
+    s->book_cl_lrnt = vec_uint_size(s->learnts);
+    s->book_vars = vec_char_size(s->assigns);
+    s->book_trail = vec_uint_size(s->trail);
+}
+
+void satoko_unbookmark(satoko_t *s)
+{
+    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;
+    unsigned n_originals = vec_uint_size(s->originals) - s->book_cl_orig;
+    unsigned n_learnts = vec_uint_size(s->learnts) - s->book_cl_lrnt;
+    struct clause **cl_to_remove;
+
+    assert(solver_dlevel(s) == 0);
+    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)
+        cl_to_remove[i] = clause_read(s, cref);
+    vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt)
+        cl_to_remove[n_originals + i] = clause_read(s, cref);
+    for (i = 0; i < n_originals + n_learnts; i++) {
+        clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i]));
+        cl_to_remove[i]->f_mark = 1;
+    }
+    vec_uint_shrink(s->originals, s->book_cl_orig);
+    vec_uint_shrink(s->learnts, s->book_cl_lrnt);
+    /* Shrink variable related vectors */
+    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_char_shrink(s->assigns, 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 */
+    solver_cancel_until(s, 0);
+    vec_uint_shrink(s->trail, s->book_trail);
+    s->book_cl_orig = 0;
+    s->book_cl_lrnt = 0;
+    s->book_vars = 0;
+    s->book_trail = 0;
+}
+
 void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
 {
     int i;

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_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)
 

src/sat/satoko/utils/vec/vec_sdbl.h

@@ -86,6 +86,12 @@ static inline unsigned vec_sdbl_size(vec_sdbl_t *p)
     return p->size;
 }
 
+static inline void vec_sdbl_shrink(vec_sdbl_t *p, unsigned new_size)
+{
+    assert(new_size <= p->cap);
+    p->size = new_size;
+}
+
 static inline void vec_sdbl_resize(vec_sdbl_t *p, unsigned new_size)
 {
     p->size = new_size;

src/sat/satoko/watch_list.h

@@ -100,6 +100,27 @@ static inline struct watcher *watch_list_array(struct watch_list *wl)
     return wl->watchers;
 }
 
+/* TODO: I still have mixed feelings if this change should be done, keeping the
+ * old code commented after it. */
+static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin)
+{
+    struct watcher *watchers = watch_list_array(wl);
+    unsigned i;
+    if (is_bin) {
+        for (i = 0; watchers[i].cref != cref; i++);
+        assert(i < watch_list_size(wl));
+        wl->n_bin--;
+        memmove((wl->watchers + i), (wl->watchers + i + 1),
+                (wl->size - i - 1) * sizeof(struct watcher));
+    } else {
+        for (i = wl->n_bin; watchers[i].cref != cref; i++);
+        assert(i < watch_list_size(wl));
+        stk_swap(struct watcher, wl->watchers[i], wl->watchers[wl->size - 1]);
+    }
+    wl->size -= 1;
+}
+
+/*
 static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin)
 {
     struct watcher *watchers = watch_list_array(wl);
@@ -114,6 +135,7 @@ static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsig
             (wl->size - i - 1) * sizeof(struct watcher));
     wl->size -= 1;
 }
+*/
 
 static inline vec_wl_t *vec_wl_alloc(unsigned cap)
 {