1 //===--- watch_list.h -------------------------------------------------------===
2 //
3 // satoko: Satisfiability solver
4 //
5 // This file is distributed under the BSD 2-Clause License.
6 // See LICENSE for details.
7 //
8 //===------------------------------------------------------------------------===
9 #ifndef satoko__watch_list_h
10 #define satoko__watch_list_h
11
12 #include "utils/mem.h"
13 #include "utils/misc.h"
14
15 #include "misc/util/abc_global.h"
16 ABC_NAMESPACE_HEADER_START
17
18 struct watcher {
19 unsigned cref;
20 unsigned blocker;
21 };
22
23 struct watch_list {
24 unsigned cap;
25 unsigned size;
26 unsigned n_bin;
27 struct watcher *watchers;
28 };
29
30 typedef struct vec_wl_t_ vec_wl_t;
31 struct vec_wl_t_ {
32 unsigned cap;
33 unsigned size;
34 struct watch_list *watch_lists;
35 };
36
37 //===------------------------------------------------------------------------===
38 // Watch list Macros
39 //===------------------------------------------------------------------------===
40 #define watch_list_foreach(vec, watch, lit) \
41 for (watch = watch_list_array(vec_wl_at(vec, lit)); \
42 watch < watch_list_array(vec_wl_at(vec, lit)) + watch_list_size(vec_wl_at(vec, lit)); \
43 watch++)
44
45 #define watch_list_foreach_bin(vec, watch, lit) \
46 for (watch = watch_list_array(vec_wl_at(vec, lit)); \
47 watch < watch_list_array(vec_wl_at(vec, lit)) + vec_wl_at(vec, lit)->n_bin; \
48 watch++)
49 //===------------------------------------------------------------------------===
50 // Watch list API
51 //===------------------------------------------------------------------------===
watch_list_free(struct watch_list * wl)52 static inline void watch_list_free(struct watch_list *wl)
53 {
54 if (wl->watchers)
55 satoko_free(wl->watchers);
56 }
57
watch_list_size(struct watch_list * wl)58 static inline unsigned watch_list_size(struct watch_list *wl)
59 {
60 return wl->size;
61 }
62
watch_list_shrink(struct watch_list * wl,unsigned size)63 static inline void watch_list_shrink(struct watch_list *wl, unsigned size)
64 {
65 assert(size <= wl->size);
66 wl->size = size;
67 }
68
watch_list_grow(struct watch_list * wl)69 static inline void watch_list_grow(struct watch_list *wl)
70 {
71 unsigned new_size = (wl->cap < 4) ? 4 : (wl->cap / 2) * 3;
72 struct watcher *watchers =
73 satoko_realloc(struct watcher, wl->watchers, new_size);
74 if (watchers == NULL) {
75 printf("Failed to realloc memory from %.1f MB to %.1f "
76 "MB.\n",
77 1.0 * wl->cap / (1 << 20),
78 1.0 * new_size / (1 << 20));
79 fflush(stdout);
80 return;
81 }
82 wl->watchers = watchers;
83 wl->cap = new_size;
84 }
85
watch_list_push(struct watch_list * wl,struct watcher w,unsigned is_bin)86 static inline void watch_list_push(struct watch_list *wl, struct watcher w, unsigned is_bin)
87 {
88 assert(wl);
89 if (wl->size == wl->cap)
90 watch_list_grow(wl);
91 wl->watchers[wl->size++] = w;
92 if (is_bin && wl->size > wl->n_bin) {
93 stk_swap(struct watcher, wl->watchers[wl->n_bin], wl->watchers[wl->size - 1]);
94 wl->n_bin++;
95 }
96 }
97
watch_list_array(struct watch_list * wl)98 static inline struct watcher *watch_list_array(struct watch_list *wl)
99 {
100 return wl->watchers;
101 }
102
103 /* TODO: I still have mixed feelings if this change should be done, keeping the
104 * old code commented after it. */
watch_list_remove(struct watch_list * wl,unsigned cref,unsigned is_bin)105 static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin)
106 {
107 struct watcher *watchers = watch_list_array(wl);
108 unsigned i;
109 if (is_bin) {
110 for (i = 0; watchers[i].cref != cref; i++);
111 assert(i < watch_list_size(wl));
112 wl->n_bin--;
113 memmove((wl->watchers + i), (wl->watchers + i + 1),
114 (wl->size - i - 1) * sizeof(struct watcher));
115 } else {
116 for (i = wl->n_bin; watchers[i].cref != cref; i++);
117 assert(i < watch_list_size(wl));
118 stk_swap(struct watcher, wl->watchers[i], wl->watchers[wl->size - 1]);
119 }
120 wl->size -= 1;
121 }
122
123 /*
124 static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin)
125 {
126 struct watcher *watchers = watch_list_array(wl);
127 unsigned i;
128 if (is_bin) {
129 for (i = 0; watchers[i].cref != cref; i++);
130 wl->n_bin--;
131 } else
132 for (i = wl->n_bin; watchers[i].cref != cref; i++);
133 assert(i < watch_list_size(wl));
134 memmove((wl->watchers + i), (wl->watchers + i + 1),
135 (wl->size - i - 1) * sizeof(struct watcher));
136 wl->size -= 1;
137 }
138 */
139
vec_wl_alloc(unsigned cap)140 static inline vec_wl_t *vec_wl_alloc(unsigned cap)
141 {
142 vec_wl_t *vec_wl = satoko_alloc(vec_wl_t, 1);
143
144 if (cap == 0)
145 vec_wl->cap = 4;
146 else
147 vec_wl->cap = cap;
148 vec_wl->size = 0;
149 vec_wl->watch_lists = satoko_calloc(
150 struct watch_list, sizeof(struct watch_list) * vec_wl->cap);
151 return vec_wl;
152 }
153
vec_wl_free(vec_wl_t * vec_wl)154 static inline void vec_wl_free(vec_wl_t *vec_wl)
155 {
156 unsigned i;
157 for (i = 0; i < vec_wl->cap; i++)
158 watch_list_free(vec_wl->watch_lists + i);
159 satoko_free(vec_wl->watch_lists);
160 satoko_free(vec_wl);
161 }
162
vec_wl_clean(vec_wl_t * vec_wl)163 static inline void vec_wl_clean(vec_wl_t *vec_wl)
164 {
165 unsigned i;
166 for (i = 0; i < vec_wl->size; i++) {
167 vec_wl->watch_lists[i].size = 0;
168 vec_wl->watch_lists[i].n_bin = 0;
169 }
170 vec_wl->size = 0;
171 }
172
vec_wl_push(vec_wl_t * vec_wl)173 static inline void vec_wl_push(vec_wl_t *vec_wl)
174 {
175 if (vec_wl->size == vec_wl->cap) {
176 unsigned new_size =
177 (vec_wl->cap < 4) ? vec_wl->cap * 2 : (vec_wl->cap / 2) * 3;
178
179 vec_wl->watch_lists = satoko_realloc(
180 struct watch_list, vec_wl->watch_lists, new_size);
181 memset(vec_wl->watch_lists + vec_wl->cap, 0,
182 sizeof(struct watch_list) * (new_size - vec_wl->cap));
183 if (vec_wl->watch_lists == NULL) {
184 printf("failed to realloc memory from %.1f mb to %.1f "
185 "mb.\n",
186 1.0 * vec_wl->cap / (1 << 20),
187 1.0 * new_size / (1 << 20));
188 fflush(stdout);
189 }
190 vec_wl->cap = new_size;
191 }
192 vec_wl->size++;
193 }
194
vec_wl_at(vec_wl_t * vec_wl,unsigned idx)195 static inline struct watch_list *vec_wl_at(vec_wl_t *vec_wl, unsigned idx)
196 {
197 assert(idx < vec_wl->cap);
198 assert(idx < vec_wl->size);
199 return vec_wl->watch_lists + idx;
200 }
201
202 ABC_NAMESPACE_HEADER_END
203 #endif /* satoko__watch_list_h */
204