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 // *********************************************************************/
35 #ifndef __ZCHAFF_DATABASE__
36 #define __ZCHAFF_DATABASE__
38 #include "zchaff_base.h"
40 #define STARTUP_LIT_POOL_SIZE 0x8000
42 // **Struct********************************************************************
44 // Synopsis [Definition of the statistics of clause database]
48 // SeeAlso [CDatabase]
50 // ****************************************************************************
52 struct CDatabaseStats {
54 unsigned init_num_clauses;
55 unsigned init_num_literals;
56 unsigned num_added_clauses;
57 long64 num_added_literals;
58 unsigned num_deleted_clauses;
59 unsigned num_del_orig_cls;
60 long64 num_deleted_literals;
65 // **Struct********************************************************************
67 // Synopsis [Definition of the parameters of clause database]
71 // SeeAlso [CDatabase]
73 // ****************************************************************************
75 struct CDatabaseParams {
79 // **Class*********************************************************************
81 // Synopsis [Definition of clause database ]
83 // Description [Clause Database is the place where the information of the
84 // SAT problem are stored. it is a parent class of CSolver ]
88 // ****************************************************************************
92 CDatabaseStats _stats;
94 CDatabaseParams _params;
96 unsigned _allocated_gid; // the gids that have already been
99 // for efficiency, the memeory management of lit pool is done by the solver
100 CLitPoolElement * _lit_pool_start; // the begin of the lit vector
101 CLitPoolElement * _lit_pool_finish; // the tail of the used lit vector
102 CLitPoolElement * _lit_pool_end_storage; // the storage end of lit vector
105 vector<CVariable> _variables; // note: first element is not used
107 vector<CClause> _clauses;
109 set<ClauseIdx> _unused_clause_idx;
111 ClauseIdx top_unsat_cls;
114 // constructors & destructors
119 void init_stats(void) {
120 _stats.mem_used_up = false;
121 _stats.init_num_clauses = num_clauses();
122 _stats.init_num_literals = num_literals();
123 _stats.num_deleted_clauses = 0;
124 _stats.num_del_orig_cls = 0;
125 _stats.num_deleted_literals = 0;
126 _stats.num_enlarge = 0;
127 _stats.num_compact = 0;
130 // lit pool naming convention follows STL Vector
131 CLitPoolElement * lit_pool_begin(void);
133 CLitPoolElement * lit_pool_end(void);
135 void lit_pool_incr_size(int size);
137 void lit_pool_push_back(int value);
139 int lit_pool_size(void);
141 int lit_pool_free_space(void);
143 double lit_pool_utilization(void);
145 CLitPoolElement & lit_pool(int i);
147 // functions on lit_pool
148 void output_lit_pool_stats(void);
150 // when allocated memeory runs out, do a reallocation
151 bool enlarge_lit_pool(void);
153 void compact_lit_pool(void); // garbage collection
155 unsigned literal_value(CLitPoolElement l) {
156 // note: it will return 0 or 1 or other, here "other" may not equal UNKNOWN
157 return (variable(l.var_index()).value() ^ l.var_sign());
160 unsigned svar_value(int svar) {
161 // note: it will return 0 or 1 or other, here "other" may not equal UNKNOWN
162 return (variable(svar >> 1).value() ^ (svar & 0x1));
166 void mark_clause_deleted(CClause & cl);
168 int find_unit_literal(ClauseIdx cl); // if not unit clause, return 0.
170 bool is_conflicting(ClauseIdx cl); // e.g. all literals assigned value 0
172 bool is_unit(ClauseIdx cl);
174 bool is_satisfied(ClauseIdx cl); // e.g. at least one literal has value 1
177 ClauseIdx get_free_clause_idx(void);
179 ClauseIdx add_clause(int * lits, int n_lits, int gflag = 0);
183 // member access function
184 inline vector<CVariable>* variables(void) {
188 inline CVariable & variable(int idx) {
189 return _variables[idx];
192 inline vector<CClause>* clauses(void) {
196 inline CClause & clause(ClauseIdx idx) {
197 return _clauses[idx];
200 inline CDatabaseStats & stats(void) {
204 inline void set_mem_limit(int n) {
205 _params.mem_limit = n;
208 // clause group management
211 void free_gid(int gid);
213 inline int get_volatile_gid(void) {
217 inline int get_permanent_gid(void) {
221 bool is_gid_allocated(int gid);
223 int merge_clause_group(int g1, int g2);
226 inline unsigned & init_num_clauses(void) {
227 return _stats.init_num_clauses;
230 inline unsigned & init_num_literals(void) {
231 return _stats.init_num_literals;
234 inline unsigned & num_added_clauses(void) {
235 return _stats.num_added_clauses;
238 inline long64 & num_added_literals(void) {
239 return _stats.num_added_literals;
242 inline unsigned & num_deleted_clauses(void) {
243 return _stats.num_deleted_clauses;
246 inline unsigned & num_del_orig_cls(void) {
247 return _stats.num_del_orig_cls;
250 inline long64 & num_deleted_literals(void) {
251 return _stats.num_deleted_literals;
254 inline unsigned num_variables(void) {
255 return variables()->size() - 1;
258 inline unsigned num_clauses(void) {
259 return _clauses.size() - _unused_clause_idx.size();
262 inline unsigned num_literals(void) {
263 return _stats.num_added_literals - _stats.num_deleted_literals;
266 inline unsigned num_mem_compacts(void) {
267 return _stats.num_compact;
270 inline unsigned num_mem_enlarges(void) { return
275 unsigned estimate_mem_usage(void);
277 unsigned mem_usage(void);
279 inline void set_variable_number(int n) {
280 variables()->resize(n + 1);
283 inline int add_variable(void) {
284 variables()->resize(variables()->size() + 1);
285 return variables()->size() - 1;
289 void detail_dump_cl(ClauseIdx cl_idx, ostream & os = cout);
291 void dump(ostream & os = cout);
293 friend ostream & operator << (ostream & os, CDatabase & db) {