clause.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file clause.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Fri Mar  7 16:03:38 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  * Class to represent a clause, which is a disjunction of formulas
00019  * which are literals for conflict clauses, and possibly more complex
00020  * formulas for the clauses derived from the user-asserted formulas.
00021  * 
00022  * class Clause is implemented as a smart pointer to ClauseValue, so
00023  * it can be freely copied and assigned with low overhead (like
00024  * Theorem or Expr).
00025  */
00026 /*****************************************************************************/
00027 
00028 // Include it before ifndef, since it includes this file recursively
00029 #ifndef DOXYGEN
00030 #include "variable.h"
00031 #endif
00032 
00033 #ifndef _cvc3__include__clause_h_
00034 #define _cvc3__include__clause_h_
00035 
00036 namespace CVC3 {
00037 
00038   class Clause;
00039   class ClauseOwner;
00040   class TheoryCore;
00041 
00042   class ClauseValue {
00043     friend class Clause;
00044   private:
00045     //! Ref. counter
00046     int d_refcount;
00047     //! Ref. counter of ClauseOwner classes holding it
00048     int d_refcountOwner;
00049     // The original clause (disjunction of literals)
00050     Theorem d_thm;
00051     // Scope where the clause is valid
00052     int d_scope;
00053     // Theorems l_i <=> l'_i for each literal l_i
00054     // FIXME: more efficient implementation for fixed arrays of CDOs
00055     std::vector<Literal> d_literals;
00056     // Disallow copy constructor and assignment (make private)
00057     ClauseValue(const ClauseValue& c); // Undefined (since it cannot be used)
00058     ClauseValue& operator=(const ClauseValue& c) { return *this; }
00059     // Pointers to watched literals (Watch Pointers).  They are not
00060     // backtrackable.
00061     size_t d_wp[2];
00062     // Direction flags for the watch pointers (1 or -1)
00063     // FIXME: should we use one bit of d_wp{1,2} instead? (efficiency
00064     // vs. space)
00065     int d_dir[2];
00066     // A flag indicating that the clause is shown satisfiable
00067     CDO<bool> d_sat;
00068     // Marks the clause as deleted
00069     bool d_deleted;
00070     // Creation file and line number (for debugging)
00071     IF_DEBUG(std::string d_file; int d_line);
00072     // Constructor: takes the main clause theorem which must be a
00073     // disjunction of literals and have no assumptions.
00074     ClauseValue(TheoryCore* core, VariableManager* vm,
00075     const Theorem& clause, int scope);
00076   public:
00077     // Destructor
00078     ~ClauseValue();
00079       
00080   }; // end of class ClauseValue
00081 
00082   //! A class representing a CNF clause (a smart pointer)
00083   class Clause {
00084   private:
00085     friend class ClauseOwner;
00086     //! The only value member
00087     ClauseValue* d_clause;
00088     //! Export owner refcounting to ClauseOwner
00089     int& countOwner() {
00090       DebugAssert(d_clause != NULL, "");
00091       return d_clause->d_refcountOwner;
00092     }
00093   public:
00094     Clause(): d_clause(NULL) { }
00095     // Constructors
00096     Clause(TheoryCore* core, VariableManager* vm, const Theorem& clause,
00097            int scope, const std::string& file = "", int line = 0)
00098       : d_clause(new ClauseValue(core, vm, clause, scope)) {
00099       d_clause->d_refcount++;
00100       IF_DEBUG(d_clause->d_file = file; d_clause->d_line=line);
00101     }
00102     // Copy constructor
00103     Clause(const Clause& c): d_clause(c.d_clause) {
00104       if(d_clause != NULL) d_clause->d_refcount++;
00105     }
00106     // Destructor
00107     ~Clause();
00108     // Assignment operator
00109     Clause& operator=(const Clause& c);
00110 
00111     bool isNull() const { return d_clause == NULL; }
00112     // Other public methods
00113     size_t size() const {
00114       return (d_clause == NULL)? 0 : d_clause->d_literals.size();
00115     }
00116     // Get the theorem representing the entire clause
00117     const Theorem& getTheorem() const {
00118       DebugAssert(!isNull(), "Clause::getTheorem(): Null Clause");
00119       return d_clause->d_thm;
00120     }
00121     // Get the scope where the clause is valid
00122     int getScope() const {
00123       if(isNull()) return 0;
00124       else return d_clause->d_scope;
00125     }
00126     // Get the current value of the i-th literal
00127     const Literal& getLiteral(size_t i) const {
00128       DebugAssert(!isNull(), "Clause::getLiteral(): Null Clause");
00129       DebugAssert(i < size(), 
00130       "Clause::getLiteral(" + int2string(i)
00131       + "): i >= size = " + int2string(size()));
00132       return d_clause->d_literals[i];
00133     }
00134     // Get the current value of the i-th literal
00135     const Literal& operator[](size_t i) const { return getLiteral(i); }
00136 
00137     // Get the reference to the vector of literals, for fast access
00138     const std::vector<Literal>& getLiterals() const {
00139       DebugAssert(!isNull(), "Clause::getLiterals(): Null Clause");
00140       return d_clause->d_literals;
00141     }
00142     // Get the values of watch pointers
00143     size_t wp(int i) const {
00144       DebugAssert(!isNull(), "Clause::wp(i): Null Clause");
00145       DebugAssert(i==0 || i==1, 
00146       "wp(i): Watch pointer index is out of bounds: i = "
00147       + int2string(i));
00148       return d_clause->d_wp[i];
00149     }
00150     // Get the watched literals
00151     const Literal& watched(int i) const { return getLiteral(wp(i)); }
00152     // Set the watch pointers and return the new value
00153     size_t wp(int i, size_t l) const {
00154       DebugAssert(!isNull(), "Clause::wp(i,l): Null Clause");
00155       DebugAssert(i==0 || i==1, 
00156       "wp(i,l): Watch pointer index is out of bounds: i = "
00157       + int2string(i));
00158       DebugAssert(l < size(), "Clause::wp(i = " + int2string(i)
00159       + ", l = " + int2string(l)
00160       + "): l >= size() = " + int2string(size()));
00161       TRACE("clauses", " **clauses** UPDATE wp(idx="
00162       +int2string(i)+", l="+int2string(l),
00163       ")\n  clause #: ", id());
00164       d_clause->d_wp[i] = l;
00165       return l;
00166     }
00167     // Get the direction of the i-th watch pointer
00168     int dir(int i) const {
00169       DebugAssert(!isNull(), "Clause::dir(i): Null Clause");
00170       DebugAssert(i==0 || i==1, 
00171       "dir(i): Watch pointer index is out of bounds: i = "
00172       + int2string(i));
00173       return d_clause->d_dir[i];
00174     }
00175     // Set the direction of the i-th watch pointer
00176     int dir(int i, int d) const {
00177       DebugAssert(!isNull(), "Clause::dir(i,d): Null Clause");
00178       DebugAssert(i==0 || i==1, 
00179       "dir(i="+int2string(i)+",d="+int2string(d)
00180       +"): Watch pointer index is out of bounds");
00181       DebugAssert(d==1 || d==-1, "dir(i="+int2string(i)+",d="+int2string(d)
00182       +"): Direction is out of bounds");
00183       d_clause->d_dir[i] = d;
00184       return d;
00185     }
00186     //! Check if the clause marked as SAT
00187     bool sat() const {
00188       DebugAssert(!isNull(), "Clause::sat()");
00189       return d_clause->d_sat;
00190     }
00191     //! Precise version of sat(): check all the literals and cache the result
00192     bool sat(bool ignored) const {
00193       DebugAssert(!isNull(), "Clause::sat()");
00194       bool flag = false;
00195       if (!d_clause->d_sat) {
00196         for (size_t i = 0; !flag && i < d_clause->d_literals.size(); ++i)
00197           if (d_clause->d_literals[i].getValue() == 1)
00198             flag = true;
00199       }
00200       if (flag) {
00201         //std::cout << "*** Manually marking SAT" << std::endl;
00202         markSat();
00203       }
00204       return d_clause->d_sat;
00205     }
00206     // Mark the clause as SAT
00207     void markSat() const {
00208       DebugAssert(!isNull(), "Clause::markSat()");
00209       d_clause->d_sat = true;
00210     }
00211     // Check / mark the clause as deleted
00212     bool deleted() const {
00213       DebugAssert(!isNull(), "Clause::deleted()");
00214       return d_clause->d_deleted;
00215     }
00216     void markDeleted() const;
00217 
00218     // For debugging: return some kind of unique ID
00219     size_t id() const { return (size_t) d_clause; }
00220 
00221     // Equality: compare the pointers
00222     bool operator==(const Clause& c) const { return d_clause == c.d_clause; }
00223 
00224     //! Tell how many owners this clause has (for debugging)
00225     int owners() const { return d_clause->d_refcountOwner; }
00226     
00227     // Printing
00228     std::string toString() const;
00229 
00230     friend std::ostream& operator<<(std::ostream& os, const Clause& c);
00231 
00232     IF_DEBUG(bool wpCheck() const;)
00233     IF_DEBUG(const std::string& getFile() const { return d_clause->d_file; })
00234     IF_DEBUG(int getLine() const { return d_clause->d_line; })
00235 
00236   }; // end of class Clause
00237 
00238   //! Same as class Clause, but when destroyed, marks the clause as deleted
00239   /*! Needed for backtraking data structures.  When the SAT solver
00240     backtracks, some clauses will be thrown away automatically, and we
00241     need to mark those as deleted. */
00242   class ClauseOwner {
00243     Clause d_clause;
00244     //! Disable default constructor
00245     ClauseOwner() { }
00246   public:
00247     //! Constructor from class Clause
00248     ClauseOwner(const Clause& c): d_clause(c) { d_clause.countOwner()++; }
00249     //! Construct a new Clause
00250     ClauseOwner(TheoryCore* core, VariableManager* vm, const Theorem& clause,
00251     int scope): d_clause(core, vm, clause, scope) {
00252       d_clause.countOwner()++;
00253     }
00254     //! Copy constructor (keep track of refcounts)
00255     ClauseOwner(const ClauseOwner& c): d_clause(c.d_clause) {
00256       d_clause.countOwner()++;
00257     }
00258     //! Assignment (keep track of refcounts)
00259     ClauseOwner& operator=(const ClauseOwner& c) {
00260       if(&c == this) return *this; // Seft-assignment
00261       DebugAssert(d_clause.countOwner() > 0, "in operator=");
00262       if(--(d_clause.countOwner()) == 0)
00263   d_clause.markDeleted();
00264       d_clause = c.d_clause;
00265       d_clause.countOwner()++;
00266       return *this;
00267     }
00268     //! Destructor: mark the clause as deleted
00269     ~ClauseOwner() {
00270       FatalAssert(d_clause.countOwner() > 0, "in ~ClauseOwner");
00271       if(--(d_clause.countOwner()) == 0) {
00272   d_clause.markDeleted();
00273       }
00274     }
00275     //! Automatic type conversion to Clause ref
00276     operator Clause& () { return d_clause; }
00277     //! Automatic type conversion to Clause const ref
00278     operator const Clause& () const { return d_clause; }
00279   }; // end of class ClauseOwner
00280     
00281 
00282   // I/O Manipulators
00283 
00284   // Print clause in a compact form: Clause[x=-1@scope, ...], mark
00285   // watched literals by '*'
00286   class CompactClause {
00287   private:
00288     Clause d_clause;
00289   public:
00290     CompactClause(const Clause& c): d_clause(c) { }
00291     friend std::ostream& operator<<(std::ostream& os, const CompactClause& c);
00292     std::string toString() const;
00293   };
00294 
00295 } // end of namespace CVC3
00296     
00297 #endif

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