Small tweak to rollback behavior.

3 files changed, 8 insertions, 0 deletions

diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 3738129b..af3dcffb 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -397,6 +397,9 @@ static inline void solver_garbage_collect(solver_t *s)
     unsigned *array;
     struct cdb *new_cdb = cdb_alloc(cdb_capacity(s->all_clauses) - cdb_wasted(s->all_clauses));
 
+    if (s->book_cdb)
+        s->book_cdb = 0;
+
     for (i = 0; i < 2 * vec_char_size(s->assigns); i++) {
         struct watcher *w;
         watch_list_foreach(s->watches, w, i)
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index dcae8f6e..33f8ce88 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -95,6 +95,7 @@ struct solver_t_ {
     /* Bookmark */
     unsigned book_cl_orig; /* Bookmark for orignal problem clauses vector */
     unsigned book_cl_lrnt; /* Bookmark for learnt clauses vector */
+    unsigned book_cdb;     /* Bookmark clause database size */
     unsigned book_vars;    /* Bookmark number of variables */
     unsigned book_trail;   /* Bookmark trail size */
 
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 90d04cfd..3cb9f3d3 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -330,6 +330,7 @@ void satoko_unbookmark(satoko_t *s)
 {
     s->book_cl_orig = 0;
     s->book_cl_lrnt = 0;
+    s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
 }
@@ -365,6 +366,7 @@ void satoko_reset(satoko_t *s)
     s->RC2 = s->opts.n_conf_fst_reduce;
     s->book_cl_orig = 0;
     s->book_cl_lrnt = 0;
+    s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
 }
@@ -412,6 +414,8 @@ void satoko_rollback(satoko_t *s)
     /* Rewind solver and cancel level 0 assignments to the trail */
     solver_cancel_until(s, 0);
     vec_uint_shrink(s->trail, s->book_trail);
+    if (s->book_cdb)
+        s->all_clauses->size = s->book_cdb;
     s->book_cl_orig = 0;
     s->book_cl_lrnt = 0;
     s->book_vars = 0;