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
findTheorem(const Expr & e) const34 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
findExpr(const Assumptions & a,const Expr & e,vector<Theorem> & gamma)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
findExprs(const Assumptions & a,const vector<Expr> & es,vector<Theorem> & gamma)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
Assumptions(const vector<Theorem> & v)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
Assumptions(const Theorem & t1,const Theorem & t2)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
add(const Theorem & t)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
add(const std::vector<Theorem> & thms)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
toString() const250 string Assumptions::toString() const {
251 ostringstream ss;
252 ss << (*this);
253 return ss.str();
254 }
255
256
print() const257 void Assumptions::print() const
258 {
259 cout << toString() << endl;
260 }
261
262
operator [](const Expr & e) const263 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
find(const Expr & e) const271 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
operator -(const Assumptions & a,const Expr & e)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
operator -(const Assumptions & a,const vector<Expr> & es)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
operator <<(ostream & os,const Assumptions & assump)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
331