CVC3

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 vector<vector<Expr> > Expr::substTriggers(const ExprHashMap<Expr> & subst,
00045       ExprHashMap<Expr> & visited) const {
00046     /* Do the substitution in triggers */
00047     vector<vector<Expr> > vvOldTriggers(getTriggers());
00048     vector<vector<Expr> > vvNewTriggers;
00049     vector<vector<Expr> >::const_iterator i, iEnd;
00050     for( i = vvOldTriggers.begin(), iEnd = vvOldTriggers.end(); i != iEnd; ++i ) {
00051       vector<Expr> vOldTriggers(*i);
00052       vector<Expr> vNewTriggers;
00053       vector<Expr>::const_iterator j, jEnd;
00054       for( j = vOldTriggers.begin(), jEnd = vOldTriggers.end(); j != jEnd; ++j ) {
00055         vNewTriggers.push_back((*j).recursiveSubst(subst, visited));
00056       }
00057       vvNewTriggers.push_back(vNewTriggers);
00058     }
00059 
00060     return vvNewTriggers;
00061 }
00062 
00063 Expr Expr::recursiveSubst(const ExprHashMap<Expr>& subst,
00064                           ExprHashMap<Expr>& visited) const {
00065   // Check the cache.
00066   // INVARIANT: visited contains all the flagged expressions, and only those
00067   if(getFlag()) return visited[*this];
00068 
00069   ExprIndex minIndex = 0;
00070   for(ExprHashMap<Expr>::const_iterator i = subst.begin(),iend=subst.end();i!=iend;++i) {
00071     if(minIndex > (i->first).getIndex())
00072       minIndex = (i->first).getIndex();
00073   }
00074 
00075   Expr replaced;
00076 
00077   if(isClosure()) {
00078     const vector<Expr> & vars = getVars();
00079     vector<Expr> common; // Bound vars which occur in subst
00080 
00081     for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();
00082   i!=iend; ++i) {
00083       if(subst.count(*i) > 0) common.push_back(*i);
00084     }
00085 
00086     if(common.size() > 0) {
00087       IF_DEBUG(debugger.counter("substExpr: bound var clashes")++;)
00088       // Reduced substitution (without the common vars)
00089       ExprHashMap<Expr> newSubst(subst);
00090       // Remove variables in "common" from the substitution
00091       for(vector<Expr>::iterator i=common.begin(), iend=common.end();
00092     i!=iend; ++i)
00093   newSubst.erase(*i);
00094 
00095       // Clear all the caches (important!)
00096       visited.clear();
00097       clearFlags();
00098       visited = newSubst;
00099 
00100       ExprHashMap<Expr>::iterator j = newSubst.begin();
00101       for (; j != newSubst.end(); ++j) { // old vars bound in e
00102   j->first.setFlag();
00103       }
00104     
00105       vector<vector<Expr> > vvNewTriggers = substTriggers(newSubst,visited);
00106 
00107       replaced = 
00108   getEM()->newClosureExpr(getKind(), vars,
00109                                 getBody().recursiveSubst(newSubst, visited),
00110                                 vvNewTriggers);
00111 
00112       // Clear the flags again, as we restore the substitution
00113       visited.clear();
00114       clearFlags();
00115       visited = subst;
00116       // Restore the flags on the original substitutions
00117       for (ExprHashMap<Expr>::const_iterator i = subst.begin(), iend=subst.end();
00118      i != iend; ++i)
00119   i->first.setFlag();
00120     } else {
00121       vector<vector<Expr> > vvNewTriggers = substTriggers(subst,visited);
00122       replaced =
00123         getEM()->newClosureExpr(getKind(), vars,
00124                                 getBody().recursiveSubst(subst, visited),
00125                                 vvNewTriggers);
00126     }
00127   } else { // Not a Closure
00128     int changed=0;
00129     vector<Expr> children;      
00130     for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i){  
00131       Expr repChild = *i;
00132       if(repChild.getIndex() >= minIndex)
00133         repChild = (*i).recursiveSubst(subst, visited);
00134       if(repChild != *i)
00135         changed++;
00136       children.push_back(repChild);
00137     }
00138     Expr opExpr;
00139     if (isApply()) {
00140       opExpr = getOpExpr().recursiveSubst(subst, visited);
00141       if (opExpr != getOpExpr()) ++changed;
00142     }
00143     if(changed > 0) {
00144       Op op = opExpr.isNull() ? getOp() : opExpr.mkOp();
00145       replaced = Expr(op, children);
00146     }
00147     else replaced = *this;
00148   }
00149   visited.insert(*this, replaced);
00150   setFlag();
00151   return replaced;
00152 }
00153 
00154 
00155 static bool subExprRec(const Expr& e1, const Expr& e2) {
00156   if(e1 == e2) return true;
00157   if(e2.getFlag()) return false;
00158   // e1 is created after e2, so e1 cannot be a subexpr of e2
00159   if(e1 > e2) return false;
00160   e2.setFlag();
00161   bool res(false);
00162   for(Expr::iterator i=e2.begin(), iend=e2.end(); !res && i!=iend; ++i)
00163     res = subExprRec(e1, *i);
00164   return res;
00165 }
00166 
00167 
00168 bool 
00169 Expr::subExprOf(const Expr& e) const {
00170   if(*this == e) return true;
00171   // "this" is created after e, so it cannot be e's subexpression
00172   if(*this > e) return false;
00173   clearFlags();
00174   return subExprRec(*this, e);
00175 }
00176 
00177 
00178 Expr Expr::substExpr(const vector<Expr>& oldTerms,
00179                      const vector<Expr>& newTerms) const
00180 {
00181   DebugAssert(oldTerms.size() == newTerms.size(), "substExpr: vectors"
00182         "don't match in size");
00183   // Catch the vacuous case
00184   if(oldTerms.size() == 0) return *this;
00185 
00186   ExprHashMap<Expr> oldToNew(10);
00187   clearFlags();
00188   for(unsigned int i=0; i<oldTerms.size(); i++) {
00189     oldToNew.insert(oldTerms[i], newTerms[i]);
00190     oldTerms[i].setFlag();
00191   }
00192   // For cache, initialized by the substitution
00193   ExprHashMap<Expr> visited(oldToNew);
00194   return recursiveSubst(oldToNew, visited);
00195 
00196 }
00197 
00198 
00199 Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const
00200 {
00201   // Catch the vacuous case
00202   if(oldToNew.size() == 0) return *this;
00203   // Rebuild the map: we'll be using it as a cache
00204   ExprHashMap<Expr> visited(oldToNew);
00205   clearFlags();
00206   // Flag all the LHS expressions in oldToNew map.  We'll be checking
00207   // all flagged expressions (and only those) for substitution.
00208   for(ExprHashMap<Expr>::const_iterator i=oldToNew.begin(), iend=oldToNew.end();
00209       i!=iend; ++i) {
00210     (*i).first.setFlag();
00211   }
00212   return recursiveSubst(oldToNew, visited);
00213 }
00214 
00215 
00216 
00217 Expr Expr::substExprQuant(const vector<Expr>& oldTerms,
00218         const vector<Expr>& newTerms) const
00219 {
00220   //let us disable this first yeting
00221   //  static ExprHashMap<Expr> substCache;
00222   //  Expr cacheIndex = Expr(RAW_LIST, *this, Expr(RAW_LIST, newTerms));
00223 
00224   //  ExprHashMap<Expr>::iterator i = substCache.find(cacheIndex);
00225   //  if (i != substCache.end()){
00226   //    return i->second;
00227   //  }
00228 
00229   DebugAssert(oldTerms.size() == newTerms.size(), "substExpr: vectors"
00230         "don't match in size");
00231   // Catch the vacuous case
00232   
00233   if(oldTerms.size() == 0) return *this;
00234 
00235   ExprHashMap<Expr> oldToNew(oldTerms.size());
00236 
00237   //  clearFlags();
00238   for(unsigned int i=0; i<oldTerms.size(); i++) {
00239     oldToNew.insert(oldTerms[i], newTerms[i]);
00240     //     oldTerms[i].setFlag();
00241   }
00242 
00243   // For cache, initialized by the substitution
00244   ExprHashMap<Expr> visited(oldToNew);
00245   Expr returnExpr = recursiveQuantSubst(oldToNew, visited);;
00246 
00247   //  substCache[cacheIndex] = returnExpr;
00248   //  cout<<"pushed " << cacheIndex << endl << "RET " << returnExpr << endl;
00249 
00250   return returnExpr;
00251 
00252 }
00253 
00254 Expr Expr::substExprQuant(const ExprHashMap<Expr>& oldToNew) const
00255 {
00256   ExprHashMap<Expr> visited(oldToNew);
00257   return recursiveQuantSubst(oldToNew,visited);
00258 }
00259 
00260 Expr Expr::recursiveQuantSubst(const ExprHashMap<Expr>& substMap,
00261              ExprHashMap<Expr>& visited) const {
00262   /* [chris 12/3/2009] It appears that visited is never used. */
00263 
00264   if (!containsBoundVar()){
00265     //    std::cout <<"no bound var " << *this << std::endl;
00266     return *this;
00267   }
00268 
00269   // Check the cache.
00270   // INVARIANT: visited contains all the flagged expressions, and only those
00271   // the above invariant is no longer true.  yeting
00272   
00273    if(getKind() == BOUND_VAR ) {
00274      ExprHashMap<Expr>::const_iterator find = substMap.find(*this);
00275      if (find != substMap.end()) {
00276        return find->second;
00277      }
00278 /*
00279      //     Expr ret  = visited[*this];
00280      const Expr ret  = substMap[*this];
00281      if (!ret.isNull()){
00282        return ret; 
00283      }
00284 */
00285    }
00286   
00287    //  if(getFlag()) return visited[*this];
00288 
00289   // why we need this.
00290 //   ExprIndex minIndex = 0;
00291 //   for(ExprHashMap<Expr>::iterator i = substMap.begin(),iend=substMap.end();i!=iend;++i) {
00292 //     if(minIndex > (i->first).getIndex())
00293 //       minIndex = (i->first).getIndex();
00294 //   }
00295 
00296   Expr replaced;
00297 
00298   if(isClosure()) {
00299     // for safety, we can wrap the following lines by if debug
00300   
00301     const vector<Expr> & vars = getVars();
00302 //     vector<Expr> common; // Bound vars which occur in subst
00303 
00304 //     for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();
00305 //  i!=iend; ++i) {
00306 //       if(substMap.count(*i) > 0) common.push_back(*i);
00307 //     }
00308 
00309 //     if(common.size() > 0) {
00310 //       cout<<"error in quant subst" << endl;
00311 //     } else {
00312 
00313       /* Perform substition on the triggers */
00314 
00315       vector<vector<Expr> > vvNewTriggers = substTriggers(substMap,visited);
00316       replaced =
00317         getEM()->newClosureExpr(getKind(), vars,
00318                                 getBody().recursiveQuantSubst(substMap, visited),
00319                                 vvNewTriggers );
00320 //     }
00321   } else { // Not a Closure
00322     int changed=0;
00323     vector<Expr> children;      
00324     for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i){  
00325       Expr repChild ;
00326       repChild = (*i).recursiveQuantSubst(substMap, visited);
00327       if(repChild != *i)
00328   changed++;
00329       children.push_back(repChild);
00330     }
00331     if(changed > 0)
00332       replaced = Expr(getOp(), children);
00333     else
00334       replaced = *this;
00335   }
00336   //  visited.insert(*this, replaced);
00337   //  setFlag();
00338   return replaced;
00339 }
00340 
00341 
00342 
00343 
00344 string Expr::toString() const {
00345   return toString(PRESENTATION_LANG);
00346 //   if(isNull()) return "Null";
00347 //   ostringstream ss;
00348 //   ss << (*this);
00349 //   return ss.str();
00350 }
00351 
00352 string Expr::toString(InputLanguage lang) const {
00353   if(isNull()) return "Null";
00354   ostringstream ss;
00355   ExprStream os(getEM());
00356   os.lang(lang);
00357   os.os(ss);
00358   os << (*this);
00359   return ss.str();
00360 }
00361 
00362 void Expr::print(InputLanguage lang, bool dagify) const {
00363   if(isNull()) {
00364     cout << "Null" << endl; return;
00365   }
00366   ExprStream os(getEM());
00367   os.lang(lang);
00368   os.dagFlag(dagify);
00369   os << *this << endl;
00370 }
00371 
00372 
00373 void Expr::pprint() const
00374 {
00375   if(isNull()) {
00376     cout << "Null" << endl; return;
00377   }
00378   ExprStream os(getEM());
00379   os << *this << endl;
00380 }
00381 
00382 
00383 void Expr::pprintnodag() const
00384 {
00385   if(isNull()) {
00386     cout << "Null" << endl; return;
00387   }
00388   ExprStream os(getEM());
00389   os.dagFlag(false);
00390   os << *this << endl;
00391 }
00392 
00393 
00394 void Expr::printnodag() const
00395 {
00396   print(AST_LANG, false);
00397 }
00398 
00399 
00400 ExprStream& Expr::printAST(ExprStream& os) const {
00401   if(isNull()) return os << "Null" << endl;
00402   bool isLetDecl(getKind() == LETDECL);
00403   os << "(" << push;
00404   os << getEM()->getKindName(getKind());
00405   if (isApply()) {
00406     os << space << "{" << getOp().getExpr() << push << "}";
00407   }
00408   else if (isSymbol()) {
00409     os << space << "{Symbol: " << getName() << "}";
00410   }
00411   else if (isClosure()) {
00412     os << space << "{" << space << "(" << push;
00413     const vector<Expr>& vars = getVars();
00414     vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00415     if(i!=iend) { os << *i; ++i; }
00416     for(; i!=iend; ++i) os << space << *i;
00417     os << push << ") " << pop << pop;
00418     os << getBody() << push << "}";
00419   }
00420   else {
00421     switch(getKind()) {
00422       case STRING_EXPR:
00423         DebugAssert(isString(), "Expected String");
00424         os << space << "{" << '"'+ getString() + '"' << "}";
00425         break;
00426       case SKOLEM_VAR:
00427         getExistential();
00428         os << space << "{SKOLEM_" << (int)getIndex() << "}";
00429         break;
00430       case RATIONAL_EXPR:
00431         os << space << "{" << getRational() << "}";
00432         break;
00433       case UCONST: 
00434         DebugAssert(isVar(), "Expected Var");
00435         os << space << "{" << getName() << "}";
00436         break;
00437       case BOUND_VAR:
00438         DebugAssert(isVar(), "Expected Var");
00439         os << space << "{"+getName()+"_"+getUid()+"}";
00440         break;
00441       case THEOREM_KIND:
00442         DebugAssert(isTheorem(), "Expected Theorem");
00443         os << space << "{Theorem: " << getTheorem().toString() << "}";
00444       default: ; // Don't do anything
00445     }
00446   }
00447 
00448   for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) {
00449     if(isLetDecl) os << nodag;
00450     os << space << *i;
00451   }
00452   os << push << ")";
00453   os.resetIndent();
00454   return os;
00455 }
00456 
00457 
00458 ExprStream& Expr::print(ExprStream& os) const {
00459   if(isNull()) return os << "Null" << endl;
00460   if (isSymbol()) return os << getName();
00461   switch(getKind()) {
00462     case TRUE_EXPR: return os << "TRUE";
00463     case FALSE_EXPR: return os << "FALSE";
00464     case NULL_KIND: return os << "Null";
00465     case STRING_EXPR: return os << '"'+ getString() + '"';
00466     case RATIONAL_EXPR: return os << getRational();
00467     case SKOLEM_VAR: return os << "SKOLEM_" <<  hash();
00468     case UCONST: return os << getName();
00469     case BOUND_VAR: return os << "(BOUND_VAR "+getName()+"_"+getUid()+")";
00470     case RAW_LIST: {
00471       os << "(" << push;
00472       bool firstTime(true);
00473       for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) {
00474         if(firstTime) firstTime = false;
00475         else os << space;
00476         os << *i;
00477       }
00478       return os << push << ")";
00479     }
00480     case FORALL:
00481     case EXISTS: 
00482       if(isQuantifier()) {
00483         os << "(" << push << getEM()->getKindName(getKind())
00484            << space << "(" << push;
00485         const vector<Expr>& vars = getVars();
00486         vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00487         if(i!=iend) { os << *i; ++i; }
00488         for(; i!=iend; ++i) os << space << *i;
00489         os << push << ") " << pop << pop;
00490         return os << getBody() << push << ")";
00491       }
00492       // If not an internal representation of quantifiers, it'll be
00493       // printed as "normal" Expr with a kind and children
00494     case RESTART: return os << "RESTART " << (*this)[0] << ";";
00495     default:
00496       //    os << "(" << push;
00497       os << getEM()->getKindName(getKind());
00498       //    os << push << ")";
00499   }
00500   os.resetIndent();
00501   return os;
00502 }
00503 
00504 
00505 //! Set initial indentation to n.
00506 /*! The indentation will be reset to default unless the second
00507     argument is true.  This setting only takes effect when printing to
00508     std::ostream.  When printing to ExprStream, the indentation can be
00509     set directly in the ExprStream. */
00510 Expr& Expr::indent(int n, bool permanent) {
00511   DebugAssert(!isNull(), "Expr::indent called on Null Expr");
00512   getEM()->indent(n, permanent);
00513   return *this;
00514 }
00515 
00516 
00517 void Expr::addToNotify(Theory* i, const Expr& e) const {
00518   DebugAssert(!isNull(), "Expr::addToNotify() on Null expr");
00519   if(getNotify() == NULL)
00520     d_expr->d_notifyList = new NotifyList(getEM()->getCurrentContext());
00521   getNotify()->add(i, e);
00522 }
00523 
00524 
00525 bool Expr::containsTermITE() const
00526 {
00527   if (getType().isBool()) {
00528 
00529     // We overload the isAtomicFlag to mean !containsTermITE for exprs
00530     // of Boolean type
00531     if (validIsAtomicFlag()) {
00532       return !getIsAtomicFlag();
00533     }
00534 
00535     for (int k = 0; k < arity(); ++k) {
00536       if ((*this)[k].containsTermITE()) {
00537         setIsAtomicFlag(false);
00538         return true;
00539       }
00540     }
00541 
00542     setIsAtomicFlag(true);
00543     return false;
00544 
00545   }
00546   else return !isAtomic();
00547 }
00548 
00549 
00550 bool Expr::isAtomic() const
00551 {
00552   if (getType().isBool()) {
00553     return isBoolConst();
00554   }
00555 
00556   if (validIsAtomicFlag()) {
00557     return getIsAtomicFlag();
00558   }
00559 
00560   for (int k = 0; k < arity(); ++k) {
00561     if (!(*this)[k].isAtomic()) {
00562       setIsAtomicFlag(false);
00563       return false;
00564     }
00565   }
00566   setIsAtomicFlag(true);
00567   return true;
00568 }
00569 
00570 
00571 bool Expr::isAtomicFormula() const
00572 {
00573   //  TRACE("isAtomic", "isAtomicFormula(", *this, ") {");
00574   if (!getType().isBool()) {
00575     //    TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }");
00576     return false;
00577   }
00578   switch(getKind()) {
00579     case FORALL: case EXISTS: case XOR:
00580     case NOT: case AND: case OR: case ITE: case IFF: case IMPLIES:
00581       //      TRACE_MSG("isAtomic", "isAtomicFormula[connective] => false }");
00582       return false;
00583   }
00584   for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) {
00585     if (!(*k).isAtomic()) {
00586       //      TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }");
00587       return false;
00588     }
00589   }
00590   //  TRACE_MSG("isAtomic", "isAtomicFormula => true }");
00591   return true;
00592 }
00593 
00594 
00595   // This is one of the most friequently called routines.  Make it as
00596   // efficient as possible.
00597 int compare(const Expr& e1, const Expr& e2) {
00598   // Quick equality check (operator== is implemented independently
00599   // and more efficiently)
00600   if(e1 == e2) return 0;
00601     
00602   if(e1.d_expr == NULL) return -1;
00603   if(e2.d_expr == NULL) return 1;
00604 
00605   // Both are non-Null.  Check for constant
00606   bool e1c = e1.isConstant();
00607   if (e1c != e2.isConstant()) {
00608     return e1c ? -1 : 1;
00609   }
00610 
00611   // Compare the indices
00612   return (e1.getIndex() < e2.getIndex())? -1 : 1;
00613 }
00614 
00615 
00616 ///////////////////////////////////////////////////////////////////////
00617 // Class Expr::iterator methods                                      //
00618 ///////////////////////////////////////////////////////////////////////
00619 
00620 
00621 ostream& operator<<(ostream& os, const Expr& e) {
00622   if(e.isNull()) return os << "Null";
00623   ExprStream es(e.getEM());
00624   es.os(os);
00625   es << e;
00626   e.getEM()->restoreIndent();
00627   return os;
00628 }
00629 
00630 
00631 // Functions from class Type
00632 
00633 
00634 Type::Type(Expr expr) : d_expr(expr)
00635 {
00636   if (expr.isNull()) return;
00637   expr.getEM()->checkType(expr);
00638 }
00639 
00640 
00641 Type Type::funType(const std::vector<Type>& typeDom, const Type& typeRan) {
00642   vector<Expr> tmp;
00643   for(vector<Type>::const_iterator i=typeDom.begin(), iend=typeDom.end();
00644       i!=iend; ++i)
00645     tmp.push_back(i->getExpr());
00646   tmp.push_back(typeRan.getExpr());
00647   return Type(Expr(ARROW, tmp));
00648 }
00649 
00650 
00651 } // end of namespace CVC3