summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorBruno Schmitt <bruno@oschmitt.com>2017-02-21 18:37:06 -0300
committerBruno Schmitt <bruno@oschmitt.com>2017-02-21 18:37:06 -0300
commit9d46d84b278acac3ca5983ddb7fbd41a9a4b926b (patch)
treed33ae3ca83994865ba3bca99e460854f22187ce7 /src
parentac1eb60db9129110e7795614ad82d85cb74d854e (diff)
downloadabc-9d46d84b278acac3ca5983ddb7fbd41a9a4b926b.tar.gz
abc-9d46d84b278acac3ca5983ddb7fbd41a9a4b926b.tar.bz2
abc-9d46d84b278acac3ca5983ddb7fbd41a9a4b926b.zip
Small tweak to rollback behavior.
Diffstat (limited to 'src')
-rw-r--r--src/sat/satoko/solver.c3
-rw-r--r--src/sat/satoko/solver.h1
-rw-r--r--src/sat/satoko/solver_api.c4
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;