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   if (!t1.getAssumptionsRef().empty()) {
00152     if (!t2.getAssumptionsRef().empty()) {
00153       switch(compare(t1, t2)) {
00154         case -1: // t1 < t2:
00155           d_vector.push_back(t1);
00156           d_vector.push_back(t2);
00157           break;
00158         case 0: // t1 == t2:
00159           d_vector.push_back(t1);
00160           break;
00161         case 1: // t1 > t2:
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   // merge
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         // copy only 1, drop down to next case
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   // Push in the remaining elements
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   //    binary search
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: // t < e
00266         lo = loc + 1;
00267         break;
00268       default: // t > e
00269         hi = loc - 1;
00270     };
00271   }
00272   return null;
00273 }
00274 
00275 
00276 ////////////////////////////////////////////////////////////////////
00277 // Assumptions friend methods
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 } // end of namespace CVC3

Generated on Tue Jul 3 14:33:34 2007 for CVC3 by  doxygen 1.5.1