CVC3

variable.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file variable.cpp
00004  * \brief Implementation of class Variable; see variable.h for detail.
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Fri Apr 25 12:30:17 2003
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #include <sstream>
00023 #include "variable.h"
00024 #include "search_rules.h"
00025 #include "memory_manager_chunks.h"
00026 #include "memory_manager_malloc.h"
00027 
00028 using namespace std;
00029 
00030 namespace CVC3 {
00031 
00032 ///////////////////////////////////////////////////////////////////////
00033 // class Variable methods
00034 ///////////////////////////////////////////////////////////////////////
00035 
00036 // Constructors
00037 Variable::Variable(VariableManager* vm, const Expr& e)
00038   : d_val(vm->newVariableValue(e))
00039 {
00040   d_val->d_refcount++;
00041 }
00042 
00043 Variable::Variable(const Variable& l): d_val(l.d_val) {
00044   if(!isNull()) d_val->d_refcount++;
00045 }
00046 
00047   // Destructor
00048 Variable::~Variable() {
00049   if(!isNull()) {
00050     if(--(d_val->d_refcount) == 0)
00051       d_val->d_vm->gc(d_val);
00052   }
00053 }
00054 
00055   // Assignment
00056 Variable&
00057 Variable::operator=(const Variable& l) {
00058   if(&l == this) return *this; // Self-assignment
00059   if(!isNull()) {
00060     if(--(d_val->d_refcount) == 0) d_val->d_vm->gc(d_val);
00061   }
00062   d_val = l.d_val;
00063   if(!isNull()) d_val->d_refcount++;
00064   return *this;
00065 }
00066 
00067 const Expr&
00068 Variable::getExpr() const {
00069   static Expr null;
00070   if(isNull()) return null;
00071   return d_val->getExpr();
00072 }
00073 
00074 const Expr&
00075 Variable::getNegExpr() const {
00076   static Expr null;
00077   if(isNull()) return null;
00078   return d_val->getNegExpr();
00079 }
00080 
00081 // IMPORTANT: Value can be -1 (false), 1 (true), or 0 (unresolved)
00082 int
00083 Variable::getValue() const {
00084   if(isNull()) return 0;
00085   return d_val->getValue();
00086 }
00087 
00088 
00089 int
00090 Variable::getScope() const {
00091   if(isNull()) return 0;
00092   return d_val->getScope();
00093 }
00094 
00095 const Theorem&
00096 Variable::getTheorem() const {
00097   static Theorem null;
00098   if(isNull()) return null;
00099   return d_val->getTheorem();
00100 }
00101 
00102 const Clause&
00103 Variable::getAntecedent() const {
00104   static Clause null;
00105   if(isNull()) return null;
00106   return d_val->getAntecedent();
00107 }
00108 
00109 int
00110 Variable::getAntecedentIdx() const {
00111   if(isNull()) return 0;
00112   return d_val->getAntecedentIdx();
00113 }
00114 
00115 const Theorem&
00116 Variable::getAssumpThm() const {
00117   static Theorem null;
00118   if(isNull()) return null;
00119   return d_val->getAssumpThm();
00120 }
00121 
00122 // Setting the attributes: it can be either derived from the
00123 // antecedent clause, or by a theorem.  The scope level is set to
00124 // the current scope.
00125 void
00126 Variable::setValue(int val, const Clause& c, int idx) {
00127   DebugAssert(!isNull(), "Variable::setValue(antecedent): var is NULL");
00128   d_val->setValue(val, c, idx);
00129 }
00130 
00131 // The theorem's expr must be the same as the variable's expr or
00132 // its negation
00133 void
00134 Variable::setValue(const Theorem& thm) {
00135   DebugAssert(!isNull(), "Variable::setValue(Theorem): var is NULL");
00136   d_val->setValue(thm, thm.getScope());
00137 }
00138 
00139 void
00140 Variable::setValue(const Theorem& thm, int scope) {
00141   DebugAssert(!isNull(), "Variable::setValue(Theorem,scope): var is NULL");
00142   d_val->setValue(thm, scope);
00143 }
00144 
00145 void
00146 Variable::setAssumpThm(const Theorem& a, int scope) {
00147   DebugAssert(!isNull(), "Variable::setAssumpThm(): var is NULL");
00148   d_val->setAssumpThm(a, scope);
00149 }
00150   
00151   // Derive the theorem for either the variable or its negation.  If
00152   // the value is set by a theorem, that theorem is returned;
00153   // otherwise a unit propagation rule is applied to the antecedent
00154   // clause, and the theorem is cached for a quick access later.
00155 Theorem
00156 Variable::deriveTheorem() const {
00157   return deriveThmRec(false);
00158 }
00159 
00160 
00161 Theorem
00162 Variable::deriveThmRec(bool checkAssump) const {
00163   DebugAssert(!isNull(), "Variable::deriveTheorem(): called on Null");
00164   DebugAssert(getValue() != 0, "Variable::deriveTheorem(): value is not set: "
00165         + toString());
00166   if(!getTheorem().isNull()) return getTheorem();
00167   if(checkAssump && !getAssumpThm().isNull()) return getAssumpThm();
00168   // Have to derive the theorem
00169   Clause c(getAntecedent());
00170   int idx(getAntecedentIdx());
00171   const vector<Literal>& lits = c.getLiterals();
00172   // Theorems for the other literals in the antecedent clause
00173   vector<Theorem> thms;
00174   int size(lits.size());
00175   // Derive theorems recursively
00176   for(int i=0; i<size; ++i)
00177     if(i!=idx) thms.push_back(lits[i].getVar().deriveThmRec(true));
00178   Theorem thm;
00179   if(idx!=-1)
00180     thm = d_val->d_vm->getRules()->unitProp(thms, c.getTheorem(), idx);
00181   else
00182     thm = d_val->d_vm->getRules()->conflictRule(thms, c.getTheorem());
00183   
00184   IF_DEBUG(Expr e(thm.getExpr());)
00185   DebugAssert(e == getExpr()
00186         || (e.isNot() && e[0] == getExpr()),
00187         "Variable::deriveTheorem: bad theorem derived: expr ="
00188         + toString() + ", thm = " + thm.toString());
00189   // Cache the result
00190   d_val->setValue(thm, getScope());
00191   return thm;
00192 }
00193 
00194 string
00195 Variable::toString() const {
00196   ostringstream ss;
00197   ss << *this;
00198   return ss.str();
00199 }
00200 
00201 // Friend methods
00202 ostream& operator<<(ostream& os, const Variable& l) {
00203   return os << (*l.d_val);
00204 }
00205 
00206 ///////////////////////////////////////////////////////////////////////
00207 // class Literal methods
00208 ///////////////////////////////////////////////////////////////////////
00209 
00210 string
00211 Literal::toString() const {
00212   ostringstream ss;
00213   ss << *this;
00214   return ss.str();
00215 }
00216 
00217 ostream& operator<<(ostream& os, const Literal& l) {
00218   os << "Lit(" << (l.isNegative()? "!" : "")
00219      << l.getVar();
00220   // Attributes
00221   os << ", count=" << l.count() << ", score=" << l.score();
00222   return os << ")";
00223 }
00224 
00225 ///////////////////////////////////////////////////////////////////////
00226 // class VariableValue methods
00227 ///////////////////////////////////////////////////////////////////////
00228 
00229 // Destructor
00230 VariableValue::~VariableValue() {
00231   if(d_val!=NULL) { delete d_val; free(d_val); d_val = NULL; }
00232   if(d_scope!=NULL) { delete d_scope; free(d_scope); d_scope = NULL; }
00233   if(d_thm!=NULL) { delete d_thm; free(d_thm); d_thm = NULL; }
00234   if(d_ante!=NULL) { delete d_ante; free(d_ante); d_ante = NULL; }
00235   if(d_anteIdx!=NULL) { delete d_anteIdx; free(d_anteIdx); d_anteIdx = NULL; }
00236   if(d_assump!=NULL) { delete d_assump; free(d_assump); d_assump = NULL; }
00237 }
00238 
00239   // Setting the attributes: it can be either derived from the
00240   // antecedent clause, or by a theorem
00241 void
00242 VariableValue::setValue(int val, const Clause& c, int idx) {
00243   if(d_val==NULL) {
00244     // Make sure d_val==0 all the way to scope 0
00245     d_val = new(true) CDO<int>(d_vm->getCM()->getCurrentContext(), 0, 0);
00246     IF_DEBUG(d_val->setName("CDO[VariableValue::d_val]");)
00247   }
00248   if(d_scope==NULL) {
00249     d_scope = new(true) CDO<int>(d_vm->getCM()->getCurrentContext());
00250     IF_DEBUG(d_scope->setName("CDO[VariableValue::d_scope]");)
00251   }
00252   if(d_ante==NULL) {
00253     d_ante = new(true) CDO<Clause>(d_vm->getCM()->getCurrentContext());
00254     IF_DEBUG(d_ante->setName("CDO[VariableValue::d_ante]");)
00255   }
00256   if(d_anteIdx==NULL) {
00257     d_anteIdx = new(true) CDO<int>(d_vm->getCM()->getCurrentContext());
00258     IF_DEBUG(d_anteIdx->setName("CDO[VariableValue::d_anteIdx]");)
00259   }
00260 
00261   // Compute the scope from the antecedent clause
00262   // Assume the clause is valid exactly at the bottom scope
00263   int scope(c.getScope());
00264   for(int i=0, iend=c.size(); i!=iend; ++i) {
00265     if(i!=idx) {
00266       int s(c[i].getScope());
00267       if(s > scope) scope = s;
00268       DebugAssert(c[i].getValue() != 0,
00269       "VariableValue::setValue(ante): literal has no value: "
00270       "i="+int2string(i)+" in\n clause = "
00271       +c.toString());
00272     }
00273   }
00274 
00275   d_val->set(val, scope);
00276   d_scope->set(scope, scope); // d_vm->getCM()->scopeLevel();
00277   d_ante->set(c, scope);
00278   d_anteIdx->set(idx, scope);
00279   // Set the theorem to null, to clean up the old value
00280   if(!getTheorem().isNull()) d_thm->set(Theorem(), scope);
00281 
00282   IF_DEBUG(Expr l((idx == -1)? getExpr().getEM()->falseExpr()
00283       : c[idx].getExpr());)
00284   DebugAssert((val > 0 && l == getExpr())
00285         || (val < 0 && l.isNot() && l[0] == getExpr()),
00286         "VariableValue::setValue(val = " + int2string(val)
00287         + ", c = " + c.toString() + ", idx = " + int2string(idx)
00288         + "):\n expr = " + getExpr().toString()
00289         + "\n literal = " + l.toString());
00290 }
00291 
00292 // The theorem's expr must be the same as the variable's expr or
00293 // its negation
00294 void
00295 VariableValue::setValue(const Theorem& thm, int scope) {
00296   if(d_val==NULL) {
00297     // Make sure d_val==0 all the way to scope 0
00298     d_val = new(true) CDO<int>(d_vm->getCM()->getCurrentContext(),0,0);
00299     IF_DEBUG(d_val->setName("CDO[VariableValue::d_val]");)
00300   }
00301   if(d_scope==NULL) {
00302     d_scope = new(true) CDO<int>(d_vm->getCM()->getCurrentContext());
00303     IF_DEBUG(d_scope->setName("CDO[VariableValue::d_scope]");)
00304   }
00305   if(d_thm==NULL) {
00306     d_thm = new(true) CDO<Theorem>(d_vm->getCM()->getCurrentContext());
00307     IF_DEBUG(d_thm->setName("CDO[VariableValue::d_thm]");)
00308   }
00309 
00310   Expr e(thm.getExpr());
00311   int val(0);
00312   if(e == d_expr) val = 1;
00313   else {
00314     DebugAssert(e.isNot() && e[0] == d_expr,
00315     "VariableValue::setValue(thm = "
00316     + thm.toString() + "): expr = " + d_expr.toString());
00317     val = -1;
00318   }
00319   // Set the values on that scope
00320   d_val->set(val, scope);
00321   d_scope->set(scope, scope); // d_vm->getCM()->scopeLevel();
00322   d_thm->set(thm, scope);
00323   // Set clause to null, to clean up the old value
00324   if(!getAntecedent().isNull()) d_ante->set(Clause(), scope);
00325 }
00326 
00327 void
00328 VariableValue::setAssumpThm(const Theorem& thm, int scope) {
00329   if(d_assump==NULL) {
00330     // Make sure d_val==0 all the way to scope 0
00331     d_assump = new(true) CDO<Theorem>(d_vm->getCM()->getCurrentContext());
00332     IF_DEBUG(d_val->setName("CDO[VariableValue::d_val]");)
00333   }
00334   d_assump->set(thm, scope);
00335 }
00336 
00337 ostream& operator<<(ostream& os, const VariableValue& v) {
00338   os << "Var(" << v.getExpr() << " = " << v.getValue();
00339   if(v.getValue() != 0) {
00340     os << " @ " << v.getScope();
00341     if(!v.getTheorem().isNull())
00342       os << "; " << v.getTheorem();
00343     else if(!v.getAntecedent().isNull()) {
00344       os << "; #" << v.getAntecedentIdx()
00345    << " in " << CompactClause(v.getAntecedent());
00346     }
00347   }
00348   return os << ")";
00349 }
00350 
00351 ///////////////////////////////////////////////////////////////////////
00352 // class VariableManager methods
00353 ///////////////////////////////////////////////////////////////////////
00354 
00355 // Creating unique VariableValue
00356 VariableValue*
00357 VariableManager::newVariableValue(const Expr& e) {
00358   VariableValue vv(this, e);
00359   VariableValueSet::iterator i(d_varSet.find(&vv)), iend(d_varSet.end());
00360   if(i != iend) return (*i);
00361   // No such variable, create and insert one
00362   VariableValue* p_vv(new(d_mm) VariableValue(this, e));
00363   d_varSet.insert(p_vv);
00364   return p_vv;
00365 }
00366 
00367 // Constructor
00368 VariableManager::VariableManager(ContextManager* cm, SearchEngineRules* rules,
00369          const string& mmFlag)
00370   : d_cm(cm), d_rules(rules), d_disableGC(false), d_postponeGC(false) {
00371   if(mmFlag == "chunks")
00372     d_mm = new MemoryManagerChunks(sizeof(VariableValue));
00373   else
00374     d_mm = new MemoryManagerMalloc();
00375 
00376   d_notifyObj = new VariableManagerNotifyObj(this, d_cm->getCurrentContext());
00377 }
00378 
00379 // Destructor
00380 VariableManager::~VariableManager() {
00381   delete d_notifyObj;
00382   // Delete the remaining variables
00383   d_disableGC = true;
00384   vector<VariableValue*> vars;
00385   for(VariableValueSet::iterator i=d_varSet.begin(), iend=d_varSet.end();
00386       i!=iend; ++i) {
00387     vars.push_back(*i);
00388     // delete(*i);
00389     // No need to free memory; we'll delete the entire d_mm
00390     // d_mm->deleteData(*i);
00391   }
00392   d_varSet.clear();
00393   for(vector<VariableValue*>::iterator i=vars.begin(), iend=vars.end();
00394       i!=iend; ++i) delete *i;
00395   delete d_mm;
00396 }
00397 
00398 // Garbage collect VariableValue pointer
00399 void
00400 VariableManager::gc(VariableValue* v) {
00401   if(!d_disableGC) {
00402     d_varSet.erase(v);
00403     if(d_postponeGC) d_deleted.push_back(v);
00404     else {
00405       delete v;
00406       d_mm->deleteData(v);
00407     }
00408   }
00409 }
00410 
00411 
00412 void
00413 VariableManager::resumeGC() {
00414   d_postponeGC = false;
00415   while(d_deleted.size() > 0) {
00416     VariableValue* v = d_deleted.back();
00417     d_deleted.pop_back();
00418     delete v;
00419     d_mm->deleteData(v);
00420   }
00421 }
00422 
00423 } // end of namespace CVC3