clause.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file clause.cpp
00004  * \brief Implementation of class Clause
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Mon Apr 28 17:20:23 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 "clause.h"
00023 #include "theory_core.h"
00024 
00025 using namespace std;
00026 
00027 namespace CVC3 {
00028 
00029 ////////////////////////////////////////////////////////////////////////
00030 //  class ClauseValue methods
00031 ////////////////////////////////////////////////////////////////////////
00032 
00033 // Constructor: takes the main clause theorem which must be a
00034 // disjunction of literals and have no assumptions.
00035 ClauseValue::ClauseValue(TheoryCore* core, VariableManager* vm,
00036        const Theorem& clause, int scope)
00037   : d_refcount(0), d_refcountOwner(0), d_thm(clause), d_scope(scope),
00038     // This backtrackable member is initialized in the first scope
00039     // (which is #0)
00040     d_sat(core->getCM()->getCurrentContext(), false, 0),
00041     d_deleted(false) {
00042   // Check the clause
00043   DebugAssert(clause.getExpr().isOr(), "Clause(): bad clause given: "
00044         + clause.toString());
00045 //   DebugAssert(clause.getExpr().arity()>0, "Clause(): empty clause: "
00046 //        + clause.toString());
00047   // Initialize watched literals to the edges with directions
00048   // pointing outwards
00049   d_wp[0]=0; d_dir[0]=-1;
00050   d_wp[1] = clause.getExpr().arity()-1; d_dir[1]=1;
00051   // Initialize the literals
00052   Expr c(clause.getExpr());
00053   d_literals.reserve(c.arity());
00054   for(Expr::iterator i=c.begin(), iend=c.end(); i!=iend; ++i) {
00055     int val(i->isNot()? -1 : 1);
00056     Variable v(vm, (val < 0)? (*i)[0] : (*i));
00057     Literal l(v, val > 0);
00058     d_literals.push_back(l);
00059     // Update the literal's count for splitter heuristics
00060     l.count()++;
00061   }
00062   IF_DEBUG(d_sat.setName("CDO[Clause.d_sat]");)
00063 }
00064 
00065 ClauseValue::~ClauseValue() {
00066   TRACE_MSG("search literals", "~ClauseValue() {");
00067   FatalAssert(d_refcount == 0, "~ClauseValue: non-zero refcount: "
00068          + int2string(d_refcount));
00069   if(!d_deleted) { // Update the literal counts for splitter heuristics
00070     for(vector<Literal>::iterator i=d_literals.begin(),
00071     iend=d_literals.end(); i!=iend; ++i) {
00072       i->count()--;
00073       IF_DEBUG(if(i->count() == 0)
00074          TRACE("search literals", "Null count for ", *i, "");)
00075     }
00076   }
00077   TRACE_MSG("search literals", "~ClauseValue() => }");
00078 }
00079   
00080 ////////////////////////////////////////////////////////////////////////
00081 //  class Clause methods
00082 ////////////////////////////////////////////////////////////////////////
00083 
00084 // Destructor
00085 Clause::~Clause() {
00086   if(d_clause != NULL) {
00087     FatalAssert(d_clause->d_refcount > 0,
00088     "~Clause: non-positive refcount: "
00089     + int2string(d_clause->d_refcount));
00090     if(--(d_clause->d_refcount) == 0) delete d_clause;
00091   }
00092 }
00093 
00094 
00095 void
00096 Clause::markDeleted() const {
00097   TRACE("search literals", "Clause::markDeleted(",
00098   CompactClause(*this), ") {");
00099   DebugAssert(!isNull(), "Clause::markDeleted()");
00100   if(!d_clause->d_deleted) {
00101     d_clause->d_deleted = true;
00102     // Update the literal counts for splitter heuristics
00103     for(vector<Literal>::iterator i=d_clause->d_literals.begin(),
00104     iend=d_clause->d_literals.end(); i!=iend; ++i) {
00105       i->count()--;
00106       IF_DEBUG(if(i->count() == 0)
00107          TRACE("search literals", "Null count for ", *i, "");)
00108     }
00109   }
00110   TRACE_MSG("search literals", "Clause::markDeleted => }");
00111 }
00112 
00113 
00114 // Assignment operator
00115 Clause& Clause::operator=(const Clause& c) {
00116   if(&c == this) return *this; // Self-assignment
00117   if(d_clause != NULL) {
00118     DebugAssert(d_clause->d_refcount > 0,
00119     "Clause::operator=: non-positive refcount: "
00120     + int2string(d_clause->d_refcount));
00121     if(--(d_clause->d_refcount) == 0) delete d_clause;
00122   }
00123   d_clause = c.d_clause;
00124   if(d_clause != NULL) d_clause->d_refcount++;
00125   return *this;
00126 }
00127 
00128 // Printing
00129 string Clause::toString() const {
00130   std::ostringstream ss;
00131   ss << *this;
00132   return ss.str();
00133 }
00134 
00135 ostream& operator<<(ostream& os, const Clause& c) {
00136   if(c.isNull()) return os << "Clause[Null]";
00137   os << "Clause[";
00138   if(c.deleted()) os << "DELETED ";
00139   os << c.id();
00140   IF_DEBUG(if(c.getFile() != "")
00141      os << ", " << c.getFile() << ":" << c.getLine();)
00142   os << "](" << c.getTheorem()
00143      << ";\n";
00144   if(c.wp(0) == c.wp(1)) os << "WARNING: wp[0] = wp[1]\n";
00145   for(unsigned i=0; i<c.size(); ++i) {
00146     if(c.wp(0) == i)
00147       os << "wp[0]" << ((c.dir(0) > 0)? "=>" : "<=") << " ";
00148     else if(c.wp(1) == i)
00149       os << "wp[1]" << ((c.dir(1) > 0)? "=>" : "<=") << " ";
00150     else
00151       os << "        ";
00152     os << c[i] << ";\n";
00153   }
00154   return os << ((c.sat())? "Clause is SAT" : "") << ")";
00155 }
00156   
00157   static void printLit(ostream& os, const Literal& l) {
00158     if(l.isNegative()) os << "!";
00159     os << l.getVar().getExpr();
00160     int val(l.getValue());
00161     if(val != 0) os << "=" << val << "@" << l.getScope();
00162   }
00163 
00164 ostream& operator<<(std::ostream& os, const CompactClause& c) {
00165   const vector<Literal>& lits = c.d_clause.getLiterals();
00166   int wp0(c.d_clause.wp(0)), wp1(c.d_clause.wp(1));
00167   int i=0, iend=c.d_clause.size();
00168   os << "Clause[";
00169   if(c.d_clause.deleted()) os << "*DELETED* ";
00170   if(c.d_clause.owners() > 0) os << "owned(" << c.d_clause.owners() << ") ";
00171   if(i!=iend) {
00172     if(i==wp0 || i==wp1) os << "*";
00173     printLit(os, lits[i]);  ++i; 
00174   }
00175   for(; i!=iend; ++i) {
00176     os << ", ";
00177     if(i==wp0 || i==wp1) os << "*";
00178     printLit(os, lits[i]);
00179   }
00180   os << "]";
00181   return os;
00182 }
00183 
00184 string CompactClause::toString() const {
00185   ostringstream ss;
00186   ss << (*this);
00187   return ss.str();
00188 }
00189 
00190 #ifdef _CVC3_DEBUG_MODE
00191 bool CVC3::Clause::wpCheck() const
00192 {
00193   if (sat(true))
00194     return true;
00195   return (getLiteral(wp(0)).getValue() == 0 && getLiteral(wp(1)).getValue() == 0);
00196 }
00197 #endif
00198 
00199 } // end of namespace CVC3

Generated on Wed Nov 18 16:13:29 2009 for CVC3 by  doxygen 1.5.2