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();
void setCachedValue(int value) const
Check if the flag attribute is set.
Data structure of expressions in CVC3.
void clearAllFlags() const
Clear the flag attribute in all the theorems.
int compare(const Expr &e1, const Expr &e2)
bool TheoremEq(const Theorem &t1, const Theorem &t2)
const Theorem & findTheorem(const Expr &e) const
#define DebugAssert(cond, str)
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
int getCachedValue() const
Check if the flag attribute is set.
ostream & operator<<(ostream &os, const Assumptions &assump)
bool isFlagged() const
Check if the flag attribute is set.
const Assumptions & getAssumptionsRef() const
Assumptions operator-(const Assumptions &a, const vector< Expr > &es)
std::vector< Theorem > d_vector
Iterator for the Assumptions: points to class Theorem.
void setFlag() const
Set the flag attribute.