diff options
author | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-06 11:34:52 -0800 |
---|---|---|
committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-06 11:34:52 -0800 |
commit | cac3967b52ae44fae3962ee9eba456221e0efda3 (patch) | |
tree | 47711960bec18836ec61ac30f1cd7dcd8d999483 /src/sat/satoko/watch_list.h | |
parent | aed9a87282bcb7937fd74e078d30ed74786abc75 (diff) | |
download | abc-cac3967b52ae44fae3962ee9eba456221e0efda3.tar.gz abc-cac3967b52ae44fae3962ee9eba456221e0efda3.tar.bz2 abc-cac3967b52ae44fae3962ee9eba456221e0efda3.zip |
Adding a new SAT solver to ABC. (Satoko)
The command is ‘satoko’
Diffstat (limited to 'src/sat/satoko/watch_list.h')
-rw-r--r-- | src/sat/satoko/watch_list.h | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h new file mode 100644 index 00000000..f492904a --- /dev/null +++ b/src/sat/satoko/watch_list.h @@ -0,0 +1,152 @@ +//===--- watch_list.h -------------------------------------------------------=== +// +// satoko: Satisfiability solver +// +// This file is distributed under the BSD 2-Clause License. +// See LICENSE for details. +// +//===------------------------------------------------------------------------=== +#ifndef satoko__watch_list_h +#define satoko__watch_list_h + +#include "utils/mem.h" + +#include "misc/util/abc_global.h" +ABC_NAMESPACE_HEADER_START + +struct watcher { + unsigned cref; + unsigned blocker; +}; + +struct watch_list { + unsigned cap; + unsigned size; + struct watcher *watchers; +}; + +typedef struct vec_wl_t_ vec_wl_t; +struct vec_wl_t_ { + unsigned cap; + unsigned size; + struct watch_list *watch_lists; +}; + +//===------------------------------------------------------------------------=== +// Watch list Macros +//===------------------------------------------------------------------------=== +#define watch_list_foreach(vec, watch, lit) \ + for (watch = watch_list_array(vec_wl_at(vec, lit)); \ + watch < watch_list_array(vec_wl_at(vec, lit)) + watch_list_size(vec_wl_at(vec, lit)); \ + watch++) + +//===------------------------------------------------------------------------=== +// Watch list API +//===------------------------------------------------------------------------=== +static inline void watch_list_free(struct watch_list *wl) +{ + if (wl->watchers) + satoko_free(wl->watchers); +} + +static inline unsigned watch_list_size(struct watch_list *wl) +{ + return wl->size; +} + +static inline void watch_list_shrink(struct watch_list *wl, unsigned size) +{ + assert(size <= wl->size); + wl->size = size; +} + +static inline void watch_list_push(struct watch_list *wl, struct watcher w) +{ + 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; + } + wl->watchers[wl->size++] = w; +} + +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) +{ + struct watcher *watchers = watch_list_array(wl); + unsigned i; + for (i = 0; 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)); + wl->size -= 1; +} + +static inline vec_wl_t *vec_wl_alloc(unsigned cap) +{ + vec_wl_t *vec_wl = satoko_alloc(vec_wl_t, 1); + + if (cap == 0) + vec_wl->cap = 4; + else + vec_wl->cap = cap; + vec_wl->size = 0; + vec_wl->watch_lists = satoko_calloc( + struct watch_list, sizeof(struct watch_list) * vec_wl->cap); + return vec_wl; +} + +static inline void vec_wl_free(vec_wl_t *vec_wl) +{ + for (unsigned i = 0; i < vec_wl->size; i++) + watch_list_free(vec_wl->watch_lists + i); + satoko_free(vec_wl->watch_lists); + satoko_free(vec_wl); +} + +static inline void vec_wl_push(vec_wl_t *vec_wl) +{ + if (vec_wl->size == vec_wl->cap) { + unsigned new_size = + (vec_wl->cap < 4) ? vec_wl->cap * 2 : (vec_wl->cap / 2) * 3; + + vec_wl->watch_lists = satoko_realloc( + struct watch_list, vec_wl->watch_lists, new_size); + memset(vec_wl->watch_lists + vec_wl->cap, 0, + sizeof(struct watch_list) * (new_size - vec_wl->cap)); + if (vec_wl->watch_lists == NULL) { + printf("failed to realloc memory from %.1f mb to %.1f " + "mb.\n", + 1.0 * vec_wl->cap / (1 << 20), + 1.0 * new_size / (1 << 20)); + fflush(stdout); + } + vec_wl->cap = new_size; + } + vec_wl->size++; +} + +static inline struct watch_list *vec_wl_at(vec_wl_t *vec_wl, unsigned idx) +{ + assert(idx < vec_wl->cap); + assert(idx < vec_wl->size); + return vec_wl->watch_lists + idx; +} + +ABC_NAMESPACE_HEADER_END +#endif /* satoko__watch_list_h */ |