1 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */
2
3 /*********************************************************************
4 Copyright 2000-2001, Princeton University. All rights reserved.
5 By using this software the USER indicates that he or she has read,
6 understood and will comply with the following:
7
8 --- Princeton University hereby grants USER nonexclusive permission
9 to use, copy and/or modify this software for internal, noncommercial,
10 research purposes only. Any distribution, including commercial sale
11 or license, of this software, copies of the software, its associated
12 documentation and/or modifications of either is strictly prohibited
13 without the prior consent of Princeton University. Title to copyright
14 to this software and its associated documentation shall at all times
15 remain with Princeton University. Appropriate copyright notice shall
16 be placed on all software copies, and a complete copy of this notice
17 shall be included in all copies of the associated documentation.
18 No right is granted to use in advertising, publicity or otherwise
19 any trademark, service mark, or the name of Princeton University.
20
21
22 --- This software and any associated documentation is provided "as is"
23
24 PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
25 OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
26 PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR
27 ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
28 TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
29
30 Princeton University shall not be liable under any circumstances for
31 any direct, indirect, special, incidental, or consequential damages
32 with respect to any claim by USER or any third party on account of
33 or arising from the use, or inability to use, this software or its
34 associated documentation, even if Princeton University has been advised
35 of the possibility of those damages.
36 *********************************************************************/
37
38 #include "xchaff_utils.h"
39 #include "xchaff_dbase.h"
40
CDatabase()41 CDatabase::CDatabase() : _variables(1)
42 {
43 _stats.mem_used_up_counts = 0;
44 _stats.mem_used_up = false;
45
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_deleted_literals = 0;
52
53 _lit_pool_start = new CLitPoolElement[STARTUP_LIT_POOL_SIZE];
54 _lit_pool_finish = _lit_pool_start;
55 _lit_pool_end_storage = _lit_pool_start + STARTUP_LIT_POOL_SIZE;
56 lit_pool_push_back(0); //set the first element as a spacing element
57
58 _mem_limit = 1024*1024*512; //that's 0.5 G
59 }
60
61
compact_lit_pool(void)62 void CDatabase::compact_lit_pool(void)
63 {
64 CHECK(cout << "Begin Compaction " << endl;);
65 int new_index = 1;
66 for (int i=1; i< lit_pool_size(); ++i){ //begin with 1 because 0 position is always 0
67 if (lit_pool(i).val()<=0 && lit_pool(i-1).val()<=0)
68 continue;
69 else {
70 lit_pool(new_index) = lit_pool(i);
71 ++new_index;
72 }
73 }
74 _lit_pool_finish = lit_pool_begin() + new_index;
75 //update all the pointers of the clauses;
76 //1. clean up the pt pointers from variables
77 for (unsigned i=1; i<variables().size(); ++i) {
78 variable(i).ht_ptr(0).clear();
79 variable(i).ht_ptr(1).clear();
80 }
81 //2. reinsert the ht_pointers
82 for (int i=1; i< lit_pool_size(); ++i) {
83 if (lit_pool(i).val() > 0 && lit_pool(i).is_ht()) {
84 int var_idx = lit_pool(i).var_index();
85 int sign = lit_pool(i).var_sign();
86 variable(var_idx).ht_ptr(sign).push_back(& lit_pool(i));
87 }
88 }
89 //3. update the clauses' first literal pointer
90 for (int i=1; i< lit_pool_size(); ++i) {
91 if (lit_pool(i).val() <= 0) {
92 int cls_idx = -lit_pool(i).val();
93 clause(cls_idx).first_lit() = &lit_pool(i) - clause(cls_idx).num_lits();
94 }
95 }
96 CHECK(output_lit_pool_state();
97 cout << endl << endl;);
98 }
99
enlarge_lit_pool(void)100 bool CDatabase::enlarge_lit_pool(void) //will return true if successful, otherwise false.
101 {
102 CHECK (output_lit_pool_state());
103 if (lit_pool_size() - num_clauses() > num_literals() * 2) {
104 //memory fragmented. ratio of efficiency < 0.5
105 //minus num_clauses() is because of spacing for
106 //each clause in lit_pool
107 compact_lit_pool();
108 return true;
109 }
110 CHECK(cout << "Begin Enlarge Lit Pool" << endl;);
111
112 //otherwise we have to enlarge it.
113 //first, check if memory is running out
114 int current_mem = estimate_mem_usage();
115 float grow_ratio;
116 if (current_mem < _mem_limit /2 ) {
117 grow_ratio = 2;
118 }
119 else if (current_mem < _mem_limit * 0.8) {
120 grow_ratio = 1.2;
121 }
122 else {
123 _stats.mem_used_up = true;
124 if (lit_pool_size() - num_clauses() > num_literals() * 1.1) {
125 compact_lit_pool();
126 return true;
127 }
128 else
129 return false;
130 }
131 //second, make room for new lit pool.
132 CLitPoolElement * old_start = _lit_pool_start;
133 CLitPoolElement * old_finish = _lit_pool_finish;
134 int old_size = _lit_pool_end_storage - _lit_pool_start;
135 int new_size = (int)(old_size * grow_ratio);
136 _lit_pool_start = new CLitPoolElement[new_size];
137 _lit_pool_finish = _lit_pool_start;
138 _lit_pool_end_storage = _lit_pool_start + new_size;
139 //copy the old content into new place
140 for (CLitPoolElement * ptr = old_start; ptr != old_finish; ++ptr) {
141 *_lit_pool_finish = *ptr;
142 _lit_pool_finish ++;
143 }
144 //update all the pointers
145 long displacement = _lit_pool_start - old_start;
146 for (unsigned i=0; i< clauses().size(); ++i)
147 if (clause(i).in_use())
148 clause(i).first_lit() += displacement;
149
150 for (unsigned i=0; i< variables().size(); ++i) {
151 CVariable & v = variable(i);
152 for (int j=0; j< 2 ; ++j) {
153 vector<CLitPoolElement *> & ht_ptr = v.ht_ptr(j);
154 for (unsigned k=0; k< ht_ptr.size(); ++k) {
155 ht_ptr[k] += displacement;
156 }
157 }
158 }
159 //free old space
160 delete [] old_start;
161 CHECK(output_lit_pool_state());
162 CHECK(cout << endl << endl);
163 return true;
164 }
165
166
output_lit_pool_state(void)167 void CDatabase::output_lit_pool_state (void)
168 {
169 cout << "Lit_Pool Used " << lit_pool_size() << " Free " << lit_pool_free_space()
170 << " Total " << lit_pool_size() + lit_pool_free_space()
171 << " Num. Cl " << num_clauses() << " Num. Lit " << num_literals();
172 cout << " Efficiency " << (float)((float)num_literals()) / (float)((lit_pool_size() - num_clauses())) << endl;
173 }
174
175
detail_dump_cl(ClauseIdx cl_idx,ostream & os)176 void CDatabase::detail_dump_cl(ClauseIdx cl_idx, ostream & os) {
177 os << "Clause : " << cl_idx;
178 CClause & cl = clause(cl_idx);
179 if (!cl.in_use())
180 os << "\t\t\t======removed=====";
181 const char * value;
182 int i, sz;
183 sz = cl.num_lits();
184 if (cl.num_lits() < 0) {
185 os << ">> " ;
186 sz = -sz;
187 }
188 for (i=0; i<sz; ++i) {
189 if (literal_value(cl.literals()[i])==0) value = "0";
190 else if (literal_value(cl.literals()[i])==1) value = "1";
191 else value = "X";
192 os << cl.literals()[i] << "(" << value << "@" << variable(cl.literal(i).var_index()).dlevel()<< ") ";
193 }
194 os << endl;
195 }
196
dump(ostream & os)197 void CDatabase::dump(ostream & os) {
198 os << "Dump Database: " << endl;
199 for(unsigned i=0; i<_clauses.size(); ++i)
200 detail_dump_cl(i);
201 // os << "Cl: " << i << " " << clause(i) << endl;
202 for(unsigned i=1; i<_variables.size(); ++i)
203 os << "VID: " << i << "\t" << variable(i);
204 }
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225