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     if (cnf[i].isUnit()) registerUnit();
00073     if (&(cnf[i]) == cnf.d_current) c = d_current;
00074   }
00075   d_current = c;
00076 }
00077 
00078 
00079 void CNF_Formula::print() const
00080 {
00081   const_iterator i, iend;
00082   for (i = begin(), iend = end(); i != iend; ++i) {
00083     (*i).print();
00084   }
00085 }
00086 
00087 
00088 const CNF_Formula& CNF_Formula::operator+=(const CNF_Formula& cnf)
00089 {
00090   Clause* c = d_current;
00091   // Don't use iterators in case cnf == *this
00092   unsigned i, iend;
00093   Clause::const_iterator j, jend;
00094   for (i = 0, iend = cnf.numClauses(); i != iend; ++i) {
00095     newClause();
00096     for (j = cnf[i].begin(), jend = cnf[i].end(); j != jend; ++j) {
00097       addLiteral(*j);
00098     }
00099     if (cnf[i].isUnit()) registerUnit();
00100   }
00101   d_current = c;
00102   return *this;
00103 }
00104 
00105 
00106 const CNF_Formula& CNF_Formula::operator+=(const Clause& c)
00107 {
00108   Clause* cur = d_current;
00109   newClause();
00110   Clause::const_iterator j, jend;
00111   for (j=c.begin(), jend = c.end(); j != jend; ++j) {
00112     addLiteral(*j);
00113   }
00114   if (c.isUnit()) registerUnit();
00115   d_current = cur;
00116   return *this;
00117 }
00118 
00119 
00120 void CNF_Formula_Impl::newClause()
00121 {
00122   d_formula.resize(d_formula.size()+1);
00123   d_current = &(d_formula.back());
00124 }
00125 
00126 
00127 void CNF_Formula_Impl::registerUnit()
00128 {
00129   DebugAssert(d_current->size()==1,"Expected unit clause");
00130   d_current->setUnit();
00131   Lit l = *(d_current->begin());
00132   d_lits[l.getID()] = true;
00133 }
00134 
00135 
00136 void CNF_Formula_Impl::simplify()
00137 {
00138   deque<Clause>::iterator i, iend;
00139   Clause::const_iterator j, jend;
00140   for (i = d_formula.begin(), iend = d_formula.end(); i != iend; ++i) {
00141     if ((*i).isUnit()) continue;
00142     for (j=(*i).begin(), jend = (*i).end(); j != jend; ++j) {
00143       if ((*j).isTrue()) {
00144         (*i).setSatisfied();
00145         break;
00146       }
00147       hash_map<int, bool>::iterator it = d_lits.find((*j).getID());
00148       if (it != d_lits.end()) {
00149         (*i).setSatisfied();
00150         break;
00151       }
00152     }
00153   }
00154 }
00155 
00156 
00157 void CNF_Formula_Impl::reset()
00158 {
00159   d_formula.clear();
00160   d_lits.clear();
00161   d_current = NULL;
00162   d_numVars = 0;
00163 }
00164 
00165 
00166 void CD_CNF_Formula::newClause()
00167 {
00168   //TODO: don't call constructor twice
00169   d_current = &(d_formula.push_back(Clause()));
00170 }
00171 
00172 
00173 void CD_CNF_Formula::registerUnit()
00174 {
00175   DebugAssert(d_current->size()==1,"Expected unit clause");
00176   d_current->setUnit();
00177 }
00178 
00179 

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