summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorBruno Schmitt <bruno@oschmitt.com>2017-02-19 15:34:21 -0800
committerBruno Schmitt <bruno@oschmitt.com>2017-02-19 15:34:21 -0800
commit68dd7806355a423af3ea400ab7c605bd3bf566d3 (patch)
tree8a46e2e3a88497e07bfba8caf7d0fe231eeba3c8 /src
parent99fe7dfe2906cafad8fafc104b23e6ec8416ce4e (diff)
downloadabc-68dd7806355a423af3ea400ab7c605bd3bf566d3.tar.gz
abc-68dd7806355a423af3ea400ab7c605bd3bf566d3.tar.bz2
abc-68dd7806355a423af3ea400ab7c605bd3bf566d3.zip
Adding new command to reset Satoko.
Small fixes in watching list data structure.
Diffstat (limited to 'src')
-rw-r--r--src/sat/satoko/cdb.h6
-rw-r--r--src/sat/satoko/satoko.h2
-rw-r--r--src/sat/satoko/solver_api.c48
-rw-r--r--src/sat/satoko/types.h1
-rw-r--r--src/sat/satoko/utils/heap.h5
-rw-r--r--src/sat/satoko/watch_list.h10
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) {