45 #define STARTUP_LIT_POOL_SIZE 0x1000
49 return (a.first==b.first && a.second == b.second);
55 return (a.first + (a.second << 16));
178 int mem_cls =
sizeof(
CClause) *
180 int mem_cls_queue =
sizeof(int) *
182 int mem_ht_ptrs =0, mem_lit_clauses = 0;
185 return (lit_pool + mem_vars + mem_cls +
186 mem_cls_queue + mem_ht_ptrs + mem_lit_clauses);
193 int mem_ht_ptrs = 0, mem_lit_clauses = 0;
194 for (
unsigned i=0; i<
variables().size(); ++i) {
196 mem_ht_ptrs += v.
ht_ptr(0).capacity() + v.
ht_ptr(1).capacity();
200 return (lit_pool + mem_vars + mem_cls +
201 mem_cls_queue + mem_ht_ptrs + mem_lit_clauses);
225 for (
int i=0; i< cl.
num_lits(); ++i) {
232 if (
variable(v_idx).in_new_cl() == -1 && phase != -1)
234 else if (
variable(v_idx).in_new_cl() != -1 && phase == -1)
236 else assert (0 &&
"How can this happen? ");
252 void dump(ostream & os = cout);