CVC3
variable.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file variable.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Fri Apr 25 11:52:17 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  * A data structure representing a variable in the search engine. It
19  * is a smart pointer with a uniquifying mechanism similar to Expr,
20  * and a variable is uniquely determined by its expression. It can be
21  * thought of as an Expr with additional attributes, but the type is
22  * different, so it will not be confused with other Exprs.
23  */
24 /*****************************************************************************/
25 
26 #ifndef _cvc3__variable_h_
27 #define _cvc3__variable_h_
28 
29 #include "expr.h"
30 
31 namespace CVC3 {
32 
33  class VariableManager;
34  class VariableValue;
35  class Clause;
36  class SearchEngineRules;
37 
38  // The main "smart pointer" class
39  class Variable {
40  private:
42  // Private methods
43  Theorem deriveThmRec(bool checkAssump) const;
44  public:
45  // Default constructor
46  Variable(): d_val(NULL) { }
47  // Constructor from an Expr; if such variable already exists, it
48  // will be found and used.
49  Variable(VariableManager* vm, const Expr& e);
50  // Copy constructor
51  Variable(const Variable& l);
52  // Destructor
53  ~Variable();
54  // Assignment
55  Variable& operator=(const Variable& l);
56 
57  bool isNull() const { return d_val == NULL; }
58 
59  // Accessors
60 
61  // Expr is the only constant attribute of a variable; other
62  // attributes can be changed.
63  const Expr& getExpr() const;
64  // The Expr of the inverse of the variable. This function is
65  // caching, so !e is only constructed once.
66  const Expr& getNegExpr() const;
67 
68  // IMPORTANT: Value can be -1 (false), 1 (true), or 0 (unresolved)
69  int getValue() const;
70  // If the value is set, scope level and either a theorem or
71  // an antecedent clause must be defined
72  int getScope() const;
73  const Theorem& getTheorem() const;
74  const Clause& getAntecedent() const;
75  // Index of this variable in the antecedent clause; if it is -1,
76  // the variable is FALSE, and that clause caused the contradiction
77  int getAntecedentIdx() const;
78  // Theorem of the form l |- l produced by the 'assump' rule, if
79  // this variable is a splitter, or a new intermediate assumption
80  // is generated for it.
81  const Theorem& getAssumpThm() const;
82  // Setting the attributes: it can be either derived from the
83  // antecedent clause, or by a theorem. The scope level is set to
84  // the current scope.
85  void setValue(int val, const Clause& c, int idx);
86  // The theorem's expr must be the same as the variable's expr or
87  // its negation, and the scope is the lowest scope where all
88  // assumptions of the theorem are true
89  void setValue(const Theorem& thm);
90  void setValue(const Theorem& thm, int scope);
91 
92  void setAssumpThm(const Theorem& a, int scope);
93  // Derive the theorem for either the variable or its negation. If
94  // the value is set by a theorem, that theorem is returned;
95  // otherwise a unit propagation rule is applied to the antecedent
96  // clause.
97  Theorem deriveTheorem() const;
98 
99  // Accessing Chaff counters (read and modified by reference)
100  unsigned& count(bool neg);
101  unsigned& countPrev(bool neg);
102  int& score(bool neg);
103  bool& added(bool neg);
104  // Read-only versions
105  unsigned count(bool neg) const;
106  unsigned countPrev(bool neg) const;
107  int score(bool neg) const;
108  bool added(bool neg) const;
109  // Watch pointer access
110  std::vector<std::pair<Clause, int> >& wp(bool neg) const;
111  // Friend methods
112  friend bool operator==(const Variable& l1, const Variable& l2) {
113  return l1.d_val == l2.d_val;
114  }
115  // Printing
116  friend std::ostream& operator<<(std::ostream& os, const Variable& l);
117  std::string toString() const;
118  }; // end of class Variable
119 
120  class Literal {
121  private:
124  public:
125  // Constructors: from a variable
126  Literal(const Variable& v, bool positive = true)
127  : d_var(v), d_negative(!positive) { }
128  // Default constructor
129  Literal(): d_negative(false) { }
130  // from Expr: if e == !e', construct negative literal of e',
131  // otherwise positive of e
132  Literal(VariableManager* vm, const Expr& e)
133  : d_var(vm, (e.isNot())? e[0] : e), d_negative(e.isNot()) { }
134  Variable& getVar() { return d_var; }
135  const Variable& getVar() const { return d_var; }
136  bool isPositive() const { return !d_negative; }
137  bool isNegative() const { return d_negative; }
138  bool isNull() const { return d_var.isNull(); }
139  // Return var or !var
140  const Expr& getExpr() const {
141  if(d_negative) return d_var.getNegExpr();
142  else return d_var.getExpr();
143  }
144  int getValue() const {
145  if(d_negative) return -(d_var.getValue());
146  else return d_var.getValue();
147  }
148  int getScope() const { return getVar().getScope(); }
149  // Set the value of the literal
150 // void setValue(int val, const Clause& c, int idx) {
151 // d_var.setValue(d_negative? -val : val, c, idx);
152 // }
153  void setValue(const Theorem& thm) {
154  d_var.setValue(thm, thm.getScope());
155  }
156  void setValue(const Theorem& thm, int scope) {
157  d_var.setValue(thm, scope);
158  }
159  const Theorem& getTheorem() const { return d_var.getTheorem(); }
160 // const Clause& getAntecedent() const { return d_var.getAntecedent(); }
161 // int getAntecedentIdx() const { return d_var.getAntecedentIdx(); }
162  // Defined when the literal has a value. Derives a theorem
163  // proving either this literal or its inverse.
164  Theorem deriveTheorem() const { return d_var.deriveTheorem(); }
165  // Accessing Chaff counters (read and modified by reference)
166  unsigned& count() { return d_var.count(d_negative); }
167  unsigned& countPrev() { return d_var.countPrev(d_negative); }
168  int& score() { return d_var.score(d_negative); }
169  bool& added() { return d_var.added(d_negative); }
170  // Read-only versions
171  unsigned count() const { return d_var.count(d_negative); }
172  unsigned countPrev() const { return d_var.countPrev(d_negative); }
173  int score() const { return d_var.score(d_negative); }
174  bool added() const { return d_var.added(d_negative); }
175  // Watch pointer access
176  std::vector<std::pair<Clause, int> >& wp() const
177  { return d_var.wp(d_negative); }
178  // Printing
179  friend std::ostream& operator<<(std::ostream& os, const Literal& l);
180  std::string toString() const;
181  // Equality
182  friend bool operator==(const Literal& l1, const Literal& l2) {
183  return (l1.d_negative == l2.d_negative && l1.d_var==l1.d_var);
184  }
185  }; // end of class Literal
186 
187  // Non-member methods: negation of Variable and Literal
188  inline Literal operator!(const Variable& v) {
189  return Literal(v, false);
190  }
191 
192  inline Literal operator!(const Literal& l) {
193  return Literal(l.getVar(), l.isNegative());
194  }
195 
196  std::ostream& operator<<(std::ostream& os, const Literal& l);
197 
198 } // end of namespace CVC3
199 
200 // Clause uses class Variable, have to include it here
201 #include "clause.h"
202 
203 namespace CVC3 {
204 
205  // The value holding class
207  friend class Variable;
208  friend class VariableManager;
209  private:
212 
214  // The inverse expression (initally Null)
216 
217  // Non-backtracking attributes (Chaff counters)
218 
219  // For positive instances
220  unsigned d_count;
221  unsigned d_countPrev;
222  int d_score;
223  // For negative instances
224  unsigned d_negCount;
225  unsigned d_negCountPrev;
227  // Whether the corresponding literal is in the list of active literals
228  bool d_added;
230  // Watch pointer lists
231  std::vector<std::pair<Clause, int> > d_wp;
232  std::vector<std::pair<Clause, int> > d_negwp;
233 
234  // Backtracking attributes
235 
236  // Value of the variable: -1 (false), 1 (true), 0 (unresolved)
238  CDO<int>* d_scope; // Scope level where the variable is assigned
239  // Theorem of the form (d_expr) or (!d_expr), reflecting d_val
241  CDO<Clause>* d_ante; // Antecedent clause and index of the variable
243  CDO<Theorem>* d_assump; // Theorem generated by assump rule, if any
244  // Constructor is private; only class Variable can create it
246  : d_vm(vm), d_refcount(0), d_expr(e),
247  d_count(0), d_countPrev(0), d_score(0),
249  d_added(false), d_negAdded(false),
250  d_val(NULL), d_scope(NULL), d_thm(NULL),
251  d_ante(NULL), d_anteIdx(NULL), d_assump(NULL) { }
252  public:
253  ~VariableValue();
254  // Accessor methods
255  const Expr& getExpr() const { return d_expr; }
256 
257  const Expr& getNegExpr() const {
258  if(d_neg.isNull()) {
259  const_cast<VariableValue*>(this)->d_neg
260  = d_expr.negate();
261  }
262  return d_neg;
263  }
264 
265  int getValue() const {
266  if(d_val==NULL) return 0;
267  else return d_val->get();
268  }
269 
270  int getScope() const {
271  if(d_scope==NULL) return 0;
272  else return d_scope->get();
273  }
274 
275  const Theorem& getTheorem() const {
276  static Theorem null;
277  if(d_thm==NULL) return null;
278  else return d_thm->get();
279  }
280 
281  const Clause& getAntecedent() const {
282  static Clause null;
283  if(d_ante==NULL) return null;
284  else return d_ante->get();
285  }
286 
287  int getAntecedentIdx() const {
288  if(d_anteIdx==NULL) return 0;
289  else return d_anteIdx->get();
290  }
291 
292  const Theorem& getAssumpThm() const {
293  static Theorem null;
294  if(d_assump==NULL) return null;
295  else return d_assump->get();
296  }
297 
298  // Setting the attributes: it can be either derived from the
299  // antecedent clause, or by a theorem
300  void setValue(int val, const Clause& c, int idx);
301  // The theorem's expr must be the same as the variable's expr or
302  // its negation
303  void setValue(const Theorem& thm, int scope);
304 
305  void setAssumpThm(const Theorem& a, int scope);
306 
307  // Chaff counters: read and modified by reference
308  unsigned& count(bool neg) {
309  if(neg) return d_negCount;
310  else return d_count;
311  }
312  unsigned& countPrev(bool neg) {
313  if(neg) return d_negCountPrev;
314  else return d_countPrev;
315  }
316  int& score(bool neg) {
317  if(neg) return d_negScore;
318  else return d_score;
319  }
320  bool& added(bool neg) {
321  if(neg) return d_negAdded;
322  else return d_added;
323  }
324 
325  // Memory management
326  void* operator new(size_t size, MemoryManager* mm) {
327  return mm->newData(size);
328  }
329  void operator delete(void* pMem, MemoryManager* mm) {
330  mm->deleteData(pMem);
331  }
332  void operator delete(void*) { }
333 
334  // friend methods
335  friend std::ostream& operator<<(std::ostream& os, const VariableValue& v);
336  friend bool operator==(const VariableValue& v1, const VariableValue& v2) {
337  return v1.d_expr == v2.d_expr;
338  }
339  }; // end of class VariableValue
340 
341  // Accessing Chaff counters (read and modified by reference)
342  inline unsigned& Variable::count(bool neg) { return d_val->count(neg); }
343  inline unsigned& Variable::countPrev(bool neg)
344  { return d_val->countPrev(neg); }
345  inline int& Variable::score(bool neg) { return d_val->score(neg); }
346  inline bool& Variable::added(bool neg) { return d_val->added(neg); }
347 
348  inline unsigned Variable::count(bool neg) const { return d_val->count(neg); }
349  inline unsigned Variable::countPrev(bool neg) const
350  { return d_val->countPrev(neg); }
351  inline int Variable::score(bool neg) const { return d_val->score(neg); }
352  inline bool Variable::added(bool neg) const { return d_val->added(neg); }
353 
354  inline std::vector<std::pair<Clause, int> >& Variable::wp(bool neg) const {
355  if(neg) return d_val->d_negwp;
356  else return d_val->d_wp;
357  }
358 
359 
361 
362  // The manager class
364  friend class Variable;
365  friend class VariableValue;
366  private:
371  //! Disable the garbage collection
372  /*! Normally, it's set in the destructor, so that we can delete
373  * all remaining variables without GC getting in the way
374  */
376  //! Postpone garbage collection
378  //! Vector of variables to be deleted (postponed during pop())
379  std::vector<VariableValue*> d_deleted;
380 
381  // Hash only by the Expr
382  class HashLV {
383  public:
384  size_t operator()(VariableValue* v) const { return v->getExpr().hash(); }
385  };
386  class EqLV {
387  public:
388  bool operator()(const VariableValue* lv1, const VariableValue* lv2) const
389  { return lv1->getExpr() == lv2->getExpr(); }
390  };
391 
392  // Hash set for existing variables
395 
396  // Creating unique VariableValue
398 
399  public:
400  // Constructor. mmFlag indicates which memory manager to use.
402  const std::string& mmFlag);
403  // Destructor
405 
406  //! Garbage collect VariableValue pointer
407  void gc(VariableValue* v);
408  //! Postpone garbage collection
409  void postponeGC() { d_postponeGC = true; }
410  //! Resume garbage collection
411  void resumeGC();
412  // Accessors
413  ContextManager* getCM() const { return d_cm; }
414  SearchEngineRules* getRules() const { return d_rules; }
415 
416  }; // end of class VariableManager
417 
418 /*****************************************************************************/
419 /*!
420  *\class VariableManagerNotifyObj
421  *\brief Notifies VariableManager before and after each pop()
422  *
423  * Author: Sergey Berezin
424  *
425  * Created: Tue Mar 1 13:52:28 2005
426  *
427  * Disables the deletion of VariableValue objects during context
428  * restoration (backtracking). This solves the problem of circular
429  * dependencies (e.g. a Variable pointing to its antecedent Clause).
430  */
431 /*****************************************************************************/
434  public:
435  //! Constructor
437  : ContextNotifyObj(cxt), d_vm(vm) { }
438 
439  void notifyPre(void) { d_vm->postponeGC(); }
440  void notify(void) { d_vm->resumeGC(); }
441  };
442 
443 
444 } // end of namespace CVC3
445 #endif