CVC3  2.4.1
cnf.cpp
Go to the documentation of this file.
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 
30 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 
42 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 
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 
85 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 
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 
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 
137 void CNF_Formula_Impl::newClause()
138 {
139  d_formula.resize(d_formula.size()+1);
140  d_current = &(d_formula.back());
141 }
142 
143 
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 
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 
175 {
176  d_formula.clear();
177  d_lits.clear();
178  d_current = NULL;
179  d_numVars = 0;
180 }
181 
182 
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 
190 void CD_CNF_Formula::registerUnit()
191 {
192  DebugAssert(d_current->size()==1,"Expected unit clause");
193  d_current->setUnit();
194 }
195 
196 
Basic classes for reasoning about formulas in CNF.
const_iterator begin() const
Definition: cnf.h:93
unsigned getMaxVar() const
Definition: cnf.cpp:30
ExprStream & reset(ExprStream &os)
Reset the indentation to the default at this level.
void print() const
Definition: cnf.cpp:42
virtual unsigned numClauses() const =0
int getID() const
Definition: cnf.h:69
T max(T a, T b)
Definition: cvc_util.h:56
std::deque< Clause >::const_iterator const_iterator
Definition: cnf.h:123
#define DebugAssert(cond, str)
Definition: debug.h:408
iterator find(const key_type &key)
operations
Definition: hash_map.h:171
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
CVC3::Theorem getClauseTheorem() const
Definition: cnf.h:108
Clause * d_current
Definition: cnf.h:114
Definition: cnf.h:51
const_iterator end() const
Definition: cnf.h:94
std::vector< Lit >::const_iterator const_iterator
Definition: cnf.h:90
bool isUnit() const
Definition: cnf.h:101
iterator end()
Definition: hash_map.h:257