CVC3
xchaff_dbase.cpp
Go to the documentation of this file.
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 
41 CDatabase::CDatabase() : _variables(1)
42 {
44  _stats.mem_used_up = false;
45 
52 
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 
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  }
97  cout << endl << endl;);
98 }
99 
100 bool CDatabase::enlarge_lit_pool(void) //will return true if successful, otherwise false.
101 {
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
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) {
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];
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;
162  CHECK(cout << endl << endl);
163  return true;
164 }
165 
166 
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 
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 
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