CVC3
xchaff_base.h
Go to the documentation of this file.
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 __BASIC_CLASSES__
40 #define __BASIC_CLASSES__
41 
42 #include <vector>
43 #include <iostream>
44 #include <assert.h>
45 using namespace std;
46 
47 typedef enum Unknown {
48  UNKNOWN = -1
49 } Unknown;
50 
51 #define NULL_CLAUSE -1
52 #define FLIPPED -2
53 
54 typedef int ClauseIdx; //used to refer a clause. Because of dynamic
55  //allocation of vector storage, no pointer is allowered
56 
57 /**Class**********************************************************************
58 
59  Synopsis [Definition of a literal]
60 
61  Description [A literal is a variable with phase. Two thing determing a lteral:
62  it's "sign", and the variable index. One bit is used to mark it's
63  sign. 0->positive, 1->negative.
64 
65  For every clause with literal count larger than 1, there are two
66  special literals which are designated ht_literal (stands for
67  head/tail literal to imitate SATO) It is specially marked with 2 bits:
68  00->not ht; dir = 1; or dir = -1; 10 is not valid.
69  Each literal is represented by a 32 bit integer, with one bit
70  representing it's phase and 2 bits indicate h/t property.
71 
72  All the literals are collected in a storage space called literal
73  pool. An element in a literal pool can be a literal or special
74  spacing element to indicate the termination of a clause. The
75  spacing element has negative value of the clause index.]
76 
77  SeeAlso [CDatabase, CClause]
78 
79 ******************************************************************************/
80 
82 {
83 protected:
84  int _val;
85 public:
86 //======constructors & destructors============
88  _val=0;
89  }
90  CLitPoolElement(int val):_val(val){}
91 //=========member access function=============
92  int & val(void) {
93  return _val;
94  }
95  int s_var(void) { //stands for signed variable, i.e. 2*var_idx + sign
96  return _val>>2;
97  }
98  int var_index(void) {
99  return _val>>3;
100  }
101  bool var_sign(void) {
102  return ( (_val>> 2)& 0x1);
103  }
104  void set (int s_var) {
105  _val = (s_var << 2);
106  }
107  void set(int v, int s) {
108  _val = (((v<<1) + s)<< 2);
109  }
110 //following are the functions for the special head/tail literals for FAST_BCP
111  int direction (void) {
112  return ((_val&0x03) - 2);
113  }
114  bool is_ht(void) {
115  return _val&0x03;
116  }
117  void unset_ht(void) {
118  _val = _val & (0x0fffffffc);
119  }
120  void set_ht(int dir) {
121  _val = _val + dir + 2;
122  }
123 
124  //following are used for spacing (e.g. indicate clause's end)
125  bool is_literal(void) {
126  return _val > 0;
127  }
128  void set_clause_index(int cl_idx) {
129  _val = - cl_idx;
130  }
131  int get_clause_index(void) {
132  return -_val;
133  }
134  //misc functions
135  int find_clause_idx(void) {
136  CLitPoolElement * ptr;
137  for (ptr = this; ptr->is_literal(); ++ ptr);
138  return ptr->get_clause_index();
139  }
140 
141  void dump(ostream & os= cout) {
142  os << (var_sign()?" -":" +") << var_index();
143  if (is_ht()) os << "*";
144  }
145  friend ostream & operator << ( ostream & os, CLitPoolElement & l) {
146  l.dump(os);
147  return os;
148  }
149 };
150 
151 /**Class**********************************************************************
152 
153  Synopsis [Definition of a clause]
154 
155  Description [A clause is consisted of a certain number of literals.
156  All literals are collected in a single large vector, we call it
157  literal pool. Each clause has a pointer to the beginning position
158  of it's literals in the pool. The boolean propagation mechanism
159  use two pointers (called head/tail pointer, by sato's convention)
160  which always point to the last assigned literals of this clause.]
161 
162  SeeAlso [CDatabase]
163 
164 ******************************************************************************/
165 class CClause
166 {
167 protected:
168  CLitPoolElement * _first_lit; //pointer to the first literal in literal pool
169  int _num_lits; //number of literals
170  bool _in_use; //indicate if this clause has been deleted or not
171 public:
172 //constructors & destructors
173  CClause(void){}
174 
175  ~CClause() {}
176 //initialization & clear up
177  void init(CLitPoolElement * head, int num_lits) { //initialization of a clause
178  _first_lit = head;
179  _num_lits = num_lits;
180  _in_use = true;
181  }
182 //member access function
183  CLitPoolElement * literals(void) { //literals()[i] is it's the i-th literal
184  return _first_lit;
185  }
186  CLitPoolElement * & first_lit(void) { //use it only if you want to modify _first_lit
187  return _first_lit;
188  }
189  int & num_lits(void) {
190  return _num_lits;
191  }
192  bool & in_use(void) {
193  return _in_use;
194  }
195  CLitPoolElement & literal(int idx) { //return the idx-th literal
196  return literals()[idx];
197  }
198 //misc functions
199  void dump(ostream & os = cout) {
200  if (!in_use())
201  os << "\t\t\t======removed=====";
202  for (int i=0, sz=num_lits(); i<sz; ++i)
203  os << literal(i);
204  os << endl;
205  }
206 // friend ostream & operator << (ostream & os, CClause & cl);
207  friend ostream & operator << ( ostream & os, CClause & cl) {
208  cl.dump(os);
209  return os;
210  }
211 };
212 
213 
214 /**Class**********************************************************************
215 
216  Synopsis [Definition of a variable]
217 
218  Description [CVariable contains the necessary information for a variable.
219  _ht_ptrs are the head/tail literals of this variable (int two phases)]
220 
221  SeeAlso [CDatabase]
222 
223 ******************************************************************************/
224 class CVariable
225 {
226 protected:
227  bool _is_marked : 1; //used in conflict analysis.
228 
229  int _in_new_cl : 2; //it can take 3 value 0: pos phase,
230  //1: neg phase, -1 : not in new clause;
231  //used to keep track of literals appearing
232  //in newly added clause so that a. each
233  //variable can only appearing in one phase
234  //b. same literal won't appear more than once.
235 
236  ClauseIdx _antecedence : 29; //used in conflict analysis
237 
238  short _value; //can be 1, 0 or UNKNOWN
239 
240  short _dlevel; //decision level this variable being assigned
241 
242  vector<CLitPoolElement *> _ht_ptrs[2]; //literal of this var appearing in h/t. 0: pos, 1: neg
243 
244 protected:
245  int _lits_count[2];
246  int _scores[2];
248 public:
249  int & score(int i) { return _scores[i]; }
250  int score(void) { return score(0)>score(1)?score(0):score(1); }
251  int & var_score_pos(void) { return _var_score_pos; }
252 public:
253 //constructors & destructors
254  CVariable(void) {
255  _value = UNKNOWN;
256  _antecedence=NULL_CLAUSE;
257  _dlevel = -1;
258  _in_new_cl = -1;
259  _is_marked = false;
260  _scores[0] = _scores[1] = 0;
261  _var_score_pos = _lits_count[0] = _lits_count[1] = 0;
262  }
263 //member access function
264  short & value(void) {
265  return _value;
266  }
267  short & dlevel(void) {
268  return _dlevel;
269  }
270  int in_new_cl(void) {
271  return _in_new_cl;
272  }
273  void set_in_new_cl(int phase) {
274  _in_new_cl = phase;
275  }
276  int & lits_count(int i) {
277  return _lits_count[i];
278  }
279 
280  bool is_marked(void) {
281  return _is_marked;
282  }
283  void set_marked(void) {
284  _is_marked = true;
285  }
286  void clear_marked(void) {
287  _is_marked = false;
288  }
289 
291  return _antecedence;
292  }
294  _antecedence = ante;
295  }
296 
297  vector<CLitPoolElement *> & ht_ptr(int i) { return _ht_ptrs[i]; }
298 
299 //misc functions
300  void dump(ostream & os=cout) {
301  if (is_marked()) os << "*" ;
302  os << "V: " << _value << " DL: " << _dlevel
303  << " Ante: " << _antecedence << endl;
304  for (int j=0; j< 2; ++j) {
305  os << (j==0?"Pos ":"Neg ") << "(" ;
306  for (unsigned i=0; i< ht_ptr(j).size(); ++i )
307  os << ht_ptr(j)[i]->find_clause_idx() << " " ;
308  os << ")" << endl;
309  }
310  os << endl;
311  }
312 // friend ostream & operator << (ostream & os, CVariable & v);
313  friend ostream & operator << ( ostream & os, CVariable & v) {
314  v.dump(os);
315  return os;
316  }
317 };
318 #endif
319 
320 
321 
322 
323 
324 
325 
326 
327 
328 
329