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 // *********************************************************************/
37 #ifndef __BASIC_CLASSES__
38 #define __BASIC_CLASSES__
42 #include "zchaff_header.h"
45 #define NULL_CLAUSE -1
47 #define VOLATILE_GID -1
48 #define PERMANENT_GID 0
49 // #define KEEP_LIT_CLAUSES
50 typedef int ClauseIdx; // Used to refer a clause. Because of dynamic
51 // allocation of vector storage, no pointer is allowered
62 // /**Class********************************************************************
64 // Synopsis [Definition of a literal]
66 // Description [A literal is a variable with phase. Two things specify a
67 // literal: its "sign", and its variable index.
69 // Each clause that has more than 1 literal contains two special
70 // literals. They are being "watched". A literal is marked with
71 // 2 bits: 00->not watched; 11->watched, direction = 1;
72 // 01->watched, dir = -1; 10 is not valid. These two bits occupy
73 // the least significant bits of the literal.
75 // Each literal is represented by a 32 bit signed integer. The
76 // higher 29 bits represent the variable index. At most 2**28
77 // varialbes are allowed. If the sign of this integer is
78 // negative, it means that it is not a valid literal. It could
79 // be a clause index or a deleted literal pool element. The 3rd
80 // least significant bit is used to mark its sign.
81 // 0->positive, 1->negative.
83 // The literals are collected in a storage space called literal
84 // pool. An element in a literal pool can be a literal or a
85 // special spacing element to indicate the termination of a
86 // clause. The spacing elements has negative value of the clause
89 // Right Hand spacing element has the clause id, so why is it
92 // SeeAlso [CDatabase, CClause]
94 // ****************************************************************************
96 class CLitPoolElement {
101 // constructors & destructors
102 CLitPoolElement(void):_val(0) {}
104 ~CLitPoolElement() {}
106 // member access function
111 // stands for signed variable, i.e. 2*var_idx + sign
116 unsigned var_index(void) {
120 unsigned var_sign(void) {
121 return ((_val >> 2) & 0x1);
124 void set(int s_var) {
128 void set(int vid, int sign) {
129 _val = (((vid << 1) + sign) << 2);
132 // followings are for manipulate watched literals
133 int direction(void) {
134 return ((_val & 0x3) - 2);
137 bool is_watched(void) {
138 return ((_val & 0x3) != 0);
142 _val = _val & (~0x3);
145 void set_watch(int dir) {
146 _val = _val + dir + 2;
149 // following are used for spacing (e.g. indicate clause's end)
150 bool is_literal(void) {
154 void set_clause_index(int cl_idx) {
158 ClauseIdx get_clause_index(void) {
164 unsigned find_clause_index(void) {
165 CLitPoolElement * ptr;
166 for (ptr = this; ptr->is_literal(); ++ptr);
167 return ptr->get_clause_index();
170 // every class should have a dump function and a self check function
171 void dump(ostream & os= cout);
173 friend ostream & operator << (ostream & os, CLitPoolElement & l) {
179 // /**Class********************************************************************
181 // Synopsis [Definition of a clause]
183 // Description [A clause is consisted of a certain number of literals.
184 // All literals are collected in a single large vector, called
185 // literal pool. Each clause has a pointer to the beginning
186 // position of it's literals in the pool.
188 // Zchaff support incremental SAT. Clauses can be added or
189 // deleted from the database during search. To accomodate this
190 // feature, some modifications are needed.
192 // Clauses can be generated during search by conflict driven
193 // analysis. Conflict clauses are generated by a resolution
194 // process. Therefore, if after one search, some clauses got
195 // deleted, then some of the learned conflict clause may be
196 // invalidated. To maintain the integrity of the clause
197 // database, it is necessary to keep track of the clauses that
198 // are involved in the resolution process for a certain conflict
199 // clause so that when those clauses are deleted, the conflict
200 // clause should also be deleted.
202 // The scheme we implement is similar to the scheme described in
203 // : Ofer Strichman, Pruning techniques for the SAT-based
204 // Bounded Model Checking Problems, in Proc. 11th Advanced
205 // Research Working Conference on Correct Hardware Design and
206 // Verification Methods (CHARME'01)
209 // SeeAlso [CDatabase]
211 // ****************************************************************************
214 CLitPoolElement * _first_lit; // pointer to the first literal
216 CLAUSE_STATUS _status : 3;
217 unsigned _id : 29; // the unique ID of a clause
218 unsigned _gflag; // the clause group id flag,
219 // maximum allow WORD_WIDTH groups
225 // constructors & destructors
232 // initialization & clear up
233 void init(CLitPoolElement * head, unsigned num_lits, unsigned gflag) {
235 _num_lits = num_lits;
239 // member access function
240 inline int & activity(void) {
244 inline int & sat_lit_idx(void) {
248 inline CLitPoolElement * literals(void) {
249 // literals()[i] is it's the i-th literal
253 // return the idx-th literal
254 inline CLitPoolElement & literal(int idx) {
255 return *(_first_lit + idx);
258 // use it only if you want to modify _first_lit
259 inline CLitPoolElement * & first_lit(void) {
263 inline unsigned & num_lits(void) {
267 inline unsigned id(void) {
271 inline void set_id(int id) {
275 inline CLAUSE_STATUS status(void) {
279 inline void set_status(CLAUSE_STATUS st) {
283 // manipulate the group flag
284 inline unsigned & gflag(void) {
288 inline bool gid(int i) {
289 assert(i >= 1 && i <= WORD_WIDTH);
290 return ((_gflag & (1 << (i - 1))) != 0);
293 inline void set_gid(int i) {
294 assert(i >= 1 && i <= WORD_WIDTH);
295 _gflag |= (1 << (i - 1));
298 inline void clear_gid(int i) {
299 assert(i >= 1 && i <= WORD_WIDTH);
300 _gflag &= ~(1 << (i - 1));
304 bool self_check(void);
306 void dump(ostream & os = cout);
308 friend ostream & operator << (ostream & os, CClause & cl) {
315 // /**Class********************************************************************
317 // Synopsis [Definition of a variable]
319 // Description [CVariable contains the necessary information for a variable.]
321 // SeeAlso [CDatabase]
323 // ****************************************************************************
326 unsigned _value : 2; // it can take 3 values, 0, 1 and UNKNOWN
327 bool _marked : 1; // used in conflict analysis.
328 unsigned _new_cl_phase : 2; // it can take 3 value
329 // 0: pos phase, 1: neg phase, UNKNOWN : not in new clause;
330 // It is used to keep track of literals appearing
331 // in newly added clause so that
332 // a. each variable can only appearing in one phase
333 // b. same literal won't appear more than once.
334 bool _enable_branch : 1; // if this variable is enabled in branch
336 int _implied_sign : 1; // when a var is implied, here is the
337 // sign (1->negative, 0->positive)
338 ClauseIdx _antecedent; // used in conflict analysis.
339 int _dlevel; // decision level this variable being assigned
340 int _assgn_stack_pos; // the position where it is in the assignment
342 int _lits_count[2]; // how many literals are there with this
343 // variable. (two phases)
344 int _2_lits_count[2]; // how many literals in 2 literal clauses are
345 // there with this variable. (two phases)
346 vector<CLitPoolElement *> _watched[2]; // watched literals of this
347 // var. 0: pos phase, 1: neg phase
349 #ifdef KEEP_LIT_CLAUSES
350 vector<ClauseIdx> _lit_clauses[2]; // this will keep track of ALL the
351 // appearance of the variable in
353 // note this will increase the database
354 // size by upto a factor of 2
356 int _scores[2]; // the score used for decision making
357 int _var_score_pos; // keep track of this variable's
358 // position in the sorted score array
361 // constructors & destructors
364 _lits_count[0] = _lits_count[1] = 0;
365 _2_lits_count[0] = _2_lits_count[1] = 0;
372 _antecedent = NULL_CLAUSE;
375 _assgn_stack_pos = -1;
376 _new_cl_phase = UNKNOWN;
377 _scores[0] = _scores[1] = 0;
378 _enable_branch = true;
381 // member access function
382 inline int & score(int i) {
386 inline int & two_lits_count(int i) {
387 return _2_lits_count[i];
390 inline int score(void) {
391 // return 1; this will make a fixed order branch heuristic
392 int result = score(0) > score(1) ? score(0) : score(1);
398 inline int & var_score_pos(void) {
399 return _var_score_pos;
402 inline void set_var_score_pos(int pos) {
403 _var_score_pos = pos;
406 inline unsigned value(void) {
410 inline void set_value(unsigned v) {
414 inline int & dlevel(void) {
418 inline int get_dlevel(void) {
422 inline void set_dlevel(int dl) {
426 inline int & assgn_stack_pos(void) {
427 return _assgn_stack_pos;
430 inline int & lits_count(int i) {
431 return _lits_count[i];
434 inline bool is_marked(void) {
438 inline int get_implied_sign(void) {
439 return _implied_sign;
442 inline void set_implied_sign(int sign) {
443 _implied_sign = sign;
446 inline unsigned new_cl_phase(void) {
447 return _new_cl_phase;
450 inline void set_new_cl_phase(unsigned phase) {
451 _new_cl_phase = phase;
454 inline void set_marked(void) {
458 inline void clear_marked(void) {
462 inline ClauseIdx & antecedent(void) {
466 inline ClauseIdx get_antecedent(void) {
470 inline void set_antecedent(ClauseIdx cl) {
474 inline vector<CLitPoolElement *> & watched(int i) {
478 inline void enable_branch(void) {
479 _enable_branch = true;
482 inline void disable_branch(void) {
483 _enable_branch = false;
486 inline bool is_branchable(void) {
487 return _enable_branch;
490 #ifdef KEEP_LIT_CLAUSES
491 inline vector<ClauseIdx> & lit_clause(int i) {
492 return _lit_clauses[i];
497 bool self_check(void);
499 void dump(ostream & os = cout);
501 friend ostream & operator << (ostream & os, CVariable & v) {