cnf.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file cnf.cpp
00004  *\brief Implementation of classes used for generic CNF formulas
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Mon Dec 12 22:16:11 2005
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 "cnf.h"
00023 
00024 
00025 using namespace std;
00026 using namespace CVC3;
00027 using namespace SAT;
00028 
00029 
00030 unsigned SAT::Clause::getMaxVar() const
00031 {
00032   unsigned max = 0;
00033   const_iterator i, iend;
00034   for (i = begin(), iend = end(); i != iend; ++i) {
00035     DebugAssert(!(*i).isNull(), "Null literal found in clause");
00036     if (unsigned((*i).getVar()) > max) max = unsigned((*i).getVar());
00037   }
00038   return max;
00039 }
00040 
00041 
00042 void SAT::Clause::print() const
00043 {
00044   if (isSatisfied()) cout << "*";
00045   const_iterator i, iend;
00046   for (i = begin(), iend = end(); i != iend; ++i) {
00047     if ((*i).isNull()) cout << "NULL";
00048     else if ((*i).isFalse()) cout << "F";
00049     else if ((*i).isTrue()) cout << "T";
00050     else {
00051       if (!(*i).isPositive()) cout << "-";
00052       cout << (*i).getVar();
00053     }
00054     cout << " ";
00055   }
00056   cout << endl;
00057 }
00058 
00059 
00060 void CNF_Formula::copy(const CNF_Formula& cnf)
00061 {
00062   setNumVars(0);
00063   Clause* c = d_current;
00064   // Don't use iterators in case cnf == *this
00065   unsigned i, iend;
00066   Clause::const_iterator j, jend;
00067   for (i = 0, iend = cnf.numClauses(); i != iend; ++i) {
00068     newClause();
00069     for (j = cnf[i].begin(), jend = cnf[i].end(); j != jend; ++j) {
00070       addLiteral(*j);
00071     }
00072     
00073     Clause oldClause = cnf[i];
00074     //    CVC3::Theorem clauseThm = oldClause.getClauseTheorem();
00075     CVC3::Theorem clauseThm = cnf[i].getClauseTheorem();
00076     getCurrentClause().setClauseTheorem(clauseThm);//by yeting
00077     
00078     if (cnf[i].isUnit()) registerUnit();
00079     if (&(cnf[i]) == cnf.d_current) c = d_current;
00080   }
00081   d_current = c;
00082 }
00083 
00084 
00085 void CNF_Formula::print() const
00086 {
00087   const_iterator i, iend;
00088   for (i = begin(), iend = end(); i != iend; ++i) {
00089     (*i).print();
00090   }
00091 }
00092 
00093 
00094 const CNF_Formula& CNF_Formula::operator+=(const CNF_Formula& cnf)
00095 {
00096   Clause* c = d_current;
00097   // Don't use iterators in case cnf == *this
00098   unsigned i, iend;
00099   Clause::const_iterator j, jend;
00100   for (i = 0, iend = cnf.numClauses(); i != iend; ++i) {
00101     newClause();
00102     for (j = cnf[i].begin(), jend = cnf[i].end(); j != jend; ++j) {
00103       addLiteral(*j);
00104     }
00105 
00106     Clause oldClause = cnf[i];
00107     CVC3::Theorem clauseThm = oldClause.getClauseTheorem();
00108     getCurrentClause().setClauseTheorem(clauseThm);//by yeting
00109 
00110     if (cnf[i].isUnit()) registerUnit();
00111   }
00112   d_current = c;
00113   return *this;
00114 }
00115 
00116 
00117 const CNF_Formula& CNF_Formula::operator+=(const Clause& c)
00118 {
00119   Clause* cur = d_current;
00120   newClause();
00121   Clause::const_iterator j, jend;
00122   for (j=c.begin(), jend = c.end(); j != jend; ++j) {
00123     addLiteral(*j);
00124   }
00125 
00126   Clause oldClause = c;
00127   CVC3::Theorem clauseThm = oldClause.getClauseTheorem();
00128   getCurrentClause().setClauseTheorem(clauseThm);//by yeting
00129     
00130 
00131   if (c.isUnit()) registerUnit();
00132   d_current = cur; 
00133   return *this;
00134 }
00135 
00136 
00137 void CNF_Formula_Impl::newClause()
00138 {
00139   d_formula.resize(d_formula.size()+1);
00140   d_current = &(d_formula.back());
00141 }
00142 
00143 
00144 void CNF_Formula_Impl::registerUnit()
00145 {
00146   DebugAssert(d_current->size()==1,"Expected unit clause");
00147   d_current->setUnit();
00148   Lit l = *(d_current->begin());
00149   d_lits[l.getID()] = true;
00150 }
00151 
00152 
00153 void CNF_Formula_Impl::simplify()
00154 {
00155   deque<Clause>::iterator i, iend;
00156   Clause::const_iterator j, jend;
00157   for (i = d_formula.begin(), iend = d_formula.end(); i != iend; ++i) {
00158     if ((*i).isUnit()) continue;
00159     for (j=(*i).begin(), jend = (*i).end(); j != jend; ++j) {
00160       if ((*j).isTrue()) {
00161         (*i).setSatisfied();
00162         break;
00163       }
00164       hash_map<int, bool>::iterator it = d_lits.find((*j).getID());
00165       if (it != d_lits.end()) {
00166         (*i).setSatisfied();
00167         break;
00168       }
00169     }
00170   }
00171 }
00172 
00173 
00174 void CNF_Formula_Impl::reset()
00175 {
00176   d_formula.clear();
00177   d_lits.clear();
00178   d_current = NULL;
00179   d_numVars = 0;
00180 }
00181 
00182 
00183 void CD_CNF_Formula::newClause()
00184 {
00185   //TODO: don't call constructor twice
00186   d_current = &(d_formula.push_back(Clause()));
00187 }
00188 
00189 
00190 void CD_CNF_Formula::registerUnit()
00191 {
00192   DebugAssert(d_current->size()==1,"Expected unit clause");
00193   d_current->setUnit();
00194 }
00195 
00196 

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