blob: 32b0bf93bf8329cde2c3a8e15dbec099f264eaf2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
//===--- cdb.h --------------------------------------------------------------===
//
// satoko: Satisfiability solver
//
// This file is distributed under the BSD 2-Clause License.
// See LICENSE for details.
//
//===------------------------------------------------------------------------===
#ifndef satoko__cdb_h
#define satoko__cdb_h
#include "clause.h"
#include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
/* Clauses DB data structure */
struct cdb {
unsigned size;
unsigned cap;
unsigned wasted;
unsigned *data;
};
//===------------------------------------------------------------------------===
// Clause DB API
//===------------------------------------------------------------------------===
static inline struct clause *cdb_handler(struct cdb *p, unsigned cref)
{
return cref != 0xFFFFFFFF ? (struct clause *)(p->data + cref) : NULL;
}
static inline unsigned cdb_cref(struct cdb *p, unsigned *clause)
{
return (unsigned)(clause - &(p->data[0]));
}
static inline void cdb_grow(struct cdb *p, unsigned cap)
{
unsigned prev_cap = p->cap;
if (p->cap >= cap)
return;
while (p->cap < cap) {
unsigned delta = ((p->cap >> 1) + (p->cap >> 3) + 2) & (unsigned)(~1);
p->cap += delta;
assert(p->cap >= prev_cap);
}
assert(p->cap > 0);
p->data = satoko_realloc(unsigned, p->data, p->cap);
}
static inline struct cdb *cdb_alloc(unsigned cap)
{
struct cdb *p = satoko_calloc(struct cdb, 1);
if (cap <= 0)
cap = 1024 * 1024;
cdb_grow(p, cap);
return p;
}
static inline void cdb_free(struct cdb *p)
{
satoko_free(p->data);
satoko_free(p);
}
static inline unsigned cdb_append(struct cdb *p, unsigned size)
{
unsigned prev_size;
assert(size > 0);
cdb_grow(p, p->size + size);
prev_size = p->size;
p->size += size;
assert(p->size > prev_size);
return prev_size;
}
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;
}
static inline unsigned cdb_size(struct cdb *p)
{
return p->size;
}
static inline unsigned cdb_wasted(struct cdb *p)
{
return p->wasted;
}
ABC_NAMESPACE_HEADER_END
#endif /* satoko__cdb_h */
|
