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());
44 if (isSatisfied()) cout <<
"*";
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";
51 if (!(*i).isPositive()) cout <<
"-";
52 cout << (*i).getVar();
67 for (i = 0, iend = cnf.
numClauses(); i != iend; ++i) {
69 for (j = cnf[i].begin(), jend = cnf[i].end(); j != jend; ++j) {
76 getCurrentClause().setClauseTheorem(clauseThm);
78 if (cnf[i].isUnit()) registerUnit();
79 if (&(cnf[i]) == cnf.
d_current) c = d_current;
85 void CNF_Formula::print()
const
88 for (i = begin(), iend = end(); i != iend; ++i) {
100 for (i = 0, iend = cnf.
numClauses(); i != iend; ++i) {
102 for (j = cnf[i].begin(), jend = cnf[i].end(); j != jend; ++j) {
106 Clause oldClause = cnf[i];
108 getCurrentClause().setClauseTheorem(clauseThm);
110 if (cnf[i].isUnit()) registerUnit();
122 for (j=c.
begin(), jend = c.
end(); j != jend; ++j) {
128 getCurrentClause().setClauseTheorem(clauseThm);
131 if (c.
isUnit()) registerUnit();
137 void CNF_Formula_Impl::newClause()
139 d_formula.resize(d_formula.size()+1);
140 d_current = &(d_formula.back());
144 void CNF_Formula_Impl::registerUnit()
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;
153 void CNF_Formula_Impl::simplify()
155 deque<Clause>::iterator i, iend;
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) {
165 if (it != d_lits.
end()) {
183 void CD_CNF_Formula::newClause()
186 d_current = &(d_formula.push_back(
Clause()));
190 void CD_CNF_Formula::registerUnit()
192 DebugAssert(d_current->size()==1,
"Expected unit clause");
193 d_current->setUnit();