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: 41 VariableValue* d_val; 42 // Private methods 43 Theorem deriveThmRec(bool checkAssump) const; 44 public: 45 // Default constructor Variable()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 isNull()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: 122 Variable d_var; 123 bool d_negative; 124 public: 125 // Constructors: from a variable 126 Literal(const Variable& v, bool positive = true) d_var(v)127 : d_var(v), d_negative(!positive) { } 128 // Default constructor Literal()129 Literal(): d_negative(false) { } 130 // from Expr: if e == !e', construct negative literal of e', 131 // otherwise positive of e Literal(VariableManager * vm,const Expr & e)132 Literal(VariableManager* vm, const Expr& e) 133 : d_var(vm, (e.isNot())? e[0] : e), d_negative(e.isNot()) { } getVar()134 Variable& getVar() { return d_var; } getVar()135 const Variable& getVar() const { return d_var; } isPositive()136 bool isPositive() const { return !d_negative; } isNegative()137 bool isNegative() const { return d_negative; } isNull()138 bool isNull() const { return d_var.isNull(); } 139 // Return var or !var getExpr()140 const Expr& getExpr() const { 141 if(d_negative) return d_var.getNegExpr(); 142 else return d_var.getExpr(); 143 } getValue()144 int getValue() const { 145 if(d_negative) return -(d_var.getValue()); 146 else return d_var.getValue(); 147 } getScope()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 // } setValue(const Theorem & thm)153 void setValue(const Theorem& thm) { 154 d_var.setValue(thm, thm.getScope()); 155 } setValue(const Theorem & thm,int scope)156 void setValue(const Theorem& thm, int scope) { 157 d_var.setValue(thm, scope); 158 } getTheorem()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. deriveTheorem()164 Theorem deriveTheorem() const { return d_var.deriveTheorem(); } 165 // Accessing Chaff counters (read and modified by reference) count()166 unsigned& count() { return d_var.count(d_negative); } countPrev()167 unsigned& countPrev() { return d_var.countPrev(d_negative); } score()168 int& score() { return d_var.score(d_negative); } added()169 bool& added() { return d_var.added(d_negative); } 170 // Read-only versions count()171 unsigned count() const { return d_var.count(d_negative); } countPrev()172 unsigned countPrev() const { return d_var.countPrev(d_negative); } score()173 int score() const { return d_var.score(d_negative); } added()174 bool added() const { return d_var.added(d_negative); } 175 // Watch pointer access wp()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 206 class VariableValue { 207 friend class Variable; 208 friend class VariableManager; 209 private: 210 VariableManager* d_vm; 211 int d_refcount; 212 213 Expr d_expr; 214 // The inverse expression (initally Null) 215 Expr d_neg; 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; 226 int d_negScore; 227 // Whether the corresponding literal is in the list of active literals 228 bool d_added; 229 bool d_negAdded; 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) 237 CDO<int>* d_val; 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 240 CDO<Theorem>* d_thm; 241 CDO<Clause>* d_ante; // Antecedent clause and index of the variable 242 CDO<int>* d_anteIdx; 243 CDO<Theorem>* d_assump; // Theorem generated by assump rule, if any 244 // Constructor is private; only class Variable can create it VariableValue(VariableManager * vm,const Expr & e)245 VariableValue(VariableManager* vm, const Expr& e) 246 : d_vm(vm), d_refcount(0), d_expr(e), 247 d_count(0), d_countPrev(0), d_score(0), 248 d_negCount(0), d_negCountPrev(0), d_negScore(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 getExpr()255 const Expr& getExpr() const { return d_expr; } 256 getNegExpr()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 getValue()265 int getValue() const { 266 if(d_val==NULL) return 0; 267 else return d_val->get(); 268 } 269 getScope()270 int getScope() const { 271 if(d_scope==NULL) return 0; 272 else return d_scope->get(); 273 } 274 getTheorem()275 const Theorem& getTheorem() const { 276 static Theorem null; 277 if(d_thm==NULL) return null; 278 else return d_thm->get(); 279 } 280 getAntecedent()281 const Clause& getAntecedent() const { 282 static Clause null; 283 if(d_ante==NULL) return null; 284 else return d_ante->get(); 285 } 286 getAntecedentIdx()287 int getAntecedentIdx() const { 288 if(d_anteIdx==NULL) return 0; 289 else return d_anteIdx->get(); 290 } 291 getAssumpThm()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 count(bool neg)308 unsigned& count(bool neg) { 309 if(neg) return d_negCount; 310 else return d_count; 311 } countPrev(bool neg)312 unsigned& countPrev(bool neg) { 313 if(neg) return d_negCountPrev; 314 else return d_countPrev; 315 } score(bool neg)316 int& score(bool neg) { 317 if(neg) return d_negScore; 318 else return d_score; 319 } added(bool neg)320 bool& added(bool neg) { 321 if(neg) return d_negAdded; 322 else return d_added; 323 } 324 325 // Memory management new(size_t size,MemoryManager * mm)326 void* operator new(size_t size, MemoryManager* mm) { 327 return mm->newData(size); 328 } delete(void * pMem,MemoryManager * mm)329 void operator delete(void* pMem, MemoryManager* mm) { 330 mm->deleteData(pMem); 331 } delete(void *)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) count(bool neg)342 inline unsigned& Variable::count(bool neg) { return d_val->count(neg); } countPrev(bool neg)343 inline unsigned& Variable::countPrev(bool neg) 344 { return d_val->countPrev(neg); } score(bool neg)345 inline int& Variable::score(bool neg) { return d_val->score(neg); } added(bool neg)346 inline bool& Variable::added(bool neg) { return d_val->added(neg); } 347 count(bool neg)348 inline unsigned Variable::count(bool neg) const { return d_val->count(neg); } countPrev(bool neg)349 inline unsigned Variable::countPrev(bool neg) const 350 { return d_val->countPrev(neg); } score(bool neg)351 inline int Variable::score(bool neg) const { return d_val->score(neg); } added(bool neg)352 inline bool Variable::added(bool neg) const { return d_val->added(neg); } 353 wp(bool neg)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 360 class VariableManagerNotifyObj; 361 362 // The manager class 363 class VariableManager { 364 friend class Variable; 365 friend class VariableValue; 366 private: 367 ContextManager* d_cm; 368 MemoryManager* d_mm; 369 SearchEngineRules* d_rules; 370 VariableManagerNotifyObj* d_notifyObj; 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 */ 375 bool d_disableGC; 376 //! Postpone garbage collection 377 bool d_postponeGC; 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: operator()384 size_t operator()(VariableValue* v) const { return v->getExpr().hash(); } 385 }; 386 class EqLV { 387 public: operator()388 bool operator()(const VariableValue* lv1, const VariableValue* lv2) const 389 { return lv1->getExpr() == lv2->getExpr(); } 390 }; 391 392 // Hash set for existing variables 393 typedef std::hash_set<VariableValue*, HashLV, EqLV> VariableValueSet; 394 VariableValueSet d_varSet; 395 396 // Creating unique VariableValue 397 VariableValue* newVariableValue(const Expr& e); 398 399 public: 400 // Constructor. mmFlag indicates which memory manager to use. 401 VariableManager(ContextManager* cm, SearchEngineRules* rules, 402 const std::string& mmFlag); 403 // Destructor 404 ~VariableManager(); 405 406 //! Garbage collect VariableValue pointer 407 void gc(VariableValue* v); 408 //! Postpone garbage collection postponeGC()409 void postponeGC() { d_postponeGC = true; } 410 //! Resume garbage collection 411 void resumeGC(); 412 // Accessors getCM()413 ContextManager* getCM() const { return d_cm; } getRules()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 /*****************************************************************************/ 432 class VariableManagerNotifyObj: public ContextNotifyObj { 433 VariableManager* d_vm; 434 public: 435 //! Constructor VariableManagerNotifyObj(VariableManager * vm,Context * cxt)436 VariableManagerNotifyObj(VariableManager* vm, Context* cxt) 437 : ContextNotifyObj(cxt), d_vm(vm) { } 438 notifyPre(void)439 void notifyPre(void) { d_vm->postponeGC(); } notify(void)440 void notify(void) { d_vm->resumeGC(); } 441 }; 442 443 444 } // end of namespace CVC3 445 #endif 446