1 /*****************************************************************************/
2 /*!
3 *\file cnf.cpp
4 *\brief Implementation of classes used for generic CNF formulas
5 *
6 * Author: Clark Barrett
7 *
8 * Created: Mon Dec 12 22:16:11 2005
9 *
10 * <hr>
11 *
12 * License to use, copy, modify, sell and/or distribute this software
13 * and its documentation for any purpose is hereby granted without
14 * royalty, subject to the terms and conditions defined in the \ref
15 * LICENSE file provided with this distribution.
16 *
17 * <hr>
18 */
19 /*****************************************************************************/
20
21
22 #include "cnf.h"
23
24
25 using namespace std;
26 using namespace CVC3;
27 using namespace SAT;
28
29
getMaxVar() const30 unsigned SAT::Clause::getMaxVar() const
31 {
32 unsigned max = 0;
33 const_iterator i, iend;
34 for (i = begin(), iend = end(); i != iend; ++i) {
35 DebugAssert(!(*i).isNull(), "Null literal found in clause");
36 if (unsigned((*i).getVar()) > max) max = unsigned((*i).getVar());
37 }
38 return max;
39 }
40
41
print() const42 void SAT::Clause::print() const
43 {
44 if (isSatisfied()) cout << "*";
45 const_iterator i, iend;
46 for (i = begin(), iend = end(); i != iend; ++i) {
47 if ((*i).isNull()) cout << "NULL";
48 else if ((*i).isFalse()) cout << "F";
49 else if ((*i).isTrue()) cout << "T";
50 else {
51 if (!(*i).isPositive()) cout << "-";
52 cout << (*i).getVar();
53 }
54 cout << " ";
55 }
56 cout << endl;
57 }
58
59
copy(const CNF_Formula & cnf)60 void CNF_Formula::copy(const CNF_Formula& cnf)
61 {
62 setNumVars(0);
63 Clause* c = d_current;
64 // Don't use iterators in case cnf == *this
65 unsigned i, iend;
66 Clause::const_iterator j, jend;
67 for (i = 0, iend = cnf.numClauses(); i != iend; ++i) {
68 newClause();
69 for (j = cnf[i].begin(), jend = cnf[i].end(); j != jend; ++j) {
70 addLiteral(*j);
71 }
72
73 Clause oldClause = cnf[i];
74 // CVC3::Theorem clauseThm = oldClause.getClauseTheorem();
75 CVC3::Theorem clauseThm = cnf[i].getClauseTheorem();
76 getCurrentClause().setClauseTheorem(clauseThm);//by yeting
77
78 if (cnf[i].isUnit()) registerUnit();
79 if (&(cnf[i]) == cnf.d_current) c = d_current;
80 }
81 d_current = c;
82 }
83
84
print() const85 void CNF_Formula::print() const
86 {
87 const_iterator i, iend;
88 for (i = begin(), iend = end(); i != iend; ++i) {
89 (*i).print();
90 }
91 }
92
93
operator +=(const CNF_Formula & cnf)94 const CNF_Formula& CNF_Formula::operator+=(const CNF_Formula& cnf)
95 {
96 Clause* c = d_current;
97 // Don't use iterators in case cnf == *this
98 unsigned i, iend;
99 Clause::const_iterator j, jend;
100 for (i = 0, iend = cnf.numClauses(); i != iend; ++i) {
101 newClause();
102 for (j = cnf[i].begin(), jend = cnf[i].end(); j != jend; ++j) {
103 addLiteral(*j);
104 }
105
106 Clause oldClause = cnf[i];
107 CVC3::Theorem clauseThm = oldClause.getClauseTheorem();
108 getCurrentClause().setClauseTheorem(clauseThm);//by yeting
109
110 if (cnf[i].isUnit()) registerUnit();
111 }
112 d_current = c;
113 return *this;
114 }
115
116
operator +=(const Clause & c)117 const CNF_Formula& CNF_Formula::operator+=(const Clause& c)
118 {
119 Clause* cur = d_current;
120 newClause();
121 Clause::const_iterator j, jend;
122 for (j=c.begin(), jend = c.end(); j != jend; ++j) {
123 addLiteral(*j);
124 }
125
126 Clause oldClause = c;
127 CVC3::Theorem clauseThm = oldClause.getClauseTheorem();
128 getCurrentClause().setClauseTheorem(clauseThm);//by yeting
129
130
131 if (c.isUnit()) registerUnit();
132 d_current = cur;
133 return *this;
134 }
135
136
newClause()137 void CNF_Formula_Impl::newClause()
138 {
139 d_formula.resize(d_formula.size()+1);
140 d_current = &(d_formula.back());
141 }
142
143
registerUnit()144 void CNF_Formula_Impl::registerUnit()
145 {
146 DebugAssert(d_current->size()==1,"Expected unit clause");
147 d_current->setUnit();
148 Lit l = *(d_current->begin());
149 d_lits[l.getID()] = true;
150 }
151
152
simplify()153 void CNF_Formula_Impl::simplify()
154 {
155 deque<Clause>::iterator i, iend;
156 Clause::const_iterator j, jend;
157 for (i = d_formula.begin(), iend = d_formula.end(); i != iend; ++i) {
158 if ((*i).isUnit()) continue;
159 for (j=(*i).begin(), jend = (*i).end(); j != jend; ++j) {
160 if ((*j).isTrue()) {
161 (*i).setSatisfied();
162 break;
163 }
164 hash_map<int, bool>::iterator it = d_lits.find((*j).getID());
165 if (it != d_lits.end()) {
166 (*i).setSatisfied();
167 break;
168 }
169 }
170 }
171 }
172
173
reset()174 void CNF_Formula_Impl::reset()
175 {
176 d_formula.clear();
177 d_lits.clear();
178 d_current = NULL;
179 d_numVars = 0;
180 }
181
182
newClause()183 void CD_CNF_Formula::newClause()
184 {
185 //TODO: don't call constructor twice
186 d_current = &(d_formula.push_back(Clause()));
187 }
188
189
registerUnit()190 void CD_CNF_Formula::registerUnit()
191 {
192 DebugAssert(d_current->size()==1,"Expected unit clause");
193 d_current->setUnit();
194 }
195
196
197