ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
vec_sdbl.h
Go to the documentation of this file.
1//===--- vec_int.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__utils__vec__vec_sdbl_h
10#define satoko__utils__vec__vec_sdbl_h
11
12#include <assert.h>
13#include <stdio.h>
14#include <string.h>
15
16#include "../mem.h"
17#include "../sdbl.h"
18
21
22typedef struct vec_sdbl_t_ vec_sdbl_t;
24 unsigned cap;
25 unsigned size;
27};
28
29//===------------------------------------------------------------------------===
30// Vector Macros
31//===------------------------------------------------------------------------===
32#define vec_sdbl_foreach(vec, entry, i) \
33 for (i = 0; (i < vec->size) && (((entry) = vec_sdbl_at(vec, i)), 1); i++)
34
35#define vec_sdbl_foreach_start(vec, entry, i, start) \
36 for (i = start; (i < vec_sdbl_size(vec)) && (((entry) = vec_sdbl_at(vec, i)), 1); i++)
37
38#define vec_sdbl_foreach_stop(vec, entry, i, stop) \
39 for (i = 0; (i < stop) && (((entry) = vec_sdbl_at(vec, i)), 1); i++)
40
41//===------------------------------------------------------------------------===
42// Vector API
43//===------------------------------------------------------------------------===
44static inline vec_sdbl_t *vec_sdbl_alloc(unsigned cap)
45{
47
48 if (cap > 0 && cap < 16)
49 cap = 16;
50 p->size = 0;
51 p->cap = cap;
52 p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL;
53 return p;
54}
55
56static inline vec_sdbl_t *vec_sdbl_alloc_exact(unsigned cap)
57{
59
60 p->size = 0;
61 p->cap = cap;
62 p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL;
63 return p;
64}
65
66static inline vec_sdbl_t *vec_sdbl_init(unsigned size, sdbl_t value)
67{
69
70 p->cap = size;
71 p->size = size;
72 p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL;
73 memset(p->data, value, sizeof(sdbl_t) * p->size);
74 return p;
75}
76
77static inline void vec_sdbl_free(vec_sdbl_t *p)
78{
79 if (p->data != NULL)
80 satoko_free(p->data);
82}
83
84static inline unsigned vec_sdbl_size(vec_sdbl_t *p)
85{
86 return p->size;
87}
88
89static inline void vec_sdbl_shrink(vec_sdbl_t *p, unsigned new_size)
90{
91 assert(new_size <= p->cap);
92 p->size = new_size;
93}
94
95static inline void vec_sdbl_resize(vec_sdbl_t *p, unsigned new_size)
96{
97 p->size = new_size;
98 if (p->cap >= new_size)
99 return;
100 p->data = satoko_realloc(sdbl_t, p->data, new_size);
101 assert(p->data != NULL);
102 p->cap = new_size;
103}
104
105static inline void vec_sdbl_reserve(vec_sdbl_t *p, unsigned new_cap)
106{
107 if (p->cap >= new_cap)
108 return;
109 p->data = satoko_realloc(sdbl_t, p->data, new_cap);
110 assert(p->data != NULL);
111 p->cap = new_cap;
112}
113
114static inline unsigned vec_sdbl_capacity(vec_sdbl_t *p)
115{
116 return p->cap;
117}
118
119static inline int vec_sdbl_empty(vec_sdbl_t *p)
120{
121 return p->size ? 0 : 1;
122}
123
124static inline void vec_sdbl_erase(vec_sdbl_t *p)
125{
126 satoko_free(p->data);
127 p->size = 0;
128 p->cap = 0;
129}
130
131static inline sdbl_t vec_sdbl_at(vec_sdbl_t *p, unsigned i)
132{
133 assert(i >= 0 && i < p->size);
134 return p->data[i];
135}
136
137static inline sdbl_t *vec_sdbl_at_ptr(vec_sdbl_t *p, unsigned i)
138{
139 assert(i >= 0 && i < p->size);
140 return p->data + i;
141}
142
143static inline sdbl_t *vec_sdbl_data(vec_sdbl_t *p)
144{
145 assert(p);
146 return p->data;
147}
148
149static inline void vec_sdbl_duplicate(vec_sdbl_t *dest, const vec_sdbl_t *src)
150{
151 assert(dest != NULL && src != NULL);
152 vec_sdbl_resize(dest, src->cap);
153 memcpy(dest->data, src->data, sizeof(sdbl_t) * src->cap);
154 dest->size = src->size;
155}
156
157static inline void vec_sdbl_copy(vec_sdbl_t *dest, const vec_sdbl_t *src)
158{
159 assert(dest != NULL && src != NULL);
160 vec_sdbl_resize(dest, src->size);
161 memcpy(dest->data, src->data, sizeof(sdbl_t) * src->size);
162 dest->size = src->size;
163}
164
165static inline void vec_sdbl_push_back(vec_sdbl_t *p, sdbl_t value)
166{
167 if (p->size == p->cap) {
168 if (p->cap < 16)
169 vec_sdbl_reserve(p, 16);
170 else
171 vec_sdbl_reserve(p, 2 * p->cap);
172 }
173 p->data[p->size] = value;
174 p->size++;
175}
176
177static inline void vec_sdbl_assign(vec_sdbl_t *p, unsigned i, sdbl_t value)
178{
179 assert((i >= 0) && (i < vec_sdbl_size(p)));
180 p->data[i] = value;
181}
182
183static inline void vec_sdbl_insert(vec_sdbl_t *p, unsigned i, sdbl_t value)
184{
185 assert((i >= 0) && (i < vec_sdbl_size(p)));
186 vec_sdbl_push_back(p, 0);
187 memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(sdbl_t));
188 p->data[i] = value;
189}
190
191static inline void vec_sdbl_drop(vec_sdbl_t *p, unsigned i)
192{
193 assert((i >= 0) && (i < vec_sdbl_size(p)));
194 memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(sdbl_t));
195 p->size -= 1;
196}
197
198static inline void vec_sdbl_clear(vec_sdbl_t *p)
199{
200 p->size = 0;
201}
202
203static inline int vec_sdbl_asc_compare(const void *p1, const void *p2)
204{
205 const sdbl_t *pp1 = (const sdbl_t *) p1;
206 const sdbl_t *pp2 = (const sdbl_t *) p2;
207
208 if (*pp1 < *pp2)
209 return -1;
210 if (*pp1 > *pp2)
211 return 1;
212 return 0;
213}
214
215static inline int vec_sdbl_desc_compare(const void* p1, const void* p2)
216{
217 const sdbl_t *pp1 = (const sdbl_t *) p1;
218 const sdbl_t *pp2 = (const sdbl_t *) p2;
219
220 if (*pp1 > *pp2)
221 return -1;
222 if (*pp1 < *pp2)
223 return 1;
224 return 0;
225}
226
227static inline void vec_sdbl_sort(vec_sdbl_t* p, int ascending)
228{
229 if (ascending)
230 qsort((void *) p->data, (size_t)p->size, sizeof(sdbl_t),
231 (int (*)(const void*, const void*)) vec_sdbl_asc_compare);
232 else
233 qsort((void *) p->data, (size_t)p->size, sizeof(sdbl_t),
234 (int (*)(const void*, const void*)) vec_sdbl_desc_compare);
235}
236
237static inline long vec_sdbl_memory(vec_sdbl_t *p)
238{
239 return p == NULL ? 0 : sizeof(sdbl_t) * p->cap + sizeof(vec_sdbl_t);
240}
241
242static inline void vec_sdbl_print(vec_sdbl_t *p)
243{
244 unsigned i;
245 assert(p != NULL);
246 fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
247 for (i = 0; i < p->size; i++)
248 fprintf(stdout, " %f", sdbl2double(p->data[i]));
249 fprintf(stdout, " }\n");
250}
251
253#endif /* satoko__utils__vec__vec_sdbl_h */
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
ABC_NAMESPACE_IMPL_START typedef signed char value
Cube * p
Definition exorList.c:222
unsigned long long size
Definition giaNewBdd.h:39
#define satoko_free(p)
Definition mem.h:20
#define satoko_realloc(type, ptr, n_elements)
Definition mem.h:19
#define satoko_alloc(type, n_elements)
Definition mem.h:17
ABC_NAMESPACE_HEADER_START typedef word sdbl_t
Definition sdbl.h:32
unsigned size
Definition vec_sdbl.h:25
sdbl_t * data
Definition vec_sdbl.h:26
unsigned cap
Definition vec_sdbl.h:24
#define assert(ex)
Definition util_old.h:213
char * memcpy()
char * memset()
char * memmove()
typedefABC_NAMESPACE_HEADER_START struct vec_sdbl_t_ vec_sdbl_t
Definition vec_sdbl.h:22