summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBruno Schmitt <bruno@oschmitt.com>2017-02-15 17:02:32 -0800
committerBruno Schmitt <bruno@oschmitt.com>2017-02-15 17:02:32 -0800
commit088aabc1023e6745bedeb16f9f8f01515c38e4b7 (patch)
tree318f0246c6b6f9d63230c26b45b4e7830e99b3ac
parent30037e06533b1c7291e32025ebb7c9a2e875e079 (diff)
downloadabc-088aabc1023e6745bedeb16f9f8f01515c38e4b7.tar.gz
abc-088aabc1023e6745bedeb16f9f8f01515c38e4b7.tar.bz2
abc-088aabc1023e6745bedeb16f9f8f01515c38e4b7.zip
- Small changes to the watch lists behavior.
- Implementation of bookmark, unbookmark and rollback procedures. - Minor changes.
-rw-r--r--src/sat/satoko/satoko.h7
-rw-r--r--src/sat/satoko/solver.c5
-rw-r--r--src/sat/satoko/solver.h6
-rw-r--r--src/sat/satoko/solver_api.c56
-rw-r--r--src/sat/satoko/types.h1
-rwxr-xr-xsrc/sat/satoko/utils/vec/vec_sdbl.h6
-rw-r--r--src/sat/satoko/watch_list.h22
7 files changed, 98 insertions, 5 deletions
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index 8d55a81c..88070eac 100644
--- a/src/sat/satoko/satoko.h
+++ b/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.
*
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index d2bf1b5e..21a4860d 100644
--- a/src/sat/satoko/solver.c
+++ b/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;
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index 84c25689..68cc97dc 100644
--- a/src/sat/satoko/solver.h
+++ b/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;
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 65fab837..9cad0a14 100644
--- a/src/sat/satoko/solver_api.c
+++ b/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;
diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h
index d51aed4c..9c47ca7c 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_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/vec/vec_sdbl.h b/src/sat/satoko/utils/vec/vec_sdbl.h
index aefd687a..ec1c731c 100755
--- a/src/sat/satoko/utils/vec/vec_sdbl.h
+++ b/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;
diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h
index 96399a83..49f419f2 100644
--- a/src/sat/satoko/watch_list.h
+++ b/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)
{