1 // *********************************************************************
2 // Copyright 2000-2004, Princeton University. All rights reserved.
3 // By using this software the USER indicates that he or she has read,
4 // understood and will comply with the following:
6 // --- Princeton University hereby grants USER nonexclusive permission
7 // to use, copy and/or modify this software for internal, noncommercial,
8 // research purposes only. Any distribution, including commercial sale
9 // or license, of this software, copies of the software, its associated
10 // documentation and/or modifications of either is strictly prohibited
11 // without the prior consent of Princeton University. Title to copyright
12 // to this software and its associated documentation shall at all times
13 // remain with Princeton University. Appropriate copyright notice shall
14 // be placed on all software copies, and a complete copy of this notice
15 // shall be included in all copies of the associated documentation.
16 // No right is granted to use in advertising, publicity or otherwise
17 // any trademark, service mark, or the name of Princeton University.
20 // --- This software and any associated documentation is provided "as is"
22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
24 // PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR
25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
28 // Princeton University shall not be liable under any circumstances for
29 // any direct, indirect, special, incidental, or consequential damages
30 // with respect to any claim by USER or any third party on account of
31 // or arising from the use, or inability to use, this software or its
32 // associated documentation, even if Princeton University has been advised
33 // of the possibility of those damages.
34 // ********************************************************************/
42 #include "zchaff_dbase.h"
44 CDatabase::CDatabase(void) {
45 _stats.mem_used_up = false;
46 _stats.init_num_clauses = 0;
47 _stats.init_num_literals = 0;
48 _stats.num_added_clauses = 0;
49 _stats.num_added_literals = 0;
50 _stats.num_deleted_clauses = 0;
51 _stats.num_del_orig_cls = 0;
52 _stats.num_deleted_literals = 0;
53 _stats.num_enlarge = 0;
54 _stats.num_compact = 0;
55 _lit_pool_start = (CLitPoolElement *) malloc(sizeof(CLitPoolElement) *
56 STARTUP_LIT_POOL_SIZE);
57 _lit_pool_finish = _lit_pool_start;
58 _lit_pool_end_storage = _lit_pool_start + STARTUP_LIT_POOL_SIZE;
59 lit_pool_push_back(0); // set the first element as a dummy element
60 _params.mem_limit = 1024 * 1024 * 1024; // that's 1 G
61 variables()->resize(1); // var_id == 0 is never used.
65 CDatabase::~CDatabase(void) {
66 free(_lit_pool_start);
69 unsigned CDatabase::estimate_mem_usage(void) {
70 unsigned mem_lit_pool = sizeof(CLitPoolElement) * (lit_pool_size() +
71 lit_pool_free_space());
72 unsigned mem_vars = sizeof(CVariable) * variables()->capacity();
73 unsigned mem_cls = sizeof(CClause) * clauses()->capacity();
74 unsigned mem_cls_queue = sizeof(int) * _unused_clause_idx.size();
75 unsigned mem_watched = 2 * num_clauses() * sizeof(CLitPoolElement *);
76 unsigned mem_lit_clauses = 0;
77 #ifdef KEEP_LIT_CLAUSES
78 mem_lit_clauses = num_literals() * sizeof(ClauseIdx);
80 return (mem_lit_pool + mem_vars + mem_cls +
81 mem_cls_queue + mem_watched + mem_lit_clauses);
84 unsigned CDatabase::mem_usage(void) {
85 int mem_lit_pool = (lit_pool_size() + lit_pool_free_space()) *
86 sizeof(CLitPoolElement);
87 int mem_vars = sizeof(CVariable) * variables()->capacity();
88 int mem_cls = sizeof(CClause) * clauses()->capacity();
89 int mem_cls_queue = sizeof(int) * _unused_clause_idx.size();
90 int mem_watched = 0, mem_lit_clauses = 0;
91 for (unsigned i = 0, sz = variables()->size(); i < sz ; ++i) {
92 CVariable & v = variable(i);
93 mem_watched += v.watched(0).capacity() + v.watched(1).capacity();
94 #ifdef KEEP_LIT_CLAUSES
95 mem_lit_clauses += v.lit_clause(0).capacity() + v.lit_clause(1).capacity();
98 mem_watched *= sizeof(CLitPoolElement*);
99 mem_lit_clauses *= sizeof(ClauseIdx);
100 return (mem_lit_pool + mem_vars + mem_cls +
101 mem_cls_queue + mem_watched + mem_lit_clauses);
104 int CDatabase::alloc_gid(void) {
105 for (unsigned i = 1; i <= WORD_WIDTH; ++i) {
106 if (is_gid_allocated(i) == false) {
107 _allocated_gid |= (1 << (i-1));
111 warning(_POSITION_, "Not enough GID");
115 void CDatabase::free_gid(int gid) {
116 assert(gid > 0 && "Can't free volatile or permanent group");
117 assert(gid <= WORD_WIDTH && "gid > WORD_WIDTH?");
118 if (!is_gid_allocated(gid)) {
119 fatal(_POSITION_, "Can't free unallocated GID");
121 _allocated_gid &= (~(1<< (gid-1)));
124 bool CDatabase::is_gid_allocated(int gid) {
125 if (gid == VOLATILE_GID || gid == PERMANENT_GID)
127 assert(gid <= WORD_WIDTH && gid > 0);
128 if (_allocated_gid & (1 << (gid -1)))
133 int CDatabase::merge_clause_group(int g2, int g1) {
134 assert(g1 >0 && g2> 0 && "Can't merge with permanent or volatile group");
136 assert(is_gid_allocated(g1) && is_gid_allocated(g2));
137 for (unsigned i = 0, sz = clauses()->size(); i < sz; ++i) {
138 if (clause(i).status() != DELETED_CL) {
139 if (clause(i).gid(g1) == true) {
140 clause(i).clear_gid(g1);
141 clause(i).set_gid(g2);
149 void CDatabase::mark_clause_deleted(CClause & cl) {
150 ++_stats.num_deleted_clauses;
151 _stats.num_deleted_literals += cl.num_lits();
152 CLAUSE_STATUS status = cl.status();
153 if (status == ORIGINAL_CL)
154 _stats.num_del_orig_cls++;
155 cl.set_status(DELETED_CL);
156 for (unsigned i = 0; i < cl.num_lits(); ++i) {
157 CLitPoolElement & l = cl.literal(i);
158 --variable(l.var_index()).lits_count(l.var_sign());
161 _unused_clause_idx.insert(&cl - &(*clauses()->begin()));
164 bool CDatabase::is_conflicting(ClauseIdx cl) {
165 CLitPoolElement * lits = clause(cl).literals();
166 for (int i = 0, sz= clause(cl).num_lits(); i < sz; ++i) {
167 if (literal_value(lits[i]) != 0)
173 bool CDatabase::is_satisfied(ClauseIdx cl) {
174 CLitPoolElement * lits = clause(cl).literals();
175 for (int i = 0, sz = clause(cl).num_lits(); i < sz; ++i) {
176 if (literal_value(lits[i]) == 1)
182 bool CDatabase::is_unit(ClauseIdx cl) {
183 int num_unassigned = 0;
184 CLitPoolElement * lits = clause(cl).literals();
185 for (unsigned i = 0, sz= clause(cl).num_lits(); i < sz; ++i) {
186 int value = literal_value(lits[i]);
192 return num_unassigned == 1;
195 int CDatabase::find_unit_literal(ClauseIdx cl) {
196 // will return 0 if not unit
198 for (int i = 0, sz = clause(cl).num_lits(); i < sz; ++i) {
199 int value = literal_value(clause(cl).literal(i));
202 else if (value != 0) {
204 unit_lit = clause(cl).literals()[i].s_var();
212 inline CLitPoolElement * CDatabase::lit_pool_begin(void) {
213 return _lit_pool_start;
216 inline CLitPoolElement * CDatabase::lit_pool_end(void) {
217 return _lit_pool_finish;
220 inline void CDatabase::lit_pool_incr_size(int size) {
221 _lit_pool_finish += size;
222 assert(_lit_pool_finish <= _lit_pool_end_storage);
225 inline void CDatabase::lit_pool_push_back(int value) {
226 assert(_lit_pool_finish <= _lit_pool_end_storage);
227 _lit_pool_finish->val() = value;
231 inline int CDatabase::lit_pool_size(void) {
232 return _lit_pool_finish - _lit_pool_start;
235 inline int CDatabase::lit_pool_free_space(void) {
236 return _lit_pool_end_storage - _lit_pool_finish;
239 inline double CDatabase::lit_pool_utilization(void) {
240 // minus num_clauses() is because of spacing (i.e. clause indices)
241 return (double)num_literals() / ((double) (lit_pool_size() - num_clauses())) ;
244 inline CLitPoolElement & CDatabase::lit_pool(int i) {
245 return _lit_pool_start[i];
248 void CDatabase::compact_lit_pool(void) {
251 // first do the compaction for the lit pool
252 for (i = 1, sz = lit_pool_size(); i < sz; ++i) {
253 // begin with 1 because 0 position is always 0
254 if (!lit_pool(i).is_literal() && !lit_pool(i-1).is_literal()) {
257 lit_pool(new_index) = lit_pool(i);
261 _lit_pool_finish = lit_pool_begin() + new_index;
262 // update all the pointers to the literals;
263 // 1. clean up the watched pointers from variables
264 for (i = 1, sz = variables()->size(); i < sz; ++i) {
265 variable(i).watched(0).clear();
266 variable(i).watched(1).clear();
268 for (i = 1, sz = lit_pool_size(); i < sz; ++i) {
269 CLitPoolElement & lit = lit_pool(i);
270 // 2. reinsert the watched pointers
271 if (lit.is_literal()) {
272 if (lit.is_watched()) {
273 int var_idx = lit.var_index();
274 int sign = lit.var_sign();
275 variable(var_idx).watched(sign).push_back(& lit_pool(i));
277 } else { // lit is not literal
278 // 3. update the clauses' first literal pointer
279 int cls_idx = lit.get_clause_index();
280 clause(cls_idx).first_lit() = &lit_pool(i) - clause(cls_idx).num_lits();
283 ++_stats.num_compact;
286 bool CDatabase::enlarge_lit_pool(void) {
287 // will return true if successful, otherwise false.
289 // if memory efficiency < 2/3, we do a compaction
290 if (lit_pool_utilization() < 0.67) {
294 // otherwise we have to enlarge it.
295 // first, check if memory is running out
296 int current_mem = estimate_mem_usage();
297 float grow_ratio = 1;
298 if (current_mem < _params.mem_limit / 4)
300 else if (current_mem < _params.mem_limit /2 )
302 else if (current_mem < _params.mem_limit * 0.8)
304 if (grow_ratio < 1.2) {
305 if (lit_pool_utilization() < 0.9) { // still has some garbage
312 // second, make room for new lit pool.
313 CLitPoolElement * old_start = _lit_pool_start;
314 CLitPoolElement * old_finish = _lit_pool_finish;
315 int old_size = _lit_pool_end_storage - _lit_pool_start;
316 int new_size = (int)(old_size * grow_ratio);
317 _lit_pool_start = (CLitPoolElement *) realloc(_lit_pool_start,
318 sizeof(CLitPoolElement) *
320 _lit_pool_finish = _lit_pool_start + (old_finish - old_start);
321 _lit_pool_end_storage = _lit_pool_start + new_size;
323 // update all the pointers
324 long long displacement = _lit_pool_start - old_start;
325 for (i = 0; i < clauses()->size(); ++i) {
326 if (clause(i).status() != DELETED_CL)
327 clause(i).first_lit() += displacement;
329 for (i = 0, sz = variables()->size(); i < sz ; ++i) {
330 CVariable & v = variable(i);
331 for (int j = 0; j < 2 ; ++j) {
333 vector<CLitPoolElement *> & watched = v.watched(j);
334 for (k = 0, sz1 = watched.size(); k < sz1 ; ++k) {
335 watched[k] += displacement;
339 ++_stats.num_enlarge;
343 ClauseIdx CDatabase::get_free_clause_idx(void) {
345 new_cl = _clauses.size();
346 _clauses.resize(new_cl + 1);
347 clause(new_cl).set_id(_stats.num_added_clauses);
351 ClauseIdx CDatabase::add_clause(int * lits, int n_lits, int gflag) {
353 // a. do we need to enlarge lits pool?
354 while (lit_pool_free_space() <= n_lits + 1) {
355 if (enlarge_lit_pool() == false)
356 return -1; // mem out, can't enlarge lit pool, because
357 // ClauseIdx can't be -1, so it shows error.
359 // b. get a free cl index;
360 new_cl = get_free_clause_idx();
361 // c. add the clause lits to lits pool
362 CClause & cl = clause(new_cl);
363 cl.init(lit_pool_end(), n_lits, gflag);
364 lit_pool_incr_size(n_lits + 1);
366 ++variable(lits[0]>>1).two_lits_count(lits[0] & 0x1);
367 ++variable(lits[1]>>1).two_lits_count(lits[1] & 0x1);
369 for (int i = 0; i < n_lits; ++i) {
370 int var_idx = lits[i] >> 1;
371 assert((unsigned)var_idx < variables()->size());
372 int var_sign = lits[i] & 0x1;
373 cl.literal(i).set(var_idx, var_sign);
374 ++variable(var_idx).lits_count(var_sign);
375 #ifdef KEEP_LIT_CLAUSES
376 variable(var_idx).lit_clause(var_sign).push_back(new_cl);
379 // the element after the last one is the spacing element
380 cl.literal(n_lits).set_clause_index(new_cl);
381 // d. set the watched pointers
382 if (cl.num_lits() > 1) {
383 // add the watched literal. note: watched literal must be the last free var
384 int max_idx = -1, max_dl = -1;
385 int i, sz = cl.num_lits();
386 // set the first watched literal
387 for (i = 0; i < sz; ++i) {
388 int v_idx = cl.literal(i).var_index();
389 int v_sign = cl.literal(i).var_sign();
390 CVariable & v = variable(v_idx);
391 if (literal_value(cl.literal(i)) != 0) {
392 v.watched(v_sign).push_back(&cl.literal(i));
393 cl.literal(i).set_watch(1);
396 if (v.dlevel() > max_dl) {
402 if (i >= sz) { // no unassigned literal. so watch literal with max dlevel
403 int v_idx = cl.literal(max_idx).var_index();
404 int v_sign = cl.literal(max_idx).var_sign();
405 variable(v_idx).watched(v_sign).push_back(&cl.literal(max_idx));
406 cl.literal(max_idx).set_watch(1);
409 // set the second watched literal
412 for (i = sz-1; i >= 0; --i) {
413 if (cl.literal(i).is_watched())
414 continue; // need to watch two different literals
415 int v_idx = cl.literal(i).var_index();
416 int v_sign = cl.literal(i).var_sign();
417 CVariable & v = variable(v_idx);
418 if (literal_value(cl.literal(i)) != 0) {
419 v.watched(v_sign).push_back(&cl.literal(i));
420 cl.literal(i).set_watch(-1);
423 if (v.dlevel() > max_dl) {
430 int v_idx = cl.literal(max_idx).var_index();
431 int v_sign = cl.literal(max_idx).var_sign();
432 variable(v_idx).watched(v_sign).push_back(&cl.literal(max_idx));
433 cl.literal(max_idx).set_watch(-1);
436 // update some statistics
437 ++_stats.num_added_clauses;
438 _stats.num_added_literals += n_lits;
442 void CDatabase::output_lit_pool_stats(void) {
443 cout << "Lit_Pool Used " << lit_pool_size() << " Free "
444 << lit_pool_free_space()
445 << " Total " << lit_pool_size() + lit_pool_free_space()
446 << " Num. Cl " << num_clauses() << " Num. Lit " << num_literals()
447 << " Efficiency " << lit_pool_utilization() << endl;
450 void CDatabase::detail_dump_cl(ClauseIdx cl_idx, ostream & os) {
451 os << "CL : " << cl_idx;
452 CClause & cl = clause(cl_idx);
453 if (cl.status() == DELETED_CL)
454 os << "\t\t\t======removed=====";
456 for (unsigned i = 0; i < cl.num_lits(); ++i) {
457 if (literal_value(cl.literal(i)) == 0)
459 else if (literal_value(cl.literal(i)) == 1)
463 os << cl.literal(i) << "(" << value << "@"
464 << variable(cl.literal(i).var_index()).dlevel()<< ") ";
469 void CDatabase::dump(ostream & os) {
471 os << "Dump Database: " << endl;
472 for (i = 0; i < _clauses.size(); ++i)
474 for (i = 1; i < _variables.size(); ++i)
475 os << "VID " << i << ":\t" << variable(i);