00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <algorithm>
00024 #include "assumptions.h"
00025
00026
00027 using namespace std;
00028 using namespace CVC3;
00029
00030
00031 Assumptions Assumptions::s_empty;
00032
00033
00034 const Theorem& Assumptions::findTheorem(const Expr& e) const {
00035 static Theorem null;
00036
00037
00038
00039 const Theorem& t = find(e);
00040 if (!t.isNull()) return t;
00041
00042 const vector<Theorem>::const_iterator aend = d_vector.end();
00043 for (vector<Theorem>::const_iterator iter2 = d_vector.begin();
00044 iter2 != aend; ++iter2) {
00045 if (iter2->isRefl() || !iter2->isFlagged()) {
00046 if (compare(*iter2, e) == 0) return *iter2;
00047 if (!iter2->isAssump()) {
00048 const Theorem& t = iter2->getAssumptionsRef().findTheorem(e);
00049 if (!t.isNull()) return t;
00050 }
00051 if (!iter2->isRefl()) iter2->setFlag();
00052 }
00053 }
00054 return null;
00055 }
00056
00057
00058 bool Assumptions::findExpr(const Assumptions& a,
00059 const Expr& e, vector<Theorem>& gamma) {
00060 bool found = false;
00061 const Assumptions::iterator aend = a.end();
00062 Assumptions::iterator iter = a.begin();
00063 for (; iter != aend; ++iter) {
00064 if (iter->isRefl()) continue;
00065 if (iter->isFlagged()) {
00066 if (iter->getCachedValue()) found = true;
00067 }
00068 else {
00069 if ((iter->getExpr() == e) ||
00070 (!iter->isAssump() &&
00071 findExpr(iter->getAssumptionsRef(), e, gamma))) {
00072 found = true;
00073 iter->setCachedValue(true);
00074 }
00075 else iter->setCachedValue(false);
00076
00077 iter->setFlag();
00078 }
00079 }
00080
00081 if (found) {
00082 for (iter = a.begin(); iter != aend; ++iter) {
00083 if (iter->isRefl()) continue;
00084 if (!iter->getCachedValue()) gamma.push_back(*iter);
00085 }
00086 }
00087
00088 return found;
00089 }
00090
00091
00092 bool Assumptions::findExprs(const Assumptions& a, const vector<Expr>& es,
00093 vector<Theorem>& gamma) {
00094 bool found = false;
00095 const vector<Expr>::const_iterator esbegin = es.begin();
00096 const vector<Expr>::const_iterator esend = es.end();
00097 const Assumptions::iterator aend = a.end();
00098 Assumptions::iterator iter = a.begin();
00099 for (; iter != aend; ++iter) {
00100 if (iter->isRefl()) continue;
00101 else if (iter->isFlagged()) {
00102 if (iter->getCachedValue()) found = true;
00103 }
00104 else {
00105
00106 if ((::find(esbegin, esend, iter->getExpr()) != esend) ||
00107 (!iter->isAssump() &&
00108 findExprs(iter->getAssumptionsRef(), es, gamma))) {
00109 found = true;
00110 iter->setCachedValue(true);
00111 }
00112 else iter->setCachedValue(false);
00113
00114 iter->setFlag();
00115 }
00116 }
00117 if (found) {
00118 for (iter = a.begin(); iter != aend; ++iter) {
00119 if (iter->isRefl()) continue;
00120 if (!iter->getCachedValue()) gamma.push_back(*iter);
00121 }
00122 }
00123 return found;
00124 }
00125
00126
00127 Assumptions::Assumptions(const vector<Theorem>& v) {
00128 if (v.empty()) return;
00129 d_vector.reserve(v.size());
00130
00131 const vector<Theorem>::const_iterator iend = v.end();
00132 vector<Theorem>::const_iterator i = v.begin();
00133
00134 for (;i != iend; ++i) {
00135 if ((!i->getAssumptionsRef().empty())) {
00136 d_vector.push_back(*i);
00137 }
00138 }
00139
00140 if (d_vector.size() <= 1) return;
00141 sort(d_vector.begin(), d_vector.end());
00142 vector<Theorem>::iterator newend =
00143 unique(d_vector.begin(), d_vector.end(), Theorem::TheoremEq);
00144
00145 d_vector.resize(newend - d_vector.begin());
00146 }
00147
00148
00149 Assumptions::Assumptions(const Theorem& t1, const Theorem& t2)
00150 {
00151 if (!t1.getAssumptionsRef().empty()) {
00152 if (!t2.getAssumptionsRef().empty()) {
00153 switch(compare(t1, t2)) {
00154 case -1:
00155 d_vector.push_back(t1);
00156 d_vector.push_back(t2);
00157 break;
00158 case 0:
00159 d_vector.push_back(t1);
00160 break;
00161 case 1:
00162 d_vector.push_back(t2);
00163 d_vector.push_back(t1);
00164 break;
00165 }
00166 } else d_vector.push_back(t1);
00167 } else if (!t2.getAssumptionsRef().empty()) {
00168 d_vector.push_back(t2);
00169 }
00170 }
00171
00172
00173 void Assumptions::add(const Theorem& t)
00174 {
00175 if (t.getAssumptionsRef().empty()) return;
00176 vector<Theorem>::iterator iter, iend = d_vector.end();
00177 iter = lower_bound(d_vector.begin(), iend, t);
00178 if (iter != iend && compare(t, *iter) == 0) return;
00179 d_vector.insert(iter, t);
00180 }
00181
00182
00183 void Assumptions::add(const std::vector<Theorem>& thms)
00184 {
00185 if (thms.size() == 0) return;
00186
00187 IF_DEBUG(
00188 vector<Theorem>::const_iterator iend = thms.end();
00189 for (vector<Theorem>::const_iterator i = thms.begin();
00190 i != iend; ++i) {
00191 if (i+1 == iend) break;
00192 DebugAssert(compare(*i, *(i+1)) == -1, "Expected sorted");
00193 }
00194 )
00195 vector<Theorem> v;
00196 v.reserve(d_vector.size()+thms.size());
00197
00198 vector<Theorem>::const_iterator i = d_vector.begin();
00199 vector<Theorem>::const_iterator j = thms.begin();
00200 const vector<Theorem>::const_iterator v1end = d_vector.end();
00201 const vector<Theorem>::const_iterator v2end = thms.end();
00202
00203
00204 while (i != v1end && j != v2end) {
00205 if (j->getAssumptionsRef().empty()) {
00206 ++j;
00207 continue;
00208 }
00209 switch(compare(*i, *j)) {
00210 case 0:
00211
00212 ++j;
00213 case -1:
00214 v.push_back(*i);
00215 ++i;
00216 break;
00217 default:
00218 v.push_back(*j);
00219 ++j;
00220 };
00221 }
00222
00223 for(; i != v1end; ++i) v.push_back(*i);
00224 for(; j != v2end; ++j) {
00225 if (!j->getAssumptionsRef().empty())
00226 v.push_back(*j);
00227 }
00228
00229 d_vector.swap(v);
00230 }
00231
00232
00233 string Assumptions::toString() const {
00234 ostringstream ss;
00235 ss << (*this);
00236 return ss.str();
00237 }
00238
00239
00240 void Assumptions::print() const
00241 {
00242 cout << toString() << endl;
00243 }
00244
00245
00246 const Theorem& Assumptions::operator[](const Expr& e) const {
00247 if (!d_vector.empty()) {
00248 d_vector.front().clearAllFlags();
00249 }
00250 return findTheorem(e);
00251 }
00252
00253
00254 const Theorem& Assumptions::find(const Expr& e) const {
00255 static Theorem null;
00256
00257 int lo = 0;
00258 int hi = d_vector.size() - 1;
00259 int loc;
00260 while (lo <= hi) {
00261 loc = (lo + hi) / 2;
00262
00263 switch (compare(d_vector[loc], e)) {
00264 case 0: return d_vector[loc];
00265 case -1:
00266 lo = loc + 1;
00267 break;
00268 default:
00269 hi = loc - 1;
00270 };
00271 }
00272 return null;
00273 }
00274
00275
00276
00277
00278
00279
00280
00281 namespace CVC3 {
00282
00283
00284 Assumptions operator-(const Assumptions& a, const Expr& e) {
00285 if (a.begin() != a.end()) {
00286 a.begin()->clearAllFlags();
00287 vector<Theorem> gamma;
00288 if (Assumptions::findExpr(a, e, gamma)) return Assumptions(gamma);
00289 }
00290 return a;
00291 }
00292
00293
00294 Assumptions operator-(const Assumptions& a, const vector<Expr>& es) {
00295 if (!es.empty() && a.begin() != a.end()) {
00296 a.begin()->clearAllFlags();
00297 vector<Theorem> gamma;
00298 if (Assumptions::findExprs(a, es, gamma)) return Assumptions(gamma);
00299 }
00300 return a;
00301 }
00302
00303
00304 ostream& operator<<(ostream& os, const Assumptions &assump) {
00305 vector<Theorem>::const_iterator i = assump.d_vector.begin();
00306 const vector<Theorem>::const_iterator iend = assump.d_vector.end();
00307 if(i != iend) { os << i->getExpr(); i++; }
00308 for(; i != iend; i++) os << ",\n " << i->getExpr();
00309 return os;
00310 }
00311
00312
00313 }