source: vis_dev/zchaff/zchaff_base.h @ 87

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

Zchaff

File size: 14.9 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
36
37#ifndef __BASIC_CLASSES__
38#define __BASIC_CLASSES__
39
40#include <assert.h>
41
42#include "zchaff_header.h"
43
44#define UNKNOWN           2
45#define NULL_CLAUSE          -1
46
47#define VOLATILE_GID   -1
48#define        PERMANENT_GID         0
49// #define KEEP_LIT_CLAUSES
50typedef int ClauseIdx;  // Used to refer a clause. Because of dynamic
51                        // allocation of vector storage, no pointer is allowered
52
53#ifndef _CLS_STATUS_
54#define _CLS_STATUS_
55enum CLAUSE_STATUS {
56  ORIGINAL_CL,
57  CONFLICT_CL,
58  DELETED_CL,
59};
60#endif
61
62// /**Class********************************************************************
63//
64//   Synopsis    [Definition of a literal]
65//
66//   Description [A literal is a variable with phase. Two things specify a
67//                literal: its "sign", and its variable index.
68//
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.
74//
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.
82//
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
87//                index.]
88//
89//                Right Hand spacing element has the clause id, so why is it
90//                not less than 0?
91//
92//   SeeAlso     [CDatabase, CClause]
93//
94// ****************************************************************************
95
96class CLitPoolElement {
97  protected:
98    int32 _val;
99
100  public:
101    // constructors & destructors
102    CLitPoolElement(void):_val(0)        {}
103
104    ~CLitPoolElement()                         {}
105
106    // member access function
107    int & val(void) {
108      return _val;
109    }
110
111    // stands for signed variable, i.e. 2*var_idx + sign
112    int s_var(void) {
113      return _val >> 2;
114    }
115
116    unsigned var_index(void) {
117      return _val >> 3;
118    }
119
120    unsigned var_sign(void) {
121      return ((_val >> 2) & 0x1);
122    }
123
124    void set(int s_var) {
125      _val = (s_var << 2);
126    }
127
128    void set(int vid, int sign) {
129      _val = (((vid << 1) + sign) << 2);
130    }
131
132    // followings are for manipulate watched literals
133    int direction(void) {
134      return ((_val & 0x3) - 2);
135    }
136
137    bool is_watched(void) {
138      return ((_val & 0x3) != 0);
139    }
140
141    void unwatch(void) {
142      _val = _val & (~0x3);
143    }
144
145    void set_watch(int dir) {
146      _val = _val + dir + 2;
147    }
148
149    // following are used for spacing (e.g. indicate clause's end)
150    bool is_literal(void) {
151      return _val > 0;
152    }
153
154    void set_clause_index(int cl_idx) {
155      _val = - cl_idx;
156    }
157
158    ClauseIdx get_clause_index(void) {
159      assert(_val <= 0);
160      return -_val;
161    }
162
163    // misc functions
164    unsigned find_clause_index(void) {
165      CLitPoolElement * ptr;
166      for (ptr = this; ptr->is_literal(); ++ptr);
167      return ptr->get_clause_index();
168    }
169
170    // every class should have a dump function and a self check function
171    void dump(ostream & os= cout);
172
173    friend ostream & operator << (ostream & os, CLitPoolElement & l) {
174      l.dump(os);
175      return os;
176    }
177};
178
179// /**Class********************************************************************
180//
181//   Synopsis    [Definition of a clause]
182//
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.
187//
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.
191//
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.
201//
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)
207//                ]
208//
209//   SeeAlso     [CDatabase]
210//
211// ****************************************************************************
212class CClause {
213  protected:
214    CLitPoolElement *   _first_lit;     // pointer to the first literal
215    unsigned            _num_lits ;
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
220    int                 _activity;
221    int                 _sat_lit_idx;
222
223  public:
224
225    // constructors & destructors
226    CClause(void) {
227      _sat_lit_idx = 0;
228    }
229
230    ~CClause() {}
231
232    // initialization & clear up
233    void init(CLitPoolElement * head, unsigned num_lits, unsigned gflag) {
234      _first_lit = head;
235      _num_lits = num_lits;
236      _gflag = gflag;
237    }
238
239    // member access function
240    inline int & activity(void) {
241      return _activity;
242    }
243
244    inline int & sat_lit_idx(void) {
245      return _sat_lit_idx;
246    }
247
248    inline CLitPoolElement * literals(void) {
249      // literals()[i] is it's the i-th literal
250      return _first_lit;
251    }
252
253    // return the idx-th literal
254    inline CLitPoolElement & literal(int idx) {
255     return *(_first_lit + idx);
256    }
257
258    // use it only if you want to modify _first_lit
259    inline CLitPoolElement * & first_lit(void) {
260      return _first_lit;
261    }
262
263    inline unsigned & num_lits(void) {
264      return _num_lits;
265    }
266
267    inline unsigned id(void) {
268      return _id;
269    }
270
271    inline void set_id(int id) {
272      _id = id;
273    }
274
275    inline CLAUSE_STATUS status(void) {
276      return _status;
277    }
278
279    inline void set_status(CLAUSE_STATUS st) {
280      _status = st;
281    }
282
283    // manipulate the group flag
284    inline unsigned & gflag(void) {
285      return _gflag;
286    }
287
288    inline bool gid(int i) {
289      assert(i >= 1 && i <= WORD_WIDTH);
290      return ((_gflag & (1 << (i - 1))) != 0);
291    }
292
293    inline void set_gid(int i) {
294      assert(i >= 1 && i <= WORD_WIDTH);
295      _gflag |= (1 << (i - 1));
296    }
297
298    inline void clear_gid(int i) {
299      assert(i >= 1 && i <= WORD_WIDTH);
300      _gflag &= ~(1 << (i - 1));
301    }
302
303    // misc function
304    bool self_check(void);
305
306    void dump(ostream & os = cout);
307
308    friend ostream & operator << (ostream & os, CClause & cl) {
309        cl.dump(os);
310        return os;
311    }
312};
313
314
315// /**Class********************************************************************
316//
317// Synopsis    [Definition of a variable]
318//
319// Description [CVariable contains the necessary information for a variable.]
320//
321// SeeAlso     [CDatabase]
322//
323// ****************************************************************************
324class CVariable {
325  protected:
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
335                                      // selection
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
341                              // stack
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
348
349#ifdef KEEP_LIT_CLAUSES
350    vector<ClauseIdx> _lit_clauses[2];  // this will keep track of ALL the
351                                        // appearance of the variable in
352                                        // clauses
353                                        // note this will increase the database
354                                        // size by upto a factor of 2
355#endif
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
359
360  public:
361    // constructors & destructors
362    CVariable(void) {
363        init();
364        _lits_count[0] = _lits_count[1] = 0;
365        _2_lits_count[0] = _2_lits_count[1] = 0;
366    }
367
368    ~CVariable() {}
369
370    void init(void) {
371      _value = UNKNOWN;
372      _antecedent = NULL_CLAUSE;
373      _marked = false;
374      _dlevel = -1;
375      _assgn_stack_pos = -1;
376      _new_cl_phase = UNKNOWN;
377      _scores[0] = _scores[1] = 0;
378      _enable_branch = true;
379    }
380
381    // member access function
382    inline int & score(int i) {
383      return _scores[i];
384    }
385
386    inline int & two_lits_count(int i) {
387      return _2_lits_count[i];
388    }
389
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);
393      if (_dlevel == 0)
394        result =-1;
395      return result;
396    }
397
398    inline int & var_score_pos(void) {
399      return _var_score_pos;
400    }
401
402    inline void set_var_score_pos(int pos) {
403      _var_score_pos = pos;
404    }
405
406    inline unsigned value(void) {
407      return _value;
408    }
409
410    inline void set_value(unsigned v) {
411      _value = v;
412    }
413
414    inline int & dlevel(void) {
415      return _dlevel;
416    }
417
418    inline int get_dlevel(void) {
419      return _dlevel;
420    }
421
422    inline void set_dlevel(int dl) {
423      _dlevel = dl;
424    }
425
426    inline int & assgn_stack_pos(void) {
427      return _assgn_stack_pos;
428    }
429
430    inline int & lits_count(int i) {
431      return _lits_count[i];
432    }
433
434    inline bool is_marked(void) {
435      return _marked;
436    }
437
438    inline int get_implied_sign(void) {
439      return _implied_sign;
440    }
441
442    inline void set_implied_sign(int sign) {
443      _implied_sign = sign;
444    }
445
446    inline unsigned new_cl_phase(void) {
447      return _new_cl_phase;
448    }
449
450    inline void set_new_cl_phase(unsigned phase) {
451      _new_cl_phase = phase;
452    }
453
454    inline void set_marked(void) {
455      _marked = true;
456    }
457
458    inline void clear_marked(void) {
459      _marked = false;
460    }
461
462    inline ClauseIdx & antecedent(void) {
463      return _antecedent;
464    }
465
466    inline ClauseIdx get_antecedent(void) {
467      return _antecedent;
468    }
469
470    inline void set_antecedent(ClauseIdx cl) {
471      _antecedent = cl;
472    }
473
474    inline vector<CLitPoolElement *> & watched(int i) {
475      return _watched[i];
476    }
477
478    inline void enable_branch(void) {
479      _enable_branch = true;
480    }
481
482    inline void disable_branch(void) {
483      _enable_branch = false;
484    }
485
486    inline bool is_branchable(void) {
487      return _enable_branch;
488    }
489
490#ifdef KEEP_LIT_CLAUSES
491    inline vector<ClauseIdx> & lit_clause(int i) {
492      return _lit_clauses[i];
493    }
494#endif
495
496    // misc function
497    bool self_check(void);
498
499    void dump(ostream & os = cout);
500
501    friend ostream & operator << (ostream & os, CVariable & v) {
502      v.dump(os);
503      return os;
504    }
505};
506#endif
Note: See TracBrowser for help on using the repository browser.