luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

- Small bug fix in var activity (improve performance) 

- New implementation of watcher lists.
This commit is contained in:
Bruno Schmitt 2017-02-14 14:43:44 -08:00
parent f4853496d7
commit 30037e0653
4 changed files with 55 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/sat/satoko/solver.c
View File

@ -114,7 +114,7 @@ static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits)
vec_uint_assign(s->stamps, lit2var(lit), s->cur_stamp);
counter = 0;
watch_list_foreach(s->bin_watches, w, neg_lit) {
watch_list_foreach_bin(s->watches, w, neg_lit) {
unsigned imp_lit = w->blocker;
if (vec_uint_at(s->stamps, lit2var(imp_lit)) == s->cur_stamp &&
lit_value(s, imp_lit) == LIT_TRUE) {
@ -400,8 +400,6 @@ static inline void solver_garbage_collect(solver_t *s)
struct watcher *w;
watch_list_foreach(s->watches, w, i)
clause_realloc(new_cdb, s->all_clauses, &(w->cref));
watch_list_foreach(s->bin_watches, w, i)
clause_realloc(new_cdb, s->all_clauses, &(w->cref));
}
for (i = 0; i < vec_uint_size(s->trail); i++)
@ -541,7 +539,7 @@ unsigned solver_propagate(solver_t *s)
struct watcher *i, *j;
n_propagations++;
watch_list_foreach(s->bin_watches, i, p) {
watch_list_foreach_bin(s->watches, i, p) {
if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
continue;
if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING)
@ -553,16 +551,14 @@ unsigned solver_propagate(solver_t *s)
ws = vec_wl_at(s->watches, p);
begin = watch_list_array(ws);
end = begin + watch_list_size(ws);
for (i = j = begin; i < end;) {
for (i = j = begin + ws->n_bin; i < end;) {
struct clause *clause;
struct watcher w;
if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
{
if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) {
*j++ = *i++;
continue;
}
if (lit_value(s, i->blocker) == LIT_TRUE) {
*j++ = *i++;
continue;
@ -590,7 +586,7 @@ unsigned solver_propagate(solver_t *s)
if (lit_value(s, lits[k]) != LIT_FALSE) {
lits[1] = lits[k];
lits[k] = neg_lit;
watch_list_push(vec_wl_at(s->watches, lit_neg(lits[1])), w);
watch_list_push(vec_wl_at(s->watches, lit_neg(lits[1])), w, 0);
goto next;
}
}

20
src/sat/satoko/solver.h
View File

@ -49,7 +49,6 @@ struct solver_t_ {
vec_uint_t *learnts;
vec_uint_t *originals;
vec_wl_t *watches;
vec_wl_t *bin_watches;
/* Activity heuristic */
act_t var_act_inc; /* Amount to bump next variable with. */
@ -200,6 +199,7 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
vec_uint_push_back(s->trail, lit);
return SATOKO_OK;
}
static inline int solver_varnum(solver_t *s)
{
return vec_char_size(s->assigns);
@ -227,25 +227,15 @@ static inline void clause_watch(solver_t *s, unsigned cref)
w2.cref = cref;
w1.blocker = clause->data[1].lit;
w2.blocker = clause->data[0].lit;
if (clause->size == 2) {
watch_list_push(vec_wl_at(s->bin_watches, lit_neg(clause->data[0].lit)), w1);
watch_list_push(vec_wl_at(s->bin_watches, lit_neg(clause->data[1].lit)), w2);
} else {
watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), w1);
watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), w2);
}
watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), w1, (clause->size == 2));
watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), w2, (clause->size == 2));
}
static inline void clause_unwatch(solver_t *s, unsigned cref)
{
struct clause *clause = cdb_handler(s->all_clauses, cref);
if (clause->size == 2) {
watch_list_remove(vec_wl_at(s->bin_watches, lit_neg(clause->data[0].lit)), cref);
watch_list_remove(vec_wl_at(s->bin_watches, lit_neg(clause->data[1].lit)), cref);
} else {
watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), cref);
watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), cref);
}
watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), cref, (clause->size == 2));
watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), cref, (clause->size == 2));
}
ABC_NAMESPACE_HEADER_END

23
src/sat/satoko/solver_api.c
View File

@ -89,7 +89,6 @@ solver_t * satoko_create()
s->originals = vec_uint_alloc(0);
s->learnts = vec_uint_alloc(0);
s->watches = vec_wl_alloc(0);
s->bin_watches = vec_wl_alloc(0);
/* Activity heuristic */
s->var_act_inc = VAR_ACT_INIT_INC;
s->clause_act_inc = CLAUSE_ACT_INIT_INC;
@ -128,7 +127,6 @@ void satoko_destroy(solver_t *s)
vec_uint_free(s->originals);
vec_uint_free(s->learnts);
vec_wl_free(s->watches);
vec_wl_free(s->bin_watches);
vec_act_free(s->activity);
heap_free(s->var_order);
vec_uint_free(s->levels);
@ -145,7 +143,8 @@ void satoko_destroy(solver_t *s)
vec_uint_free(s->stack);
vec_uint_free(s->last_dlevel);
vec_uint_free(s->stamps);
if (s->marks) vec_char_free(s->marks);
if (s->marks)
vec_char_free(s->marks);
satoko_free(s);
}
@ -220,13 +219,9 @@ int satoko_simplify(solver_t * s)
void satoko_add_variable(solver_t *s, char sign)
{
unsigned var = vec_act_size(s->activity);
vec_wl_push(s->bin_watches);
vec_wl_push(s->bin_watches);
vec_wl_push(s->watches);
vec_wl_push(s->watches);
/* Variable activity are initialized with the lowest possible value
* which in satoko double implementation (SDBL) is the constant 1 */
vec_act_push_back(s->activity, SDBL_CONST1);
vec_act_push_back(s->activity, 0);
vec_uint_push_back(s->levels, 0);
vec_char_push_back(s->assigns, VAR_UNASSING);
vec_char_push_back(s->polarity, sign);
@ -320,23 +315,23 @@ satoko_stats_t satoko_stats(satoko_t *s)
return s->stats;
}
void satoko_mark_cone(satoko_t *s, int * pvars, int nvars)
void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
{
int i;
if (!solver_has_marks(s))
s->marks = vec_char_init(solver_varnum(s), 0);
for (i = 0; i < nvars; i++)
{
s->marks = vec_char_init(solver_varnum(s), 0);
for (i = 0; i < n_vars; i++) {
var_set_mark(s, pvars[i]);
if (!heap_in_heap(s->var_order, pvars[i]))
heap_insert(s->var_order, pvars[i]);
}
}
void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars)
void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars)
{
int i;
assert(solver_has_marks(s));
for (i = 0; i < nvars; i++)
for (i = 0; i < n_vars; i++)
var_clean_mark(s, pvars[i]);
}

54
src/sat/satoko/watch_list.h
View File

@ -10,6 +10,7 @@
#define satoko__watch_list_h
#include "utils/mem.h"
#include "utils/misc.h"
#include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
@ -22,6 +23,7 @@ struct watcher {
struct watch_list {
unsigned cap;
unsigned size;
unsigned n_bin;
struct watcher *watchers;
};
@ -40,6 +42,10 @@ struct vec_wl_t_ {
watch < watch_list_array(vec_wl_at(vec, lit)) + watch_list_size(vec_wl_at(vec, lit)); \
watch++)
#define watch_list_foreach_bin(vec, watch, lit) \
for (watch = watch_list_array(vec_wl_at(vec, lit)); \
watch < watch_list_array(vec_wl_at(vec, lit)) + vec_wl_at(vec, lit)->n_bin; \
watch++)
//===------------------------------------------------------------------------===
// Watch list API
//===------------------------------------------------------------------------===
@ -60,25 +66,33 @@ static inline void watch_list_shrink(struct watch_list *wl, unsigned size)
wl->size = size;
}
static inline void watch_list_push(struct watch_list *wl, struct watcher w)
static inline void watch_list_grow(struct watch_list *wl)
{
unsigned new_size = (wl->cap < 4) ? 4 : (wl->cap / 2) * 3;
struct watcher *watchers =
satoko_realloc(struct watcher, wl->watchers, new_size);
if (watchers == NULL) {
printf("Failed to realloc memory from %.1f MB to %.1f "
"MB.\n",
1.0 * wl->cap / (1 << 20),
1.0 * new_size / (1 << 20));
fflush(stdout);
return;
}
wl->watchers = watchers;
wl->cap = new_size;
}
static inline void watch_list_push(struct watch_list *wl, struct watcher w, unsigned is_bin)
{
assert(wl);
if (wl->size == wl->cap) {
unsigned new_size = (wl->cap < 4) ? 4 : (wl->cap / 2) * 3;
struct watcher *watchers =
satoko_realloc(struct watcher, wl->watchers, new_size);
if (watchers == NULL) {
printf("Failed to realloc memory from %.1f MB to %.1f "
"MB.\n",
1.0 * wl->cap / (1 << 20),
1.0 * new_size / (1 << 20));
fflush(stdout);
return;
}
wl->watchers = watchers;
wl->cap = new_size;
}
if (wl->size == wl->cap)
watch_list_grow(wl);
wl->watchers[wl->size++] = w;
if (is_bin && wl->size > wl->n_bin) {
stk_swap(struct watcher, wl->watchers[wl->n_bin], wl->watchers[wl->size - 1]);
wl->n_bin++;
}
}
static inline struct watcher *watch_list_array(struct watch_list *wl)
@ -86,11 +100,15 @@ static inline struct watcher *watch_list_array(struct watch_list *wl)
return wl->watchers;
}
static inline void watch_list_remove(struct watch_list *wl, unsigned cref)
static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin)
{
struct watcher *watchers = watch_list_array(wl);
unsigned i;
for (i = 0; watchers[i].cref != cref; i++);
if (is_bin) {
for (i = 0; watchers[i].cref != cref; i++);
wl->n_bin--;
} else
for (i = wl->n_bin; watchers[i].cref != cref; i++);
assert(i < watch_list_size(wl));
memmove((wl->watchers + i), (wl->watchers + i + 1),
(wl->size - i - 1) * sizeof(struct watcher));