CVC3  2.4.1
xchaff_dbase.h
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 
39 #ifndef __DATABASE__
40 #define __DATABASE__
41 
42 #include "xchaff_base.h"
43 #include <queue>
44 
45 #define STARTUP_LIT_POOL_SIZE 0x1000
46 
48  bool operator () (pair<int,int> a, pair<int,int> b) {
49  return (a.first==b.first && a.second == b.second);
50  }
51 };
52 
54  size_t operator () (const pair<int, int> a) const {
55  return (a.first + (a.second << 16));
56  }
57 };
58 
59 /**Struct**********************************************************************
60 
61  Synopsis [Definition of the statistics of clause database]
62 
63  Description []
64 
65  SeeAlso [CDatabase]
66 
67 ******************************************************************************/
68 
78 };
79 
80 /**Class**********************************************************************
81 
82  Synopsis [Definition of clause database ]
83 
84  Description [Clause Database is the place where the information of the
85  SAT problem are stored. it is a parent class of CSolver ]
86 
87  SeeAlso [CSolver]
88 
89 ******************************************************************************/
90 class CDatabase
91 {
92 protected:
94  //for efficiency, the memeory management of lit pool is done by the solver
95 
96  CLitPoolElement * _lit_pool_start; //the begin of the lit vector
97  CLitPoolElement * _lit_pool_finish; //the tail of the used lit vector
98  CLitPoolElement * _lit_pool_end_storage; //the storage end of lit vector
99 
100  vector<CVariable> _variables; //note: first element is not used
101  vector<CClause> _clauses;
102  queue<ClauseIdx> _unused_clause_idx_queue;
103 
106 public:
107 //constructors & destructors
108  CDatabase() ;
110  delete [] _lit_pool_start;
111  }
112  void init(void) {
115  }
116 //member access function
117  vector<CVariable>& variables(void) {
118  return _variables;
119  }
120  vector<CClause>& clauses(void) {
121  return _clauses;
122  }
123  CVariable & variable(int idx) {
124  return _variables[idx];
125  }
127  return _clauses[idx];
128  }
130  return _stats;
131  }
132  void set_mem_limit(int n) {
133  _mem_limit = n;
134  }
135 //some stats
136  int & init_num_clauses() { return _stats.init_num_clauses; }
137  int & init_num_literals () { return _stats.init_num_literals; }
138  int & num_added_clauses () { return _stats.num_added_clauses; }
139  int & num_added_literals() { return _stats.num_added_literals; }
140  int & num_deleted_clauses() { return _stats.num_deleted_clauses; }
141  int & num_deleted_literals() { return _stats.num_deleted_literals; }
142 
143 //lit pool naming convention is following STL Vector
145  return _lit_pool_start;
146  }
148  return _lit_pool_finish;
149  }
150  void lit_pool_push_back(int value) {
151  assert (_lit_pool_finish <= _lit_pool_end_storage );
152  _lit_pool_finish->val() = value;
153  ++ _lit_pool_finish;
154  }
155  int lit_pool_size(void) {
156  return _lit_pool_finish - _lit_pool_start;
157  }
158  int lit_pool_free_space(void) {
159  return _lit_pool_end_storage - _lit_pool_finish;
160  }
162  return _lit_pool_start[i];
163  }
164 //functions on lit_pool
165  void output_lit_pool_state(void);
166 
167  bool enlarge_lit_pool(void);
168 
169  void compact_lit_pool(void);
170 
171 //functions
172  int estimate_mem_usage (void)
173  {
174  int lit_pool = sizeof(CLitPoolElement) *
176  int mem_vars = sizeof(CVariable) *
177  variables().capacity();
178  int mem_cls = sizeof(CClause) *
179  clauses().capacity();
180  int mem_cls_queue = sizeof(int) *
181  _unused_clause_idx_queue.size();
182  int mem_ht_ptrs =0, mem_lit_clauses = 0;
183  mem_ht_ptrs = sizeof(CLitPoolElement*) *
184  (clauses().size()-_unused_clause_idx_queue.size()) * 2;
185  return (lit_pool + mem_vars + mem_cls +
186  mem_cls_queue + mem_ht_ptrs + mem_lit_clauses);
187  }
188  int mem_usage(void) {
190  int mem_vars = sizeof(CVariable) * variables().capacity();
191  int mem_cls = sizeof(CClause) * clauses().capacity();
192  int mem_cls_queue = sizeof(int) * _unused_clause_idx_queue.size();
193  int mem_ht_ptrs = 0, mem_lit_clauses = 0;
194  for (unsigned i=0; i< variables().size(); ++i) {
195  CVariable & v = variable(i);
196  mem_ht_ptrs += v.ht_ptr(0).capacity() + v.ht_ptr(1).capacity();
197  }
198  mem_ht_ptrs *= sizeof(CLitPoolElement*);
199  mem_lit_clauses *= sizeof(ClauseIdx);
200  return (lit_pool + mem_vars + mem_cls +
201  mem_cls_queue + mem_ht_ptrs + mem_lit_clauses);
202  }
203  void set_variable_number(int n) {
204  variables().resize(n + 1) ;
205  }
206  int add_variable(void) {
207  variables().resize( variables().size() + 1);
208  return variables().size() - 1;
209  }
210  int num_variables(void) {
211  return variables().size() - 1;
212  }
213 
214  int num_clauses(void) {
215  return _clauses.size() - _unused_clause_idx_queue.size();
216  }
217  int num_literals(void) {
218  return _stats.num_added_literals - _stats.num_deleted_literals;
219  }
220 
222  ++_stats.num_deleted_clauses;
223  _stats.num_deleted_literals += cl.num_lits();
224  cl.in_use() = false;
225  for (int i=0; i< cl.num_lits(); ++i) {
226  CLitPoolElement & l = cl.literal(i);
227  --variable(l.var_index()).lits_count(l.var_sign());
228  l.val() = 0;
229  }
230  }
231  void mark_var_in_new_cl(int v_idx, int phase ) {
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? ");
237  variable(v_idx).set_in_new_cl( phase );
238  }
239  int literal_value (CLitPoolElement l) { //note: it will return 0 or 1 or other ,
240  //here "other" may not equal UNKNOWN
241  return variable(l.var_index()).value() ^ l.var_sign();
242  }
243 
244  int find_unit_literal(ClauseIdx cl); //if not unit clause, return 0.
245 
246  bool is_conflict(ClauseIdx cl); //e.g. all literals assigned value 0
247 
248  bool is_satisfied(ClauseIdx cl); //e.g. at least one literal has value 1
249 
250  void detail_dump_cl(ClauseIdx cl_idx, ostream & os = cout);
251 
252  void dump(ostream & os = cout);
253 };
254 
255 #endif
256 
257 
258 
259 
260 
261 
262 
263 
264 
265 
266 
267 
268 
269 
270 
int find_unit_literal(ClauseIdx cl)
void compact_lit_pool(void)
size_t operator()(const pair< int, int > a) const
Definition: xchaff_dbase.h:54
int literal_value(CLitPoolElement l)
Definition: xchaff_dbase.h:239
int lit_pool_free_space(void)
Definition: xchaff_dbase.h:158
CLitPoolElement * lit_pool_begin(void)
Definition: xchaff_dbase.h:144
void mark_clause_deleted(CClause &cl)
Definition: xchaff_dbase.h:221
void dump(ostream &os=cout)
vector< CClause > _clauses
Definition: xchaff_dbase.h:101
vector< CClause > & clauses(void)
Definition: xchaff_dbase.h:120
int & num_lits(void)
Definition: xchaff_base.h:189
int add_variable(void)
Definition: xchaff_dbase.h:206
int & num_added_clauses()
Definition: xchaff_dbase.h:138
int & num_added_literals()
Definition: xchaff_dbase.h:139
bool is_conflict(ClauseIdx cl)
void mark_var_in_new_cl(int v_idx, int phase)
Definition: xchaff_dbase.h:231
CDatabaseStats & stats(void)
Definition: xchaff_dbase.h:129
void set_in_new_cl(int phase)
Definition: xchaff_base.h:273
void lit_pool_push_back(int value)
Definition: xchaff_dbase.h:150
bool & in_use(void)
Definition: xchaff_base.h:192
CLitPoolElement & literal(int idx)
Definition: xchaff_base.h:195
int num_clauses(void)
Definition: xchaff_dbase.h:214
vector< CVariable > & variables(void)
Definition: xchaff_dbase.h:117
CLitPoolElement * _lit_pool_end_storage
Definition: xchaff_dbase.h:98
void output_lit_pool_state(void)
int estimate_mem_usage(void)
Definition: xchaff_dbase.h:172
CDatabaseStats _stats
Definition: xchaff_dbase.h:93
int & init_num_literals()
Definition: xchaff_dbase.h:137
queue< ClauseIdx > _unused_clause_idx_queue
Definition: xchaff_dbase.h:102
CLitPoolElement * _lit_pool_finish
Definition: xchaff_dbase.h:97
CVariable & variable(int idx)
Definition: xchaff_dbase.h:123
CLitPoolElement * lit_pool_end(void)
Definition: xchaff_dbase.h:147
vector< CLitPoolElement * > & ht_ptr(int i)
Definition: xchaff_base.h:297
int lit_pool_size(void)
Definition: xchaff_dbase.h:155
int var_index(void)
Definition: xchaff_base.h:98
int & val(void)
Definition: xchaff_base.h:92
int num_added_literals
Definition: xchaff_dbase.h:75
int ClauseIdx
Definition: xchaff_base.h:54
bool var_sign(void)
Definition: xchaff_base.h:101
void set_mem_limit(int n)
Definition: xchaff_dbase.h:132
void set_variable_number(int n)
Definition: xchaff_dbase.h:203
int & num_deleted_literals()
Definition: xchaff_dbase.h:141
int _num_var_in_new_cl
Definition: xchaff_dbase.h:104
bool enlarge_lit_pool(void)
int num_deleted_clauses
Definition: xchaff_dbase.h:76
int num_literals(void)
Definition: xchaff_dbase.h:217
int mem_usage(void)
Definition: xchaff_dbase.h:188
CLitPoolElement * _lit_pool_start
Definition: xchaff_dbase.h:96
CLitPoolElement & lit_pool(int i)
Definition: xchaff_dbase.h:161
void detail_dump_cl(ClauseIdx cl_idx, ostream &os=cout)
int & init_num_clauses()
Definition: xchaff_dbase.h:136
bool operator()(pair< int, int > a, pair< int, int > b)
Definition: xchaff_dbase.h:48
int mem_used_up_counts
Definition: xchaff_dbase.h:70
void init(void)
Definition: xchaff_dbase.h:112
bool is_satisfied(ClauseIdx cl)
int num_variables(void)
Definition: xchaff_dbase.h:210
int _mem_limit
Definition: xchaff_dbase.h:105
CClause & clause(ClauseIdx idx)
Definition: xchaff_dbase.h:126
vector< CVariable > _variables
Definition: xchaff_dbase.h:100
int num_deleted_literals
Definition: xchaff_dbase.h:77
int & num_deleted_clauses()
Definition: xchaff_dbase.h:140