assumptions.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file assumptions.cpp
00004  *\brief Implementation of class Assumptions
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Thu Jan  5 06:25:52 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
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   //  TRACE_MSG("assumptions", "findTheorem");
00038 
00039   const Theorem& t = find(e);
00040   if (!t.isNull()) return t;
00041   // recurse
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; // not found
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       // switch to binary search below? (sort es first)
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     
00152   if (!t1.getAssumptionsRef().empty()) {
00153     if (!t2.getAssumptionsRef().empty()) {
00154       switch(compare(t1, t2)) {
00155         case -1: // t1 < t2:
00156           d_vector.push_back(t1);
00157           d_vector.push_back(t2);
00158           break;
00159         case 0: // t1 == t2:
00160           d_vector.push_back(t1);
00161           break;
00162         case 1: // t1 > t2:
00163           d_vector.push_back(t2);
00164           d_vector.push_back(t1);
00165           break;
00166       }
00167     } else d_vector.push_back(t1);
00168   } else if (!t2.getAssumptionsRef().empty()) {
00169     d_vector.push_back(t2);
00170   }
00171   
00172   /*
00173   switch(compare(t1, t2)) {
00174   case -1: // t1 < t2:
00175     d_vector.push_back(t1);
00176     d_vector.push_back(t2);
00177     break;
00178   case 0: // t1 == t2:
00179     d_vector.push_back(t1);
00180     break;
00181   case 1: // t1 > t2:
00182     d_vector.push_back(t2);
00183     d_vector.push_back(t1);
00184     break;
00185   }
00186   */
00187 }
00188 
00189 
00190 void Assumptions::add(const Theorem& t)
00191 {
00192   if (t.getAssumptionsRef().empty()) return;
00193   vector<Theorem>::iterator iter, iend = d_vector.end();
00194   iter = lower_bound(d_vector.begin(), iend, t);
00195   if (iter != iend && compare(t, *iter) == 0) return;
00196   d_vector.insert(iter, t);
00197 }
00198 
00199 
00200 void Assumptions::add(const std::vector<Theorem>& thms)
00201 {
00202   if (thms.size() == 0) return;
00203 
00204 IF_DEBUG(
00205   vector<Theorem>::const_iterator iend = thms.end();
00206   for (vector<Theorem>::const_iterator i = thms.begin(); 
00207        i != iend; ++i) {
00208     if (i+1 == iend) break;
00209     DebugAssert(compare(*i, *(i+1)) == -1, "Expected sorted");
00210   }
00211 )
00212   vector<Theorem> v;
00213   v.reserve(d_vector.size()+thms.size());
00214 
00215   vector<Theorem>::const_iterator i = d_vector.begin();
00216   vector<Theorem>::const_iterator j = thms.begin();
00217   const vector<Theorem>::const_iterator v1end = d_vector.end();
00218   const vector<Theorem>::const_iterator v2end = thms.end();
00219 
00220   // merge
00221   while (i != v1end && j != v2end) {
00222     if (j->getAssumptionsRef().empty()) {
00223       ++j;
00224       continue;
00225     }
00226     switch(compare(*i, *j)) {
00227       case 0:
00228         // copy only 1, drop down to next case
00229         ++j;
00230       case -1: // <
00231         v.push_back(*i);
00232         ++i;
00233         break;
00234       default: // >
00235         v.push_back(*j);
00236         ++j;
00237     };
00238   }
00239   // Push in the remaining elements
00240   for(; i != v1end; ++i) v.push_back(*i);
00241   for(; j != v2end; ++j) {
00242     if (!j->getAssumptionsRef().empty())
00243       v.push_back(*j);
00244   }
00245 
00246   d_vector.swap(v);
00247 }
00248 
00249 
00250 string Assumptions::toString() const {
00251   ostringstream ss;
00252   ss << (*this);
00253   return ss.str();
00254 }
00255 
00256 
00257 void Assumptions::print() const
00258 {
00259   cout << toString() << endl;
00260 }
00261       
00262 
00263 const Theorem& Assumptions::operator[](const Expr& e) const {
00264   if (!d_vector.empty()) {
00265     d_vector.front().clearAllFlags();
00266   }
00267   return findTheorem(e);
00268 }
00269 
00270 
00271 const Theorem& Assumptions::find(const Expr& e) const {
00272   static Theorem null;
00273   //    binary search
00274   int lo = 0; 
00275   int hi = d_vector.size() - 1;
00276   int loc;
00277   while (lo <= hi) {
00278     loc = (lo + hi) / 2;
00279  
00280     switch (compare(d_vector[loc], e)) {
00281       case 0: return d_vector[loc];
00282       case -1: // t < e
00283         lo = loc + 1;
00284         break;
00285       default: // t > e
00286         hi = loc - 1;
00287     };
00288   }
00289   return null;
00290 }
00291 
00292 
00293 ////////////////////////////////////////////////////////////////////
00294 // Assumptions friend methods
00295 ////////////////////////////////////////////////////////////////////
00296 
00297 
00298 namespace CVC3 {
00299 
00300 
00301 Assumptions operator-(const Assumptions& a, const Expr& e) {
00302   if (a.begin() != a.end()) {
00303     a.begin()->clearAllFlags();
00304     vector<Theorem> gamma;
00305     if (Assumptions::findExpr(a, e, gamma)) return Assumptions(gamma);
00306   } 
00307   return a;
00308 }
00309 
00310 
00311 Assumptions operator-(const Assumptions& a, const vector<Expr>& es) {
00312   if (!es.empty() && a.begin() != a.end()) {
00313     a.begin()->clearAllFlags();
00314     vector<Theorem> gamma;
00315     if (Assumptions::findExprs(a, es, gamma)) return Assumptions(gamma);
00316   }
00317   return a;
00318 }
00319 
00320 
00321 ostream& operator<<(ostream& os, const Assumptions &assump) {
00322   vector<Theorem>::const_iterator i = assump.d_vector.begin();
00323   const vector<Theorem>::const_iterator iend = assump.d_vector.end();
00324   if(i != iend) { os << i->getExpr(); i++; }
00325   for(; i != iend; i++) os << ",\n " << i->getExpr();
00326   return os;
00327 }
00328 
00329 
00330 } // end of namespace CVC3

Generated on Wed Nov 18 16:13:28 2009 for CVC3 by  doxygen 1.5.2