variable.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file variable.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Fri Apr 25 11:52:17 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  * A data structure representing a variable in the search engine.  It
00019  * is a smart pointer with a uniquifying mechanism similar to Expr,
00020  * and a variable is uniquely determined by its expression.  It can be
00021  * thought of as an Expr with additional attributes, but the type is
00022  * different, so it will not be confused with other Exprs.
00023  */
00024 /*****************************************************************************/
00025 
00026 #ifndef _cvc3__variable_h_
00027 #define _cvc3__variable_h_
00028 
00029 #include "expr.h"
00030 
00031 namespace CVC3 {
00032 
00033   class VariableManager;
00034   class VariableValue;
00035   class Clause;
00036   class SearchEngineRules;
00037 
00038   // The main "smart pointer" class
00039   class Variable {
00040   private:
00041     VariableValue* d_val;
00042     // Private methods
00043     Theorem deriveThmRec(bool checkAssump) const;
00044   public:
00045     // Default constructor
00046     Variable(): d_val(NULL) { }
00047     // Constructor from an Expr; if such variable already exists, it
00048     // will be found and used.
00049     Variable(VariableManager* vm, const Expr& e);
00050     // Copy constructor
00051     Variable(const Variable& l);
00052     // Destructor
00053     ~Variable();
00054     // Assignment
00055     Variable& operator=(const Variable& l);
00056 
00057     bool isNull() const { return d_val == NULL; }
00058 
00059     // Accessors
00060 
00061     // Expr is the only constant attribute of a variable; other
00062     // attributes can be changed.
00063     const Expr& getExpr() const;
00064     // The Expr of the inverse of the variable.  This function is
00065     // caching, so !e is only constructed once.
00066     const Expr& getNegExpr() const;
00067     
00068     // IMPORTANT: Value can be -1 (false), 1 (true), or 0 (unresolved)
00069     int getValue() const;
00070     // If the value is set, scope level and either a theorem or
00071     // an antecedent clause must be defined
00072     int getScope() const;
00073     const Theorem& getTheorem() const;
00074     const Clause& getAntecedent() const;
00075     // Index of this variable in the antecedent clause; if it is -1,
00076     // the variable is FALSE, and that clause caused the contradiction
00077     int getAntecedentIdx() const;
00078     // Theorem of the form l |- l produced by the 'assump' rule, if
00079     // this variable is a splitter, or a new intermediate assumption
00080     // is generated for it.
00081     const Theorem& getAssumpThm() const;
00082     // Setting the attributes: it can be either derived from the
00083     // antecedent clause, or by a theorem.  The scope level is set to
00084     // the current scope.
00085     void setValue(int val, const Clause& c, int idx);
00086     // The theorem's expr must be the same as the variable's expr or
00087     // its negation, and the scope is the lowest scope where all
00088     // assumptions of the theorem are true
00089     void setValue(const Theorem& thm);
00090     void setValue(const Theorem& thm, int scope);
00091     
00092     void setAssumpThm(const Theorem& a, int scope);
00093     // Derive the theorem for either the variable or its negation.  If
00094     // the value is set by a theorem, that theorem is returned;
00095     // otherwise a unit propagation rule is applied to the antecedent
00096     // clause.
00097     Theorem deriveTheorem() const;
00098 
00099     // Accessing Chaff counters (read and modified by reference)
00100     unsigned& count(bool neg);
00101     unsigned& countPrev(bool neg);
00102     int& score(bool neg);
00103     bool& added(bool neg);
00104     // Read-only versions
00105     unsigned count(bool neg) const;
00106     unsigned countPrev(bool neg) const;
00107     int score(bool neg) const;
00108     bool added(bool neg) const;
00109     // Watch pointer access
00110     std::vector<std::pair<Clause, int> >& wp(bool neg) const;
00111     // Friend methods
00112     friend bool operator==(const Variable& l1, const Variable& l2) {
00113       return l1.d_val == l2.d_val;
00114     }
00115     // Printing
00116     friend std::ostream& operator<<(std::ostream& os, const Variable& l);
00117     std::string toString() const;
00118   }; // end of class Variable
00119 
00120   class Literal {
00121   private:
00122     Variable d_var;
00123     bool d_negative;
00124   public:
00125     // Constructors: from a variable
00126     Literal(const Variable& v, bool positive = true)
00127       : d_var(v), d_negative(!positive) { }
00128     // Default constructor
00129     Literal(): d_negative(false) { }
00130     // from Expr: if e == !e', construct negative literal of e',
00131     // otherwise positive of e
00132     Literal(VariableManager* vm, const Expr& e)
00133       : d_var(vm, (e.isNot())? e[0] : e), d_negative(e.isNot()) { }
00134     Variable& getVar() { return d_var; }
00135     const Variable& getVar() const { return d_var; }
00136     bool isPositive() const { return !d_negative; }
00137     bool isNegative() const { return d_negative; }
00138     bool isNull() const { return d_var.isNull(); }
00139     // Return var or !var
00140     const Expr& getExpr() const {
00141       if(d_negative) return d_var.getNegExpr();
00142       else return d_var.getExpr();
00143     }
00144     int getValue() const {
00145       if(d_negative) return -(d_var.getValue());
00146       else return d_var.getValue();
00147     }
00148     int getScope() const { return getVar().getScope(); }
00149     // Set the value of the literal
00150 //     void setValue(int val, const Clause& c, int idx) {
00151 //       d_var.setValue(d_negative? -val : val, c, idx);
00152 //     }
00153     void setValue(const Theorem& thm) {
00154       d_var.setValue(thm, thm.getScope());
00155     }
00156     void setValue(const Theorem& thm, int scope) {
00157       d_var.setValue(thm, scope);
00158     }
00159     const Theorem& getTheorem() const { return d_var.getTheorem(); }
00160 //     const Clause& getAntecedent() const { return d_var.getAntecedent(); }
00161 //     int getAntecedentIdx() const { return d_var.getAntecedentIdx(); }
00162     // Defined when the literal has a value.  Derives a theorem
00163     // proving either this literal or its inverse.
00164     Theorem deriveTheorem() const { return d_var.deriveTheorem(); }
00165     // Accessing Chaff counters (read and modified by reference)
00166     unsigned& count() { return d_var.count(d_negative); }
00167     unsigned& countPrev() { return d_var.countPrev(d_negative); }
00168     int& score() { return d_var.score(d_negative); }
00169     bool& added() { return d_var.added(d_negative); }
00170     // Read-only versions
00171     unsigned count() const { return d_var.count(d_negative); }
00172     unsigned countPrev() const { return d_var.countPrev(d_negative); }
00173     int score() const { return d_var.score(d_negative); }
00174     bool added() const { return d_var.added(d_negative); }
00175     // Watch pointer access
00176     std::vector<std::pair<Clause, int> >& wp() const
00177       { return d_var.wp(d_negative); }
00178     // Printing
00179     friend std::ostream& operator<<(std::ostream& os, const Literal& l);
00180     std::string toString() const;
00181     // Equality
00182     friend bool operator==(const Literal& l1, const Literal& l2) {
00183       return (l1.d_negative == l2.d_negative && l1.d_var==l1.d_var);
00184     }
00185   }; // end of class Literal
00186 
00187   // Non-member methods: negation of Variable and Literal
00188   inline Literal operator!(const Variable& v) {
00189     return Literal(v, false);
00190   }
00191 
00192   inline Literal operator!(const Literal& l) {
00193     return Literal(l.getVar(), l.isNegative());
00194   }
00195 
00196   std::ostream& operator<<(std::ostream& os, const Literal& l);
00197 
00198 } // end of namespace CVC3
00199 
00200 // Clause uses class Variable, have to include it here
00201 #include "clause.h"
00202 
00203 namespace CVC3 {
00204 
00205   // The value holding class
00206   class VariableValue {
00207     friend class Variable;
00208     friend class VariableManager;
00209   private:
00210     VariableManager* d_vm;
00211     int d_refcount;
00212 
00213     Expr d_expr;
00214     // The inverse expression (initally Null)
00215     Expr d_neg;
00216 
00217     // Non-backtracking attributes (Chaff counters)
00218 
00219     // For positive instances
00220     unsigned d_count;
00221     unsigned d_countPrev;
00222     int d_score;
00223     // For negative instances
00224     unsigned d_negCount;
00225     unsigned d_negCountPrev;
00226     int d_negScore;
00227     // Whether the corresponding literal is in the list of active literals
00228     bool d_added;
00229     bool d_negAdded;
00230     // Watch pointer lists
00231     std::vector<std::pair<Clause, int> > d_wp;
00232     std::vector<std::pair<Clause, int> > d_negwp;
00233 
00234     // Backtracking attributes
00235 
00236     // Value of the variable: -1 (false), 1 (true), 0 (unresolved)
00237     CDO<int>* d_val;
00238     CDO<int>* d_scope; // Scope level where the variable is assigned
00239     // Theorem of the form (d_expr) or (!d_expr), reflecting d_val
00240     CDO<Theorem>* d_thm;
00241     CDO<Clause>* d_ante; // Antecedent clause and index of the variable
00242     CDO<int>* d_anteIdx;
00243     CDO<Theorem>* d_assump; // Theorem generated by assump rule, if any
00244     // Constructor is private; only class Variable can create it
00245     VariableValue(VariableManager* vm, const Expr& e)
00246       : d_vm(vm), d_refcount(0), d_expr(e),
00247       d_count(0), d_countPrev(0), d_score(0),
00248       d_negCount(0), d_negCountPrev(0), d_negScore(0),
00249       d_added(false), d_negAdded(false),
00250       d_val(NULL), d_scope(NULL), d_thm(NULL),
00251       d_ante(NULL), d_anteIdx(NULL), d_assump(NULL) { }
00252   public:
00253     ~VariableValue();
00254     // Accessor methods
00255     const Expr& getExpr() const { return d_expr; }
00256 
00257     const Expr& getNegExpr() const {
00258       if(d_neg.isNull()) {
00259   const_cast<VariableValue*>(this)->d_neg
00260     = d_expr.negate();
00261       }
00262       return d_neg;
00263     }
00264 
00265     int getValue() const {
00266       if(d_val==NULL) return 0;
00267       else return d_val->get();
00268     }
00269     
00270     int getScope() const {
00271       if(d_scope==NULL) return 0;
00272       else return d_scope->get();
00273     }
00274 
00275     const Theorem& getTheorem() const {
00276       static Theorem null;
00277       if(d_thm==NULL) return null;
00278       else return d_thm->get();
00279     }
00280 
00281     const Clause& getAntecedent() const {
00282       static Clause null;
00283       if(d_ante==NULL) return null;
00284       else return d_ante->get();
00285     }
00286 
00287     int getAntecedentIdx() const {
00288       if(d_anteIdx==NULL) return 0;
00289       else return d_anteIdx->get();
00290     }
00291     
00292     const Theorem& getAssumpThm() const {
00293       static Theorem null;
00294       if(d_assump==NULL) return null;
00295       else return d_assump->get();
00296     }
00297 
00298     // Setting the attributes: it can be either derived from the
00299     // antecedent clause, or by a theorem
00300     void setValue(int val, const Clause& c, int idx);
00301     // The theorem's expr must be the same as the variable's expr or
00302     // its negation
00303     void setValue(const Theorem& thm, int scope);
00304 
00305     void setAssumpThm(const Theorem& a, int scope);
00306 
00307     // Chaff counters: read and modified by reference
00308     unsigned& count(bool neg) {
00309       if(neg) return d_negCount;
00310       else return d_count;
00311     }
00312     unsigned& countPrev(bool neg) {
00313       if(neg) return d_negCountPrev;
00314       else return d_countPrev;
00315     }
00316     int& score(bool neg) {
00317       if(neg) return d_negScore;
00318       else return d_score;
00319     }
00320     bool& added(bool neg) {
00321       if(neg) return d_negAdded;
00322       else return d_added;
00323     }
00324 
00325     // Memory management
00326     void* operator new(size_t size, MemoryManager* mm) {
00327       return mm->newData(size);
00328     }
00329     void operator delete(void* pMem, MemoryManager* mm) {
00330       mm->deleteData(pMem);
00331     }
00332     void operator delete(void*) { }
00333 
00334     // friend methods
00335     friend std::ostream& operator<<(std::ostream& os, const VariableValue& v);
00336     friend bool operator==(const VariableValue& v1, const VariableValue& v2) {
00337       return v1.d_expr == v2.d_expr;
00338     }
00339   }; // end of class VariableValue
00340 
00341     // Accessing Chaff counters (read and modified by reference)
00342   inline unsigned& Variable::count(bool neg) { return d_val->count(neg); }
00343   inline unsigned& Variable::countPrev(bool neg)
00344     { return d_val->countPrev(neg); }
00345   inline int& Variable::score(bool neg) { return d_val->score(neg); }
00346   inline bool& Variable::added(bool neg) { return d_val->added(neg); }
00347 
00348   inline unsigned Variable::count(bool neg) const { return d_val->count(neg); }
00349   inline unsigned Variable::countPrev(bool neg) const
00350     { return d_val->countPrev(neg); }
00351   inline int Variable::score(bool neg) const { return d_val->score(neg); }
00352   inline bool Variable::added(bool neg) const { return d_val->added(neg); }
00353 
00354   inline std::vector<std::pair<Clause, int> >& Variable::wp(bool neg) const {
00355     if(neg) return d_val->d_negwp;
00356     else return d_val->d_wp;
00357   }
00358 
00359 
00360   class VariableManagerNotifyObj;
00361 
00362   // The manager class
00363   class VariableManager {
00364     friend class Variable;
00365     friend class VariableValue;
00366   private:
00367     ContextManager* d_cm;
00368     MemoryManager* d_mm;
00369     SearchEngineRules* d_rules;
00370     VariableManagerNotifyObj* d_notifyObj;
00371     //! Disable the garbage collection
00372     /*! Normally, it's set in the destructor, so that we can delete
00373      * all remaining variables without GC getting in the way
00374      */
00375     bool d_disableGC;
00376     //! Postpone garbage collection
00377     bool d_postponeGC;
00378     //! Vector of variables to be deleted (postponed during pop())
00379     std::vector<VariableValue*> d_deleted;
00380     
00381     // Hash only by the Expr
00382     class HashLV {
00383     public:
00384       size_t operator()(VariableValue* v) const { return v->getExpr().hash(); }
00385     };
00386     class EqLV {
00387     public:
00388       bool operator()(const VariableValue* lv1, const VariableValue* lv2) const
00389   { return lv1->getExpr() == lv2->getExpr(); }
00390     };
00391 
00392     // Hash set for existing variables
00393     typedef std::hash_set<VariableValue*, HashLV, EqLV> VariableValueSet;
00394     VariableValueSet d_varSet;
00395     
00396     // Creating unique VariableValue
00397     VariableValue* newVariableValue(const Expr& e);
00398 
00399   public:
00400     // Constructor.  mmFlag indicates which memory manager to use.
00401     VariableManager(ContextManager* cm, SearchEngineRules* rules,
00402         const std::string& mmFlag);
00403     // Destructor
00404     ~VariableManager();
00405 
00406     //! Garbage collect VariableValue pointer
00407     void gc(VariableValue* v);
00408     //! Postpone garbage collection
00409     void postponeGC() { d_postponeGC = true; }
00410     //! Resume garbage collection
00411     void resumeGC();
00412     // Accessors
00413     ContextManager* getCM() const { return d_cm; }
00414     SearchEngineRules* getRules() const { return d_rules; }
00415 
00416   }; // end of class VariableManager
00417 
00418 /*****************************************************************************/
00419 /*!
00420  *\class VariableManagerNotifyObj
00421  *\brief Notifies VariableManager before and after each pop()
00422  *
00423  * Author: Sergey Berezin
00424  *
00425  * Created: Tue Mar  1 13:52:28 2005
00426  *
00427  * Disables the deletion of VariableValue objects during context
00428  * restoration (backtracking).  This solves the problem of circular
00429  * dependencies (e.g. a Variable pointing to its antecedent Clause).
00430  */
00431 /*****************************************************************************/
00432   class VariableManagerNotifyObj: public ContextNotifyObj {
00433     VariableManager* d_vm;
00434   public:
00435     //! Constructor
00436   VariableManagerNotifyObj(VariableManager* vm, Context* cxt)
00437     : ContextNotifyObj(cxt), d_vm(vm) { }
00438     
00439     void notifyPre(void) { d_vm->postponeGC(); }
00440     void notify(void) { d_vm->resumeGC(); }
00441   };
00442 
00443 
00444 } // end of namespace CVC3
00445 #endif

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1