CVC3  2.4.1
variable.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file variable.cpp
4  * \brief Implementation of class Variable; see variable.h for detail.
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Fri Apr 25 12:30:17 2003
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #include <sstream>
23 #include "variable.h"
24 #include "search_rules.h"
25 #include "memory_manager_chunks.h"
26 #include "memory_manager_malloc.h"
27 
28 using namespace std;
29 
30 namespace CVC3 {
31 
32 ///////////////////////////////////////////////////////////////////////
33 // class Variable methods
34 ///////////////////////////////////////////////////////////////////////
35 
36 // Constructors
37 Variable::Variable(VariableManager* vm, const Expr& e)
38  : d_val(vm->newVariableValue(e))
39 {
40  d_val->d_refcount++;
41 }
42 
43 Variable::Variable(const Variable& l): d_val(l.d_val) {
44  if(!isNull()) d_val->d_refcount++;
45 }
46 
47  // Destructor
49  if(!isNull()) {
50  if(--(d_val->d_refcount) == 0)
51  d_val->d_vm->gc(d_val);
52  }
53 }
54 
55  // Assignment
56 Variable&
58  if(&l == this) return *this; // Self-assignment
59  if(!isNull()) {
60  if(--(d_val->d_refcount) == 0) d_val->d_vm->gc(d_val);
61  }
62  d_val = l.d_val;
63  if(!isNull()) d_val->d_refcount++;
64  return *this;
65 }
66 
67 const Expr&
69  static Expr null;
70  if(isNull()) return null;
71  return d_val->getExpr();
72 }
73 
74 const Expr&
76  static Expr null;
77  if(isNull()) return null;
78  return d_val->getNegExpr();
79 }
80 
81 // IMPORTANT: Value can be -1 (false), 1 (true), or 0 (unresolved)
82 int
84  if(isNull()) return 0;
85  return d_val->getValue();
86 }
87 
88 
89 int
91  if(isNull()) return 0;
92  return d_val->getScope();
93 }
94 
95 const Theorem&
97  static Theorem null;
98  if(isNull()) return null;
99  return d_val->getTheorem();
100 }
101 
102 const Clause&
104  static Clause null;
105  if(isNull()) return null;
106  return d_val->getAntecedent();
107 }
108 
109 int
111  if(isNull()) return 0;
112  return d_val->getAntecedentIdx();
113 }
114 
115 const Theorem&
117  static Theorem null;
118  if(isNull()) return null;
119  return d_val->getAssumpThm();
120 }
121 
122 // Setting the attributes: it can be either derived from the
123 // antecedent clause, or by a theorem. The scope level is set to
124 // the current scope.
125 void
126 Variable::setValue(int val, const Clause& c, int idx) {
127  DebugAssert(!isNull(), "Variable::setValue(antecedent): var is NULL");
128  d_val->setValue(val, c, idx);
129 }
130 
131 // The theorem's expr must be the same as the variable's expr or
132 // its negation
133 void
135  DebugAssert(!isNull(), "Variable::setValue(Theorem): var is NULL");
136  d_val->setValue(thm, thm.getScope());
137 }
138 
139 void
140 Variable::setValue(const Theorem& thm, int scope) {
141  DebugAssert(!isNull(), "Variable::setValue(Theorem,scope): var is NULL");
142  d_val->setValue(thm, scope);
143 }
144 
145 void
146 Variable::setAssumpThm(const Theorem& a, int scope) {
147  DebugAssert(!isNull(), "Variable::setAssumpThm(): var is NULL");
148  d_val->setAssumpThm(a, scope);
149 }
150 
151  // Derive the theorem for either the variable or its negation. If
152  // the value is set by a theorem, that theorem is returned;
153  // otherwise a unit propagation rule is applied to the antecedent
154  // clause, and the theorem is cached for a quick access later.
155 Theorem
157  return deriveThmRec(false);
158 }
159 
160 
161 Theorem
162 Variable::deriveThmRec(bool checkAssump) const {
163  DebugAssert(!isNull(), "Variable::deriveTheorem(): called on Null");
164  DebugAssert(getValue() != 0, "Variable::deriveTheorem(): value is not set: "
165  + toString());
166  if(!getTheorem().isNull()) return getTheorem();
167  if(checkAssump && !getAssumpThm().isNull()) return getAssumpThm();
168  // Have to derive the theorem
169  Clause c(getAntecedent());
170  int idx(getAntecedentIdx());
171  const vector<Literal>& lits = c.getLiterals();
172  // Theorems for the other literals in the antecedent clause
173  vector<Theorem> thms;
174  int size(lits.size());
175  // Derive theorems recursively
176  for(int i=0; i<size; ++i)
177  if(i!=idx) thms.push_back(lits[i].getVar().deriveThmRec(true));
178  Theorem thm;
179  if(idx!=-1)
180  thm = d_val->d_vm->getRules()->unitProp(thms, c.getTheorem(), idx);
181  else
182  thm = d_val->d_vm->getRules()->conflictRule(thms, c.getTheorem());
183 
184  IF_DEBUG(Expr e(thm.getExpr());)
185  DebugAssert(e == getExpr()
186  || (e.isNot() && e[0] == getExpr()),
187  "Variable::deriveTheorem: bad theorem derived: expr ="
188  + toString() + ", thm = " + thm.toString());
189  // Cache the result
190  d_val->setValue(thm, getScope());
191  return thm;
192 }
193 
194 string
196  ostringstream ss;
197  ss << *this;
198  return ss.str();
199 }
200 
201 // Friend methods
202 ostream& operator<<(ostream& os, const Variable& l) {
203  return os << (*l.d_val);
204 }
205 
206 ///////////////////////////////////////////////////////////////////////
207 // class Literal methods
208 ///////////////////////////////////////////////////////////////////////
209 
210 string
212  ostringstream ss;
213  ss << *this;
214  return ss.str();
215 }
216 
217 ostream& operator<<(ostream& os, const Literal& l) {
218  os << "Lit(" << (l.isNegative()? "!" : "")
219  << l.getVar();
220  // Attributes
221  os << ", count=" << l.count() << ", score=" << l.score();
222  return os << ")";
223 }
224 
225 ///////////////////////////////////////////////////////////////////////
226 // class VariableValue methods
227 ///////////////////////////////////////////////////////////////////////
228 
229 // Destructor
231  if(d_val!=NULL) { delete d_val; free(d_val); d_val = NULL; }
232  if(d_scope!=NULL) { delete d_scope; free(d_scope); d_scope = NULL; }
233  if(d_thm!=NULL) { delete d_thm; free(d_thm); d_thm = NULL; }
234  if(d_ante!=NULL) { delete d_ante; free(d_ante); d_ante = NULL; }
235  if(d_anteIdx!=NULL) { delete d_anteIdx; free(d_anteIdx); d_anteIdx = NULL; }
236  if(d_assump!=NULL) { delete d_assump; free(d_assump); d_assump = NULL; }
237 }
238 
239  // Setting the attributes: it can be either derived from the
240  // antecedent clause, or by a theorem
241 void
242 VariableValue::setValue(int val, const Clause& c, int idx) {
243  if(d_val==NULL) {
244  // Make sure d_val==0 all the way to scope 0
245  d_val = new(true) CDO<int>(d_vm->getCM()->getCurrentContext(), 0, 0);
246  IF_DEBUG(d_val->setName("CDO[VariableValue::d_val]");)
247  }
248  if(d_scope==NULL) {
249  d_scope = new(true) CDO<int>(d_vm->getCM()->getCurrentContext());
250  IF_DEBUG(d_scope->setName("CDO[VariableValue::d_scope]");)
251  }
252  if(d_ante==NULL) {
253  d_ante = new(true) CDO<Clause>(d_vm->getCM()->getCurrentContext());
254  IF_DEBUG(d_ante->setName("CDO[VariableValue::d_ante]");)
255  }
256  if(d_anteIdx==NULL) {
257  d_anteIdx = new(true) CDO<int>(d_vm->getCM()->getCurrentContext());
258  IF_DEBUG(d_anteIdx->setName("CDO[VariableValue::d_anteIdx]");)
259  }
260 
261  // Compute the scope from the antecedent clause
262  // Assume the clause is valid exactly at the bottom scope
263  int scope(c.getScope());
264  for(int i=0, iend=c.size(); i!=iend; ++i) {
265  if(i!=idx) {
266  int s(c[i].getScope());
267  if(s > scope) scope = s;
268  DebugAssert(c[i].getValue() != 0,
269  "VariableValue::setValue(ante): literal has no value: "
270  "i="+int2string(i)+" in\n clause = "
271  +c.toString());
272  }
273  }
274 
275  d_val->set(val, scope);
276  d_scope->set(scope, scope); // d_vm->getCM()->scopeLevel();
277  d_ante->set(c, scope);
278  d_anteIdx->set(idx, scope);
279  // Set the theorem to null, to clean up the old value
280  if(!getTheorem().isNull()) d_thm->set(Theorem(), scope);
281 
282  IF_DEBUG(Expr l((idx == -1)? getExpr().getEM()->falseExpr()
283  : c[idx].getExpr());)
284  DebugAssert((val > 0 && l == getExpr())
285  || (val < 0 && l.isNot() && l[0] == getExpr()),
286  "VariableValue::setValue(val = " + int2string(val)
287  + ", c = " + c.toString() + ", idx = " + int2string(idx)
288  + "):\n expr = " + getExpr().toString()
289  + "\n literal = " + l.toString());
290 }
291 
292 // The theorem's expr must be the same as the variable's expr or
293 // its negation
294 void
295 VariableValue::setValue(const Theorem& thm, int scope) {
296  if(d_val==NULL) {
297  // Make sure d_val==0 all the way to scope 0
298  d_val = new(true) CDO<int>(d_vm->getCM()->getCurrentContext(),0,0);
299  IF_DEBUG(d_val->setName("CDO[VariableValue::d_val]");)
300  }
301  if(d_scope==NULL) {
302  d_scope = new(true) CDO<int>(d_vm->getCM()->getCurrentContext());
303  IF_DEBUG(d_scope->setName("CDO[VariableValue::d_scope]");)
304  }
305  if(d_thm==NULL) {
306  d_thm = new(true) CDO<Theorem>(d_vm->getCM()->getCurrentContext());
307  IF_DEBUG(d_thm->setName("CDO[VariableValue::d_thm]");)
308  }
309 
310  Expr e(thm.getExpr());
311  int val(0);
312  if(e == d_expr) val = 1;
313  else {
314  DebugAssert(e.isNot() && e[0] == d_expr,
315  "VariableValue::setValue(thm = "
316  + thm.toString() + "): expr = " + d_expr.toString());
317  val = -1;
318  }
319  // Set the values on that scope
320  d_val->set(val, scope);
321  d_scope->set(scope, scope); // d_vm->getCM()->scopeLevel();
322  d_thm->set(thm, scope);
323  // Set clause to null, to clean up the old value
324  if(!getAntecedent().isNull()) d_ante->set(Clause(), scope);
325 }
326 
327 void
328 VariableValue::setAssumpThm(const Theorem& thm, int scope) {
329  if(d_assump==NULL) {
330  // Make sure d_val==0 all the way to scope 0
331  d_assump = new(true) CDO<Theorem>(d_vm->getCM()->getCurrentContext());
332  IF_DEBUG(d_val->setName("CDO[VariableValue::d_val]");)
333  }
334  d_assump->set(thm, scope);
335 }
336 
337 ostream& operator<<(ostream& os, const VariableValue& v) {
338  os << "Var(" << v.getExpr() << " = " << v.getValue();
339  if(v.getValue() != 0) {
340  os << " @ " << v.getScope();
341  if(!v.getTheorem().isNull())
342  os << "; " << v.getTheorem();
343  else if(!v.getAntecedent().isNull()) {
344  os << "; #" << v.getAntecedentIdx()
345  << " in " << CompactClause(v.getAntecedent());
346  }
347  }
348  return os << ")";
349 }
350 
351 ///////////////////////////////////////////////////////////////////////
352 // class VariableManager methods
353 ///////////////////////////////////////////////////////////////////////
354 
355 // Creating unique VariableValue
358  VariableValue vv(this, e);
359  VariableValueSet::iterator i(d_varSet.find(&vv)), iend(d_varSet.end());
360  if(i != iend) return (*i);
361  // No such variable, create and insert one
362  VariableValue* p_vv(new(d_mm) VariableValue(this, e));
363  d_varSet.insert(p_vv);
364  return p_vv;
365 }
366 
367 // Constructor
369  const string& mmFlag)
370  : d_cm(cm), d_rules(rules), d_disableGC(false), d_postponeGC(false) {
371  if(mmFlag == "chunks")
372  d_mm = new MemoryManagerChunks(sizeof(VariableValue));
373  else
374  d_mm = new MemoryManagerMalloc();
375 
377 }
378 
379 // Destructor
381  delete d_notifyObj;
382  // Delete the remaining variables
383  d_disableGC = true;
384  vector<VariableValue*> vars;
386  i!=iend; ++i) {
387  vars.push_back(*i);
388  // delete(*i);
389  // No need to free memory; we'll delete the entire d_mm
390  // d_mm->deleteData(*i);
391  }
392  d_varSet.clear();
393  for(vector<VariableValue*>::iterator i=vars.begin(), iend=vars.end();
394  i!=iend; ++i) delete *i;
395  delete d_mm;
396 }
397 
398 // Garbage collect VariableValue pointer
399 void
401  if(!d_disableGC) {
402  d_varSet.erase(v);
403  if(d_postponeGC) d_deleted.push_back(v);
404  else {
405  delete v;
406  d_mm->deleteData(v);
407  }
408  }
409 }
410 
411 
412 void
414  d_postponeGC = false;
415  while(d_deleted.size() > 0) {
416  VariableValue* v = d_deleted.back();
417  d_deleted.pop_back();
418  delete v;
419  d_mm->deleteData(v);
420  }
421 }
422 
423 } // end of namespace CVC3
int getAntecedentIdx() const
Definition: variable.h:287
Data structure of expressions in CVC3.
Definition: expr.h:133
void clear()
Definition: hash_set.h:151
std::string toString() const
Definition: clause.cpp:129
unsigned & count()
Definition: variable.h:166
const Theorem & getTheorem() const
Definition: variable.h:275
int & score()
Definition: variable.h:168
bool d_disableGC
Disable the garbage collection.
Definition: variable.h:375
CDO< int > * d_val
Definition: variable.h:237
std::string toString() const
Definition: variable.cpp:195
size_t size() const
Definition: clause.h:113
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
const Theorem & getTheorem() const
Definition: variable.cpp:96
void set(const T &data, int scope=-1)
Definition: cdo.h:63
void gc(VariableValue *v)
Garbage collect VariableValue pointer.
Definition: variable.cpp:400
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
bool isNull() const
Definition: clause.h:111
Variable & getVar()
Definition: variable.h:134
VariableManagerNotifyObj * d_notifyObj
Definition: variable.h:370
CDO< int > * d_scope
Definition: variable.h:238
#define DebugAssert(cond, str)
Definition: debug.h:408
int getScope() const
Definition: clause.h:122
int getScope() const
Definition: theorem.cpp:486
virtual Theorem unitProp(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)=0
Unit propagation rule: .
virtual Theorem conflictRule(const std::vector< Theorem > &thms, const Theorem &clause)=0
"Conflict" rule (all literals in a clause become FALSE)
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
Context * getCurrentContext()
Definition: context.h:406
Abstract proof rules interface to the simple search engine.
const Theorem & getTheorem() const
Definition: clause.h:117
bool isNegative() const
Definition: variable.h:137
std::string toString() const
Definition: theorem.h:404
VariableValue * newVariableValue(const Expr &e)
Definition: variable.cpp:357
int getScope() const
Definition: variable.cpp:90
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
Variable & operator=(const Variable &l)
Definition: variable.cpp:57
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
CDO< Clause > * d_ante
Definition: variable.h:241
std::string int2string(int n)
Definition: cvc_util.h:46
size_type erase(const key_type &key)
Definition: hash_set.h:180
friend std::ostream & operator<<(std::ostream &os, const VariableValue &v)
Definition: variable.cpp:337
const Expr & getExpr() const
Definition: variable.cpp:68
iterator begin()
iterators
Definition: hash_set.h:224
const Theorem & getAssumpThm() const
Definition: variable.h:292
#define IF_DEBUG(code)
Definition: debug.h:406
virtual void deleteData(void *d)=0
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
void resumeGC()
Resume garbage collection.
Definition: variable.cpp:413
std::string toString() const
Definition: variable.cpp:211
const Expr & getNegExpr() const
Definition: variable.cpp:75
int getAntecedentIdx() const
Definition: variable.cpp:110
int getValue() const
Definition: variable.cpp:83
VariableManager * d_vm
Definition: variable.h:210
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
int getValue() const
Definition: variable.h:265
iterator end()
Definition: hash_set.h:235
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
Notifies VariableManager before and after each pop()
Definition: variable.h:432
bool isNull() const
Definition: variable.h:57
CDO< Theorem > * d_assump
Definition: variable.h:243
const Expr & getNegExpr() const
Definition: variable.h:257
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
const std::vector< Literal > & getLiterals() const
Definition: clause.h:138
ContextManager * d_cm
Definition: variable.h:367
void setAssumpThm(const Theorem &a, int scope)
Definition: variable.cpp:328
VariableValueSet d_varSet
Definition: variable.h:394