CVC3  2.4.1
assumptions.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file assumptions.cpp
4  *\brief Implementation of class Assumptions
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Thu Jan 5 06:25:52 2006
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 
23 #include <algorithm>
24 #include "assumptions.h"
25 
26 
27 using namespace std;
28 using namespace CVC3;
29 
30 
31 Assumptions Assumptions::s_empty;
32 
33 
34 const Theorem& Assumptions::findTheorem(const Expr& e) const {
35  static Theorem null;
36 
37  // TRACE_MSG("assumptions", "findTheorem");
38 
39  const Theorem& t = find(e);
40  if (!t.isNull()) return t;
41  // recurse
42  const vector<Theorem>::const_iterator aend = d_vector.end();
43  for (vector<Theorem>::const_iterator iter2 = d_vector.begin();
44  iter2 != aend; ++iter2) {
45  if (iter2->isRefl() || !iter2->isFlagged()) {
46  if (compare(*iter2, e) == 0) return *iter2;
47  if (!iter2->isAssump()) {
48  const Theorem& t = iter2->getAssumptionsRef().findTheorem(e);
49  if (!t.isNull()) return t;
50  }
51  if (!iter2->isRefl()) iter2->setFlag();
52  }
53  }
54  return null; // not found
55 }
56 
57 
58 bool Assumptions::findExpr(const Assumptions& a,
59  const Expr& e, vector<Theorem>& gamma) {
60  bool found = false;
61  const Assumptions::iterator aend = a.end();
62  Assumptions::iterator iter = a.begin();
63  for (; iter != aend; ++iter) {
64  if (iter->isRefl()) continue;
65  if (iter->isFlagged()) {
66  if (iter->getCachedValue()) found = true;
67  }
68  else {
69  if ((iter->getExpr() == e) ||
70  (!iter->isAssump() &&
71  findExpr(iter->getAssumptionsRef(), e, gamma))) {
72  found = true;
73  iter->setCachedValue(true);
74  }
75  else iter->setCachedValue(false);
76 
77  iter->setFlag();
78  }
79  }
80 
81  if (found) {
82  for (iter = a.begin(); iter != aend; ++iter) {
83  if (iter->isRefl()) continue;
84  if (!iter->getCachedValue()) gamma.push_back(*iter);
85  }
86  }
87 
88  return found;
89 }
90 
91 
92 bool Assumptions::findExprs(const Assumptions& a, const vector<Expr>& es,
93  vector<Theorem>& gamma) {
94  bool found = false;
95  const vector<Expr>::const_iterator esbegin = es.begin();
96  const vector<Expr>::const_iterator esend = es.end();
97  const Assumptions::iterator aend = a.end();
98  Assumptions::iterator iter = a.begin();
99  for (; iter != aend; ++iter) {
100  if (iter->isRefl()) continue;
101  else if (iter->isFlagged()) {
102  if (iter->getCachedValue()) found = true;
103  }
104  else {
105  // switch to binary search below? (sort es first)
106  if ((::find(esbegin, esend, iter->getExpr()) != esend) ||
107  (!iter->isAssump() &&
108  findExprs(iter->getAssumptionsRef(), es, gamma))) {
109  found = true;
110  iter->setCachedValue(true);
111  }
112  else iter->setCachedValue(false);
113 
114  iter->setFlag();
115  }
116  }
117  if (found) {
118  for (iter = a.begin(); iter != aend; ++iter) {
119  if (iter->isRefl()) continue;
120  if (!iter->getCachedValue()) gamma.push_back(*iter);
121  }
122  }
123  return found;
124 }
125 
126 
127 Assumptions::Assumptions(const vector<Theorem>& v) {
128  if (v.empty()) return;
129  d_vector.reserve(v.size());
130 
131  const vector<Theorem>::const_iterator iend = v.end();
132  vector<Theorem>::const_iterator i = v.begin();
133 
134  for (;i != iend; ++i) {
135  if ((!i->getAssumptionsRef().empty())) {
136  d_vector.push_back(*i);
137  }
138  }
139 
140  if (d_vector.size() <= 1) return;
141  sort(d_vector.begin(), d_vector.end());
142  vector<Theorem>::iterator newend =
143  unique(d_vector.begin(), d_vector.end(), Theorem::TheoremEq);
144 
145  d_vector.resize(newend - d_vector.begin());
146 }
147 
148 
149 Assumptions::Assumptions(const Theorem& t1, const Theorem& t2)
150 {
151 
152  if (!t1.getAssumptionsRef().empty()) {
153  if (!t2.getAssumptionsRef().empty()) {
154  switch(compare(t1, t2)) {
155  case -1: // t1 < t2:
156  d_vector.push_back(t1);
157  d_vector.push_back(t2);
158  break;
159  case 0: // t1 == t2:
160  d_vector.push_back(t1);
161  break;
162  case 1: // t1 > t2:
163  d_vector.push_back(t2);
164  d_vector.push_back(t1);
165  break;
166  }
167  } else d_vector.push_back(t1);
168  } else if (!t2.getAssumptionsRef().empty()) {
169  d_vector.push_back(t2);
170  }
171 
172  /*
173  switch(compare(t1, t2)) {
174  case -1: // t1 < t2:
175  d_vector.push_back(t1);
176  d_vector.push_back(t2);
177  break;
178  case 0: // t1 == t2:
179  d_vector.push_back(t1);
180  break;
181  case 1: // t1 > t2:
182  d_vector.push_back(t2);
183  d_vector.push_back(t1);
184  break;
185  }
186  */
187 }
188 
189 
190 void Assumptions::add(const Theorem& t)
191 {
192  if (t.getAssumptionsRef().empty()) return;
193  vector<Theorem>::iterator iter, iend = d_vector.end();
194  iter = lower_bound(d_vector.begin(), iend, t);
195  if (iter != iend && compare(t, *iter) == 0) return;
196  d_vector.insert(iter, t);
197 }
198 
199 
200 void Assumptions::add(const std::vector<Theorem>& thms)
201 {
202  if (thms.size() == 0) return;
203 
204 IF_DEBUG(
205  vector<Theorem>::const_iterator iend = thms.end();
206  for (vector<Theorem>::const_iterator i = thms.begin();
207  i != iend; ++i) {
208  if (i+1 == iend) break;
209  DebugAssert(compare(*i, *(i+1)) == -1, "Expected sorted");
210  }
211 )
212  vector<Theorem> v;
213  v.reserve(d_vector.size()+thms.size());
214 
215  vector<Theorem>::const_iterator i = d_vector.begin();
216  vector<Theorem>::const_iterator j = thms.begin();
217  const vector<Theorem>::const_iterator v1end = d_vector.end();
218  const vector<Theorem>::const_iterator v2end = thms.end();
219 
220  // merge
221  while (i != v1end && j != v2end) {
222  if (j->getAssumptionsRef().empty()) {
223  ++j;
224  continue;
225  }
226  switch(compare(*i, *j)) {
227  case 0:
228  // copy only 1, drop down to next case
229  ++j;
230  case -1: // <
231  v.push_back(*i);
232  ++i;
233  break;
234  default: // >
235  v.push_back(*j);
236  ++j;
237  };
238  }
239  // Push in the remaining elements
240  for(; i != v1end; ++i) v.push_back(*i);
241  for(; j != v2end; ++j) {
242  if (!j->getAssumptionsRef().empty())
243  v.push_back(*j);
244  }
245 
246  d_vector.swap(v);
247 }
248 
249 
250 string Assumptions::toString() const {
251  ostringstream ss;
252  ss << (*this);
253  return ss.str();
254 }
255 
256 
257 void Assumptions::print() const
258 {
259  cout << toString() << endl;
260 }
261 
262 
263 const Theorem& Assumptions::operator[](const Expr& e) const {
264  if (!d_vector.empty()) {
265  d_vector.front().clearAllFlags();
266  }
267  return findTheorem(e);
268 }
269 
270 
271 const Theorem& Assumptions::find(const Expr& e) const {
272  static Theorem null;
273  // binary search
274  int lo = 0;
275  int hi = d_vector.size() - 1;
276  int loc;
277  while (lo <= hi) {
278  loc = (lo + hi) / 2;
279 
280  switch (compare(d_vector[loc], e)) {
281  case 0: return d_vector[loc];
282  case -1: // t < e
283  lo = loc + 1;
284  break;
285  default: // t > e
286  hi = loc - 1;
287  };
288  }
289  return null;
290 }
291 
292 
293 ////////////////////////////////////////////////////////////////////
294 // Assumptions friend methods
295 ////////////////////////////////////////////////////////////////////
296 
297 
298 namespace CVC3 {
299 
300 
301 Assumptions operator-(const Assumptions& a, const Expr& e) {
302  if (a.begin() != a.end()) {
303  a.begin()->clearAllFlags();
304  vector<Theorem> gamma;
305  if (Assumptions::findExpr(a, e, gamma)) return Assumptions(gamma);
306  }
307  return a;
308 }
309 
310 
311 Assumptions operator-(const Assumptions& a, const vector<Expr>& es) {
312  if (!es.empty() && a.begin() != a.end()) {
313  a.begin()->clearAllFlags();
314  vector<Theorem> gamma;
315  if (Assumptions::findExprs(a, es, gamma)) return Assumptions(gamma);
316  }
317  return a;
318 }
319 
320 
321 ostream& operator<<(ostream& os, const Assumptions &assump) {
322  vector<Theorem>::const_iterator i = assump.d_vector.begin();
323  const vector<Theorem>::const_iterator iend = assump.d_vector.end();
324  if(i != iend) { os << i->getExpr(); i++; }
325  for(; i != iend; i++) os << ",\n " << i->getExpr();
326  return os;
327 }
328 
329 
330 } // end of namespace CVC3
void setCachedValue(int value) const
Check if the flag attribute is set.
Definition: theorem.cpp:435
Data structure of expressions in CVC3.
Definition: expr.h:133
void clearAllFlags() const
Clear the flag attribute in all the theorems.
Definition: theorem.cpp:422
int compare(const Expr &e1, const Expr &e2)
Definition: expr.cpp:597
bool TheoremEq(const Theorem &t1, const Theorem &t2)
const Theorem & findTheorem(const Expr &e) const
Definition: assumptions.cpp:34
#define DebugAssert(cond, str)
Definition: debug.h:408
iterator end() const
Definition: assumptions.h:152
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
int getCachedValue() const
Check if the flag attribute is set.
Definition: theorem.cpp:441
ostream & operator<<(ostream &os, const Assumptions &assump)
iterator begin() const
Definition: assumptions.h:151
bool isFlagged() const
Check if the flag attribute is set.
Definition: theorem.cpp:416
#define IF_DEBUG(code)
Definition: debug.h:406
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
Assumptions operator-(const Assumptions &a, const vector< Expr > &es)
std::vector< Theorem > d_vector
Definition: assumptions.h:48
bool isRefl() const
Definition: theorem.h:171
bool empty() const
Definition: assumptions.h:95
Iterator for the Assumptions: points to class Theorem.
Definition: assumptions.h:118
bool isAssump() const
Definition: theorem.cpp:395
void setFlag() const
Set the flag attribute.
Definition: theorem.cpp:429