00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
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
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
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
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