source: vis_dev/zchaff/zchaff_dbase.h @ 27

Last change on this file since 27 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 8.5 KB
Line 
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:
5//
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.
18//
19//
20// --- This software and any associated documentation is provided "as is"
21//
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.
27//
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__
37
38#include "zchaff_base.h"
39
40#define STARTUP_LIT_POOL_SIZE 0x8000
41
42// **Struct********************************************************************
43//
44// Synopsis    [Definition of the statistics of clause database]
45//
46//  Description []
47//
48//  SeeAlso     [CDatabase]
49//
50// ****************************************************************************
51
52struct CDatabaseStats {
53  bool             mem_used_up;
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;
61  unsigned         num_compact;
62  unsigned         num_enlarge;
63};
64
65// **Struct********************************************************************
66//
67//  Synopsis    [Definition of the parameters of clause database]
68//
69//  Description []
70//
71//  SeeAlso     [CDatabase]
72//
73// ****************************************************************************
74
75struct CDatabaseParams {
76  int         mem_limit;
77};
78
79// **Class*********************************************************************
80//
81//  Synopsis    [Definition of clause database ]
82//
83//  Description [Clause Database is the place where the information of the
84//               SAT problem are stored. it is a parent class of CSolver ]
85//
86//  SeeAlso     [CSolver]
87//
88// ****************************************************************************
89
90class CDatabase {
91  protected:
92    CDatabaseStats      _stats;
93
94    CDatabaseParams     _params;
95
96    unsigned            _allocated_gid;    // the gids that have already been
97                                           // allocated
98
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
103
104
105    vector<CVariable>   _variables;     // note: first element is not used
106
107    vector<CClause>     _clauses;
108
109    set<ClauseIdx>      _unused_clause_idx;
110
111    ClauseIdx           top_unsat_cls;
112
113  protected:
114    // constructors & destructors
115    CDatabase() ;
116
117    ~CDatabase();
118
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;
128    }
129
130    // lit pool naming convention follows STL Vector
131    CLitPoolElement * lit_pool_begin(void);
132
133    CLitPoolElement * lit_pool_end(void);
134
135    void lit_pool_incr_size(int size);
136
137    void lit_pool_push_back(int value);
138
139    int lit_pool_size(void);
140
141    int lit_pool_free_space(void);
142
143    double lit_pool_utilization(void);
144
145    CLitPoolElement & lit_pool(int i);
146
147    // functions on lit_pool
148    void output_lit_pool_stats(void);
149
150    // when allocated memeory runs out, do a reallocation
151    bool enlarge_lit_pool(void);
152
153    void compact_lit_pool(void);        // garbage collection
154
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());
158    }
159
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));
163    }
164
165    // clause properties
166    void mark_clause_deleted(CClause & cl);
167
168    int find_unit_literal(ClauseIdx cl);  // if not unit clause, return 0.
169
170    bool is_conflicting(ClauseIdx cl);    // e.g. all literals assigned value 0
171
172    bool is_unit(ClauseIdx cl);
173
174    bool is_satisfied(ClauseIdx cl);   // e.g. at least one literal has value 1
175
176    // others
177    ClauseIdx get_free_clause_idx(void);
178
179    ClauseIdx add_clause(int * lits, int n_lits, int gflag = 0);
180
181  public:
182
183    // member access function
184    inline vector<CVariable>* variables(void) {
185      return &_variables;
186    }
187
188    inline CVariable & variable(int idx) {
189      return _variables[idx];
190    }
191
192    inline vector<CClause>* clauses(void) {
193      return &_clauses;
194    }
195
196    inline CClause & clause(ClauseIdx idx) {
197      return _clauses[idx];
198    }
199
200    inline CDatabaseStats & stats(void) {
201      return _stats;
202    }
203
204    inline void set_mem_limit(int n) {
205      _params.mem_limit = n;
206    }
207
208    // clause group management
209    int alloc_gid(void);
210
211    void free_gid(int gid);
212
213    inline int get_volatile_gid(void) {
214      return -1;
215    }
216
217    inline int get_permanent_gid(void) {
218      return 0;
219    }
220
221    bool is_gid_allocated(int gid);
222
223    int merge_clause_group(int g1, int g2);
224
225    // some stats
226    inline unsigned & init_num_clauses(void) {
227      return _stats.init_num_clauses;
228    }
229
230    inline unsigned & init_num_literals(void) {
231      return _stats.init_num_literals;
232    }
233
234    inline unsigned & num_added_clauses(void) {
235      return _stats.num_added_clauses;
236    }
237
238    inline long64  & num_added_literals(void) {
239      return _stats.num_added_literals;
240    }
241
242    inline unsigned & num_deleted_clauses(void) {
243      return _stats.num_deleted_clauses;
244    }
245
246    inline unsigned & num_del_orig_cls(void) {
247      return _stats.num_del_orig_cls;
248    }
249
250    inline long64 & num_deleted_literals(void) {
251      return _stats.num_deleted_literals;
252    }
253
254    inline unsigned num_variables(void) {
255      return variables()->size() - 1;
256    }
257
258    inline unsigned num_clauses(void) {
259      return _clauses.size() - _unused_clause_idx.size();
260    }
261
262    inline unsigned num_literals(void) {
263      return _stats.num_added_literals - _stats.num_deleted_literals;
264    }
265
266    inline unsigned num_mem_compacts(void) {
267      return _stats.num_compact;
268    }
269
270    inline unsigned num_mem_enlarges(void) { return
271      _stats.num_enlarge;
272    }
273
274    // functions
275    unsigned estimate_mem_usage(void);
276
277    unsigned mem_usage(void);
278
279    inline void set_variable_number(int n) {
280      variables()->resize(n + 1);
281    }
282
283    inline int add_variable(void) {
284      variables()->resize(variables()->size() + 1);
285      return variables()->size() - 1;
286    }
287
288    // dump functions
289    void detail_dump_cl(ClauseIdx cl_idx, ostream & os = cout);
290
291    void dump(ostream & os = cout);
292
293    friend ostream & operator << (ostream & os, CDatabase & db) {
294      db.dump(os);
295      return os;
296    }
297};
298#endif
Note: See TracBrowser for help on using the repository browser.