expr.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr.cpp
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Thu Dec  5 11:35:55 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 #include <algorithm>
00023 
00024 
00025 #include "expr.h"
00026 #include "pretty_printer.h"
00027 #include "expr_stream.h"
00028 #include "notifylist.h"
00029 #include "exception.h"
00030 
00031 
00032 using namespace std;
00033 
00034 
00035 namespace CVC3 {
00036 
00037 
00038 Expr Expr::s_null;
00039 
00040 ///////////////////////////////////////////////////////////////////////
00041 // Class Expr methods                                                //
00042 ///////////////////////////////////////////////////////////////////////
00043 
00044 
00045 Expr Expr::recursiveSubst(const ExprHashMap<Expr>& subst,
00046                           ExprHashMap<Expr>& visited) const {
00047   // Check the cache.
00048   // INVARIANT: visited contains all the flagged expressions, and only those
00049   if(getFlag()) return visited[*this];
00050 
00051   ExprIndex minIndex = 0;
00052   for(ExprHashMap<Expr>::iterator i = subst.begin(),iend=subst.end();i!=iend;++i) {
00053     if(minIndex > (i->first).getIndex())
00054       minIndex = (i->first).getIndex();
00055   }
00056 
00057   Expr replaced;
00058 
00059   if(isClosure()) {
00060     const vector<Expr> & vars = getVars();
00061     vector<Expr> common; // Bound vars which occur in subst
00062 
00063     for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();
00064   i!=iend; ++i) {
00065       if(subst.count(*i) > 0) common.push_back(*i);
00066     }
00067 
00068     if(common.size() > 0) {
00069       IF_DEBUG(debugger.counter("substExpr: bound var clashes")++);
00070       // Reduced substitution (without the common vars)
00071       ExprHashMap<Expr> newSubst(subst);
00072       // Remove variables in "common" from the substitution
00073       for(vector<Expr>::iterator i=common.begin(), iend=common.end();
00074     i!=iend; ++i)
00075   newSubst.erase(*i);
00076 
00077       // Clear all the caches (important!)
00078       visited.clear();
00079       clearFlags();
00080       visited = newSubst;
00081 
00082       ExprHashMap<Expr>::iterator j = newSubst.begin();
00083       for (; j != newSubst.end(); ++j) { // old vars bound in e
00084   j->first.setFlag();
00085       }
00086     
00087       replaced = 
00088   getEM()->newClosureExpr(getKind(), vars,
00089                                 getBody().recursiveSubst(newSubst, visited));
00090 
00091       // Clear the flags again, as we restore the substitution
00092       visited.clear();
00093       clearFlags();
00094       visited = subst;
00095       // Restore the flags on the original substitutions
00096       for (ExprHashMap<Expr>::iterator i = subst.begin(), iend=subst.end();
00097      i != iend; ++i)
00098   i->first.setFlag();
00099     } else {
00100       replaced =
00101         getEM()->newClosureExpr(getKind(), vars,
00102                                 getBody().recursiveSubst(subst, visited));
00103     }
00104   } else { // Not a Closure
00105       int changed=0;
00106       vector<Expr> children;      
00107       for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i){  
00108   Expr repChild = *i;
00109   if(repChild.getIndex() >= minIndex)
00110     repChild = (*i).recursiveSubst(subst, visited);
00111   if(repChild != *i)
00112     changed++;
00113   children.push_back(repChild);
00114       }
00115       if(changed > 0)
00116   replaced = Expr(getOp(), children);
00117       else
00118   replaced = *this;
00119   }
00120   visited.insert(*this, replaced);
00121   setFlag();
00122   return replaced;
00123 }
00124 
00125 
00126 static bool subExprRec(const Expr& e1, const Expr& e2) {
00127   if(e1 == e2) return true;
00128   if(e2.getFlag()) return false;
00129   // e1 is created after e2, so e1 cannot be a subexpr of e2
00130   if(e1 > e2) return false;
00131   e2.setFlag();
00132   bool res(false);
00133   for(Expr::iterator i=e2.begin(), iend=e2.end(); !res && i!=iend; ++i)
00134     res = subExprRec(e1, *i);
00135   return res;
00136 }
00137 
00138 
00139 bool 
00140 Expr::subExprOf(const Expr& e) const {
00141   if(*this == e) return true;
00142   // "this" is created after e, so it cannot be e's subexpression
00143   if(*this > e) return false;
00144   clearFlags();
00145   return subExprRec(*this, e);
00146 }
00147 
00148 
00149 Expr Expr::substExpr(const vector<Expr>& oldTerms,
00150                      const vector<Expr>& newTerms) const
00151 {
00152   DebugAssert(oldTerms.size() == newTerms.size(), "substExpr: vectors"
00153         "don't match in size");
00154   // Catch the vacuous case
00155   if(oldTerms.size() == 0) return *this;
00156 
00157   ExprHashMap<Expr> oldToNew(10);
00158   clearFlags();
00159   for(unsigned int i=0; i<oldTerms.size(); i++) {
00160     oldToNew.insert(oldTerms[i], newTerms[i]);
00161     oldTerms[i].setFlag();
00162   }
00163   // For cache, initialized by the substitution
00164   ExprHashMap<Expr> visited(oldToNew);
00165   return recursiveSubst(oldToNew, visited);
00166 
00167 }
00168 
00169 
00170 Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const
00171 {
00172   // Catch the vacuous case
00173   if(oldToNew.size() == 0) return *this;
00174   // Rebuild the map: we'll be using it as a cache
00175   ExprHashMap<Expr> visited(oldToNew);
00176   clearFlags();
00177   // Flag all the LHS expressions in oldToNew map.  We'll be checking
00178   // all flagged expressions (and only those) for substitution.
00179   for(ExprHashMap<Expr>::iterator i=oldToNew.begin(), iend=oldToNew.end();
00180       i!=iend; ++i) {
00181     (*i).first.setFlag();
00182   }
00183   return recursiveSubst(oldToNew, visited);
00184 }
00185 
00186 
00187 string Expr::toString() const {
00188   return toString(PRESENTATION_LANG);
00189 //   if(isNull()) return "Null";
00190 //   ostringstream ss;
00191 //   ss << (*this);
00192 //   return ss.str();
00193 }
00194 
00195 string Expr::toString(InputLanguage lang) const {
00196   if(isNull()) return "Null";
00197   ostringstream ss;
00198   ExprStream os(getEM());
00199   os.lang(lang);
00200   os.os(ss);
00201   os << (*this);
00202   return ss.str();
00203 }
00204 
00205 void Expr::print(InputLanguage lang, bool dagify) const {
00206   if(isNull()) {
00207     cout << "Null" << endl; return;
00208   }
00209   ExprStream os(getEM());
00210   os.lang(lang);
00211   os.dagFlag(dagify);
00212   os << *this << endl;
00213 }
00214 
00215 
00216 void Expr::pprint() const
00217 {
00218   if(isNull()) {
00219     cout << "Null" << endl; return;
00220   }
00221   ExprStream os(getEM());
00222   os << *this << endl;
00223 }
00224 
00225 
00226 void Expr::pprintnodag() const
00227 {
00228   if(isNull()) {
00229     cout << "Null" << endl; return;
00230   }
00231   ExprStream os(getEM());
00232   os.dagFlag(false);
00233   os << *this << endl;
00234 }
00235 
00236 
00237 void Expr::printnodag() const
00238 {
00239   print(AST_LANG, false);
00240 }
00241 
00242 
00243 ExprStream& Expr::printAST(ExprStream& os) const {
00244   if(isNull()) return os << "Null" << endl;
00245   bool isLetDecl(getKind() == LETDECL);
00246   os << "(" << push;
00247   os << getEM()->getKindName(getKind());
00248   if (isApply()) {
00249     os << space << "{" << getOp().getExpr() << push << "}";
00250   }
00251   else if (isSymbol()) {
00252     os << space << "{Symbol: " << getName() << "}";
00253   }
00254   else if (isClosure()) {
00255     os << space << "{" << space << "(" << push;
00256     const vector<Expr>& vars = getVars();
00257     vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00258     if(i!=iend) { os << *i; ++i; }
00259     for(; i!=iend; ++i) os << space << *i;
00260     os << push << ") " << pop << pop;
00261     os << getBody() << push << "}";
00262   }
00263   else {
00264     switch(getKind()) {
00265       case STRING_EXPR:
00266         DebugAssert(isString(), "Expected String");
00267         os << space << "{" << '"'+ getString() + '"' << "}";
00268         break;
00269       case SKOLEM_VAR:
00270         getExistential();
00271         os << space << "{SKOLEM_" << (int)getIndex() << "}";
00272         break;
00273       case RATIONAL_EXPR:
00274         os << space << "{" << getRational() << "}";
00275         break;
00276       case UCONST: 
00277         DebugAssert(isVar(), "Expected Var");
00278         os << space << "{" << getName() << "}";
00279         break;
00280       case BOUND_VAR:
00281         DebugAssert(isVar(), "Expected Var");
00282         os << space << "{"+getName()+"_"+getUid()+"}";
00283         break;
00284       case THEOREM_KIND:
00285         DebugAssert(isTheorem(), "Expected Theorem");
00286         os << space << "{Theorem: " << getTheorem().toString() << "}";
00287       default: ; // Don't do anything
00288     }
00289   }
00290 
00291   for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) {
00292     if(isLetDecl) os << nodag;
00293     os << space << *i;
00294   }
00295   os << push << ")";
00296   os.resetIndent();
00297   return os;
00298 }
00299 
00300 
00301 ExprStream& Expr::print(ExprStream& os) const {
00302   if(isNull()) return os << "Null" << endl;
00303   DebugAssert(arity() == 0, "Expected arity 0");
00304   if (isSymbol()) return os << getName();
00305   switch(getKind()) {
00306     case TRUE_EXPR: return os << "TRUE";
00307     case FALSE_EXPR: return os << "FALSE";
00308     case NULL_KIND: return os << "Null";
00309     case STRING_EXPR: return os << '"'+ getString() + '"';
00310     case RATIONAL_EXPR: return os << getRational();
00311     case SKOLEM_VAR: return os << "SKOLEM_" <<  hash();
00312     case UCONST: return os << getName();
00313     case BOUND_VAR: return os << "(BOUND_VAR "+getName()+"_"+getUid()+")";
00314     case RAW_LIST: {
00315       os << "(" << push;
00316       bool firstTime(true);
00317       for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) {
00318         if(firstTime) firstTime = false;
00319         else os << space;
00320         os << *i;
00321       }
00322       return os << push << ")";
00323     }
00324     case FORALL:
00325     case EXISTS: 
00326       if(isQuantifier()) {
00327         os << "(" << push << getEM()->getKindName(getKind())
00328            << space << "(" << push;
00329         const vector<Expr>& vars = getVars();
00330         vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00331         if(i!=iend) { os << *i; ++i; }
00332         for(; i!=iend; ++i) os << space << *i;
00333         os << push << ") " << pop << pop;
00334         return os << getBody() << push << ")";
00335       }
00336       // If not an internal representation of quantifiers, it'll be
00337       // printed as "normal" Expr with a kind and children
00338     default:
00339       //    os << "(" << push;
00340       os << getEM()->getKindName(getKind());
00341       //    os << push << ")";
00342   }
00343   os.resetIndent();
00344   return os;
00345 }
00346 
00347 
00348 //! Set initial indentation to n.
00349 /*! The indentation will be reset to default unless the second
00350     argument is true.  This setting only takes effect when printing to
00351     std::ostream.  When printing to ExprStream, the indentation can be
00352     set directly in the ExprStream. */
00353 Expr& Expr::indent(int n, bool permanent) {
00354   DebugAssert(!isNull(), "Expr::indent called on Null Expr");
00355   getEM()->indent(n, permanent);
00356   return *this;
00357 }
00358 
00359 
00360 void Expr::addToNotify(Theory* i, const Expr& e) const {
00361   DebugAssert(!isNull(), "Expr::addToNotify() on Null expr");
00362   if(getNotify() == NULL)
00363     d_expr->d_notifyList = new NotifyList(getEM()->getCurrentContext());
00364   getNotify()->add(i, e);
00365 }
00366 
00367 
00368 bool Expr::isAtomic() const
00369 {
00370   //  TRACE("isAtomic", "isAtomic(", *this, ") {");
00371   if (validIsAtomicFlag()) {
00372     //    TRACE("isAtomic", "isAtomic[cached] => ",
00373     //    getIsAtomicFlag()? "true" : "false", " }");
00374     return getIsAtomicFlag();
00375   }
00376   if (getType().isBool() && !isBoolConst()) {
00377     setIsAtomicFlag(false);
00378     //    TRACE_MSG("isAtomic", "isAtomic[bool] => false }");
00379     return false;
00380   }
00381   for (int k = 0; k < arity(); ++k) {
00382     if (!(*this)[k].isAtomic()) {
00383       setIsAtomicFlag(false);
00384       //      TRACE_MSG("isAtomic", "isAtomic[kid] => false }");
00385       return false;
00386     }
00387   }
00388   setIsAtomicFlag(true);
00389   //  TRACE_MSG("isAtomic", "isAtomic[kid] => true }");
00390   return true;
00391 }
00392 
00393 
00394 bool Expr::isAtomicFormula() const
00395 {
00396   //  TRACE("isAtomic", "isAtomicFormula(", *this, ") {");
00397   if (!getType().isBool()) {
00398     //    TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }");
00399     return false;
00400   }
00401   switch(getKind()) {
00402     case FORALL: case EXISTS: case XOR:
00403     case NOT: case AND: case OR: case ITE: case IFF: case IMPLIES:
00404       //      TRACE_MSG("isAtomic", "isAtomicFormula[connective] => false }");
00405       return false;
00406   }
00407   for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) {
00408     if (!(*k).isAtomic()) {
00409       //      TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }");
00410       return false;
00411     }
00412   }
00413   //  TRACE_MSG("isAtomic", "isAtomicFormula => true }");
00414   return true;
00415 }
00416 
00417 
00418   // This is one of the most friequently called routines.  Make it as
00419   // efficient as possible.
00420 int compare(const Expr& e1, const Expr& e2) {
00421   // Quick equality check (operator== is implemented independently
00422   // and more efficiently)
00423   if(e1 == e2) return 0;
00424     
00425   if(e1.d_expr == NULL) return -1;
00426   if(e2.d_expr == NULL) return 1;
00427   // Both are non-Null.  Compare the indices.
00428   return (e1.getIndex() < e2.getIndex())? -1 : 1;
00429 }
00430 
00431 
00432 ///////////////////////////////////////////////////////////////////////
00433 // Class Expr::iterator methods                                      //
00434 ///////////////////////////////////////////////////////////////////////
00435 
00436 
00437 ostream& operator<<(ostream& os, const Expr& e) {
00438   if(e.isNull()) return os << "Null";
00439   ExprStream es(e.getEM());
00440   es.os(os);
00441   es << e;
00442   e.getEM()->restoreIndent();
00443   return os;
00444 }
00445 
00446 
00447 // Functions from class Type
00448 
00449 
00450 Type::Type(Expr expr) : d_expr(expr)
00451 {
00452   if (expr.isNull()) return;
00453   expr.getEM()->checkType(expr);
00454 }
00455 
00456 
00457 Type Type::funType(const std::vector<Type>& typeDom, const Type& typeRan) {
00458   vector<Expr> tmp;
00459   for(vector<Type>::const_iterator i=typeDom.begin(), iend=typeDom.end();
00460       i!=iend; ++i)
00461     tmp.push_back(i->getExpr());
00462   tmp.push_back(typeRan.getExpr());
00463   return Type(Expr(ARROW, tmp));
00464 }
00465 
00466 
00467 } // end of namespace CVC3

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