CVC3  2.4.1
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
void setValue(const Theorem &thm)
Definition: variable.h:153
unsigned & count(bool neg)
Definition: variable.h:342
std::vector< std::pair< Clause, int > > d_wp
Definition: variable.h:231
bool isNull() const
Definition: expr.h:1223
int getAntecedentIdx() const
Definition: variable.h:287
Literal(VariableManager *vm, const Expr &e)
Definition: variable.h:132
Data structure of expressions in CVC3.
Definition: expr.h:133
unsigned d_countPrev
Definition: variable.h:221
std::hash_set< VariableValue *, HashLV, EqLV > VariableValueSet
Definition: variable.h:393
int getValue() const
Definition: variable.h:144
unsigned & countPrev(bool neg)
Definition: variable.h:343
unsigned & count()
Definition: variable.h:166
const Theorem & getTheorem() const
Definition: variable.h:275
std::vector< std::pair< Clause, int > > & wp() const
Definition: variable.h:176
int & score()
Definition: variable.h:168
friend bool operator==(const Variable &l1, const Variable &l2)
Definition: variable.h:112
bool d_disableGC
Disable the garbage collection.
Definition: variable.h:375
CDO< int > * d_val
Definition: variable.h:237
bool isPositive() const
Definition: variable.h:136
std::string toString() const
Definition: variable.cpp:195
size_t operator()(VariableValue *v) const
Definition: variable.h:384
std::vector< std::pair< Clause, int > > & wp(bool neg) const
Definition: variable.h:354
Theorem deriveTheorem() const
Definition: variable.h:164
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
const Theorem & getTheorem() const
Definition: variable.cpp:96
void gc(VariableValue *v)
Garbage collect VariableValue pointer.
Definition: variable.cpp:400
unsigned count() const
Definition: variable.h:171
VariableValue * d_val
Definition: variable.h:41
SearchEngineRules * getRules() const
Definition: variable.h:414
ContextManager * getCM() const
Definition: variable.h:413
void setValue(int val, const Clause &c, int idx)
Definition: variable.cpp:126
int score() const
Definition: variable.h:173
friend std::ostream & operator<<(std::ostream &os, const Variable &l)
Definition: variable.cpp:202
VariableManagerNotifyObj(VariableManager *vm, Context *cxt)
Constructor.
Definition: variable.h:436
Variable & getVar()
Definition: variable.h:134
bool added() const
Definition: variable.h:174
VariableManagerNotifyObj * d_notifyObj
Definition: variable.h:370
Literal operator!(const Variable &v)
Definition: variable.h:188
bool isNull() const
Definition: variable.h:138
CDO< int > * d_scope
Definition: variable.h:238
friend std::ostream & operator<<(std::ostream &os, const Literal &l)
Definition: variable.cpp:217
int getScope() const
Definition: theorem.cpp:486
int getScope() const
Definition: variable.h:148
const Theorem & getAssumpThm() const
Definition: variable.cpp:116
void setAssumpThm(const Theorem &a, int scope)
Definition: variable.cpp:146
bool d_postponeGC
Postpone garbage collection.
Definition: variable.h:377
void setValue(const Theorem &thm, int scope)
Definition: variable.h:156
unsigned d_count
Definition: variable.h:220
bool & added()
Definition: variable.h:169
bool isNegative() const
Definition: variable.h:137
unsigned & countPrev(bool neg)
Definition: variable.h:312
int & score(bool neg)
Definition: variable.h:316
std::vector< std::pair< Clause, int > > d_negwp
Definition: variable.h:232
friend bool operator==(const VariableValue &v1, const VariableValue &v2)
Definition: variable.h:336
VariableValue * newVariableValue(const Expr &e)
Definition: variable.cpp:357
int getScope() const
Definition: variable.cpp:90
Variable & operator=(const Variable &l)
Definition: variable.cpp:57
unsigned d_negCount
Definition: variable.h:224
Theorem deriveTheorem() const
Definition: variable.cpp:156
CDO< int > * d_anteIdx
Definition: variable.h:242
A class representing a CNF clause (a smart pointer)
Definition: clause.h:83
VariableManager * d_vm
Definition: variable.h:433
const Theorem & getTheorem() const
Definition: variable.h:159
Expr negate() const
Definition: expr.h:937
CDO< Clause > * d_ante
Definition: variable.h:241
bool & added(bool neg)
Definition: variable.h:346
friend std::ostream & operator<<(std::ostream &os, const VariableValue &v)
Definition: variable.cpp:337
const Expr & getExpr() const
Definition: variable.cpp:68
const Expr & getExpr() const
Definition: variable.h:140
const Theorem & getAssumpThm() const
Definition: variable.h:292
bool & added(bool neg)
Definition: variable.h:320
int & score(bool neg)
Definition: variable.h:345
unsigned & count(bool neg)
Definition: variable.h:308
Variable d_var
Definition: variable.h:122
void resumeGC()
Resume garbage collection.
Definition: variable.cpp:413
const T & get() const
Definition: cdo.h:64
std::string toString() const
Definition: variable.cpp:211
static size_t hash(const Expr &e)
Definition: expr.h:992
const Expr & getNegExpr() const
Definition: variable.cpp:75
friend bool operator==(const Literal &l1, const Literal &l2)
Definition: variable.h:182
int getAntecedentIdx() const
Definition: variable.cpp:110
bool operator()(const VariableValue *lv1, const VariableValue *lv2) const
Definition: variable.h:388
int getValue() const
Definition: variable.cpp:83
VariableManager * d_vm
Definition: variable.h:210
unsigned & countPrev()
Definition: variable.h:167
std::vector< VariableValue * > d_deleted
Vector of variables to be deleted (postponed during pop())
Definition: variable.h:379
MemoryManager * d_mm
Definition: variable.h:368
const Variable & getVar() const
Definition: variable.h:135
int getValue() const
Definition: variable.h:265
bool d_negative
Definition: variable.h:123
unsigned d_negCountPrev
Definition: variable.h:225
Definition of the API to expression package. See class Expr for details.
VariableManager(ContextManager *cm, SearchEngineRules *rules, const std::string &mmFlag)
Definition: variable.cpp:368
const Expr & getExpr() const
Definition: variable.h:255
int getScope() const
Definition: variable.h:270
API to the proof rules for the Search Engines.
Definition: search_rules.h:35
VariableValue(VariableManager *vm, const Expr &e)
Definition: variable.h:245
Literal(const Variable &v, bool positive=true)
Definition: variable.h:126
Notifies VariableManager before and after each pop()
Definition: variable.h:432
bool isNull() const
Definition: variable.h:57
const Expr & getNegExpr() const
Definition: variable.h:257
CDO< Theorem > * d_assump
Definition: variable.h:243
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
void setValue(int val, const Clause &c, int idx)
Definition: variable.cpp:242
const Clause & getAntecedent() const
Definition: variable.cpp:103
Theorem deriveThmRec(bool checkAssump) const
Definition: variable.cpp:162
CDO< Theorem > * d_thm
Definition: variable.h:240
const Clause & getAntecedent() const
Definition: variable.h:281
SearchEngineRules * d_rules
Definition: variable.h:369
ContextManager * d_cm
Definition: variable.h:367
void setAssumpThm(const Theorem &a, int scope)
Definition: variable.cpp:328
unsigned countPrev() const
Definition: variable.h:172
void postponeGC()
Postpone garbage collection.
Definition: variable.h:409
VariableValueSet d_varSet
Definition: variable.h:394