34 const Theorem& Assumptions::findTheorem(
const Expr& e)
const {
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()) {
51 if (!iter2->isRefl()) iter2->
setFlag();
59 const Expr& e, vector<Theorem>& gamma) {
63 for (; iter != aend; ++iter) {
64 if (iter->
isRefl())
continue;
82 for (iter = a.
begin(); iter != aend; ++iter) {
83 if (iter->
isRefl())
continue;
92 bool Assumptions::findExprs(
const Assumptions& a,
const vector<Expr>& es,
93 vector<Theorem>& gamma) {
95 const vector<Expr>::const_iterator esbegin = es.begin();
96 const vector<Expr>::const_iterator esend = es.end();
99 for (; iter != aend; ++iter) {
100 if (iter->
isRefl())
continue;
106 if ((::find(esbegin, esend, iter->
getExpr()) != esend) ||
118 for (iter = a.
begin(); iter != aend; ++iter) {
119 if (iter->
isRefl())
continue;
127 Assumptions::Assumptions(
const vector<Theorem>& v) {
128 if (v.empty())
return;
129 d_vector.reserve(v.size());
131 const vector<Theorem>::const_iterator iend = v.end();
132 vector<Theorem>::const_iterator i = v.begin();
134 for (;i != iend; ++i) {
135 if ((!i->getAssumptionsRef().empty())) {
136 d_vector.push_back(*i);
140 if (d_vector.size() <= 1)
return;
141 sort(d_vector.begin(), d_vector.end());
142 vector<Theorem>::iterator newend =
145 d_vector.resize(newend - d_vector.begin());
156 d_vector.push_back(t1);
157 d_vector.push_back(t2);
160 d_vector.push_back(t1);
163 d_vector.push_back(t2);
164 d_vector.push_back(t1);
167 }
else d_vector.push_back(t1);
169 d_vector.push_back(t2);
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);
200 void Assumptions::add(
const std::vector<Theorem>& thms)
202 if (thms.size() == 0)
return;
205 vector<Theorem>::const_iterator iend = thms.end();
206 for (vector<Theorem>::const_iterator i = thms.begin();
208 if (i+1 == iend)
break;
213 v.reserve(d_vector.size()+thms.size());
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();
221 while (i != v1end && j != v2end) {
222 if (j->getAssumptionsRef().empty()) {
240 for(; i != v1end; ++i) v.push_back(*i);
241 for(; j != v2end; ++j) {
242 if (!j->getAssumptionsRef().empty())
250 string Assumptions::toString()
const {
257 void Assumptions::print()
const
259 cout << toString() <<
endl;
264 if (!d_vector.empty()) {
267 return findTheorem(e);
275 int hi = d_vector.size() - 1;
280 switch (
compare(d_vector[loc], e)) {
281 case 0:
return d_vector[loc];
304 vector<Theorem> gamma;
305 if (Assumptions::findExpr(a, e, gamma))
return Assumptions(gamma);
312 if (!es.empty() && a.
begin() != a.
end()) {
314 vector<Theorem> gamma;
315 if (Assumptions::findExprs(a, es, gamma))
return Assumptions(gamma);
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();