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 47 struct pair_int_equal { operatorpair_int_equal48 bool operator () (pair<int,int> a, pair<int,int> b) { 49 return (a.first==b.first && a.second == b.second); 50 } 51 }; 52 53 struct pair_int_hash_fun { operatorpair_int_hash_fun54 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 69 struct CDatabaseStats { 70 int mem_used_up_counts; 71 bool mem_used_up; 72 int init_num_clauses; 73 int init_num_literals; 74 int num_added_clauses; 75 int num_added_literals; 76 int num_deleted_clauses; 77 int num_deleted_literals; 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: 93 CDatabaseStats _stats; 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 104 int _num_var_in_new_cl; 105 int _mem_limit; 106 public: 107 //constructors & destructors 108 CDatabase() ; ~CDatabase()109 ~CDatabase() { 110 delete [] _lit_pool_start; 111 } init(void)112 void init(void) { 113 init_num_clauses() = num_clauses(); 114 init_num_literals() = num_literals(); 115 } 116 //member access function variables(void)117 vector<CVariable>& variables(void) { 118 return _variables; 119 } clauses(void)120 vector<CClause>& clauses(void) { 121 return _clauses; 122 } variable(int idx)123 CVariable & variable(int idx) { 124 return _variables[idx]; 125 } clause(ClauseIdx idx)126 CClause & clause(ClauseIdx idx) { 127 return _clauses[idx]; 128 } stats(void)129 CDatabaseStats & stats(void) { 130 return _stats; 131 } set_mem_limit(int n)132 void set_mem_limit(int n) { 133 _mem_limit = n; 134 } 135 //some stats init_num_clauses()136 int & init_num_clauses() { return _stats.init_num_clauses; } init_num_literals()137 int & init_num_literals () { return _stats.init_num_literals; } num_added_clauses()138 int & num_added_clauses () { return _stats.num_added_clauses; } num_added_literals()139 int & num_added_literals() { return _stats.num_added_literals; } num_deleted_clauses()140 int & num_deleted_clauses() { return _stats.num_deleted_clauses; } num_deleted_literals()141 int & num_deleted_literals() { return _stats.num_deleted_literals; } 142 143 //lit pool naming convention is following STL Vector lit_pool_begin(void)144 CLitPoolElement * lit_pool_begin(void) { 145 return _lit_pool_start; 146 } lit_pool_end(void)147 CLitPoolElement * lit_pool_end(void) { 148 return _lit_pool_finish; 149 } lit_pool_push_back(int value)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 } lit_pool_size(void)155 int lit_pool_size(void) { 156 return _lit_pool_finish - _lit_pool_start; 157 } lit_pool_free_space(void)158 int lit_pool_free_space(void) { 159 return _lit_pool_end_storage - _lit_pool_finish; 160 } lit_pool(int i)161 CLitPoolElement & lit_pool(int i) { 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 estimate_mem_usage(void)172 int estimate_mem_usage (void) 173 { 174 int lit_pool = sizeof(CLitPoolElement) * 175 (lit_pool_size() + lit_pool_free_space()); 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 } mem_usage(void)188 int mem_usage(void) { 189 int lit_pool = (lit_pool_size() + lit_pool_free_space()) * sizeof(CLitPoolElement); 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 } set_variable_number(int n)203 void set_variable_number(int n) { 204 variables().resize(n + 1) ; 205 } add_variable(void)206 int add_variable(void) { 207 variables().resize( variables().size() + 1); 208 return variables().size() - 1; 209 } num_variables(void)210 int num_variables(void) { 211 return variables().size() - 1; 212 } 213 num_clauses(void)214 int num_clauses(void) { 215 return _clauses.size() - _unused_clause_idx_queue.size(); 216 } num_literals(void)217 int num_literals(void) { 218 return _stats.num_added_literals - _stats.num_deleted_literals; 219 } 220 mark_clause_deleted(CClause & cl)221 void mark_clause_deleted(CClause & cl) { 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 } mark_var_in_new_cl(int v_idx,int phase)231 void mark_var_in_new_cl(int v_idx, int phase ) { 232 if (variable(v_idx).in_new_cl() == -1 && phase != -1) 233 ++ _num_var_in_new_cl; 234 else if (variable(v_idx).in_new_cl() != -1 && phase == -1) 235 -- _num_var_in_new_cl; 236 else assert (0 && "How can this happen? "); 237 variable(v_idx).set_in_new_cl( phase ); 238 } literal_value(CLitPoolElement l)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 271